MightyPPL: Verification of MITL with Past and Pnueli Modalities
Fuente:
arXiv
Saved in:
| Main Authors: | , , , , |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866912622576664576 |
|---|---|
| author | Ho, Hsi-Ming Krishna, Shankara Narayanan Madnani, Khushraj Majumdar, Rupak Pandya, Paritosh |
| author_facet | Ho, Hsi-Ming Krishna, Shankara Narayanan Madnani, Khushraj Majumdar, Rupak Pandya, Paritosh |
| contents | Metric Interval Temporal Logic (MITL) is a popular formalism for specifying properties of reactive systems with timing constraints. Existing approaches to using MITL in verification tasks, however, have notable drawbacks: they either support only limited fragments of the logic or allow for only incomplete verification. This paper introduces MightyPPL, a new tool for translating formulae in Metric Interval Temporal Logic with Past and Pnueli modalities (MITPPL) over the pointwise semantics into timed automata. MightyPPL enables satisfiability and model checking of a much more expressive specification logic over both finite and infinite words and incorporates a number of performance optimisations, including a novel symbolic encoding of transitions and a symmetry reduction technique that leads to an exponential improvement in the number of reachable discrete states. For a given MITPPL formula, MightyPPL can generate either a network of timed automata or a single timed automaton that is language-equivalent and compatible with multiple verification back-ends, including Uppaal, TChecker, and LTSmin, which supports multi-core model checking. We evaluate the performance of the toolchain across various case studies and configuration options. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2510_01490 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | MightyPPL: Verification of MITL with Past and Pnueli Modalities Ho, Hsi-Ming Krishna, Shankara Narayanan Madnani, Khushraj Majumdar, Rupak Pandya, Paritosh Formal Languages and Automata Theory Logic in Computer Science Metric Interval Temporal Logic (MITL) is a popular formalism for specifying properties of reactive systems with timing constraints. Existing approaches to using MITL in verification tasks, however, have notable drawbacks: they either support only limited fragments of the logic or allow for only incomplete verification. This paper introduces MightyPPL, a new tool for translating formulae in Metric Interval Temporal Logic with Past and Pnueli modalities (MITPPL) over the pointwise semantics into timed automata. MightyPPL enables satisfiability and model checking of a much more expressive specification logic over both finite and infinite words and incorporates a number of performance optimisations, including a novel symbolic encoding of transitions and a symmetry reduction technique that leads to an exponential improvement in the number of reachable discrete states. For a given MITPPL formula, MightyPPL can generate either a network of timed automata or a single timed automaton that is language-equivalent and compatible with multiple verification back-ends, including Uppaal, TChecker, and LTSmin, which supports multi-core model checking. We evaluate the performance of the toolchain across various case studies and configuration options. |
| title | MightyPPL: Verification of MITL with Past and Pnueli Modalities |
| topic | Formal Languages and Automata Theory Logic in Computer Science |
| url | https://arxiv.org/abs/2510.01490 |