Preface

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:

• The monadic theory of linear orders, by Thomas Colcombet (CNRS, Paris FRANCE)
• Dependence, Independence, and Incomplete Information, by Erich Grädel (RWTH Aachen University, GERMANY)
• The Rise and Fall of LTL, by Moshe Vardi (Rice University, Houston USA)

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

• Angelo Montanari (Università di Udine, Italy)

Program Chairs

• Giovanna D'Agostino (Università di Udine, Italy)
• Salvatore La Torre (Università di Salerno, Italy)

Program Committee

• Krishnendu Chatterjee (Inst. of Science and Tech, Austria)
• Swarat Chaudhuri (Pennsylvania State University, USA)
• Giorgio Delzanno (Università di Genova, Italy)
• Javier Esparza (Technische Universität München, Germany)
• Erich Grädel (RWTH Aachen University, Germany)
• Neil Immerman (University of Massachusetts, USA)
• Wojtek Jamroga (University of Luxembourg, Luxebourg)
• Vineet Kahlon (NEC Labs, Princeton, USA)
• Martin Leucker (University of Lubeck, Germany)
• Jerzy Marcinkowski (University of Wroclaw, Poland)
• Aniello Murano (University of Napoli "Federico II", Italy)
• Mimmo Parente (Università di Salerno, Italy)
• Gabriele Puppis (Oxford University, UK)
• Alexander Rabinovich (Tel Aviv University, Israel)
• Jean Francois Raskin (University Libre de Bruxelles, Belgium)
• Colin Stirling (University of Edimburgh, UK)
• Tayssir Touili (University Paris Diderot, France)
• Yde Venema (ILLC, University of Amsterdam, The Netherlands)
• Bow-Yaw Wang (INRIA, France and Academy, Taiwan)
• Igor Walukiewicz (LaBRI, Universi,ty of Bordeaux1, France)

Steering Committee

• Mikolaj Bojańczyk (Warsaw University, Poland)
• Javier Esparza (University of Munich, Germany)
• Angelo Montanari (Università di Udine, Italy)
• Margherita Napoli (Università di Salerno, Italy)
• Mimmo Parente (Università di Salerno, Italy)
• Wolfgang Thomas (RWTH Aachen University, Germany)
• Wieslaw Zielonka (University of Paris7, France)

Advisory Board

• Stefano Crespi Reghizzi (Politecnico of Milan, Italy)
• Jozef Gruska (Masaryk University, Czech Republik)
• Oscar H. Ibarra (UCSB, USA)
• Andrea Maggiolo-Schettini (Università di Pisa, Italy)

Organizing Committee

• Marco Faella, chair (Università di Napoli "Federico II", Italy)
• Ciro D'Aniello (Università di Salerno, Italy)
• Ilaria De Crescenzo (Università di Salerno, Italy)
• Dario Della Monica (Università di Salerno, Italy)
• Barbara Di Giampaolo (Università di Salerno, Italy)
• Stefano Minopoli (Università di Napoli "Federico II", Italy)

Additional Referees

The monadic theory of linear orders

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

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

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.