Multi-timed Bisimulation for Distributed Timed Automata

Résultats de recherche: Recherche - Revue par des pairsChapitre (revu par des pairs)

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.

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 9th NASA Formal Methods Symposium NFM 2017 Springer.
@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",
booktitle = "9th NASA Formal Methods Symposium NFM 2017",
publisher = "Springer",

}

Ortiz Vega, JJ, Schobbens, P & Amrani, M 2017, Multi-timed Bisimulation for Distributed Timed Automata. Dans 9th NASA Formal Methods Symposium NFM 2017 . Springer, NASA Formal Methods Symposium, San Jose, États-Unis, 16/05/17.

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

9th NASA Formal Methods Symposium NFM 2017 . Springer, 2017.

Résultats de recherche: Recherche - Revue par des pairsChapitre (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.

M3 - Chapter (peer-reviewed)

BT - 9th NASA Formal Methods Symposium NFM 2017

PB - Springer

ER -

Ortiz Vega JJ, Schobbens P, Amrani M. Multi-timed Bisimulation for Distributed Timed Automata. Dans 9th NASA Formal Methods Symposium NFM 2017 . Springer. 2017.