Weak Kripke structures and LTL

DOI10.1007/978-3-642-23217-6_28MaRDI QIDQ3090846zbMATH OpenOpenAlexFDO

Authors Lars Kuhtz, Bernd Finkbeiner

Publication date 2 September 2011

Published in CONCUR 2011 – Concurrency Theory (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-23217-6_28

Mathematics Subject Classification ID

Temporal logic (03B44) Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17) Analysis of algorithms and problem complexity (68Q25) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• The tractability of model checking for LTL: the good, the bad, and the ugly fragments
• scientific article; zbMATH DE number 2196601
• The tractability of model-checking for LTL: the good, the bad, and the ugly fragments
• The complexity of propositional linear temporal logics in simple cases
• On the Complexity of Temporal-Logic Path Checking

Cites work

• A parametric analysis of the state-explosion problem in model checking
• Combining test case generation and runtime verification
• CONCUR 2004 - Concurrency Theory
• scientific article; zbMATH DE number 3940713 (Why is no real title available?)
• scientific article; zbMATH DE number 1905115 (Why is no real title available?)
• Logical definability and query languages over ranked and unranked trees
• LTL Path Checking Is Efficiently Parallelizable
• Model checking a path (preliminary report)
• Mu-calculus path checking
• On the complexity of elementary modal logics
• The Complexity of Generalized Satisfiability for Linear Temporal Logic
• The complexity of poor man's logic
• The complexity of propositional linear temporal logics
• The complexity of propositional linear temporal logics in simple cases
• The Computational Complexity of Provability in Systems of Modal Propositional Logic
• The stuttering principle revisited
• The tractability of model-checking for LTL: the good, the bad, and the ugly fragments

Cited in

(8)

• Applications of weak Kripke semantics to intermediate consequences
• Taming past LTL and flat counter systems
• Program Repair for Hyperproperties
• Model-Checking Counting Temporal Logics on Flat Structures
• Register games
• Model Checking Almost All Paths Can Be Less Expensive Than Checking All Paths
• QLTL model-checking
• Complexity of model checking second-order hyperproperties on finite structures

This page was built for publication: Weak Kripke structures and LTL

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