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)

24 Téléchargements (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
Etat de la publicationPublié - 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 Examiner les sujets de recherche de « Multi-timed Bisimulation for Distributed Timed Automata ». Ensemble, ils forment une empreinte digitale unique.

  • Contient cette citation

    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