Antichains: Alternative Algorithms for LTL Satisfiability and Model-Checking

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

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

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

68Q60: Specification and verification (program logics, model checking, etc.)

03B44: Temporal logic

Related Items

Antichains: Alternative Algorithms for LTL Satisfiability and Model-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, 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