Published: 4th June 2011
DOI: 10.4204/EPTCS.54
ISSN: 2075-2180


Proceedings Second International Symposium on
Games, Automata, Logics and Formal Verification
Minori, Italy, 15-17th June 2011

Edited by: Giovanna D'Agostino and Salvatore La Torre

Giovanna D'Agostino and Salvatore La Torre
Invited Presentation: The monadic theory of linear orders
Thomas Colcombet
Invited Presentation: The Rise and Fall of LTL
Moshe Y. Vardi
Invited Presentation: Dependence, Independence, and Imperfect Information
Erich Grädel
Synthesis from Recursive-Components Libraries
Yoad Lustig and Moshe Vardi
Improving BDD Based Symbolic Model Checking with Isomorphism Exploiting Transition Relations
Christian Appold
Computing the Reveals Relation in Occurrence Nets
Stefan Haar, Christian Kern and Stefan Schwoon
Automated Analysis of MUTEX Algorithms with FASE
Federico Buti, Massimo Callisto De Donato, Flavio Corradini, Maria Rita Di Berardini and Walter Vogler
Optimal Strategies in Infinite-state Stochastic Reachability Games
Václav Brožek
A reduction from parity games to simple stochastic games
Krishnendu Chatterjee and Nathanaël Fijalkow
Opacity Issues in Games with Imperfect Information
Bastien Maubert, Sophie Pinchinat and Laura Bozzelli
Type Inference for Bimorphic Recursion
Makoto Tatsuta and Ferruccio Damiani
A Decidable Extension of Data Automata
Zhilin Wu
Connectivity Games over Dynamic Networks
Sten Grüner, Frank G. Radmacher and Wolfgang Thomas
Optimal Bounds in Parametric LTL Games
Martin Zimmermann
New results on pushdown module checking with imperfect information
Laura Bozzelli
Reactive Safety
Rüdiger Ehlers and Bernd Finkbeiner
An Optimal Decision Procedure for MPNL over the Integers
Davide Bresolin, Angelo Montanari, Pietro Sala and Guido Sciavicco
Separation of Test-Free Propositional Dynamic Logics over Context-Free Languages
Markus Latte
On P-transitive graphs and applications
Giacomo Lenzi
A Game-Theoretic approach to Fault Diagnosis of Hybrid Systems
Davide Bresolin and Marta Capiluppi
Deciding Reachability for 3-Dimensional Multi-Linear Systems
Olga Tveretina and Daniel Funke
Towards Efficient Exact Synthesis for Linear Hybrid Systems
Massimo Benerecetti, Marco Faella and Stefano Minopoli


The International Symposium on Games, Automata, Logics, and Formal Verification (GandALF) is this year on its second edition. Despite its youth, the symposium is registering a growing interest by the scientific community, also testified by the increasing number of submissions and the entusiastic adhesions by many widely-recognized high-profile scientists to partecipate and contribute to the success of GandALF in several ways.

GandALF was founded 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. Its aim is to provide a forum where people from different areas, and possibly with a different background, can successfully 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 the programme.

This year GandALF has hosted three invited talks:

and 19 presentations which have been selected among 38 submissions.
Each paper has been revised by three referees and the papers have been selected according to originality, quality, and relevance to the topics of the symposium.

We have several acknowledgements to make.

Let us first thank the Advisory Board and the Streering Committee for giving us the opportunity and the honour to supervise GandALF 2011, the useful suggestions and for their support and encouragement. Many thanks go to all the Program Committee members and the additional reviewers for the excellent work, the fruitful discussions and the active participation during the reviewing process. Special thanks go to Angelo Montanari, Margherita Napoli and Mimmo Parente for their constant advising and help also with practical matters.

We would like also to express our appreciation and gratitude to Aniello Murano for taking care of the funding from private companies and all the members of the Organizing Committee for the great work, and especially to: Marco Faella for taking care of the web page of the conference, supervising the local organization of the event, and for taking care of the applications for grants in support of the conference; and Dario Della Monica for assisting us with the organization of the whole event.

Moreover, we would like to acknowledge the EASYCHAIR organization for supporting all the tasks related to the selection of contributions, and EPTCS for hosting the proceedings of GandALF 2011. Finally, we gratefully acknowledge the financial support to GandALF 2011 from private and public sponsors, especially the Dipartimento di Informatica (Università degli Studi di Salerno), the Biblioteca of the Università degli Studi di Salerno, the Gruppo Nazionale per il Calcolo Scientifico, the Ente Provinciale per il Turismo della Provincia di Salerno, and the company Unlimited Software Srl.

June 2011,
                                          Giovanna D'Agostino and Salvatore La Torre

General Chair

Program Chairs

Program Committee

Steering Committee

Advisory Board

Organizing Committee

Additional Referees

Eugene Asarin, Mohamed Faouzi Atig, Alexandru Baltag, Massimo Benerecetti, Nathalie Bertrand, Udi Boker, Thomas Brihaye, Alarico Campetelli, Pavol Cerny, Willem Conradie, Dario Della Monica, Laurent Doyen, Alessandro Facchini, Emanuela Fachini, Marco Faella, Oliver Friedmann, Valerio Genovese, Julian Haselmayr, Lukasz Kaiser, Jan Kretinsky, Ruggero Lanotte, Michael Luttenberger, Matthijs Melissen, Paul-André Melliès, Jakub Michaliszyn, Stefano Minopoli, Fabio Mogavero, Margherita Napoli, Carla Piazza, Bernd Puchala, Arjun Radhakrishna, Ivano Salvo, Francesco Sorrentino, Annette Stümpel, Daniel Thoma, Szymon Torunczyk, Tomasz Truderung, Jan Van Eijck.

The monadic theory of linear orders

Thomas Colcombet (CNRS, Paris FRANCE)

In this talk, we will survey the classical results concerning the monadic theory of linear orders, of Büchi, Rabin and Shellah. We will then present more recent contributions obtained in collaboration with Olivier Carton and Gabriele Puppis. In particular, we will present the first known collapse results for monadic logic over countable linear orders.

The Rise and Fall of LTL

Moshe Y. Vardi (Rice University, Houston USA)

One of the surprising developments in the area of program verification in the late part of the 20th Century is the emergence of Linear Temporal Logic (LTL), a logic that emerged in philosophical studies of free will, as the canonical language for describing temporal behavior of computer systems. LTL, however, is not expressive enough for industrial applications. The first decade of the 21st Century saw the emergence of industrial temporal logics such as ForSpec, PSL, and SVA. These logics, however, are not clean enough to serve as objects of theoretical study. This talk will describe the rise and fall of LTL, and will propose a new canonical temporal logic: Linear Dynamic Logic (LDL).

Dependence, Independence, and Imperfect Information

Erich Grädel (RWTH Aachen University, Germany)

We discuss how notions such as dependence and independence can be incorporated into logical systems, and how they are connected to imperfect information in associated games. Specifically, we propose to use independence (rather than dependence) as a basic construct and show that this leads to a more powerful logic with somewhat different model-theoretic properties.