EPTCS 96
Proceedings Third International Symposium on
Games, Automata, Logics and Formal Verification
Napoli, Italy, September 6-8, 2012
Edited by: Marco Faella and Aniello Murano
Preface
|
Invited Presentation:
Biological Networks on (a Lattice of) Hybrid Automata
Alberto Policriti and Luca Bortolussi |
Invited Presentation:
Automata-theoretic hierarchies
Damian Niwiński |
Invited Presentation:
Multi-dimension Quantitative Games: Complexity and Strategy Synthesis
Jean-François Raskin |
Invited Presentation:
Constructive decision theory: Decision theory with subjective states and outcomes
Joe Halpern |
Modelling Implicit Communication in Multi-Agent Systems with Hybrid Input/Output Automata
Marta Capiluppi and Roberto Segala | 1 |
Rapid Recovery for Systems with Scarce Faults
Chung-Hao Huang, Doron Peled, Sven Schewe and Farn Wang | 15 |
Interface Simulation Distances
Pavol Černý, Martin Chmelík, Thomas A. Henzinger and Arjun Radhakrishna | 29 |
Model-Checking Process Equivalences
Martin Lange, Etienne Lozes and Manuel Vargas Guzmán | 43 |
Can Nondeterminism Help Complementation?
Yang Cai and Ting Zhang | 57 |
Learn with SAT to Minimize Büchi Automata
Stephan Barth and Martin Hofmann | 71 |
Automata-based Static Analysis of XML Document Adaptation
Alessandro Solimando, Giorgio Delzanno and Giovanna Guerrini | 85 |
Symbolic Representation of Algorithmic Game Semantics
Aleksandar S. Dimovski | 99 |
The μ-Calculus Alternation Hierarchy Collapses over Structures with Restricted Connectivity
Julian Gutierrez, Felix Klaedtke and Martin Lange | 113 |
Deciding KAT and Hoare Logic with Derivatives
Ricardo Almeida, Sabine Broda and Nelma Moreira | 127 |
Satisfiability vs. Finite Satisfiability in Elementary Modal Logics
Jakub Michaliszyn, Jan Otop and Piotr Witkowski | 141 |
Interval Temporal Logics over Strongly Discrete Linear Orders: the Complete Picture
Davide Bresolin, Dario Della Monica, Angelo Montanari, Pietro Sala and Guido Sciavicco | 155 |
Down the Borel Hierarchy: Solving Muller Games via Safety Games
Daniel Neider, Roman Rabinovich and Martin Zimmermann | 169 |
Playing Pushdown Parity Games in a Hurry
Wladimir Fridman and Martin Zimmermann | 183 |
The discrete strategy improvement algorithm for parity games and complexity measures for directed graphs
Felix Canavoi, Erich Grädel and Roman Rabinovich | 197 |
Higher-Order Pushdown Systems with Data
Paweł Parys | 210 |
A decidable quantified fragment of set theory with ordered pairs and some undecidable extensions
Domenico Cantone and Cristiano Longo | 224 |
A Myhill-Nerode theorem for automata with advice
Alex Kruckman, Sasha Rubin, John Sheridan and Ben Zax | 238 |
Unambiguous Tree Languages Are Topologically Harder Than Deterministic Ones
Szczepan Hummel | 247 |
This volume contains the proceedings of the Third International Symposium
on Games, Automata, Logic and Formal Verification (GandALF), held in Naples (Italy)
from September 6th to 8th, 2012.
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 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 the programme.
This year GandALF has hosted four invited talks, three of which were shared
with the co-located Annual Workshop of the ESF Networking Programme on Games for Design and Verification:
- Biological networks on (a lattice of) Hybrid Automata, by Alberto Policriti (Università di Udine, Italy)
- Automata-theoretic hierarchies, by Damian Niwinski (Warsaw University, Poland)
- Multi-dimensional quantitative games: complexity and strategy synthesis, by Jean-Francois Raskin (Université Libre de Bruxelles, Belgium)
- Constructive decision theory: Decision theory with subjective states and outcomes, by Joseph Halpern (Cornell University, USA)
Moreover, the program committee selected 19 contributed talks among 39 submissions.
Each paper has been revised by at least three referees and the papers have been selected according to originality, quality, and relevance to the topics of the symposium.
We would like to acknowledge the people, institutions, and companies which
contributed to the success of this edition of GandALF.
Let us first thank the Advisory Board and the Steering Committee for giving us the opportunity and the honor to supervise GandALF 2012.
Many thanks go to all the Program Committee members and the additional reviewers for their excellent work, the fruitful discussions and the active participation during the reviewing process. companies and all the members of the Organizing Committee for the great work.
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. Finally, we gratefully acknowledge the financial support to GandALF 2012 from private and public sponsors, including the Università degli Studi di Napoli "Federico II", the Gruppo Nazionale per il Calcolo Scientifico,
the Comune di Napoli, and the company Gruppo Tufano.
September 2012,
Marco Faella and Aniello Murano
Program Chairs
- Marco Faella (Università di Napoli "Federico II", Italy)
- Aniello Murano (Università di Napoli "Federico II", Italy)
Program Committee
- Veronique Bruyere (Université de Mons, Belgium)
- Agostino Cortesi (Università di Venezia, Italy)
- Luca de Alfaro (University of California, USA)
- Kousha Etessami (University of Edinburgh, Scotland, UK)
- Erich Grädel (RWTH Aachen University, Germany)
- Arie Gurfinkel (Carnegie Mellon, USA)
- Orna Kupferman (Hebrew Unversity, Israel)
- Martin Lange (University of Kassel, Germany)
- Carsten Lutz (University of Bremen, Germany)
- Oded Maler (Verimag, France)
- Nicolas Markey (CNRS Cachan, France)
- Anca Muscholl (Université Bordeaux 1, France)
- Margherita Napoli (Università di Salerno, Italy)
- Damian Niwinski (Universitet Warszawski, Poland)
- Carla Piazza (Università di Udine, Italy)
- Nir Piterman (University of Leicester, UK)
- Gabriele Puppis (University of Oxford, UK)
- Ramaswamy Ramanujam (IMSC Chennai, India)
- Natasha Sharygina (University of Lugano, Switzerland)
- Sven Schewe (University of Liverpool, UK)
- Mariëlle Stoelinga (University of Twente, The Netherlands)
- Enrico Tronci (Università di Roma "La Sapienza", Italy)
- Helmut Veith (Technische Universität Wien, Austria)
- Tiziano Villa (Università di Verona, Italy)
- Mahesh Viswanathan (University of Illinois, USA)
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
- Valerio Maggio (Università di Napoli "Federico II", Italy)
- Marilena Marotta
- Dario Della Monica (Reykjavik University, Iceland)
- Stefano Minopoli (Università di Napoli "Federico II", Italy)
- Milena Pugliese
Additional Referees
Francesco Alberti, Henning Bordihn, Davide Bresolin, Gianfranco Ciardo,
Ene Cristian, Giovanna D'Agostino, Aldric Degorre, Dario Della Monica, Laurent Doyen,
John Fearnley, Grigory Fedyukovich, Olivier Finkel, Seth Fogarty,
Dominik D. Freydenberger, Olivier Gauwin, Raffaella Gentilini, Stefan Göller,
Antti Hyvärinen, Salvatore La Torre, Kamal Lodaya, Damiano Macedonio,
Dejan Nickovic, Eugenio Omodeo, Mimmo Parente, Soumya Paul, Samuel Rota Bulò,
Sylvain Salvati, Olivier Serre, Anil Seth, Sunil Easaw Simon, Ramesh Viswanathan,
Josef Widder, Konrad Zdanowski, and Florian Zuleger.
Alberto Policriti (Università di Udine, Italy)
Luca Bortolussi (Università di Trieste, Italy)
We discuss the problem of designing and implementing formalisms
suitable to represent continuous and discrete evolving processes,
operating in a combined and cooperating fashion and capable to
encompass some level of stochastic behavior.
In this context we present a language allowing to write programs
used, for example, to simulate Biological Networks and incorporating
the possibility to model stochastic interactions. The language we
employ is stochastic Concurrent Constraint Programming (sCCP), a
stochastic process algebra admitting a semantics given in terms of
stochastic Hybrid Automata with piecewise deterministic continuous
dynamics.
We then proceed outlining a framework in which it is possible to
associate to each sCCP program, a collection of different hybrid
models. The stochastic Hybrid Automata associated to a given sCCP
program can be presented in a lattice, in which the position is
determined by the degrees of discreteness and stochasticity to be
found in the automaton.
We conclude discussing some interesting properties of the automata in
this lattice and observing, for example, how different discretization
strategies naturally correspond to different implementation schemata
for the same program.
Damian Niwiński (University of Warsaw, Poland)
Hierarchies appear in many places in computer science, as a tool to
classify objects according to their complexity. For automata on
infinite words and trees, a relevant complexity measure is the
Rabin-Mostowski index of the acceptance condition. The strictness of
the induced index hierarchy for alternating automata on infinite trees
has been a major open problem eventually solved by Bradfield in 1998.
We show a somewhat simpler argument here, based on an analogy
with deterministic automata on infinite words via suitable games.
We also present the state-of-the-art regarding the separation
and reduction properties, which in classical examples orientate the
hierarchies (Π vs. Σ). We will outline the connections between the
automata-theoretic hierarchies and other hierarchies in the literature,
in particular in the μ-calculus and descriptive set theory, and point
to some intriguing open problems concerning decidability issues.
Jean-François Raskin (Université Libre de Bruxelles, U.L.B., Belgium)
In mean-payoff games, the objective of the protagonist is to ensure that the limit average of an infinite sequence of numeric weights is nonnegative. In energy games, the objective is to ensure that the running sum of weights is always nonnegative. Multi-mean-payoff and multi-energy games replace individual weights by tuples, and the limit average (resp. running sum) of each coordinate must be (resp. remain) nonnegative. These games have applications in the synthesis of resource-bounded processes with multiple resources.
In this talk, I will summarize several recent results that we have obtained recently:
- We prove the finite-memory determinacy of multi-energy games and show the inter-reducibility of multi-mean-payoff and multi-energy games for finite-memory strategies.
- We improve the computational complexity for solving both classes of games with finite-memory strategies: while the previously best known upper bound was ExpSpace, and no lower bound was known, we give an optimal coNP-complete bound. For memoryless strategies, we show that the problem of deciding the existence of a winning strategy for the protagonist is NP-complete.
- We provide an optimal symbolic and incremental algorithm to synthesis strategies in multi-energy games.
- We present the first solution of multi-mean-payoff games with infinite-memory strategies. We show that multi-mean-payoff games with mean-payoff- sup objectives can be decided in
NP ∩ coNP, whereas multi-mean-payoff games with mean-payoff-inf objectives are
coNP-complete.
Joe Halpern (Cornell University, USA)
The standard approach in decision theory (going back to Savage) is to place
a preference order on acts, where an act is a function from states to
outcomes. If the preference order satisfies appropriate postulates,
then the decision maker can be viewed as acting as if he has a
probability on states and a utility function on outcomes, and is
maximizing expected utility. This framework implicitly assumes that the
decision maker knows what the states and outcomes are. That isn't
reasonable in a complex situation. For example, in trying to decide
whether or not to attack Iraq, what are the states and what are the
outcomes? We redo Savage viewing acts essentially as syntactic
programs. We don't need to assume either states or outcomes. However,
among other things, we can get representation theorems in the spirit of
Savage's theorems; for Savage, the agent's probability and utility are
subjective; for us, in addition to the probability and utility being
subjective, so is the state space and the outcome space. I discuss the
benefits, both conceptual and pragmatic, of this approach. As I show,
among
other things, it provides an elegant solution to framing problems.
No prior knowledge of Savage's work is assumed.
Further details can be found in the following paper:
L. Blume, D. Easley, and J. Y. Halpern. Redoing the foundations of decision theory.
In Principles of Knowledge Representation and Reasoning: Proc. Tenth International
Conference (KR 2006), pages 14--24, 2006. A longer version, with the title "Constructive
decision theory", is available online.