Abstract
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 language | English |
---|---|
Title of host publication | NASA Formal Methods - 9th International Symposium, NFM 2017 Moffett Field, Proceedings |
Editors | Misty Davies, Temesghen Kahsai, Clark Barrett |
Publisher | Springer |
Pages | 52-67 |
Number of pages | 16 |
ISBN (Print) | 9783319572871 |
DOIs | |
Publication status | Published - 1 Jan 2017 |
Event | NASA Formal Methods Symposium - Moffett Field, CA, USA, San Jose, United States Duration: 16 May 2017 → 18 May 2017 Conference number: 9th https://ti.arc.nasa.gov/events/nfm-2017/ |
Publication series
Name | Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) |
---|---|
Volume | 10227 LNCS |
ISSN (Print) | 0302-9743 |
ISSN (Electronic) | 1611-3349 |
Conference
Conference | NASA Formal Methods Symposium |
---|---|
Abbreviated title | NFM 2017 |
Country/Territory | United States |
City | San Jose |
Period | 16/05/17 → 18/05/17 |
Internet address |