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

MaRDI QIDQ3384889FDOQ3384889

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

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

Mathematics Subject Classification ID

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

Cites Work

• A really temporal logic
• Real-time logics: Complexity and expressiveness
• Title not available (Why is that?)
• Title not available (Why is that?)
• Propositional temporal logics: decidability and completeness
• Title not available (Why is that?)
• A one-pass tree-shaped tableau for LTL+past
• A new rule for LTL tableaux

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)