Symbolic Robustness Analysis of Timed Automata

C.F. Daws, P.T. Kordy

    Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

    17 Citations (Scopus)


    We propose a symbolic algorithm for the analysis of the robustness of timed automata, that is the correctness of the model in presence of small drifts on the clocks or imprecision in testing guards. This problem is known to be decidable with an algorithm based on detecting strongly connected components on the region graph, which, for complexity reasons, is not effective in practice. Our symbolic algorithm is based on the standard algorithm for symbolic reachability analysis using zones to represent symbolic states and can then be easily integrated within tools for the verification of timed automata models. It relies on the computation of the stable zone of each cycle in a timed automaton. The stable zone is the largest set of states that can reach and be reached from itself through the cycle. To compute the robust reachable set, each stable zone that intersects the set of explored states has to be added to the set of states to be explored.
    Original languageUndefined
    Title of host publicationFormal Modeling and Analysis of Timed Systems
    EditorsE. Asarin, P. Bouyer
    Place of PublicationBerlin
    Number of pages13
    ISBN (Print)978-3-540-45026-9
    Publication statusPublished - Sep 2006
    Event4th International Conference on Formal Modeling and Analysis of Timed Systems, FORMATS 2006 - Université Paris La Sorbonne, Paris, France
    Duration: 25 Sep 200627 Sep 2006
    Conference number: 4

    Publication series

    NameLecture Notes in Computer Science
    PublisherSpringer Verlag


    Conference4th International Conference on Formal Modeling and Analysis of Timed Systems, FORMATS 2006
    Abbreviated titleFORMATS
    Internet address


    • METIS-238172
    • EWI-6932
    • IR-63435

    Cite this