### 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 L_{v} 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 ML_{v}, an extension of L_{v} 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 ML_{v} over executions of MLTS with such a semantics and we show that its model checking problem against ML_{v} is EXPTIME-complete.

Original language | English |
---|---|

Title of host publication | NASA Formal Methods - 11th International Symposium, NFM 2019, Proceedings |

Editors | Julia M. Badger, Kristin Yvonne Rozier |

Publisher | Springer Verlag |

Pages | 19-35 |

Number of pages | 17 |

ISBN (Print) | 9783030206512 |

DOIs | |

Publication status | Published - 23 May 2019 |

Event | 11th International Symposium on NASA Formal Methods, NFM 2019 - Houston, United States Duration: 7 May 2019 → 9 May 2019 |

### Publication series

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

Volume | 11460 LNCS |

ISSN (Print) | 0302-9743 |

ISSN (Electronic) | 1611-3349 |

### Conference

Conference | 11th International Symposium on NASA Formal Methods, NFM 2019 |
---|---|

Country | United States |

City | Houston |

Period | 7/05/19 → 9/05/19 |

## Fingerprint Dive into the research topics of 'ML<sub>v</sub>: A distributed real-time modal logic'. Together they form a unique fingerprint.

## Cite this

_{v}: A distributed real-time modal logic. In J. M. Badger, & K. Y. Rozier (Eds.),

*NASA Formal Methods - 11th International Symposium, NFM 2019, Proceedings*(pp. 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