Published: 23rd September 2015
DOI: 10.4204/EPTCS.193
ISSN: 2075-2180

EPTCS 193

Proceedings Sixth International Symposium on
Games, Automata, Logics and Formal Verification
Genoa, Italy, 21-22nd September 2015

Edited by: Javier Esparza and Enrico Tronci

Preface
Javier Esparza and Enrico Tronci
Invited Presentation: Parity games through the ages
Sven Schewe
Invited Presentation: Parameterized verification of probabilistic networks
Nathalie Bertrand
Invited Presentation: Reasoning under Release-Acquire Consistency
Viktor Vafeiadis
Average-energy games
Patricia Bouyer, Nicolas Markey, Mickael Randour, Kim G. Larsen and Simon Laursen
1
Making the Best of Limited Memory in Multi-Player Discounted Sum Games
Anshul Gupta, Sven Schewe and Dominik Wojtczak
16
Negotiation Games
Philipp Hoffmann
31
ATLsc with partial observation
François Laroussinie, Nicolas Markey and Arnaud Sangnier
43
Synchronous Subsequentiality and Approximations to Undecidable Problems
Christian Wurm
58
Tractability Frontier of Data Complexity in Team Semantics
Arnaud Durand, Juha Kontinen, Nicolas de Rugy-Altherre and Jouko Väänänen
73
Simulator Semantics for System Level Formal Verification
Toni Mancini, Federico Mari, Annalisa Massini, Igor Melatti and Enrico Tronci
86
Reachability Analysis of Reversal-bounded Automata on Series-Parallel Graphs
Rayna Dimitrova and Rupak Majumdar
100
Well Structured Transition Systems with History
Parosh Abdulla, Giorgio Delzanno and Marco Montali
115
The expressive power of modal logic with inclusion atoms
Lauri Hella and Johanna Stumpf
129
Parameterized Linear Temporal Logics Meet Costs: Still not Costlier than LTL
Martin Zimmermann
144
Improvement in Small Progress Measures
Maciej Gazda and Tim A.C. Willemse
158
An Automata Theoretic Approach to the Zero-One Law for Regular Languages: Algorithmic and Logical Aspects
Ryoma Sin'ya
172

Preface

This volume contains the proceedings of the Sixth International Symposium on Games, Automata, Logic and Formal Verification (GandALF 2015). The symposium took place in Genoa, Italy, on the 21st and 22nd of September 2015.

The GandALF symposium was established by a number 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. Even though the idea of the symposium emerged within the Italian research community, the event has a truly international nature, as witnessed by the composition of the conference committees and by the country distribution of the submitted papers.

The programme committee received 22 submissions and selected 13 of them 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 preentations on algorithmic game theory, automata theory, formal verification, and modal and temporal logics. Additionally, three invited talks were given by Sven Schewe (University of Liverpool), Nathalie Bertrand (INRIA Rennes), and Viktor Vafeiadis (Max Planck Institute for Software Systems, Kaiserslautern); their titles and abstracts can be found below.

We wish to express our thanks to the authors who submitted extended abstracts for consideration, the speakers and invited speakers, the programme committee members (also listed below), and the additional reviewers for their excellent work.

We thank the Gruppo Nazionale per il Calcolo Scientifico (GNCS/Indam), the Italian Chapter of EATCS, the University of Genoa, and in particular its Dipartimento di Informatica, Bioingegneria, Robotica ed Ingegneria dei Sistemi (DIBRIS), for their help in the organization of the event. 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, composed by Giorgio Delzanno, Elena Zucca, Alessandro Solimando, Daniela Briola, Andrea Corradi, and Federico Frassetto, for setting up an attractive scientific and social program, and to the General Chair of GandALF, Margherita Napoli, for her constant support.

September 2015,
Javier Esparza and Enrico Tronci

Programm Committee

Parosh Aziz Abdulla, Univ. of Uppsala, Sweden
Ahmed Bouajjani, LIAFA, France
Thomas Brihaye, Mons University, Belgium
Pavol Cerny, University of Colorado, Boulder, USA
Krishnendu Chatterjee, Inst. of Science and Tech., Austria
Giorgio Delzanno, University of Genoa, Italy
Laurent Doyen, LSV, France
Bernd Finkbeiner, Universität Saarbrücken, Germany
Pierre Ganty, IMDEA, Spain
Antonin Kucera, Masaryk University, Brno, Czech Republic
K. Narayan Kumar, Chennai Mathematical Institute, India
Orna Kupferman, Hebrew Unversity, Jerusalem, Israel
Christof Löding, RWTH-Aachen, Germany
Richard Mayr, University of Edinburgh, UK
Igor Melatti, Sapienza University of Rome, Italy
Henryk Michalewski, University of Warsaw, Poland
Luke Ong, University of Oxford, UK
Mimmo Parente, University of Salerno, Italy
Gennaro Parlato, University of Southampton, UK
Doron Peled, Bar Ilan University, Israel
Ruzica Piskac, Yale University, USA
Hiroshi Umeo. University of Osaka Electro-Communication, Japan
Helmut Veith, Technische Universität Wien, Austria
Marc Zeitoun, LaBRI, France


Parity games through the ages

Sven Schewe (University of Liverpool)

Parity games are simple two player games played on a finite arena that have all that it takes to attract the attention of researchers: it is a simple problem which is hard to analyse - a pocket version of P vs. NP. Parity games are known to be in UP, CoUP, PPAD, and PLS (and some more classes), but whether or not they are in P has proven to be a rather elusive question. What is more, when you work with them, you will have the constant feeling that there is a polynomial time solution just around the corner, although it dissolves into nothingness when you look more closely. This talk is about the beauty of these games, the relevant algorithmic approaches and their complexity and development over time. But be careful: they are addictive, don't get hooked!


Parameterized verification of probabilistic networks

Nathalie Bertrand (INRIA Rennes)

We study verification problems for a model of network with the following characteristics: communication is performed through broadcast with adjacent neighbours, entities can change their internal state probabilistically, and reconfiguration of the communication topology can happen at any time. For such reconfigurable probabilistic broadcast networks, the semantics is given in terms of a Markov decision process, combining non-determinism with probabilities. Importantly, although the number of nodes is finite and fixed during a computation, it is unknown and represented by a parameter. We are interested in parameterized qualitative problems like whether independently of the number of nodes, there exists a resolution of the non-determinism such that a configuration exhibiting an error state is almost surely reached. We show that all variants of this qualitative reachability problem are decidable. Some proofs are based on solving a infinite-state 2-player games with parity and safety objectives, described as reconfigurable broadcast networks.
This is based on a joint work with Paulin Fournier and Arnaud Sangnier.


Reasoning under Release-Acquire Consistency

Viktor Vafeiadis (Max Planck Institute for Software Systems, Kaiserslautern)

In this talk, I will introduce weak memory consistency models and the challenges it poses on software verification. I will then focus on the release-acquire memory model, an important fragment of the C/C++ memory model, and present a few verification results that allow us to reason about concurrent programs under the release-acquire model.