One-pass and tree-shaped tableau systems for TPTL and TPTL_b+Past

MaRDI QIDQ3384889zbMATH OpenFDO

Authors Luca Geatti, Nicola Gigante, Angelo Montanari, Mark Alexander Reynolds

Publication date 17 December 2021

Full work available at URL https://arxiv.org/abs/1809.03101, http://eptcs.web.cse.unsw.edu.au/paper.cgi?GandALF18.13

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Applications of game theory (91A80) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• One-pass and tree-shaped tableau systems for TPTL and \(\mathrm{TPTL_b+Past}\)
• A one-pass tree-shaped tableau for LTL+past
• A really temporal logic
• One-pass Context-based Tableaux Systems for CTL and ECTL
• A tableau for temporal logic over the reals

Cites work

• scientific article; zbMATH DE number 7445165 (Why is no real title available?)
• scientific article; zbMATH DE number 1189110 (Why is no real title available?)
• scientific article; zbMATH DE number 1395652 (Why is no real title available?)
• A new rule for LTL tableaux
• A one-pass tree-shaped tableau for LTL+past
• A really temporal logic
• Propositional temporal logics: decidability and completeness
• Real-time logics: Complexity and expressiveness

Cited in

(2)

• SAT meets tableaux for linear temporal logic satisfiability
• A One-Pass Tree-Shaped Tableau for Defeasible LTL

This page was built for publication: One-pass and tree-shaped tableau systems for \(\mathrm{TPTL}\) and \(\mathrm{TPTL}_b+\mathrm{Past}\)

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3384889)