Multi-timed Bisimulation for Distributed Timed Automata

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

19 Downloads (Pure)

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 languageEnglish
Title of host publicationNASA Formal Methods - 9th International Symposium, NFM 2017 Moffett Field, Proceedings
EditorsMisty Davies, Temesghen Kahsai, Clark Barrett
PublisherSpringer
Pages52-67
Number of pages16
ISBN (Print)9783319572871
DOIs
Publication statusPublished - 2017
EventNASA Formal Methods Symposium - Moffett Field, CA, USA, San Jose, United States
Duration: 16 May 201718 May 2017
Conference number: 9th
https://ti.arc.nasa.gov/events/nfm-2017/

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

Conference

ConferenceNASA Formal Methods Symposium
Abbreviated titleNFM 2017
CountryUnited States
CitySan Jose
Period16/05/1718/05/17
Internet address

Fingerprint

Real time systems
Clocks
Computability and decidability
Explosions

Cite this

Ortiz Vega, J. J., Schobbens, P., & Amrani, M. (2017). Multi-timed Bisimulation for Distributed Timed Automata. In M. Davies, T. Kahsai, & C. Barrett (Eds.), NASA Formal Methods - 9th International Symposium, NFM 2017 Moffett Field, Proceedings (pp. 52-67). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 10227 LNCS). Springer. https://doi.org/10.1007/978-3-319-57288-8_4
Ortiz Vega, James Jerson ; Schobbens, Pierre ; Amrani, Moussa. / Multi-timed Bisimulation for Distributed Timed Automata. NASA Formal Methods - 9th International Symposium, NFM 2017 Moffett Field, Proceedings. editor / Misty Davies ; Temesghen Kahsai ; Clark Barrett. Springer, 2017. pp. 52-67 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
@inbook{5b3a2ff041d849589dac447bb0a8dce0,
title = "Multi-timed Bisimulation for Distributed Timed Automata",
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.",
author = "{Ortiz Vega}, {James Jerson} and Pierre Schobbens and Moussa Amrani",
year = "2017",
doi = "10.1007/978-3-319-57288-8_4",
language = "English",
isbn = "9783319572871",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer",
pages = "52--67",
editor = "Misty Davies and Temesghen Kahsai and Clark Barrett",
booktitle = "NASA Formal Methods - 9th International Symposium, NFM 2017 Moffett Field, Proceedings",

}

Ortiz Vega, JJ, Schobbens, P & Amrani, M 2017, Multi-timed Bisimulation for Distributed Timed Automata. in M Davies, T Kahsai & C Barrett (eds), NASA Formal Methods - 9th International Symposium, NFM 2017 Moffett Field, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 10227 LNCS, Springer, pp. 52-67, NASA Formal Methods Symposium, San Jose, United States, 16/05/17. https://doi.org/10.1007/978-3-319-57288-8_4

Multi-timed Bisimulation for Distributed Timed Automata. / Ortiz Vega, James Jerson; Schobbens, Pierre; Amrani, Moussa.

NASA Formal Methods - 9th International Symposium, NFM 2017 Moffett Field, Proceedings. ed. / Misty Davies; Temesghen Kahsai; Clark Barrett. Springer, 2017. p. 52-67 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 10227 LNCS).

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

TY - CHAP

T1 - Multi-timed Bisimulation for Distributed Timed Automata

AU - Ortiz Vega, James Jerson

AU - Schobbens, Pierre

AU - Amrani, Moussa

PY - 2017

Y1 - 2017

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=85018710883&partnerID=8YFLogxK

U2 - 10.1007/978-3-319-57288-8_4

DO - 10.1007/978-3-319-57288-8_4

M3 - Chapter (peer-reviewed)

SN - 9783319572871

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 52

EP - 67

BT - NASA Formal Methods - 9th International Symposium, NFM 2017 Moffett Field, Proceedings

A2 - Davies, Misty

A2 - Kahsai, Temesghen

A2 - Barrett, Clark

PB - Springer

ER -

Ortiz Vega JJ, Schobbens P, Amrani M. Multi-timed Bisimulation for Distributed Timed Automata. In Davies M, Kahsai T, Barrett C, editors, NASA Formal Methods - 9th International Symposium, NFM 2017 Moffett Field, Proceedings. Springer. 2017. p. 52-67. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). https://doi.org/10.1007/978-3-319-57288-8_4