Published: 7th September 2018
DOI: 10.4204/EPTCS.277
ISSN: 2075-2180

EPTCS 277

Proceedings Ninth International Symposium on
Games, Automata, Logics, and Formal Verification
Saarbrücken, Germany, 26-28th September 2018

Edited by: Andrea Orlandini and Martin Zimmermann

Preface
Quantitative Reductions and Vertex-Ranked Infinite Games
Alexander Weinert
1
Constrained Existence Problem for Weak Subgame Perfect Equilibria with ω-Regular Boolean Objectives
Thomas Brihaye, Véronique Bruyère, Aline Goeminne and Jean-François Raskin
16
Parameterized Games and Parameterized Automata
Arno Pauly
30
Classical Proofs as Parallel Programs
Federico Aschieri, Agata Ciabattoni and Francesco Antonio Genco
43
Safe Dependency Atoms and Possibility Operators in Team Semantics
Pietro Galliani
58
A Simplicial Complex Model for Dynamic Epistemic Logic to study Distributed Task Computability
Éric Goubault, Jérémy Ledent and Sergio Rajsbaum
73
Solving QBF by Abstraction
Jesko Hecking-Harbusch and Leander Tentrup
88
A Comparison of BDD-Based Parity Game Solvers
Lisette Sanchez, Wieger Wesselink and Tim A.C. Willemse
103
Tester versus Bug: A Generic Framework for Model-Based Testing via Games
Petra van den Bos and Marielle Stoelinga
118
Parameterized Verification of Coverability in Well-Structured Broadcast Networks
A.R. Balasubramanian
133
Effortless Fault Localisation: Conformance Testing of Real-Time Systems in Ecdar
Tobias R. Gundersen, Florian Lorber, Ulrik Nyman and Christian Ovesen
147
Temporal Logic and Model Checking for Operator Precedence Languages
Michele Chiari, Dino Mandrioli and Matteo Pradella
161
One-Pass and Tree-Shaped Tableau Systems for TPTL and TPTLb+Past
Luca Geatti, Nicola Gigante, Angelo Montanari and Mark Reynolds
176
Complexity of Timeline-Based Planning over Dense Temporal Domains: Exploring the Middle Ground
Laura Bozzelli, Alberto Molinari, Angelo Montanari and Adriano Peron
191
On Computing the Measures of First-Order Definable Sets of Trees
Marcin Przybyłko
206
On Finding a First-Order Sentence Consistent with a Sample of Strings
Thiago Alves Rocha, Ana Teresa Martins and Francicleber Martins Ferreira
220
Timed Context-Free Temporal Logics
Laura Bozzelli, Aniello Murano and Adriano Peron
235
Multi-weighted Markov Decision Processes with Reachability Objectives
Patricia Bouyer, Mauricio González, Nicolas Markey and Mickael Randour
250
Regular omega-Languages with an Informative Right Congruence
Dana Angluin and Dana Fisman
265

Preface

This volume contains the proceedings of the Ninth International Symposium on Games, Automata, Logic and Formal Verification (GandALF 2018). The symposium took place in Saarbrücken, Germany, from the 26th to the 28th of September 2018, the first edition hosted outside of Italy.

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 program committee selected 19 papers for presentation at the symposium. Each paper was reviewed 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 infinite games, automata and formal languages, formal verification, planning, proof theory, reachability analysis, and first-order, temporal, and epistemic logics. The program included three invited talks given by Saddek Bensalem (Université Grenoble Alpes, France), Véronique Bruyère (University of Mons, Belgium) and Kim G. Larsen (Aalborg University, Denmark).

The abstract of the invited 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 the German Research Foundation (DFG) for financial support.

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, in particular Alexander Weinert and Christa Schäfer, for local arrangements and for setting up an attractive social program, and to Angelo Montanari for his continuous support and great commitment to the event.

Andrea Orlandini and Martin Zimmermann

Program Chairs

Andrea Orlandini (ISTC-CNR, Italy)
Martin Zimmermann (Saarland University, Germany)

Conference Chair

Martin Zimmermann (Saarland University, Germany)

Program Committee

Mohamed Faouzi Atig (Uppsala University, Sweden)
Christel Baier (TU Dresden, Germany)
Patricia Bouyer (LSV, CNRS & ENS Cachan, Université Paris Saclay, France)
Laura Bozzelli (Università degli Studi di Napoli Federico II, Italy)
Thomas Colcombet (CNRS, France)
Dario Della Monica (Istituto Nazionale di Alta Matematica "F. Severi" (INdAM), Italy)
Jie-Hong Roland Jiang (National Taiwan University, Taiwan)
Ranko Lazic (The University of Warwick, United Kingdom)
Jérôme Leroux (CNRS, France)
Radu Mardare (Aalborg University, Denmark)
Angelo Montanari (University of Udine, Italy)
Andrea Orlandini (ISTC-CNR, Italy)
Gennaro Parlato (University of Southampton, United Kingdom)
Doron Peled (Bar Ilan University, Israel)
Mickael Randour (UMONS - Université de Mons, Belgium)
Mark Reynolds (The University of Western Australia, Australia)
Pietro Sala (University of Verona, Italy)
Pierluigi San Pietro (Politecnico di Milano, Italy)
B Srivathsan (Chennai Mathematical Institute, India)
Martin Zimmermann (Saarland University, Germany)

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

Dietmar Berwanger, Nick Bezhanishvili, Adrien Boiret, Luc Dartois, Laure Daviaud, Hans van Ditmarsch, Claudia Faggian, David de Frutos Escrig, Nicola Gigante, Quentin Hautem, Florian Horn, Kamal Lodaya, Bastien Maubert, Filip Mazowiecki, Alberto Molinari, Aniello Murano, Adriano Peron, Nir Piterman, Gabriele Puppis, Olivier Serre, and Patrick Totzke.

Invited Talks

Rigorous System Design: The BIP Framework

Saddek Bensalem
Université Grenoble Alpes, France

Rigorous system design requires the use of a single powerful component framework allowing the representation of the designed system at different levels of detail, from application software to its implementation. This is essential for ensuring the overall coherency and correctness. This talk introduces a rigorous design flow based on the BIP (Behavior, Interaction, Priority) component framework. This design flow relies on several, tool-supported, source-to-source transformations allowing to progressively and correctly transform high level application software towards efficient implementations for specific platforms.

On the Synthesis of Equilibria in Graph Games

Véronique Bruyère
University of Mons, Belgium

In this invited talk, we focus on games played on graphs by several players who aim at satisfying their objective. We survey and discuss several solution concepts useful for the synthesis of systems, the most famous one being the notion of Nash equilibrium. We present several results about their existence (possibly constrained by some conditions on the payoffs), the objectives of the players being qualitative or quantitative. We also provide some illustrative examples as well as intuitions on the proofs.

Energy Timed Automata and Games

Kim G. Larsen
Aalborg University, Denmark

The first part of the talk will provide an overview of the results obtained over the last 10 years when considering Timed Automata and Timed Games extended with continuous variables (cost) that may evolve with different (positive or negative) weights with particular interest in infinite energy-bounded runs/strategies. In the second part we review recent results obtained for a subclass called Segmented Energy Timed Games, where we have decidability, thus allowing for the automatic synthesis of robust and optimal energy-aware controllers. We prove decidability of the energy-constrained infinite run problem in settings with both certainty and uncertainty of the energy-rates. We also consider the optimization problem of identifying the minimal upper bound that will permit existence of infinite energy constrained runs. Our algorithms are based on quantifier elimination for linear real arithmetic. Using Mathematica and Mjollnir, we illustrate our framework through a real industrial example of a hydraulic oil pump. Compared with previous approaches our method is completely automated and provides significantly improved results.