Skip to Main content Skip to Navigation
Conference papers

An effective fixed point calculus for deterministic systems applied to model checking

Julien Musset 1 Michaël Rusinowitch 1
1 PROTHEO - Constraints, automatic deduction and software properties proofs
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : Transition systems has been intensively applied to the modeling of complex systems, for example they have been used for giving semantics to synchronous languages such as Lustre or Signal, or to hybrid automata. Properties of their behavior can be verified using model checking procedures, which rely on an iterative computation of least or greatest fixed points. For instance, safety properties can be proved by a fixed point computation of the set of all the states that can access to the forbidden states and verifying that it does not contain an initial state. This approach has to face two main difficulties : the complexity of the data types domain and the termination of the iterative algorithm. They are solved by approximation heuristics such as abstract interpretations and widening operators. However, in many cases, a sharper analysis of the transition system can be exploited to speed up the calculus. Consequently, we propose an other algorithm to compute this fixed point taking advantage of the decomposition of the relation in an union of simpler relations. If the transition system is deterministic, then our algorithm computes the exact fixed point, otherwise it computes an over approximation. We have implemented this algorithm on top of a linear constraint solver over real number and applied it to the proof of a safety property of a reactive system and we compare with the model checker Hytech.
Document type :
Conference papers
Complete list of metadata

https://hal.inria.fr/inria-00100501
Contributor : Publications Loria <>
Submitted on : Tuesday, September 26, 2006 - 2:46:20 PM
Last modification on : Friday, February 26, 2021 - 3:28:05 PM

Identifiers

  • HAL Id : inria-00100501, version 1

Collections

Citation

Julien Musset, Michaël Rusinowitch. An effective fixed point calculus for deterministic systems applied to model checking. First International Workshop on Automated Verification of Infinite-State Systems - AVIS'01, Mar 2001, Berlin, Germany, 4 p. ⟨inria-00100501⟩

Share

Metrics

Record views

196