This page shows all publications that appeared in the IASI annual research reports. Authors currently affiliated with the Institute are always listed with the full name.

You can browse through them using either the links of the following line or those associated with author names.

Show all publications of the year  ALL, with author Fioravanti F., in the category IASI Research Reports (or show them all):

---

IASI Research Report n. 657  (Previous    Next)  

Fioravanti F., Alberto Pettorossi, Maurizio Proietti

Verifying Infinite State Systems by Specializing Constraint Logic Programs

ABSTRACT

We propose a method for the specification and the automated verification of temporal properties of infinite state reactive systems. Given a reactive system K and a formula F of the branching time temporal logic CTL, we construct a locally stratified constraint logic program P_K[F] such that the system K verifies F if and only if prop belongs to M(P_K[F]), where prop is a predicate symbol defined in P_K[F] and M(P_K[F]) is the perfect model of P_K[F]. Then we check whether or not prop belongs to M(P_K[F]) by specializing the program P_K[F] w.r.t. prop and deriving a new program P_sp containing either the fact prop <- (in which case the temporal formula F is verified by the system) or no clause for prop (in which case the temporal formula F is not verified by the system). Our specialization method makes use of: (i) a set of specialization rules that preserve the perfect model of constraint logic programs, and (ii) an automatic strategy that guides the application of these rules for deriving the specialized program P_sp. Our strategy always terminates and is sound for verifying CTL formulas. Due to the undecidability of CTL formulas in the case of infinite state systems, our strategy is incomplete, that is, we may derive a specialized program P_sp containing a clause for prop different from the fact prop <-. However, as indicated by the results we have obtained by using our prototype verification system, our strategy allows us to verify a large collection of properties of infinite state systems.