Simplifying Fixpoint Computations in Verification of Real-Time Systems

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.