Published: 7th October 2012|
|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|
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.
Marco Faella and Aniello Murano
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.
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.
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:
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.