|
Published: 24th August 2014 DOI: 10.4204/EPTCS.161 ISSN: 2075-2180 |
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
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).