Proceedings Fourth International Symposium on
Edited by: Gabriele Puppis and Tiziano Villa
Games, Automata, Logics and Formal Verification
Borca di Cadore, Dolomites, Italy, 29-31th August 2013
Gabriele Puppis and Tiziano Villa|
Games with delay for automaton synthesis
New trends in program synthesis
Thomas A. Henzinger||3|
Temporal logic satisfiability for the design of complex systems
Alessandro Cimatti and Stefano Tonetta||4|
Zielonka's Recursive Algorithm: dull, weak and solitaire games and tighter bounds
Maciej Gazda and Tim A.C. Willemse||7|
Simple strategies for Banach-Mazur games and fairly correct systems
Thomas Brihaye and Quentin Menet||21|
The Rabin index of parity games
Michael Huth, Jim Huan-Pu Kuo and Nir Piterman||35|
A Faster Tableau for CTL*
Deciding the Satisfiability of MITL Specifications
Marcello Maria Bersani, Matteo Rossi and Pierluigi San Pietro||64|
Improving HyLTL model checking of hybrid systems
Upwards Closed Dependencies in Team Semantics
Profile Trees for Büchi Word Automata, with Application to Determinization
Seth Fogarty, Orna Kupferman, Moshe Y. Vardi and Thomas Wilke||107|
Weighted Automata and Monadic Second Order Logic
Nadia Labai and Johann A. Makowsky||122|
Approximating the minimum cycle mean
Krishnendu Chatterjee, Monika Henzinger, Sebastian Krinninger and Veronika Loitzenbauer||136|
Probabilistic data flow analysis: a linear equational approach
Alessandra Di Pierro and Herbert Wiklicky||150|
Slot Games for Detecting Timing Leaks of Programs
Aleksandar S. Dimovski||166|
Social Network Games with Obligatory Product Selection
Krzysztof R. Apt and Sunil Simon||180|
Alternating-time temporal logic with finite-memory strategies
Satisfiability of ATL with strategy contexts
François Laroussinie and Nicolas Markey||208|
Modularity and Openness in Modeling Multi-Agent Systems
Wojciech Jamroga, Artur Mȩski and Maciej Szreter||224|
Model checking coalitional games in shortage resource scenarios
Dario Della Monica, Margherita Napoli and Mimmo Parente||240|
This volume contains the proceedings of the Fourth International Symposium on Games, Automata, Logic and Formal Verification (GandALF 2013). The symposium took place in Borca di Cadore, Italy, from 29th to 31st of August 2013.
The GandALF symposium was established 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. It aims 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 by the country distribution of the submitted papers.
In response to the Call for Papers, the program committee received 34 submissions and selected 17 of them to be included in the conference program. Each paper was revised by at least three referees and the selection was based on originality, quality, and relevance to the topics of the symposium. The scientific program consisted of papers on a wide variety of topics, including algorithmic and behavioral game theory, game semantics, formal languages and automata theory, modal and temporal logics, software verification, hybrid systems.
This fourth edition of GandALF has also hosted three invited talks:
- Games with delay for automaton synthesis, by Christof Löding (Lehrstuhl Informatik 7, RWTH Aachen University, Germany)
- New trends in program synthesis, by Thomas A. Henzinger (IST, Austria)
- Temporal logic satisfiability for the design of complex systems, by Alessandro Cimatti and Stefano
Tonetta (Center for Information Technology, Fondazione Bruno Kessler, Trento, Italy)
We wish to express our thanks to the authors who submitted extended abstracts for consideration.
We would like to thank also the steering committee for giving us the opportunity and the honor to supervise GandALF 2013, as well as the program committee members and the additional reviewers for their excellent work, fruitful discussions and active participation during the evaluation process.
We would like to thank the people, institutions, and companies for contributing to the success of this edition of GandALF. In particular, we gratefully acknowledge the financial support from private and public sponsors, including: Dipartimento d'Informatica - Università di Verona, Dipartimento d'Informatica - Università di Salerno, Comune di Borca di Cadore.
We also thank the EasyChair organization for supporting all the tasks related to the selection of contributions, EPTCS and arXiv for hosting the proceedings.
Finally, we would like to extend special thanks to the organizing chair, Pietro Sala, for his care and tireless efforts in making the local arrangements and organizing an attractive social program. Without his dedicated help and diligent work the conference would not have been such a success.
Gabriele Puppis and Tiziano Villa
Luca Aceto, University of Reykjavik, Iceland
Rajeev Alur, University of Pennsylvania, United States
Arnaud Carayol, IGM, Marne-la-Vallee, France
Anuj Dawar, University of Cambridge, United Kingdom
Stephane Demri, CNRS/New York University, United States
Volker Diekert, University of Stuttgart, Germany
Javier Esparza, University of Munich, Germany
Valentin Goranko, Technical University of Denmark, Denmark
Bakhadyr Khoussainov, University of Auckland, New Zealand
Naoki Kobayashi, University of Tokyo, Japan
Stephan Kreutzer, University of Berlin, Germany
Marta Kwiatkowska, University of Oxford, United Kingdom
Martin Lange, University of Kassel, Germany
Angelo Montanari, University of Udine, Italy
Mimmo Parente, University of Salerno, Italy
Adriano Peron, University of Naples, Italy
Gabriele Puppis, LaBRI, Bordeaux, France (co-chair)
Alexander Rabinovich, University of Tel Aviv, Israel
Ramaswamy Ramanujam, Institute of Mathematical Sciences, Chennai, India
Jean Francois Raskin, University of Bruxelles, Belgium
Davide Sangiorgi, University of Bologna, Italy
Olivier Serre, LIAFA, Paris, France
Sharon Shoham, Academic College of Tel Aviv Yaffo, Israel
Szymon Torunczyk, University of Warsaw, Poland
Tiziano Villa, University of Verona, Italy (co-chair)
Zhilin Wu, State Key Laboratory of Computer Science, China
Hsu-Chun Yen, National Taiwan University, Taiwan
Pietro Sala, University of Verona, Italy
Mikolaj Bojanczyk, University of Warsaw, Poland
Javier Esparza, University of Munich, Germany
Andrea Maggiolo-Schettini, University of Pisa, Italy
Angelo Montanari, University of Udine, Italy
Margherita Napoli, University of Salerno, Italy
Mimmo Parente, University of Salerno, Italy
Wolfgang Thomas, RWTH Aachen University, Germany
Wieslaw Zielonka, University of Paris 7, France
Massimo Benerecetti, Nataliia Bielova, Davide Bresolin, Nils Bulling, Supratik Chakraborty, Taolue Chen, David Cock, Catalin Dima, Klaus Dräger, Marco Faella, Moran Feldman, Nathanaël Fijalkow, Goran Frehse, Oliver Friedmann, Gilles Geeraerts, Dan Ghica, Hugo Gimbert, Paul Hunter, Yoshinao Isobe, Lukasz Kaiser, Curtis Kent, Aleks Kissinger, Denis Kuperberg, Simon Leßenich, Kamal Lodaya, Etienne Lozes, Michael Luttenberger, Radu Mardare, Bastien Maubert, Till Mossakowski, Aniello Murano, Sylvain Perifel, Pietro Sala, Ulrich Schöpp, Sarai Sheinvald, Aistis Simaitis, Hans Tompits, Dirk Walther.
Christof Löding (Lehrstuhl Informatik 7, RWTH Aachen University, Germany)
The framework of infinite two-player games is a powerful and flexible
tool to verify and synthesize systems from given specifications. The
origin of this work is the problem of automatic circuit synthesis from
specifications, as posed in . A circuit can be viewed
as a device that transforms input sequences of bit vectors into output
sequences of bit vectors. If the circuit acts as a kind of control
device, then these sequences are assumed to be infinite because the
computation should never halt.
The task in synthesis is to construct such a circuit based on a formal
specification describing the desired input/output behaviour. This
problem setting can be viewed as a game of infinite duration between
two players: The first player provides the bit vectors for the input,
and the second player produces the output bit vectors. The winning
condition of the game is given by the specification. The goal is to
find a strategy for the second player, such that all pairs of
input/output sequences that can be produced according to the
strategy, satisfy the specification. Such a strategy can be seen as a
realisation of the specification.
This approach using games as a model for the synthesis problem has
been taken in , where it is shown that the synthesis
problem can be solved by an algorithm for specifications that are
written in monadic second-order logic. Furthermore, for a given
specification, one can construct a strategy represented by a finite
transducer that reads the input sequence and synchronously produces an
output sequence such that the resulting pair of input/output sequence
satisfies the specification.
An interesting variation of the problem arises when the constructed
strategy can use a lookahead: it does not need to produce an output in
each step. In the corresponding game this means that the second
player, who is in charge of the output, can delay some of his moves.
An early decidability result in such a setting has been obtained in
, where the strategy is allowed to skip a bounded
number of moves in order to obtain a bounded look-ahead.
The aim of this presentation is to survey some recent results that
have been obtained for games with delay, as for example, games with
arbitrary (not necessarily bounded) delay , delay games
with deterministic pushdown specifications , and delay
games over finite words for the synthesis of sequential transducers
J. Richard Büchi & Lawrence H. Landweber (1969):
Solving sequential conditions by finite-state strategies.
Transactions of the American Mathematical Society 138,
Arnaud Carayol & Christof Löding:
Uniformization in Automata Theory.
To appear in the Proceedings of the 14th Congress of Logic, Methodology and Philosophy of Science Nancy, July 19-26, 2011.
Alonzo Church (1962):
Logic, Arithmetic and Automata.
In: Proceedings of the International Congress of Mathematicians,
Wladimir Fridman, Christof Löding & Martin Zimmermann (2011):
Degrees of Lookahead in Context-free Infinite Games.
In: Marc Bezem: Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL,
Leibniz International Proceedings in Informatics (LIPIcs) 12.
Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik,
Michael Holtmann, Łukasz Kaiser & Wolfgang Thomas (2010):
Degrees of Lookahead in Regular Infinite Games.
In: Foundations of Software Science and Computational Structures,
Lecture Notes in Computer Science 6014.
Frederick A. Hosch & Lawrence H. Landweber (1972):
Finite Delay Solutions for Sequential Conditions.
Thomas A. Henzinger (IST Austria)
The synthesis of reactive programs from omega-regular specifications
is based on finding winning strategies in graph games. In recent
years, program synthesis has seen a revival due to several variations
and extensions of this basic theme. We survey three such new trends.
First, partial program synthesis shifts the emphasis from the problem
of synthesizing whole programs from specifications to the problem of
completing a partial program so that it satisfies a desired property.
Second, quantitative program synthesis aims to find a solution that
optimizes a given criterion, such as performance, robustness, or
resource consumption. Third, concurrent program synthesis may require
the computation of equilibria in graph games with multiple players
that represent independent concurrent processes. Recent progress in
these directions promises to replace some particularly intricate
aspects of programming, such as the placement of synchronization
or security primitives, by automatic code generation.
This work has been supported in part by an ERC Advanced Grant (QUAREM -
Quantitative Reactive Models) and by an FWF National Research Network
(RISE - Rigorous Systems Engineering).
Alessandro Cimatti (Center for Information Technology, Fondazione Bruno Kessler, Trento, Italy)
Stefano Tonetta (Center for Information Technology, Fondazione Bruno Kessler, Trento, Italy)
The development of computer-based dynamic systems is a very hard
task. On the one hand, the required functionalities are very complex,
and often include inherently contradicting aspects (e.g. moving trains
in a railways station versus avoiding crashes). On the other hand, it
is required to integrate the continuous dynamics of physical plants
with the discrete dynamics in the control modules and procedures.
In addition, such systems often carry out critical functions, which
calls for rigorous means to support a development process. The use of
a formal approach, coupled with suitable reasoning tools, has found
its way in several practical domains, such as
railways , industrial production , hardware
design [2,13,11], and avionics .
Most formal approaches focus on a behavioral characterization of a
system, possibly expressed as an automaton or network/hierarchy of
automata. Model-based approaches build this behavioral model as a
result of semantics-preserving transformation of some design language,
and use the model to verify the system description. The verification
uses some properties, in form of first-order or temporal formulas,
which represent the requirements and are typically assumed to be
More recently, the role of properties is being recognized as
increasingly important. For example, in hardware design, specification
languages for properties (e.g. PSL , SVA ) have
been introduced to increase expressive power (augmenting for example
Linear-time Temporal Logic (LTL) with regular expressions) and
usability (using natural language expressions and maximizing the
syntactic sugar). The quality of the assertions
expressed with such languages has emerged as a problem leading to the
development of specialized techniques for their
Interestingly, the same type of problem has been addressed in
requirements engineering, across domains, for many years. According to
studies sponsored by NASA in 90s, many software bugs in
safety-critical embedded systems were due to flaws in
requirements . The role of formal methods in finding such
errors is becoming more and more important (e.g., ).
The role of properties is also fundamental in compositional
reasoning , where a global verification problem is
decomposed into a number of localized problems. Finally, contract
based design  allows to decompose
the properties of the architectural blocks according to the
hierarchical system decomposition, before behavioral descriptions are
available, and provides a strong support for property-based refinement
and reuse of components .
In the talk, we explore the role of temporal logic satisfiability in
the design of complex systems, focusing on a property-based design,
where behaviors of systems are expressed as formulas in temporal
logics. We first discuss the challenges resulting in practice from
requirements analysis, compositional reasoning, and contract-based
design, showing that satisfiability of temporal formulas is a crucial
Then, we analyze the satisfiability problem for various logics of
interest. We adopt a linear model of time, and take into account two
kinds of traces: discrete traces and hybrid traces.
Properties are therefore represented by sets of traces and temporal
formulas are used to specify such sets.
We analyze two classes of temporal logics of practical interest. The
first class is interpreted over discrete traces, that are sequences of
states (assignments to sets of variables). It includes the usual
temporal operators of Linear Temporal Logic (LTL) ,
regular expression and suffix operators [10,4]. In
addition, it allows for first order atoms, composed of symbols to be
interpreted according to a background theory, similarly to
Satisfiability Modulo Theories . We call this class
RELTL(T), LTL with regular expressions Modulo Theory. This class is
decidable for specific classes of theories and if the variable
interpretation is local to each state .
The second class, referred to as HRELTL, for Hybrid
RELTL , is interpreted over hybrid traces. Hybrid traces
are useful to model the behaviors of systems featuring continuous
transitions, with discrete, instantaneous transitions. Continuous
variables are interpreted as functions of time, and the predicates are
required to have a uniform interpretation over all interval.
The satisfiability problem for HRELTL is undecidable. However, there
exists a satisfiability-preserving reduction from HRELTL to RELTL(T)
over discrete traces .
The main idea is to introduce a sufficient number of constraints on
the temporal evolution of the evaluation of predicates to guarantee
that the nature of the hybrid dynamics is retained also in the
We conclude the talk with an overview of the practical effectiveness
of the current methods, and the open challenges in the area.
C.W. Barrett, R. Sebastiani, S.A. Seshia & C. Tinelli (2009):
Satisfiability Modulo Theories.
In: Handbook of Satisfiability,
M. Bernardo & A. Cimatti (2006):
Formal Methods for Hardware Verification, 6th International School on Formal Methods for the Design of Computer, Communication, and Software Systems, SFM 2006, Bertinoro, Italy, May 22-27, 2006, Advanced Lectures.
Lecture Notes in Computer Science 3965.
R. Bloem, R. Cavada, I. Pill, M. Roveri & A. Tchaltsev (2007):
RAT: A Tool for the Formal Analysis of Requirements.
D. Bustan, A. Flaisher, O. Grumberg, O. Kupferman & M.Y. Vardi (2005):
A. Cimatti, R. Corvino, A. Lazzaro, I. Narasamdya, T. Rizzo, M. Roveri, A. Sanseviero & A. Tchaltsev (2012):
Formal Verification and Validation of ERTMS Industrial Railway Train Spacing System.
A. Cimatti, M. Roveri, V. Schuppan & S. Tonetta (2007):
Boolean Abstraction for Temporal Logic Satisfiability.
A. Cimatti, M. Roveri, A. Susi & S. Tonetta (2012):
Validation of requirements for hybrid systems: A formal approach.
ACM Trans. Softw. Eng. Methodol. 21(4),
A. Cimatti, M. Roveri & S. Tonetta (2009):
Requirements Validation for Hybrid Systems.
A. Cimatti & S. Tonetta (2012):
A Property-Based Proof System for Contract-Based Design.
C. Eisner & D. Fisman (2006):
A Practical Introduction to PSL (Series on Integrated Circuits and Systems).
Springer-Verlag New York, Inc.,
A. Franzén, A. Cimatti, A. Nadel, R. Sebastiani & J. Shalev (2010):
Applying SMT in symbolic execution of microcode.
Available at http://ieeexplore.ieee.org/xpls/abs_all.jsp?arnumber=5770940.
S. Ghilardi, E. Nicolini, S. Ranise & D. Zucchelli (2007):
Combination Methods for Satisfiability and Model-Checking of Infinite-State Systems.
W.A. Hunt, Jr., S. Swords, J. Davis & A. Slobodová (2010):
Use of Formal Verification at Centaur Technology.
In: Design and Verification of Microprocessor Systems for High-Assurance Applications.
R.R. Lutz (1993):
Analyzing Software Requirements Errors in Safety-Critical, Embedded Systems.
S.P. Miller, M.W. Whalen & D. D. Cofer (2010):
Software model checking takes off.
Commun. ACM 53(2),
A. Pnueli (1977):
The Temporal Logic of Programs.
W.P. de Roever, F.S. de Boer, U. Hannemann, J. Hooman, Y. Lakhnech, M. Poel & J. Zwiers (2001):
Concurrency Verification: Introduction to Compositional and Noncompositional Methods.
Cambridge Tracts in Theoretical Computer Science 54.
Cambridge University Press.
A.L. Sangiovanni-Vincentelli, W. Damm & R. Passerone (2012):
Taming Dr. Frankenstein: Contract-Based Design for Cyber-Physical Systems.
Eur. J. Control 18(3),
S. Vijayaraghavan & M. Ramanathan (2005):
A Practical Guide for SystemVerilog Assertions.
M. Weißmann, S. Bedenk, C. Buckl & A. Knoll (2011):
Model Checking Industrial Robot Systems.