Preface

It is our pleasure to write this foreword to the proceedings of the first Symposium on "Games, Automata, Logic, and Formal Verification (GandALF)", held in Minori (Amalfi coast), Italy, 17-18 June 2010. The symposium has been promoted 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. Such a research community involves people from a number of Italian universities. Its members participate in various italian and international projects on related topics. Many of them have a high-level internationally-recognized scientific profile.

The Symposium covers a large spectrum of research topics, ranging from theoretical aspects to concrete applications. 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 program committee and by the final program.

The invited talks have been given by Mikołaj Bojańczyk, Javier Esparza, Pino Persiano, and Wolfgang Thomas. We received 31 abstract submissions from 13 different countries (Austria, Bulgaria, Czech Republic, France, Germany, India, Italy, Luxembourg, Netherlands, Romania, Russian Federation, United Kingdom, United States). 26 of them have been turned into actual paper submissions. 16 papers have been selected for presentation and publication in these proceedings. The selection of the papers was based on originality, quality, and relevance to the topics of the symposium. Each paper received at least 3 reports and final decisions about acceptance/rejection benefitted from an extensive electronic discussion among program committee members. An extended and revised version of the best symposium papers will be invited for submission to a special issue of one of the major computer science journals.

We wish to thank all the authors of the submitted papers for their interest in GandALF 2010. We also thank the program and organizing committees and all referees for their fruitful work. We gratefully acknowledge the support to GandALF 2010 from private and public sponsors, especially from the Dipartimento di Informatica ed Applicazioni "R.M. Capocelli" and the Gruppo Nazionale per il Calcolo Scientifico. The support and encouragment of the Advisory Chairs helped us a lot to guarantee a high-quality level to the symposium. Finally, let us thank EPTCS for having hosted the Symposium proceedings and for their invaluable contribute to the open access practice.

We hope that GandALF will rapidly become a significant annual appointment for the scientists working in the areas of Games, Automata, Logic, and Formal Verification. We would like to conclude our preface with the words from one of the invited speakers:

"It seems to me that Gandalf may be a new element of the landscape! And of course, I will be coming to Minori and I am already dreaming about walking around in the lemon groves."

Automata for Data Words and Data Trees

University of Warsaw, Poland
bojan@mimuw.edu.pl

Data words and data trees appear in verification and XML processing. The term "data" means that positions of the word, or tree, are decorated with elements of an infinite set of data values, such as natural numbers or ASCII strings. This talk is a survey of the various automaton models that have been developed for data words and data trees. It has two parts.

The first part is related to verification. In this setting, a data word or data tree models the behavior of a system. For example, the data word represents a log of actions of multiple concurrent processes, and data values are used for process identifiers. An automaton reads a data word or data tree and says "yes" if it represents an incorrect behavior. In this situation, the relevant algorithmic problem for the automata is emptiness. Numerous models of automata for data words and data trees have been proposed, representing different tradeoffs between expressive power and complexity of emptiness. The general theme is that, in the presence of data, for almost any automaton model with reasonable closure properties, the emptiness problem is undecidable, or at least prohibitively complex. Even the simplest mechanisms for accessing data can be used to encode such difficult problems as reachability in gainy counter automata, or reachability in Petri nets. These questions, revolving around the emptiness problem for automata with data, will be the topic of the first part of this talk.

The second part is related to query evaluation. XML documents can be naturally modeled as data trees. The data values are used to represent attribute values in XML documents, information that would get lost when modeling an XML document as a tree over a fixed alphabet. A central problem in databases is query evaluation, which is similar to model-checking: given a query φ(x₁,...,x_n) which selects n-tuples of nodes in an XML document, and given an input document t, find the set of n-tuples selected by φ in t. Typical situations are when n is 0 (the query says "yes" or "no"), and when n=1 (the query selects a subset of nodes). Due to the size of XML documents, an evaluation algorithm should be really efficient in terms of the document size, e.g. linear and not quadratic. The mechanisms for accessing data make evaluation a problem that is much more sophisticated than simply running a few passes of a finite-state automaton, a s would be the case for trees without data. Nevertheless, techniques from automata theory (and from algebra) are useful in designing such efficient evaluation algorithms. These questions, revolving around the evaluation problem for automata with data, will be the topic of the second part of this talk.

References

[1] Michael Benedikt, Wenfei Fan, and Floris Geerts. XPath satisfiability in the presence of DTDs. In PODS, pages 25-36, 2005.

[2] H. Björklund and T. Schwentick. On notions of regularity for data languages. In FCT, pages 88-99, 2007.

[3] Mikołaj Bojańczyk, Sławomir Lasota. An extension of data automata that captures XPath. To appear in LICS, 2010.

[4] Mikołaj Bojańczyk, Anca Muscholl, Thomas Schwentick, and Luc Segoufin. Two-variable logic on data trees and XML reasoning. J. ACM, 56(3), 2009.

[5] Mikołaj Bojańczyk, Anca Muscholl, Thomas Schwentick, Luc Segoufin, and Claire David. Two-variable logic on words with data. In LICS, pages 7-16, 2006.

[6] Mikołaj Bojańczyk, Paweł Parys. Efficient evaluation of nondeterministic automata using factorization forests. To appear in ICALP, 2010.

[7] Stéphane Demri and Ranko Lazić. LTL with the freeze quantifier and register automata. ACM Trans. Comput. Log., 10(3), 2009.

[8] Diego Figueira. Forward-XPath and extended register automata on data-trees. In ICDT, 2010. To appear.

[9] Marcin Jurdziński and Ranko Lazić. Alternation-free modal mu-calculus for data trees. In LICS, pages 131-140, 2007.

[10] Michael Kaminski and Nissim Francez. Finite-memory automata. Theor. Comput. Sci., 134(2):329-63, 1994.

[11] Luc Segoufin. Automata and logics for words and trees over an infinite alphabet. In CSL, pages 41-57, 2006.

Stochastic Branching Processes: A Computer Science Perspective

Institut für Informatik, Technische Universität München, Garching bei München, Germany

In stochastic theory, a branching process is a random process modeling a population in which individuals are born, reproduce, and die according to a given probabilistic law. Branching processes have been studied in depth, and there exist several excellent books, some of them classics [1,5]. The theory finds many applications in biology (e.g., study of cell cycles), theoretical ecology (animal populations), physics (particle cascades) or chemistry (study of chemical reactions).
In the last two years my coauthors and I have studied the theory of branching processes from a computer science point of view, and have contributed to it in two different ways.

Single-processor systems. Computer science systems often consist of entities that "reproduce", "replicate", or "create new instances". Obvious examples are threads in multithreaded programs, processes in operating systems, and computer viruses; less obvious examples include procedure calls, which create new incarnations of the callee, or divide-and-conquer procedures, which split a problem into subproblems. When we tried to apply the theory of branching processes to these systems, we observed that computer science applications introduce an essential new aspect: the distinction between processes (software) and processors (hardware). In ecology scenarios each individual animal is both a process and the processor executing it, and the same identification occurs in physics or chemistry applications. So, from a computer science perspective, probability theorists have only studied systems with an unbounded number of processors, in which every new process is immediately assigned a fresh processor. Systems in which one single processor (or a fixed number of them) execute all processes have received, to the best of our knowledge, no attention. In two recent papers, coauthored with Tomás Brázdil, Stefan Kiefer, and Michael Luttenberger[2,3], we have studied the memory consumption of branching processes in which one single processor is in charge of executing all processes. More precisely, we present tail bounds on the random variable modeling the amount of memory used by the processor in order to store the tasks pending execution.

Solving fundamental equations. The theory of branching processes studies how to compute parameters like the probability of extinction of a species, the probability that a neutron will produce a chain reaction, or the expected runtime of a program. In most cases there is no closed-form expression for the parameter, and the theory provides an equation or system of equations having the parameter as solution. A class of equations turns out to be particularly pervasive: systems of fixed-point equations of the form

References

[1] K.B. Athreya & P.E. Ney (1972): Branching Processes. Springer.

[2] Tomás Brázdil, Javier Esparza & Stefan Kiefer (2009): On the Memory Consumption of Probabilistic Pushdown Automata. In: Ravi Kannan & K. Narayan Kumar, editors: FSTTCS, LIPIcs 4, Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, pp. 49-60. Available at http://dx.doi.org/10.4230/LIPIcs.FSTTCS.2009.2306.

[3] Tomás Brázdil, Javier Esparza, Stefan Kiefer & Michael Luttenberger (2010): Space-efficient scheduling of stochastically generated tasks. In: ICALP, Lecture Notes in Computer Science (to appear), Springer.

[4] Javier Esparza, Andreas Gaiser & Stefan Kiefer (2010): Computing Least Fixed Points of Proba- bilistic Systems of Polynomials. In: Jean-Yves Marion & Thomas Schwentick, editors: STACS, LIPIcs 5, Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, pp. 359-370. Available at http://dx.doi.org/10.4230/LIPIcs.STACS.2010.2468.

[5] T.E. Harris (1963): The Theory of Branching Processes. Springer.

On the Mixing Time of the Logit Dynamics of Strategic Games

Dipartimento di Informatica ed Appl. "Renato M. Capocelli", Universita' di Salerno.
giuper@dia.unisa.it

In this talk I will overview the results on the mixing time of the logit dynamics [2] for strategic games. At every stage of the game a player is selected uniformly at random and she plays according to a noisy best-response dynamics where the noise level is tuned by a parameter beta. Such a dynamics defines a family of ergodic Markov chains, indexed by beta, over the set of strategy profiles. The aim is twofold: On the one hand, one is interested in the expected social welfare when the strategy profiles are random according to the stationary distribution of the Markov chain, because it gives a meaningful description of the long-term behavior of the system. On the other hand, one wants to estimate how long it takes, for a system starting at an arbitrary profile and running the logit dynamics, to get close to the stationary distribution; i.e., the mixing time of the chain.

I will show results on the stationary expected social welfare for the 3-player CK game[3], for 2-player coordination games (the same class of games studied in [2]), 2-player anti-coordination games, and for a simple n-player game. For all these games, we give almost-tight upper and lower bounds on the mixing time of logit dynamics.

Work partially supported by FRONTS EU project.

Joint work with: Vincenzo Auletta, Diodato Ferraioli and Francesco Pasquale

References

[1] Vincenzo Auletta, Diodato Ferraioli, Francesco Pasquale & Giuseppe Persiano (2010): Mixing Time and Stationary Expected Social Welfare of Logit Dynamics. CoRR abs/1002.3474. Available at http://arxiv.org/abs/1002.3474.

[2] Lawrence E. Blume (1993): The Statistical Mechanics of Strategic Interaction. Games and Economic Behavior 5, pp. 387-424.

[3] George Christodoulou & Elias Koutsoupias (2005): The price of anarchy of finite congestion games. In: Proc. of the 37th Annual ACM Symposium on Theory of Computing (STOC'05), ACM, pp. 67-73.

Infinite Games: Tema con Due Variazioni

RWTH Aachen, Lehrstuhl für Informatik 7, D-52056 Aachen
thomas@automata.rwth-aachen.de

The original setting of Church's Problem on the solvability of regular infinite games has been varied in a great number of ways. In this talk we discuss two variations that were touched already in early research on Church's problem and have been revived in recent work.

The first variation is concerned with the relation between game specifications and winning strategies, starting from the observation that regular (or: MSO-definable) infinite games are solvable with "regular" (or again MSO-definable) winning strategies. Such a close connection can be established also for other notions of definability, either in terms of logics or in terms of types of automata. We present recent results and some perspectives.

The second variation addresses a widening of the concept of strategy, taking up the classical view that a strategy in an infinite game defines a special kind of continuous function over omega-sequences. We study the question of solvability of games with strategies that represent different degrees of continuity. This discussion leads naturally to generalized versions of concurrent games. We present basic results and indicate applications in discrete control.

(The first part reports on joint work with A. Rabinovich, J. Olschewski, and W. Fridman, the second part on joint work with M. Holtmann, L. Kaiser, and F. Pöttgen.)