A one-pass tree-shaped tableau for LTL+past

DOI10.29007/3HB9MaRDI QIDQ4645753zbMATH OpenOpenAlexFDO

Authors Nicola Gigante, Angelo Montanari, Mark Alexander Reynolds

Publication date 10 January 2019

Published in EPiC Series in Computing (Search for Journal in Brave)

Full work available at URL https://doi.org/10.29007/3hb9

zbMATH Keywords

linear temporal logictableauxpast operators

Mathematics Subject Classification ID

Temporal logic (03B44)

Recommendations

• A new rule for LTL tableaux
• A SAT-based encoding of the one-pass and tree-shaped tableau system for LTL
• Regular linear temporal logic with past
• Formal Methods in Computer-Aided Design
• \textit{Once} and \textit{for all}

Cited in

(7)

• scientific article; zbMATH DE number 7445165 (Why is no real title available?)
• scientific article; zbMATH DE number 7447742 (Why is no real title available?)
• A new rule for LTL tableaux
• One-pass and tree-shaped tableau systems for TPTL and \(\mathrm{TPTL_b+Past}\)
• SAT meets tableaux for linear temporal logic satisfiability
• A One-Pass Tree-Shaped Tableau for Defeasible LTL
• A SAT-based encoding of the one-pass and tree-shaped tableau system for LTL

This page was built for publication: A one-pass tree-shaped tableau for LTL+past

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