Published: 13th September 2016
DOI: 10.4204/EPTCS.226
ISSN: 2075-2180

EPTCS 226

Proceedings of the Seventh International Symposium on
Games, Automata, Logics and Formal Verification
Catania, Italy, 14-16 September 2016

Edited by: Domenico Cantone and Giorgio Delzanno

Preface Domenico Cantone and Giorgio Delzanno
Partial Solvers for Parity Games: Effective Polynomial-Time Composition Patrick Ah-Fat and Michael Huth	1
Relation-Changing Logics as Fragments of Hybrid Logics Carlos Areces, Raul Fervari, Guillaume Hoffmann and Mauricio Martel	16
A Delayed Promotion Policy for Parity Games Massimo Benerecetti, Daniele Dell'Erba and Fabio Mogavero	30
Games for Topological Fixpoint Logic Nick Bezhanishvili and Clemens Kupke	46
Stochastic Equilibria under Imprecise Deviations in Terminal-Reward Concurrent Games Patricia Bouyer, Nicolas Markey and Daniel Stan	61
Model Checking the Logic of Allen's Relations Meets and Started-by is P^NP-Complete Laura Bozzelli, Alberto Molinari, Angelo Montanari, Adriano Peron and Pietro Sala	76
On the Expressive Power of Sub-Propositional Fragments of Modal Logic Davide Bresolin, Emilio Muñoz-Velasco and Guido Sciavicco	91
Alternation Is Strict For Higher-Order Modal Fixpoint Logic Florian Bruse	105
A Canonical Model Construction for Iteration-Free PDL with Intersection Florian Bruse, Daniel Kernberger and Martin Lange	120
Window Parity Games: An Alternative Approach Toward Parity Games with Time Bounds Véronique Bruyère, Quentin Hautem and Mickael Randour	135
Weighted Linear Dynamic Logic Manfred Droste and George Rahonis	149
Cycle Detection in Computation Tree Logic Gaëlle Fontaine, Fabio Mogavero, Aniello Murano, Giuseppe Perelli and Loredana Sorrentino	164
Bounded-oscillation Pushdown Automata Pierre Ganty and Damir Valput	178
On Quantified Propositional Logics and the Exponential Time Hierarchy Miika Hannula, Juha Kontinen, Martin Lück and Jonni Virtema	198
Multi-Buffer Simulations for Trace Language Inclusion Milka Hutagalung, Norbert Hundeshagen, Dietrich Kuske, Martin Lange and Etienne Lozes	213
Distributed PROMPT-LTL Synthesis Swen Jacobs, Leander Tentrup and Martin Zimmermann	228
A Semi-Potential for Finite and Infinite Sequential Games (Extended Abstract) Stéphane Le Roux and Arno Pauly	242
Certification of Prefixed Tableau Proofs for Modal Logic Tomer Libal and Marco Volpe	257
The Almost Equivalence by Asymptotic Probabilities for Regular Languages and Its Computational Complexities Yoshiki Nakamura	272
A New Rule for LTL Tableaux Mark Reynolds	287
Approximating Optimal Bounds in Prompt-LTL Realizability in Doubly-exponential Time Leander Tentrup, Alexander Weinert and Martin Zimmermann	302

Preface

This volume contains the proceedings of the Seventh International Symposium on Games, Automata, Logic and Formal Verification (GandALF 2016). The symposium took place in Catania, Italy, from the 14th to the 16th of September 2016. 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 21 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, and temporal logics. The program included three invited talks given by Luca Bortolussi (University of Trieste), Joanna Golinska-Pilarek (Institute of Philosophy, University of Warsaw), and Arnaud Sangnier (Laboratoire IRIF, University Paris Diderot). The abstract of the talks are listed below. We wish to express our thanks to the authors who submitted extended abstracts for consideration, the speakers, the program committee members and the additional reviewers (also listed below) for their excellent work. We also thank the ''Gruppo Nazionale per il Calcolo Scientifico'' (GNCS/Indam), the Italian Chapter of EATCS, the University of Catania (and in particular its Department of Mathematics and Computer Science), the University of Genova, and N.C.E. Network Consulting Engineering srl, for their help and support 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 Simone Faro, Cristiano Longo, Marianna Nicolosi Asmundo, and Daniele Francesco Santamaria, for helping setting up an attractive scientific and social program, and to Angelo Montanari for his continuous support to the event.

September 2016,
Domenico Cantone and Giorgio Delzanno

Steering Committee

Javier Esparza, University of Munich, Germany
Angelo Montanari, University of Udine, Italy
Margherita Napoli, University of Salerno, Italy
Mimmo Parente, University of Salerno, Italy
Wolfgang Thomas, Aachen University, Germany

Program Chairs

Domenico Cantone, University of Catania, Italy
Giorgio Delzanno, University of Genova, Italy

Program Committee

Parosh Aziz Abdulla, University of Uppsala, Sweden
Ahmed Bouajjani, LIAFA University Paris Diderot, France
Patricia Bouyer-Decitre, CNRS & LSV, France
Krishnendu Chatterjee, Inst. of Science and Tech. Austria
Vincenzo Ciancia, CNR, Italy
Laurent Doyen, CNRS & LSV, France
Bernd Finkbeiner, Universität des Saarlandes, Germany
Antonín Kucera, Masaryk University (Brno), Czech Republic
K. Narayan Kumar, Chennai Mathematical Institute, India
Henryk Michalewski, University of Warsaw, Poland
Angelo Montanari, University of Udine, Italy
Doron Peled, Bar Ilan University, Israel
Norbert Preining, Japan Advanced Institute of Science and Technology
Sasha Rubin, University of Napoli "Federico II", Italy
Sven Schewe, University of Liverpool, UK
Enrico Tronci, University of Roma "La Sapienza", Italy
Damien Zufferey, MIT CSAIL, USA

External Reviewers

P. Balbiani, N. Basset, D. Berwanger, B. Bollig, T. Brazdil, M. Colange, D. Della Monica, S. Enqvist, J. Golinska-Pilarek, J. Goubault-Larrecq, S. La Torre, F. Laroussinie, M. Miculan, F. Mogavero, M. Nicolosi-Asmundo, D. Niwinski, P. Novotny, J. Obdrzalek, D. Pattinson, M. Praveen, A. Pulvirenti, V. Rehak, P. Sala, A. Sangnier, H. Torfah, E. Zucca

Invited Talks

Machine learning meets formal verification
Luca Bortolussi
University of Trieste, Italy

Many current scientific and technological challenges are related to understanding, designing and controlling complex systems, from epidemic spreading to performance of computer systems, from biological networks to bike and car sharing. Model-based approaches are one of the key strategies to face such challenges. Models of such systems are typically specified in terms of local interactions between entities involved, but the interest is in global behaviours at the system level, typically known as emergent properties. Our goal is to study such properties, starting from a stochastic Markov model, with the machinery of formal verification. More precisely, the focus is on the formalisation of such properties in a suitable logical language and on the automatic verification of these properties in a given model (the so called model checking problem), which in a probabilistic setting takes the form of computing the probability with which such properties are satisfied. However, the models we can construct are always uncertain, in particular in the value of their parameters, due to lack of information and their phenomenological nature. To deal consistently with such an uncertainty, we have combined formal verification techniques with state-of-the-art Machine Learning statistical tools, based on Gaussian Processes. We will show how to efficiently compute the satisfaction probability of a behavioural property when model parameters are unknown, but assumed to lie in a bounded interval, a method we called Smoothed Model Checking. Combining these ideas with Bayesian Optimisation, we can then efficiently solve system design problems, i.e. fixing controllable model parameters so that the system robustly exhibits a desired behaviour. This talk will be a gentle introduction to these ideas.

Relational decision procedures with their applications to nonclassical logics
Joanna Golinska-Pilarek
Institute of Philosophy, University of Warsaw, Poland

Relational decision procedures are based on relational dual tableaux, a powerful tool for verification of validity as well as for proving entailment, model checking and satisfiability checking. Dual tableaux are top-down validity checkers and it holds a duality relation between them and the well known tableau systems. The common language of most relational dual tableaux is the logic of binary relations which was introduced as a logical counterpart to the class of representable relation algebras defined by Tarski. The methods of relational deduction may be applied to various theories that are translatable into an appropriate fragment and/or extension of the relational logic. Thus, the main advantage of the relational methodology is that it makes it possible to represent within a uniform formalism the three basic components of formal systems: syntax, semantics, and deduction apparatus. Research from the last few decades has shown that the relational approach can be seen as a general framework for representing, investigating, implementing and comparing theories with incompatible languages and/or semantics. In this talk, we will present some basics of relational dual tableaux methodology and discuss the current state of research on relational decision procedures. We will also show some new results concerning relational decision procedures for some qualitative logics for order of magnitude reasoning.

Fixpoints in VASS: Results and applications
Arnaud Sangnier
Laboratoire IRIF, Université Paris Diderot, France

VASS (Vector Addition Systems with States), which are equivalent to Petri nets, are automata equipped with natural variables that can be decremented or incremented. VASS are a powerful model which has been intensively studied in the last decades. Many verification techniques have been developed to analyse them and the frontier between the decidable and undecidable problems related to VASS begins to be well known. One interesting point is that the model-checking of linear temporal logics (like LTL or linear mu-calculus) is decidable for this model but this is not anymore the case when considering branching time temporal logics. However some restrictions can be imposed on the logics and on the studied system in order to regain decidability. In this talk, we will present these results concerning the model-checking of VASS and the techniques leading to the decidability results. We will then show how these techniques and results can be used to analyse some extensions of VASS with probabilities, namely probabilistic VASS and VASS Markov Decision Processes.