Preface

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.

August 2013,
Gabriele Puppis and Tiziano Villa

Program Committee

Organizing Chair

Steering Committee

Additional Reviewers

Games with delay for automaton synthesis

Abstract

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

Abstract

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

Abstract

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.