Published: 24th August 2014|
|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|
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.
Adriano Peron and Carla Piazza
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.
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 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).