Simplifying Fixpoint Computations in Verification of Real-Time Systems
TR-2002-15, Author: Jesper B. Møller
Jesper B. Møller April 2002
Abstract
Symbolic verification of real-time systems consists of computing the least fixpoint of a functional which given a set of states $\phi$ returns the states that are reachable from $\phi$ (in forward reachability), or that can reach $\phi$ (in backward reachability). This paper presents two techniques for simplifying the fixpoint computation: First, I demonstrate that in backwards reachability, clock resets and discrete state changes can be performed as substitutions instead of existential quantifications over reals and Booleans, respectively. Second, I introduce a local-time model for real-time systems which allows clocks to advance asynchronously, thus resulting in an over-approximation of the least fixpoint, but which in some cases is sufficient for verifying a temporal property.
Technical report TR-2002-15 in IT University Technical Report Series, April 2002.
Available as
PDF.