On the Symbolic Verification of Timed Systems

Jesper Moeller, Jacob Lichtenberg, Henrik Reif Andersen, Henrik Hulgaard

    Research output: Chapter in Book/Report/Conference proceedingArticle in proceedingsResearch


    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 languageEnglish
    Title of host publicationOn the Symbolic Verification of Timed Systems
    Publication date1999
    Publication statusPublished - 1999
    EventComputer Aided Verification (CAV) - Trento, Italy
    Duration: 1 Jan 1999 → …


    ConferenceComputer Aided Verification (CAV)
    CityTrento, Italy
    Period01/01/1999 → …

    Cite this