The Coarsest Congruence for Timed Automata with Deadlines Contained in Bisimulation

P.R. d' Argenio, Biniam Gebremichael

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

    3 Citations (Scopus)
    38 Downloads (Pure)


    Delaying the synchronization of actions may reveal some hidden behavior that would not happen if the synchronization met the specified deadlines. This precise phenomenon makes bisimulation fail to be a congruence for the parallel composition of timed automata with deadlines, a variant of timed automata where time progress is controlled by deadlines imposed on each transition. This problem has been known and unsolved for several years. In this paper we give a characterization of the coarsest congruence that is included in the bisimulation relation. In addition, a symbolic characterization of such relation is provided and shown to be decidable. We also discuss the pitfalls of existing parallel compositions in this setting and argue that our definition is both reasonable and sufficiently expressive as to consider the modeling of both soft and hard real-time constraints.
    Original languageEnglish
    Title of host publicationCONCUR 2005 – Concurrency Theory
    Subtitle of host publication16th International Conference, CONCUR 2005, San Francisco, CA, USA, August 23-26, 2005. Proceedings
    EditorsMartín Abadi, Luca de Alfaro
    Place of PublicationBerlin
    Number of pages16
    ISBN (Electronic)978-3-540-31934-4
    ISBN (Print)978-3-540-28309-6
    Publication statusPublished - 2005
    Event16th International Conference on Concurrency Theory, CONCUR 2005 - San Francisco, United States
    Duration: 23 Aug 200526 Aug 2005
    Conference number: 16

    Publication series

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


    Conference16th International Conference on Concurrency Theory, CONCUR 2005
    Abbreviated titleCONCUR
    Country/TerritoryUnited States
    CitySan Francisco


    • Parallel composition
    • Process algebra
    • Time progress
    • Time automaton
    • Small relation


    Dive into the research topics of 'The Coarsest Congruence for Timed Automata with Deadlines Contained in Bisimulation'. Together they form a unique fingerprint.

    Cite this