Antichains: Alternative Algorithms for LTL Satisfiability and Model-Checking

DOI10.1007/978-3-540-78800-3_6zbMath1134.68404OpenAlexW1592306554MaRDI QIDQ5458321

Nicolas Maquet, Laurent Doyen, Martin De Wulf, Jean-François Raskin

Publication date: 11 April 2008

Published in: Tools and Algorithms for the Construction and Analysis of Systems (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-540-78800-3_6

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Temporal logic (03B44)

Related Items (max. 100)

Extracting unsatisfiable cores for LTL via temporal resolution ⋮ A symbolic decision procedure for symbolic alternating finite automata ⋮ Symbolic Model Checking in Non-Boolean Domains ⋮ Synthesising succinct strategies in safety games with an application to real-time scheduling ⋮ From linear temporal logics to Büchi automata: the early and simple principle ⋮ Towards a notion of unsatisfiable and unrealizable cores for LTL ⋮ An explicit transition system construction approach to LTL satisfiability checking ⋮ Strategy construction for parity games with imperfect information ⋮ Fixed point guided abstraction refinement for alternating automata ⋮ Strategy Construction for Parity Games with Imperfect Information ⋮ From LTL and Limit-Deterministic Büchi Automata to Deterministic Parity Automata ⋮ Enhancing unsatisfiable cores for LTL with information on temporal relevance ⋮ Antichains: Alternative Algorithms for LTL Satisfiability and Model-Checking ⋮ Automata terms in a lazy \(\mathrm{WS}k\mathrm{S}\) decision procedure ⋮ Automata terms in a lazy \(\mathrm{WS}k\mathrm{S}\) decision procedure ⋮ Fixpoint Guided Abstraction Refinement for Alternating Automata

Uses Software

• NuSMV
• CUDD
• LTL2BA

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Reasoning about infinite computations
• NuSMV: A new symbolic model checker
• Constructing Büchi Automata from Linear Temporal Logic Using Simulation Relations for Alternating Büchi Automata
• A new solution of Dijkstra's concurrent programming problem
• Model Checking Software
• Antichains: Alternative Algorithms for LTL Satisfiability and Model-Checking
• Computer Aided Verification
• Antichains: A New Algorithm for Checking Universality of Finite Automata
• Improved Algorithms for the Automata-Based Approach to Model-Checking
• Correct Hardware Design and Verification Methods

This page was built for publication: Antichains: Alternative Algorithms for LTL Satisfiability and Model-Checking