Published: 6th September 2017
DOI: 10.4204/EPTCS.256
ISSN: 2075-2180

EPTCS 256

Proceedings Eighth International Symposium on
Games, Automata, Logics and Formal Verification
Roma, Italy, 20-22 September 2017

Edited by: Patricia Bouyer, Andrea Orlandini and Pierluigi San Pietro

Preface
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

Preface

This volume contains the proceedings of the Eighth International Symposium on Games, Automata, Logic and Formal Verification (GandALF 2017). The symposium took place in Roma, Italy, from the 20th to the 22nd of September 2017. The GandALF symposium was established by a group of Italian computer scientists interested in mathematical logic, automata theory, game theory, and their applications to the specification, design, and verification of complex systems. Its aim is to provide a forum where people from different areas, and possibly with different backgrounds, can fruitfully interact. GandALF has a truly international spirit, as witnessed by the composition of the program and steering committee and by the country distribution of the submitted papers.

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

Program Chairs

Patricia Bouyer, LSV, CNRS and ENS Paris-Saclay, France
Pierluigi San Pietro, Politecnico di Milano, Italy

General Chair

Amedeo Cesta, ISTC-CNR, Italy

Conference Chair

Andrea Orlandini, ISTC-CNR, Italy

Programme Committee

Parosh A. Abdulla (Uppsala University, Sweden)
Benedikt Bollig (LSV, CNRS and ENS Paris-Saclay, France)
Patricia Bouyer (LSV, CNRS and ENS Paris-Saclay, France)
Tomas Brazdil (Masaryk University, Brno, Czech Republic)
Marta Cialdea Mayer (University of Roma TRE, Italy)
Thomas Colcombet (IRIF, CNRS and Université Paris-Diderot, France)
Bernd Finkbeiner (Saarland University, Germany)
Hugo Gimbert (LaBRI, CNRS and Université de Bordeaux, France)
Rasmus Ibsen-Jensen (IST, Vienna, Austria)
Angelo Montanari (University of Udine, Italy)
Andrea Orlandini (ISTC-CNR Roma, Italy)
Doron Peled (Bar Ilan University, Israel)
R. Ramanujam (IMSc, Chennai, India)
Mickael Randour (ULB, Brussels, Belgium)
Matteo Rossi (Politecnico di Milano, Italy)
Pierluigi San Pietro (Politecnico di Milano, Italy)

Steering Committee

Luca Aceto, School of Computer Science, Reykjavik University, Iceland and Gran Sasso Science Institute, L'Aquila, Italy
Javier Esparza, University of Munich, Germany
Salvatore La Torre, University of Salerno, Italy
Angelo Montanari, University of Udine, Italy
Mimmo Parente, University of Salerno, Italy
Wolfgang Thomas, Aachen University, Germany

External Reviewers

Alessandro Artale, Marcello M. Bersani, Dietmar Berwanger, Serenella Cerrito, Johanne Cohen, Evelyne Contejean, Bui Phi Diep, John Fearnley, Vojtech Forejt, Marco Gario, Nicola Gigante, Antonin Kucera, Nicolas Markey, Bastien Maubert, Alberto Molinari, Benjamin Monmege, Yoram Moses, Andrzej Murawski, Pavel Naumov, Guillermo Perez, Sophie Pinchinat, Vojtech Rehak. Othmane Rezine, Sunil Easaw Simon, Michał Skrzypczak, Martin Strecker, Jan Strejček, Cong Quy Trinh, Alexander Weinert, Georg Zetzsche.

Invited Talks

Theoretical Foundations for Runtime Monitoring

Luca Aceto
School of Computer Science, Reykjavik University, Iceland, and Gran Sasso Science Institute, L'Aquila, Italy.

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/).

Succinct Progress Measures and Solving Parity Games in Quasi-Polynomial Time

Ranko Lazic
Department of Computer Science, University of Warwick, UK

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.

How to Free Yourself from the Curse of Bad Equilibria

Michael Wooldridge
Department of Computer Science, University of Oxford, UK

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.