On the Symbolic Verification of Timed Systems
Jesper Møller
Jakob Lichtenberg
Henrik Reif Andersen
Henrik Hulgaard
February 1999
Abstract
This paper describes how to analyze a timed system symbolically. That is,
given a symbolic representation of a set of (timed) states (as an
expression), we describe how to determine an expression that represents the
set of states that can be reached either by firing a discrete transition or
by advancing time. These operations are used to determine the set of
reachable states symbolically. We also show how to symbolically determine
the set of states that can reach a given set of states (i.e., a backwards
step), thus making it possible to verify TCTL-formulae symbolically. The
analysis is fully symbolic in the sense that both the discrete and the
continuous part of the state space are represented symbolically.
Furthermore, both the synchronous and asynchronous concurrent composition of
timed systems can be performed symbolically. The symbolic
representations are given as formulae expressed in a simple first-order
logic over difference constraints containing only the Boolean operators and
existential quantification. Together with a recently developed data
structure for efficient manipulations of the logic, the symbolic
representation provides the potential of drastically increasing the size of
timed systems that can be verified in practice.
