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