Published: 6th September 2017|
|Probabilistic Analysis Based On Symbolic Game Semantics and Model Counting Aleksandar S. Dimovski||1|
|Parametric Markov Chains: PCTL Complexity and Fraction-free Gaussian Elimination Lisa Hutschenreiter, Christel Baier and Joachim Klein||16|
|On the Complexity of Model Checking for Syntactically Maximal Fragments of the Interval Temporal Logic HS with Regular Expressions Laura Bozzelli, Alberto Molinari, Angelo Montanari and Adriano Peron||31|
|An Existence Theorem of Nash Equilibrium in Coq and Isabelle Stéphane Le Roux, Érik Martin-Dorel and Jan-Georg Smaus||46|
|The Satisfiability Problem for Boolean Set Theory with a Choice Correspondence Domenico Cantone, Alfio Giarlotta and Stephen Watson||61|
|The Descriptive Complexity of Modal μ Model-checking Games Karoliina Lehtinen||76|
|Approximation of Weighted Automata with Storage Tobias Denkinger||91|
|MK-fuzzy Automata and MSO Logics Manfred Droste, Temur Kutsia, George Rahonis and Wolfgang Schreiner||106|
|Robust Exponential Worst Cases for Divide-et-Impera Algorithms for Parity Games Massimo Benerecetti, Daniele Dell'Erba and Fabio Mogavero||121|
|Dynamics and Coalitions in Sequential Games Thomas Brihaye, Gilles Geeraerts, Marion Hallet and Stéphane Le Roux||136|
|Finite-state Strategies in Delay Games Martin Zimmermann||151|
|A Parallel Linear Temporal Logic Tableau John C. McCabe-Dansted and Mark Reynolds||166|
|LTL to Deterministic Emerson-Lei Automata David Müller and Salomon Sickert||180|
|Linear-time Temporal Logic with Event Freezing Functions Stefano Tonetta||195|
|Emptiness Problems for Distributed Automata Antti Kuusisto and Fabian Reiter||210|
|Beyond ωBS-regular Languages: ωT-regular Expressions and Counter-Check Automata Dario Della Monica, Angelo Montanari and Pietro Sala||223|
|Model Checking Social Network Models Raúl Pardo and Gerardo Schneider||238|
|A Backward-traversal-based Approach for Symbolic Model Checking of Uniform Strategies for Constrained Reachability Simon Busard and Charles Pecheur||253|
|On the Complexity of ATL and ATL* Module Checking Laura Bozzelli and Aniello Murano||268|
|ParaPlan: A Tool for Parallel Reachability Analysis of Planar Polygonal Differential Inclusion Systems Andrei Sandler and Olga Tveretina||283|
The programme committee selected 20 papers for presentation at the symposium. Each paper was revised by at least three referees, and the selection was based on originality, quality, and relevance to the topics of the call for papers. The scientific program contained presentations on algorithmic game theory, automata and formal languages, formal verification, proof theory, modal logic, reachability analysis and temporal logics. The program included three invited talks given by Luca Aceto (Reykjavik University, Iceland and Gran Sasso Science Institute, L'Aquila, Italy), Ranko Lazic (University of Warwick, UK) and Michael Wooldridge (University of Oxford, UK). The abstract of the talks are reported below.
We wish to express our thanks to the authors who submitted papers for consideration, to the speakers, to the program committee members and the additional reviewers (also listed below) for their excellent work. We also gratefully thank for their financial support the Gruppo Nazionale per il Calcolo Scientifico (GNCS/Indam), the European Association for Artificial Intelligence (EurAI), the National Research Council of Italy (CNR) and the Institute of Cognitive Science and Technology (ISTC-CNR) with the Planning and Scheduling Technology Laboratory (PST Lab), the Laboratoire Spécification et Vérification (LSV) of CNRS and ENS Paris-Saclay, and the Italian Association for Artificial Intelligence (AIxIA).
We also thank the EasyChair organization for supporting all the tasks related to the selection of contributions, and EPTCS and arXiv for hosting the proceedings. We would like to extend special thanks to the organizing committee, led by Amedeo Cesta, for helping setting up an attractive scientific and social program, and to Angelo Montanari for his continuous support and great commitment to the event.Patricia Bouyer, Andrea Orlandini, Pierluigi San Pietro
Runtime Verification is a lightweight technique that complements other verification methods in a multi-pronged approach towards ensuring software correctness. The technique poses novel questions to software engineers: it is not easy to see which specifications are amenable to runtime monitoring, and it is not clear which monitors perform the required runtime analysis correctly. In this talk, I will present a theoretical framework that can be used to provide answers to those questions. Our approach uses the classic Hennessy-Milner with recursion as a specification logic that is agnostic of the adopted verification method and is general enough to embed commonly used specification logics. I also present an operational semantics for an elemental framework that describes the runtime analysis carried out by monitors. This allows us to establish a correspondence between the property satisfactions in the logic and the verdicts reached by the monitors carrying out the analysis. I will show how this correspondence is used to identify which subsets of the logic can be adequately monitored for, to study the power of deterministic monitors and to define various notions of monitor correctness. In this talk, I will assume no prior knowledge of runtime verification. The talk is based on joint work with Antonis Achilleos (Reykjavik University), Duncan Paul Attard (University of Malta), Ian Cassar (University of Malta), Adrian Francalanza (University of Malta) and Anna Ingólfsdóttir ((Reykjavik University), carried out within the framework of the project "Theoretical Foundations for Monitorability" (http://icetcs.ru.is/theofomon/).
The recent breakthrough paper by Calude et al. (a winner of STOC 2017 Best Paper Award) has given the first algorithm for solving parity games in quasi-polynomial time, where previously the best algorithms were mildly sub-exponential. We devise an alternative quasi-polynomial time algorithm based on progress measures, which allows us to reduce the space required from quasi-polynomial to nearly linear. Our key technical tools are a novel concept of ordered tree coding, and a succinct tree coding result that we prove using bounded adaptive multi-counters, both of which are interesting in their own right. Apart from presenting our technical work on succinct progress measures, I will survey the relevance of parity games to the theory and practice of computer-aided verification and synthesis, their surprising impact on broader theoretical computer science, the history of results and techniques used for solving parity games, and the recent advances in the state of the art. This is joint work with Marcin Jurdzinski.
A standard problem in game theory is the existence of equilibria with undesirable properties. To pick a famous example, in the Prisoners Dilemma, the unique dominant strategy equilibrium leads to the only Pareto inefficient outcome in the game, which is strictly worse for all players than an alternative outcome. If we are interested in applying game theoretic solution concepts to the analysis of distributed and multi-agent systems, then these undesirable outcomes correspond to undesirable system properties. So, what can we do about this? In this talk, I describe the work we have initiated on this problem. Using Boolean Games as a model with which to frame the problem, I discuss three approaches to dealing with this problem in multi-agent systems: the design of norms or social laws; the use of communication to manipulate the beliefs of players; and in particular, the use of taxation schemes to incentivise desirable behaviours.