Multi-timed Bisimulation for Distributed Timed Automata

Research output: Contribution in Book/Catalog/Report/Conference proceedingChapter (peer-reviewed)peer-review

55 Downloads (Pure)


Timed bisimulation is an important technique which can be used for reasoning about behavioral equivalence between different com- ponents of a complex real-time system. The verification of timed bisimu- lation is a difficult and challenging problem because the state explosion caused by both functional and timing constraints must be taken into account. Timed bisimulation was shown decidable for Timed Automata (TA). Distributed TA and TA with Independent Clocks (icTA) were introduced to model Distributed Real-time Systems. They are a variant of TA with local clocks that may not run at the same rate. In this paper, we first propose to extend the theory of Timed Labeled Transition Sys- tems to Multi-Timed Labeled Transition Systems, and relate them by an extension of timed bisimulation to multi-timed bisimulation. We prove the decidability of multi-timed bisimulation and present an EXPTIME algorithm for deciding whether two icTA are multi-timed bisimilar. For multi-timed bisimilarity, an extension of the standard refinement algo- rithm is described.
Original languageEnglish
Title of host publicationNASA Formal Methods - 9th International Symposium, NFM 2017 Moffett Field, Proceedings
EditorsMisty Davies, Temesghen Kahsai, Clark Barrett
Number of pages16
ISBN (Print)9783319572871
Publication statusPublished - 1 Jan 2017
EventNASA Formal Methods Symposium - Moffett Field, CA, USA, San Jose, United States
Duration: 16 May 201718 May 2017
Conference number: 9th

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume10227 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


ConferenceNASA Formal Methods Symposium
Abbreviated titleNFM 2017
Country/TerritoryUnited States
CitySan Jose
Internet address


Dive into the research topics of 'Multi-timed Bisimulation for Distributed Timed Automata'. Together they form a unique fingerprint.

Cite this