Published: 24th August 2014
DOI: 10.4204/EPTCS.161
ISSN: 2075-2180

EPTCS 161

Proceedings Fifth International Symposium on
Games, Automata, Logics and Formal Verification
Verona, Italy, 10th - 12th September 2014

Edited by: Adriano Peron and Carla Piazza

Preface
Adriano Peron and Carla Piazza
Invited Presentation: Advances in symbolic model checking for multi-agent systems
Alessio R. Lomuscio
1
Invited Presentation: Termination of Linear Programs: Advances and Challenges
Joel Ouaknine
2
Invited Presentation: Schema Mappings and Data Examples: An Interplay between Syntax and Semantics
Phokion G. Kolaitis
3
Some Turing-Complete Extensions of First-Order Logic
Antti Kuusisto
4
Complexity of validity for propositional dependence logics
Jonni Virtema
18
The Hardness of Finding Linear Ranking Functions for Lasso Programs
Amir M. Ben-Amram
32
Kleene Algebras, Regular Languages and Substructural Logics
Christian Wurm
46
Parametric Linear Dynamic Logic
Peter Faymonville and Martin Zimmermann
60
On the Path-Width of Integer Linear Programming
Constantin Enea, Peter Habermehl, Omar Inverso and Gennaro Parlato
74
Synthesis of Deterministic Top-down Tree Transducers from Automatic Tree Relations
Christof Löding and Sarah Winter
88
Interval-based Synthesis
Angelo Montanari and Pietro Sala
102
The Fixpoint-Iteration Algorithm for Parity Games
Florian Bruse, Michael Falk and Martin Lange
116
Model Checking Paxos in Spin
Giorgio Delzanno, Michele Tatarek and Riccardo Traverso
131
Infinite Networks, Halting and Local Algorithms
Antti Kuusisto
147
A Formulation of the Potential for Communication Condition using C2KA
Jason Jaskolka and Ridha Khedri
161
Hourglass Automata
Yuki Osada, Tim French, Mark Reynolds and Harry Smallbone
175
Deterministic Automata for Unordered Trees
Adrien Boiret, Vincent Hugot, Joachim Niehren and Ralf Treinen
189
Deterministic Timed Finite State Machines: Equivalence Checking and Expressive Power
Davide Bresolin, Khaled El-Fakih, Tiziano Villa and Nina Yevtushenko
203
Petri Games: Synthesis of Distributed Systems with Causal Memory
Bernd Finkbeiner and Ernst-Rüdiger Olderog
217
Tree games with regular objectives
Marcin Przybyłko
231
Improved Undecidability Results for Reachability Games on Recursive Timed Automata
Shankara Narayanan Krishna, Lakshmi Manasa and Ashutosh Trivedi
245
Visibly Pushdown Modular Games
Ilaria De Crescenzo, Salvatore La Torre and Yaron Velner
260

Preface

This volume contains the proceedings of the Fourth International Symposium on Games, Automata, Logic and Formal Verification (GandALF 2014). The symposium took place in Verona, Italy, from 10th to 12th of September 2014.

The GandALF symposium was established by a number of Italian computer scientists interested in mathematical logic, automata theory, game theory, and their applications to the specification, design, and verification of complex systems. It aims to provide a forum where people from different areas, and possibly with different backgrounds, can fruitfully interact. Even though the idea of the symposium emerged within the Italian research community, the event has a truly international nature, as witnessed by the composition of the conference committees and by the country distribution of the submitted papers.

In response to the Call for Papers, the program committee received 36 submissions and selected 19 of them to be included in the conference program. Each paper was revised by at least three referees and the selection was based on originality, quality, and relevance to the topics of the symposium. The scientific program consisted of papers on a wide variety of topics, including algorithmic and behavioral game theory, game semantics, formal languages and automata theory, modal and temporal logics, software verification, hybrid systems.

This fifth edition of GandALF, colocated with TIME 2014, has also hosted three invited talks:

We wish to express our thanks to the authors who submitted extended abstracts for consideration. We would like to thank also the steering committee for giving us the opportunity and the honor to supervise GandALF 2014, as well as the program committee members and the additional reviewers for their excellent work, fruitful discussions and active participation during the evaluation process.

We would like to thank the people, institutions, and companies for contributing to the success of this edition of GandALF. In particular, we gratefully acknowledge the financial support from INDAM-GNCS (Istituto Nazionale di Alta Matematica - Gruppo Nazionale per il Calcolo Scientifico). We also thank the EasyChair organization for supporting all the tasks related to the selection of contributions, EPTCS and arXiv for hosting the proceedings.

We would like to extend special thanks to the organizing committe -- composed by Barbara Oliboni, Carlo Combi, Gabriele Pozzani, and Pietro Sala -- for their efforts in making the local arrangements and organizing an attractive social program. We are also grateful to Aniello Murano for helping us in advertising the event.


September 2014,
Adriano Peron and Carla Piazza


Program Committee


Steering Committee


Local Organisation


Program co-Chairs


Advances in symbolic model checking for multi-agent systems

Alessio R. Lomuscio (Imperial College London)

Multi-agent systems (MAS) are distributed autonomous systems in which the components, or agents, act autonomously or collectively in order to reach private or common goals. Logic-based specifications for MAS typically do not only involve their temporal evolution, but also other agent attitudes, including their knowledge, intentions, their strategic abilities, etc.

This talk will survey some of our work on model checking MAS against agent-based specifications. Serial and parallel algorithms for symbolic model checking against temporal-epistemic specifications as well as bounded-model checking procedures will be discussed. MCMAS, an open-source model checker, developed in the VAS group at Imperial College London, will be briefly demonstrated. A case study concerning the verification of diagnosability and fault-tolerance of an autonomous underwater vehicles will be discussed.


Termination of Linear Programs: Advances and Challenges

Joel Ouaknine (Oxford University)

In the quest for program analysis and verification, program termination - determining whether a given program will always halt or could execute forever - has emerged as a pivotal component. Although proven undecidable in the general case by Alan Turing over 80 years ago, decidability results have been obtained in a variety of restricted instances. We survey the situation with a focus on simple linear programs, i.e., WHILE loops in which all assignments and guards are linear, discussing recent progress as well as ongoing and emerging challenges.


Schema Mappings and Data Examples: An Interplay between Syntax and Semantics

Phokion G. Kolaitis (University of California, Santa Cruz and IBM Research, Almaden (USA))

Schema mappings are high-level specifications that describe the relationship between two database schemas. Schema mappings constitute the essential building blocks in such critical data inter-operability tasks as data exchange and data integration. For this reason, schema mappings have been the focus of extensive research investigations over the past several years. Since in real-life applications schema mappings can be quite complex, it is important to develop methods and tools for illustrating, explaining, and deriving schema mappings. A promising approach to this effect is to use "good" data examples that illustrate the schema mapping at hand.

In this talk, we will present an overview of recent work on characterizing and deriving schema mappings via a finite set of data examples. We will focus on unique characterizations of schema mappings via a finite set of universal examples and on the learnability of schema mappings from data examples. Along the way, we will unveil a tight connection between unique characterizability of schema mappings and homomorphism dualities in constraint satisfaction.

This is joint work with Bogdan Alexe (IBM Research - Almaden), Balder ten Cate (LogicBlox and UC Santa Cruz), and Wang-Chiew Tan (UC Santa Cruz).