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

DOI10.29007/3HB9zbMATH Open1402.03026OpenAlexW2740520395MaRDI QIDQ4645753FDOQ4645753

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

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}

zbMATH Keywords

linear temporal logictableauxpast operators

Mathematics Subject Classification ID

Temporal logic (03B44)

Cited In (7)

• Title not available (Why is that?)
• 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
• Title not available (Why is that?)

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)