MLv: A distributed real-time modal logic

Résultats de recherche: Contribution dans un livre/un catalogue/un rapport/dans les actes d'une conférenceArticle dans les actes d'une conférence/un colloque

Résumé

Distributed Real-Time Systems (DRTS) can be characterized by several communicating components whose behavior depends on a large number of timing constraints and such components can basically be located at several computers spread over a communication network. Extensions of Timed Modal Logics (TML) such as, Timed Propositional Modal Logic (TPML), Timed Modal μ-calculus and Lv have been proposed to capture timed and temporal properties in real-time systems. However, these logics rely on a so-called mono-timed semantics for the underlying Timed Labelled Transition Systems (TLTS). This semantics does not capture complex interactions between components with their associated local clocks, thus missing possible action sequences. Based on Multi-Timed Labelled Transition Systems (MLTS), which are an extension of TLTS in order to cope with the notion of distributed clocks, we propose MLv, an extension of Lv that relies on a distributed semantics for Timed Automata (TA) instead of considering uniform clocks over the distributed systems, we let time vary independently in each TA. We define the syntax and the semantics of MLv over executions of MLTS with such a semantics and we show that its model checking problem against MLv is EXPTIME-complete.

langue originaleAnglais
titreNASA Formal Methods - 11th International Symposium, NFM 2019, Proceedings
rédacteurs en chefKristin Yvonne Rozier, Julia M. Badger
EditeurSpringer Verlag
Pages19-35
Nombre de pages17
ISBN (imprimé)9783030206512
Les DOIs
étatPublié - 23 mai 2019
Evénement11th International Symposium on NASA Formal Methods, NFM 2019 - Houston, États-Unis
Durée: 7 mai 20199 mai 2019

Série de publications

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

Une conférence

Une conférence11th International Symposium on NASA Formal Methods, NFM 2019
PaysÉtats-Unis
La villeHouston
période7/05/199/05/19

Empreinte digitale

Modal Logic
Labeled Transition System
Semantics
Real-time
Clocks
Timed Automata
Real time systems
Distributed Systems
Propositional Logic
Model checking
Communication Networks
Model Checking
Telecommunication networks
Timing
Calculus
Vary
Logic
Interaction

Citer ceci

Ortiz Vega, J. J., Amrani, M., & Schobbens, P. Y. (2019). MLv: A distributed real-time modal logic. Dans K. Y. Rozier, & J. M. Badger (eds.), NASA Formal Methods - 11th International Symposium, NFM 2019, Proceedings (p. 19-35). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol 11460 LNCS). Springer Verlag. https://doi.org/10.1007/978-3-030-20652-9_2
Ortiz Vega, James Jerson ; Amrani, Moussa ; Schobbens, Pierre Yves. / MLv : A distributed real-time modal logic. NASA Formal Methods - 11th International Symposium, NFM 2019, Proceedings. Editeur / Kristin Yvonne Rozier ; Julia M. Badger. Springer Verlag, 2019. p. 19-35 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
@inproceedings{315f94f8fe634b418c5481cbf344541a,
title = "MLv: A distributed real-time modal logic",
abstract = "Distributed Real-Time Systems (DRTS) can be characterized by several communicating components whose behavior depends on a large number of timing constraints and such components can basically be located at several computers spread over a communication network. Extensions of Timed Modal Logics (TML) such as, Timed Propositional Modal Logic (TPML), Timed Modal μ-calculus and Lv have been proposed to capture timed and temporal properties in real-time systems. However, these logics rely on a so-called mono-timed semantics for the underlying Timed Labelled Transition Systems (TLTS). This semantics does not capture complex interactions between components with their associated local clocks, thus missing possible action sequences. Based on Multi-Timed Labelled Transition Systems (MLTS), which are an extension of TLTS in order to cope with the notion of distributed clocks, we propose MLv, an extension of Lv that relies on a distributed semantics for Timed Automata (TA) instead of considering uniform clocks over the distributed systems, we let time vary independently in each TA. We define the syntax and the semantics of MLv over executions of MLTS with such a semantics and we show that its model checking problem against MLv is EXPTIME-complete.",
author = "{Ortiz Vega}, {James Jerson} and Moussa Amrani and Schobbens, {Pierre Yves}",
year = "2019",
month = "5",
day = "23",
doi = "10.1007/978-3-030-20652-9_2",
language = "English",
isbn = "9783030206512",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "19--35",
editor = "Rozier, {Kristin Yvonne} and Badger, {Julia M.}",
booktitle = "NASA Formal Methods - 11th International Symposium, NFM 2019, Proceedings",
address = "Germany",

}

Ortiz Vega, JJ, Amrani, M & Schobbens, PY 2019, MLv: A distributed real-time modal logic. Dans KY Rozier & JM Badger (eds), NASA Formal Methods - 11th International Symposium, NFM 2019, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), VOL. 11460 LNCS, Springer Verlag, p. 19-35, 11th International Symposium on NASA Formal Methods, NFM 2019, Houston, États-Unis, 7/05/19. https://doi.org/10.1007/978-3-030-20652-9_2

MLv : A distributed real-time modal logic. / Ortiz Vega, James Jerson; Amrani, Moussa; Schobbens, Pierre Yves.

NASA Formal Methods - 11th International Symposium, NFM 2019, Proceedings. Ed. / Kristin Yvonne Rozier; Julia M. Badger. Springer Verlag, 2019. p. 19-35 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol 11460 LNCS).

Résultats de recherche: Contribution dans un livre/un catalogue/un rapport/dans les actes d'une conférenceArticle dans les actes d'une conférence/un colloque

TY - GEN

T1 - MLv

T2 - A distributed real-time modal logic

AU - Ortiz Vega, James Jerson

AU - Amrani, Moussa

AU - Schobbens, Pierre Yves

PY - 2019/5/23

Y1 - 2019/5/23

N2 - Distributed Real-Time Systems (DRTS) can be characterized by several communicating components whose behavior depends on a large number of timing constraints and such components can basically be located at several computers spread over a communication network. Extensions of Timed Modal Logics (TML) such as, Timed Propositional Modal Logic (TPML), Timed Modal μ-calculus and Lv have been proposed to capture timed and temporal properties in real-time systems. However, these logics rely on a so-called mono-timed semantics for the underlying Timed Labelled Transition Systems (TLTS). This semantics does not capture complex interactions between components with their associated local clocks, thus missing possible action sequences. Based on Multi-Timed Labelled Transition Systems (MLTS), which are an extension of TLTS in order to cope with the notion of distributed clocks, we propose MLv, an extension of Lv that relies on a distributed semantics for Timed Automata (TA) instead of considering uniform clocks over the distributed systems, we let time vary independently in each TA. We define the syntax and the semantics of MLv over executions of MLTS with such a semantics and we show that its model checking problem against MLv is EXPTIME-complete.

AB - Distributed Real-Time Systems (DRTS) can be characterized by several communicating components whose behavior depends on a large number of timing constraints and such components can basically be located at several computers spread over a communication network. Extensions of Timed Modal Logics (TML) such as, Timed Propositional Modal Logic (TPML), Timed Modal μ-calculus and Lv have been proposed to capture timed and temporal properties in real-time systems. However, these logics rely on a so-called mono-timed semantics for the underlying Timed Labelled Transition Systems (TLTS). This semantics does not capture complex interactions between components with their associated local clocks, thus missing possible action sequences. Based on Multi-Timed Labelled Transition Systems (MLTS), which are an extension of TLTS in order to cope with the notion of distributed clocks, we propose MLv, an extension of Lv that relies on a distributed semantics for Timed Automata (TA) instead of considering uniform clocks over the distributed systems, we let time vary independently in each TA. We define the syntax and the semantics of MLv over executions of MLTS with such a semantics and we show that its model checking problem against MLv is EXPTIME-complete.

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

U2 - 10.1007/978-3-030-20652-9_2

DO - 10.1007/978-3-030-20652-9_2

M3 - Conference contribution

SN - 9783030206512

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

SP - 19

EP - 35

BT - NASA Formal Methods - 11th International Symposium, NFM 2019, Proceedings

A2 - Rozier, Kristin Yvonne

A2 - Badger, Julia M.

PB - Springer Verlag

ER -

Ortiz Vega JJ, Amrani M, Schobbens PY. MLv: A distributed real-time modal logic. Dans Rozier KY, Badger JM, rédacteurs en chef, NASA Formal Methods - 11th International Symposium, NFM 2019, Proceedings. Springer Verlag. 2019. p. 19-35. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). https://doi.org/10.1007/978-3-030-20652-9_2