Published: 4th June 2011|
|Preface 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||1|
|Improving BDD Based Symbolic Model Checking with Isomorphism Exploiting Transition Relations Christian Appold||17|
|Computing the Reveals Relation in Occurrence Nets Stefan Haar, Christian Kern and Stefan Schwoon||31|
|Automated Analysis of MUTEX Algorithms with FASE Federico Buti, Massimo Callisto De Donato, Flavio Corradini, Maria Rita Di Berardini and Walter Vogler||45|
|Optimal Strategies in Infinite-state Stochastic Reachability Games Václav Brožek||60|
|A reduction from parity games to simple stochastic games Krishnendu Chatterjee and Nathanaël Fijalkow||74|
|Opacity Issues in Games with Imperfect Information Bastien Maubert, Sophie Pinchinat and Laura Bozzelli||87|
|Type Inference for Bimorphic Recursion Makoto Tatsuta and Ferruccio Damiani||102|
|A Decidable Extension of Data Automata Zhilin Wu||116|
|Connectivity Games over Dynamic Networks Sten Grüner, Frank G. Radmacher and Wolfgang Thomas||131|
|Optimal Bounds in Parametric LTL Games Martin Zimmermann||146|
|New results on pushdown module checking with imperfect information Laura Bozzelli||162|
|Reactive Safety Rüdiger Ehlers and Bernd Finkbeiner||178|
|An Optimal Decision Procedure for MPNL over the Integers Davide Bresolin, Angelo Montanari, Pietro Sala and Guido Sciavicco||192|
|Separation of Test-Free Propositional Dynamic Logics over Context-Free Languages Markus Latte||207|
|On P-transitive graphs and applications Giacomo Lenzi||222|
|A Game-Theoretic approach to Fault Diagnosis of Hybrid Systems Davide Bresolin and Marta Capiluppi||237|
|Deciding Reachability for 3-Dimensional Multi-Linear Systems Olga Tveretina and Daniel Funke||250|
|Towards Efficient Exact Synthesis for Linear Hybrid Systems Massimo Benerecetti, Marco Faella and Stefano Minopoli||263|
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:
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.
Giovanna D'Agostino and Salvatore La Torre
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.
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).
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.