Published: 7th September 2018|
|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|
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
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.
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.
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.