Published: 23rd September 2015|
|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|
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.
Javier Esparza and Enrico Tronci
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 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!
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.
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.