Preface

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.

Program Chairs

Conference Chair

Program Committee

Steering Committee

External Reviewers

Invited Talks

Rigorous System Design: The BIP Framework

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

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

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.