One-pass and tree-shaped tableau systems for TPTL and \(\mathrm{TPTL_b+Past}\)

DOI10.1016/j.ic.2020.104599OpenAlexW3034562037MaRDI QIDQ2029608

Nicola Gigante, Angelo Montanari, Luca Geatti, M. A. Reynolds

Publication date: 3 June 2021

Published in: Information and Computation (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.ic.2020.104599

Mathematics Subject Classification ID

Temporal logic (03B44)

Uses Software

• Leviathan

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Real-time logics: Complexity and expressiveness
• Temporal Logics in Computer Science
• Temporal logic can be more expressive
• The complexity of propositional linear temporal logics
• A really temporal logic
• Propositional temporal logics: decidability and completeness
• Handbook of Model Checking
• A One-Pass Tree-Shaped Tableau for LTL+Past
• A Simple and Optimal Complementation Algorithm for Büchi Automata