Published: 16th July 2013
DOI: 10.4204/EPTCS.119
ISSN: 2075-2180

EPTCS 119

Proceedings Fourth International Symposium on
Games, Automata, Logics and Formal Verification
Borca di Cadore, Dolomites, Italy, 29-31th August 2013

Edited by: Gabriele Puppis and Tiziano Villa

Preface
Gabriele Puppis and Tiziano Villa
Invited Presentation: Games with delay for automaton synthesis
Christof Löding
1
Invited Presentation: New trends in program synthesis
Thomas A. Henzinger
3
Invited Presentation: 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*
Mark Reynolds
50
Deciding the Satisfiability of MITL Specifications
Marcello Maria Bersani, Matteo Rossi and Pierluigi San Pietro
64
Improving HyLTL model checking of hybrid systems
Davide Bresolin
79
Upwards Closed Dependencies in Team Semantics
Pietro Galliani
93
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
Steen Vester
194
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

Preface

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:

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.


August 2013,
Gabriele Puppis and Tiziano Villa

Program Committee

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

Organizing Chair

Pietro Sala, University of Verona, Italy

Steering Committee

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

Additional Reviewers

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.

Games with delay for automaton synthesis

Christof Löding (Lehrstuhl Informatik 7, RWTH Aachen University, Germany)

Abstract

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 [3]. 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 [1], 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 [6], 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 [5], delay games with deterministic pushdown specifications [4], and delay games over finite words for the synthesis of sequential transducers [2].

References

  1. J. Richard Büchi & Lawrence H. Landweber (1969): Solving sequential conditions by finite-state strategies. Transactions of the American Mathematical Society 138, pp. 295–311, doi:10.2307/1994916.
  2. 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.
  3. Alonzo Church (1962): Logic, Arithmetic and Automata. In: Proceedings of the International Congress of Mathematicians, pp. 23–35.
  4. 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, Dagstuhl, Germany, pp. 264–276, doi:10.4230/LIPIcs.CSL.2011.264.
  5. 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. Springer, pp. 252–266, doi:10.1007/978-3-642-12032-9_18.
  6. Frederick A. Hosch & Lawrence H. Landweber (1972): Finite Delay Solutions for Sequential Conditions. In: ICALP, pp. 45–60.

New trends in program synthesis

Thomas A. Henzinger (IST Austria)

Abstract

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).


Temporal logic satisfiability for the design of complex systems

Alessandro Cimatti (Center for Information Technology, Fondazione Bruno Kessler, Trento, Italy)
Stefano Tonetta (Center for Information Technology, Fondazione Bruno Kessler, Trento, Italy)

Abstract

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 [5], industrial production [20], hardware design [2,13,11], and avionics [15].

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 correct. More recently, the role of properties is being recognized as increasingly important. For example, in hardware design, specification languages for properties (e.g. PSL [10], SVA [19]) 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 validation [3,6]. 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 [14]. The role of formal methods in finding such errors is becoming more and more important (e.g., [7]). The role of properties is also fundamental in compositional reasoning [17], where a global verification problem is decomposed into a number of localized problems. Finally, contract based design [18] 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 [9].

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 problem.

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) [16], 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 [1]. 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 [12].

The second class, referred to as HRELTL, for Hybrid RELTL [8], 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 [8]. 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 discrete case.

We conclude the talk with an overview of the practical effectiveness of the current methods, and the open challenges in the area.

References

  1. C.W. Barrett, R. Sebastiani, S.A. Seshia & C. Tinelli (2009): Satisfiability Modulo Theories. In: Handbook of Satisfiability, pp. 825–885, doi:10.3233/978-1-58603-929-5-825.
  2. 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. Springer.
  3. R. Bloem, R. Cavada, I. Pill, M. Roveri & A. Tchaltsev (2007): RAT: A Tool for the Formal Analysis of Requirements. In: CAV, pp. 263–267, doi:10.1007/978-3-540-73368-3_30.
  4. D. Bustan, A. Flaisher, O. Grumberg, O. Kupferman & M.Y. Vardi (2005): Regular Vacuity. In: CHARME, pp. 191–206, doi:10.1007/11560548_16.
  5. 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. In: CAV, pp. 378–393, doi:10.1007/978-3-642-31424-7_29.
  6. A. Cimatti, M. Roveri, V. Schuppan & S. Tonetta (2007): Boolean Abstraction for Temporal Logic Satisfiability. In: CAV, pp. 532–546, doi:10.1007/978-3-540-73368-3_53.
  7. 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), pp. 22, doi:10.1145/2377656.2377659.
  8. A. Cimatti, M. Roveri & S. Tonetta (2009): Requirements Validation for Hybrid Systems. In: CAV, pp. 188–203, doi:10.1007/978-3-642-02658-4_17.
  9. A. Cimatti & S. Tonetta (2012): A Property-Based Proof System for Contract-Based Design. In: EUROMICRO-SEAA, pp. 21–28, doi:10.1109/SEAA.2012.68.
  10. C. Eisner & D. Fisman (2006): A Practical Introduction to PSL (Series on Integrated Circuits and Systems). Springer-Verlag New York, Inc., doi:10.1007/978-0-387-36123-9.
  11. A. Franzén, A. Cimatti, A. Nadel, R. Sebastiani & J. Shalev (2010): Applying SMT in symbolic execution of microcode. In: FMCAD, pp. 121–128. Available at http://ieeexplore.ieee.org/xpls/abs_all.jsp?arnumber=5770940.
  12. S. Ghilardi, E. Nicolini, S. Ranise & D. Zucchelli (2007): Combination Methods for Satisfiability and Model-Checking of Infinite-State Systems. In: CADE, pp. 362–378, doi:10.1007/978-3-540-73595-3_25.
  13. 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. Springer, pp. 65–88, doi:10.1007/978-1-4419-1539-9_3.
  14. R.R. Lutz (1993): Analyzing Software Requirements Errors in Safety-Critical, Embedded Systems. In: RE, pp. 126–133, doi:10.1109/ISRE.1993.324825.
  15. S.P. Miller, M.W. Whalen & D. D. Cofer (2010): Software model checking takes off. Commun. ACM 53(2), pp. 58–64, doi:10.1145/1646353.1646372.
  16. A. Pnueli (1977): The Temporal Logic of Programs. In: FOCS, pp. 46–57, doi:10.1109/SFCS.1977.32.
  17. 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.
  18. A.L. Sangiovanni-Vincentelli, W. Damm & R. Passerone (2012): Taming Dr. Frankenstein: Contract-Based Design for Cyber-Physical Systems. Eur. J. Control 18(3), pp. 217–238, doi:10.3166/ejc.18.217-238.
  19. S. Vijayaraghavan & M. Ramanathan (2005): A Practical Guide for SystemVerilog Assertions. Springer, doi:10.1007/b137011.
  20. M. Weißmann, S. Bedenk, C. Buckl & A. Knoll (2011): Model Checking Industrial Robot Systems. In: SPIN, pp. 161–176, doi:10.1007/978-3-642-22306-8_11.