Abstract
his paper presents a modal mu-calculus, Lrelμ,ν, for encoding properties of systems modeled as timed automata. Our logic includes
arbitrary fixpoints and an until-like modal operator for time elapses, and is shown to be strictly more expressive than existing timed modal mu-calculi introduced in the literature. It also enjoys decidable model checking, as it respects the traditional region-graph construction for timed automata. We additionally establish that, in contrast to the other mu-calculi, Lrel μ,ν is strictly more expressive than Timed Computation Tree Logic (TCTL) in the setting of general timed automata, meaning that model checkers for Lrel μ,ν are immediately usable as model checkers for TCTL for general timed automata
arbitrary fixpoints and an until-like modal operator for time elapses, and is shown to be strictly more expressive than existing timed modal mu-calculi introduced in the literature. It also enjoys decidable model checking, as it respects the traditional region-graph construction for timed automata. We additionally establish that, in contrast to the other mu-calculi, Lrel μ,ν is strictly more expressive than Timed Computation Tree Logic (TCTL) in the setting of general timed automata, meaning that model checkers for Lrel μ,ν are immediately usable as model checkers for TCTL for general timed automata
| Original language | English |
|---|---|
| Title of host publication | Quantitative Evaluation of Systems and Formal Modeling and Analysis of Timed Systems |
| Subtitle of host publication | First International Joint Conference, QEST+FORMATS 2024, Calgary, AB, Canada, September 9–13, 2024, Proceedings |
| Editors | Jane Hillston, Sadegh Soudjani, Masaki Waga |
| Place of Publication | Cham |
| Publisher | Springer |
| Pages | 160-178 |
| Number of pages | 19 |
| ISBN (Electronic) | 978-3-031-68416-6 |
| ISBN (Print) | 978-3-031-68415-9 |
| DOIs | |
| Publication status | Published - 29 Aug 2024 |
| Event | 1st International Conference on Quantitative Evaluation of Systems and Formal Modeling and Analysis of Timed Systems, QUEST + FORMATS 2024 - Calgary, Canada Duration: 9 Sept 2024 → 13 Sept 2024 |
Publication series
| Name | Lecture Notes in Computer Science (LNCS) |
|---|---|
| Volume | 14996 |
| ISSN (Print) | 0302-9743 |
| ISSN (Electronic) | 1611-3349 |
Conference
| Conference | 1st International Conference on Quantitative Evaluation of Systems and Formal Modeling and Analysis of Timed Systems, QUEST + FORMATS 2024 |
|---|---|
| Abbreviated title | QUEST + FORMATS 2024 |
| Country/Territory | Canada |
| City | Calgary |
| Period | 9/09/24 → 13/09/24 |