A Calculus for Timed Automata (Extended Abstract)

Pedro R. D'Argenio, Ed Brinksma

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

    16 Downloads (Pure)

    Abstract

    A language for representing timed automata is introduced. Its semantics is defined in terms of timed automata. This language is complete in the sense that any timed automaton can be represented by a term in the language. We also define a direct operational semantics for the language in terms of (timed) transition systems. This is proven to be equivalent (or, more precisely, timed bisimilar) to the interpretation in terms of timed automata.

    In addition, a set of axioms is given that is shown to be sound for timed bisimulation. Finally, we introduce several features including the parallel composition and derived time operations like wait, time-out and urgency. We conclude with an example and show that we can eliminate non-reachable states using algebraic techniques.
    Original languageEnglish
    Title of host publicationFormal Techniques in Real-Time and Fault-Tolerant Systems
    Subtitle of host publication4th International Symposium Uppsala, Sweden, September 9–13, 1996. Proceedings
    EditorsBengt Jonsson, Joachim Parrow
    Place of PublicationBerlin, Heidelberg
    PublisherSpringer
    Pages110-129
    Number of pages20
    ISBN (Electronic)978-3-540-70653-3
    ISBN (Print)978-3-540-61648-1
    DOIs
    Publication statusPublished - 1996
    Event4th International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems, FTRTFT 1996 - Uppsala, Sweden
    Duration: 9 Sep 199613 Sep 1996
    Conference number: 4

    Publication series

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

    Conference

    Conference4th International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems, FTRTFT 1996
    Abbreviated titleFTRTFT
    CountrySweden
    CityUppsala
    Period9/09/9613/09/96

      Fingerprint

    Keywords

    • FMT-PA: PROCESS ALGEBRAS
    • FMT-RT: VERIFICATION OF REAL-TIME SYSTEMS
    • Parallel operator
    • Equational theory
    • Parallel composition
    • Process algebra
    • Conservative extension

    Cite this

    D'Argenio, P. R., & Brinksma, E. (1996). A Calculus for Timed Automata (Extended Abstract). In B. Jonsson, & J. Parrow (Eds.), Formal Techniques in Real-Time and Fault-Tolerant Systems: 4th International Symposium Uppsala, Sweden, September 9–13, 1996. Proceedings (pp. 110-129). (Lecture Notes in Computer Science; Vol. 1135). Berlin, Heidelberg: Springer. https://doi.org/10.1007/3-540-61648-9_37