Multi-timed Bisimulation for Distributed Timed Automata

Résultats de recherche: Contribution dans un livre/un catalogue/un rapport/dans les actes d'une conférenceChapitre (revu par des pairs)

18 Downloads (Pure)

Résumé

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.
langue originaleAnglais
titreNASA Formal Methods - 9th International Symposium, NFM 2017 Moffett Field, Proceedings
rédacteurs en chefMisty Davies, Temesghen Kahsai, Clark Barrett
EditeurSpringer
Pages52-67
Nombre de pages16
ISBN (imprimé)9783319572871
Les DOIs
étatPublié - 2017
EvénementNASA Formal Methods Symposium - Moffett Field, CA, USA, San Jose, États-Unis
Durée: 16 mai 201718 mai 2017
Numéro de conférence: 9th
https://ti.arc.nasa.gov/events/nfm-2017/

Série de publications

NomLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume10227 LNCS
ISSN (imprimé)0302-9743
ISSN (Electronique)1611-3349

Une conférence

Une conférenceNASA Formal Methods Symposium
Titre abrégéNFM 2017
PaysÉtats-Unis
La villeSan Jose
période16/05/1718/05/17
Adresse Internet

Empreinte digitale

Real time systems
Clocks
Computability and decidability
Explosions

Citer ceci

Ortiz Vega, J. J., Schobbens, P., & Amrani, M. (2017). Multi-timed Bisimulation for Distributed Timed Automata. Dans M. Davies, T. Kahsai, & C. Barrett (eds.), NASA Formal Methods - 9th International Symposium, NFM 2017 Moffett Field, Proceedings (p. 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. Editeur / 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)).
@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. Dans 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, p. 52-67, NASA Formal Methods Symposium, San Jose, États-Unis, 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).

Résultats de recherche: Contribution dans un livre/un catalogue/un rapport/dans les actes d'une conférenceChapitre (revu par des pairs)

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. Dans Davies M, Kahsai T, Barrett C, rédacteurs en chef, 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