Étienne André (CNRS-LSV, Cachan, France)
Fabio Fioravanti (University of Chieti-Pescara and IASI-CNR, Italy)
Fulvio Forni (University of Rome "Tor Vergata", Italy)
Laurent Fribourg (CNRS-LSV, Cachan, France)
Alberto Pettorossi (University of Rome "Tor Vergata", Italy)
Maurizio Proietti (IASI-CNR, Italy)

July 5, 15:00
Étienne André (CNRS-LSV, Cachan, France)
"Synthesis of Constraints in Order to Generalize a Reference Behavior in Timed Automata" [slides]

Abstract. We present an inverse method allowing to synthesize constraints on timing delays (seen as parameters) in the framework of timed automata. We take advantage of a given reference valuation of the parameters for which the system is known to behave properly, and we want to generalize this valuation. Our aim is to generate a constraint such that, under any valuation satisfying this constraint, the traces of the system (viewed as alternating sequences of locations and actions) are equivalent to the traces under the reference valuation. In particular, LTL formulas are preserved. This is useful for safely relaxing some values of the reference valuation. By iterating this inverse method on integer points of a rectangular parameter domain, we are then able to partition the parametric space into good and bad zones with respect to a given property on traces. A tool, IMITATOR, was developed and was successfully applied to various examples of asynchronous circuits and protocols.

July 5, 16:00
Fulvio Forni (DISP, Univ. Roma Tor Vergata)
"Rectangular automata and hybrid-time: Some extensions of classical concepts" [slides]

Abstract. We consider the class of rectangular automata and we propose a new approach to the characterization of the working mechanism of these automata. We replace the classical approach with transition systems (whose labeled transition relation is related either to the jumps or to the flows of the automaton, [4]) by a direct definition of solution to a rectangular automaton. In particular, we use the notions of hybrid-time and solution to a hybrid system, from the literature on hybrid systems [3], adapting them to the case of rectangular automata (rectangular automata are indeed hybrid systems). Then, we propose a branching logic called HTCTL - hybrid time computation tree logic. HTCTL can be considered as a generalization of TCTL [1] to hybrid-time. Indeed, the notions of time intervals and set of divergent paths used in the definition of the TCTL semantics, are replaced by hybrid-time intervals and complete solutions, respectively, in the definition of the HTCTL semantics. Then, we claim that TCTL is a fragment of HTCTL, when a suitable set of solutions to the rectangular automaton is considered. We develop also a comparison between CTL [2] and HTCTL. Analogously to the TCTL case, we claim that CTL is a fragment of HTCTL, when the set of discrete solutions to the rectangular automaton is considered. In fact, the semantics of CTL is based on infinite sequences of states, that can be easily related to the solutions of a rectangular automaton that only jumps. Thus, on that particular set of solutions, CTL and HTCTL can be compared. Finally, we outline a method to reduce the computation of the set of states that satisfy a given HTCTL formula to a fixpoint computation over subsets of the state-space of the automaton [5].

References
[1] C. Baier and J.P. Katoen. Principles of Model Checking (Representation and Mind Series). The MIT Press, 2008.
[2] E. M. Clarke, O. Grumberg, and D. A. Peled. Model Checking. The MIT Press, 2000.
[3] R. Goebel and A.R. Teel. Solutions to hybrid inclusions via set and graphical convergence with stability theory applications. Automatica, 42(4):573 – 587, 2006.
[4] T.A. Henzinger. The theory of hybrid automata. Symposium on Logic in Computer Science, 0:278, 1996.
[5] T.A. Henzinger, X. Nicollin, J. Sifakis, and S. Yovine. Symbolic model checking for real-time systems. Inf. Comput., 111(2):193–244, 1994.

July 6, 15:00
Fabio Fioravanti (Univ. ‘G. D’Annunzio’ Pescara and IASI-CNR)
"Generalization Strategies for the Verification of Infinite State Systems" [slides]

Abstract. We present a comparative evaluation of some generalization strategies which are applied by a method for the automated verification of infinite state reactive systems. The verification method is based on (1) the specialization of the constraint logic program which encodes the system with respect to the initial state and the property to be verified, and (2) a bottom-up evaluation of the specialized program. The generalization strategies are used during the program specialization phase for controlling when and how to perform generalization. Selecting a good generalization strategy is not a trivial task because it must guarantee the termination of the specialization phase itself, and it should be a good balance between precision and performance. Indeed, a coarse generalization strategy may prevent one to prove the properties of interest, while an unnecessarily precise strategy may lead to high verification times. We perform an experimental evaluation of various generalization strategies on several infinite state systems and properties to be verified.