A Symbolic Algorithm for the Analysis of Robust Timed Automata

P.T. Kordy, Romanus Langerak, Sjouke Mauw, Jan W. Polderman

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

    3 Citations (Scopus)
    17 Downloads (Pure)


    We propose an algorithm for the analysis of robustness of timed automata, that is, the correctness of a model in the presence of small drifts of the clocks. The algorithm is an extension of the region based algorithm of Puri and uses the idea of stable zones as introduced by Daws and Kordy. Similarly to the assumptions made by Puri, we restrict our analysis to the class of timed automata with closed guards, progress cycles, and bounded clocks. We have implemented the algorithm and applied it to several benchmark specifications. The algorithm is a depth-first search based on on-the-fly reachability using zones.
    Original languageUndefined
    Title of host publication19th International Symposium on Formal Methods, FM 2014
    EditorsC. Jones, P. Pihlajasaari, J.W. Sun
    Place of PublicationLondon
    Number of pages16
    ISBN (Print)978-3-319-06409-3
    Publication statusPublished - 2014
    Event19th International Symposium on Formal Methods - Singapore, Singapore
    Duration: 12 May 201416 May 2014
    Conference number: 19th

    Publication series

    NameLecture Notes in Computer Science
    PublisherSpringer Verlag
    ISSN (Print)0302-9743
    ISSN (Electronic)1611-3349


    Conference19th International Symposium on Formal Methods
    Abbreviated titleFM 2014


    • EWI-25008
    • Timed Automata
    • IR-91926
    • Verification
    • METIS-306004
    • Formal Modelling

    Cite this