### 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 ti

Original language | English |
---|---|

Title of host publication | On the Symbolic Verification of Timed Systems |

Publication date | 1999 |

Publication status | Published - 1999 |

Event | Computer Aided Verification (CAV) - Trento, Italy Duration: 1 Jan 1999 → … |

### Conference

Conference | Computer Aided Verification (CAV) |
---|---|

City | Trento, Italy |

Period | 01/01/1999 → … |

## Cite this

Moeller, J., Lichtenberg, J., Andersen, H. R., & Hulgaard, H. (1999). On the Symbolic Verification of Timed Systems. In

*On the Symbolic Verification of Timed Systems*