| Autor: |
Bozzelli, L., Molinari, A., Montanari, A., Peron, A. |
| Přispěvatelé: |
Alessandra Cherubini Nicoletta Sabadini Simone Tini, Bozzelli, L., Molinari, A., Montanari, A., Peron, A., Alessandra Cherubini, Nicoletta Sabadini, Simone Tini |
| Jazyk: |
angličtina |
| Rok vydání: |
2019 |
| Předmět: |
|
| Popis: |
In this paper, we introduce an automaton-theoretic approach to model checking linear time properties of timeline-based systems over dense temporal domains. The system under consideration is specified by means of (a decidable fragment of) timeline structures, timelines for short, which are a formal setting proposed in the literature to model planning problems in a declarative way. Timelines provide an interval-based description of the behavior of the system, instead of a more conventional point-based one. The relevant system properties are expressed by formulas of the logic MITL (a well-known timed extension of LTL) to be checked against timelines. In the paper, we prove that the model checking problem for MITL formulas (resp., its fragment MITL(0,∞)) over timelines is EXPSPACE-complete (resp., PSPACE-complete). |
| Databáze: |
OpenAIRE |
| Externí odkaz: |
|
