A tableau construction for finite linear-time temporal logic

DOI10.1016/J.JLAMP.2021.100743MaRDI QIDQ2669249zbMATH OpenOpenAlexFDO

Authors Yanyan Li

Publication date 9 March 2022

Published in Journal of Logical and Algebraic Methods in Programming (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1910.09339

Mathematics Subject Classification ID

Computer science (68-XX)

Recommendations

• A tableau for general linear temporal logic
• Tableau-based automata construction for dynamic linear time temporal logic
• scientific article; zbMATH DE number 1696514
• scientific article; zbMATH DE number 980417
• scientific article; zbMATH DE number 3937153
• Labelled tableaux for propositional linear time logic over finite frames
• A tableau for temporal logic over the reals
• scientific article
• An improved on-the-fly tableau construction for a real-time temporal logic.

Cites work

• scientific article; zbMATH DE number 1670794 (Why is no real title available?)
• scientific article; zbMATH DE number 3937153 (Why is no real title available?)
• scientific article; zbMATH DE number 1487477 (Why is no real title available?)
• Alternation
• An implementation of an efficient algorithm for bisimulation equivalence
• Comparing LTL semantics for runtime verification
• Deterministic planning in the fifth international planning competition: PDDL3 and experimental evaluation of the planners
• Finite-trace linear temporal logic: coinductive completeness
• Model-checking in dense real-time
• Results on the propositional \(\mu\)-calculus
• Three Partition Refinement Algorithms
• Variants of LTL query checking
• “Sometimes” and “not never” revisited

Cited in

(10)

• scientific article; zbMATH DE number 7445165 (Why is no real title available?)
• Temporalising tableaux
• Designing tableau-like axiomatization for propositional linear temporal logic at home of Arthur Prior
• Learning and characterizing fully-ordered lattice automata
• Tableaux for constructive concurrent dynamic logic
• Towards an efficient implementation of a tableau method for reactive safety specifications
• Tableau method and NEXPTIME-completeness of DEL-sequents
• Optimal Tableaux-Based Decision Procedure for Testing Satisfiability in the Alternating-Time Temporal Logic ATL+
• Specification and verification of a linear-time temporal logic for graph transformation
• scientific article; zbMATH DE number 1189099 (Why is no real title available?)

Describes a project that uses

Uses Software

• SPOT
• SymPy

This page was built for publication: A tableau construction for finite linear-time temporal logic

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