A new rule for LTL tableaux

MaRDI QIDQ5015285zbMATH OpenFDO

Authors

Publication date 7 December 2021

Full work available at URL https://arxiv.org/abs/1609.04102, http://eptcs.web.cse.unsw.edu.au/paper.cgi?GandALF2016.20

Mathematics Subject Classification ID

Temporal logic (03B44) Logic in computer science (03B70)

Recommendations

• scientific article
• Systematic semantic tableaux for PLTL
• Labelled tableaux for propositional linear time logic over finite frames
• A one-pass tree-shaped tableau for LTL+past
• A tableau-based decision procedure for CTL\(^*\)

Cites work

• scientific article; zbMATH DE number 1189110 (Why is no real title available?)
• scientific article; zbMATH DE number 1903365 (Why is no real title available?)
• scientific article; zbMATH DE number 2102740 (Why is no real title available?)
• scientific article; zbMATH DE number 814821 (Why is no real title available?)
• scientific article; zbMATH DE number 3274715 (Why is no real title available?)
• A PLTL-prover based on labelled superposition with partial model guidance
• Cut-free sequent systems for temporal logic
• Efficient loop-check for backward proof search in some non-classical propositional logics
• Implementing a fair monodic temporal logic prover
• Mathematical Logic for Computer Science
• Reasoning about infinite computations
• Systematic semantic tableaux for PLTL
• The temporal logic of branching time
• Two loop detection mechanisms: a comparison

Cited in

(13)

• Systematic semantic tableaux for PLTL
• Theorem proving for pointwise metric temporal logic over the naturals via translations
• scientific article; zbMATH DE number 7447742 (Why is no real title available?)
• SAT meets tableaux for linear temporal logic satisfiability
• Labelled tableaux for propositional linear time logic over finite frames
• scientific article; zbMATH DE number 1189110 (Why is no real title available?)
• A SAT-based encoding of the one-pass and tree-shaped tableau system for LTL
• One-pass and tree-shaped tableau systems for TPTL and \(\mathrm{TPTL_b+Past}\)
• A one-pass tree-shaped tableau for LTL+past
• The saturated tableaux for linear miniscope Horn-like temporal logic
• A One-Pass Tree-Shaped Tableau for Defeasible LTL
• scientific article; zbMATH DE number 7445165 (Why is no real title available?)
• And-or tableaux for fixpoint logics with converse: LTL, CTL, PDL and CPDL

Describes a project that uses

Uses Software

• NuSMV
• TSPASS
• TTM
• TRP++
• Leviathan
• Aalta

This page was built for publication: A new rule for LTL tableaux

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