TY - RPRT
T1 - Simplifying Fixpoint Computations in Verification of Real-Time Systems
AU - Møller, Jesper B.
PY - 2002/4
Y1 - 2002/4
N2 - 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.
AB - 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.
KW - Symbolic verification
KW - Real-time systems
KW - Fixpoint computation
KW - Backwards reachability
KW - Local-time model
M3 - Report
T3 - IT University Technical Report Series
BT - Simplifying Fixpoint Computations in Verification of Real-Time Systems
PB - IT-Universitetet i København
CY - Copenhagen
ER -