Antichains: Alternative Algorithms for LTL Satisfiability and Model-Checking
From MaRDI portal
Recommendations
- SAT-based explicit LTL reasoning and its application to satisfiability checking
- An explicit transition system construction approach to LTL satisfiability checking
- LTL semantic tableaux and alternating -automata via linear factors
- Antichains and compositional algorithms for LTL synthesis
- Accelerating LTL satisfiability checking by SAT solvers
Cites work
- A new solution of Dijkstra's concurrent programming problem
- Antichains: A New Algorithm for Checking Universality of Finite Automata
- Antichains: Alternative Algorithms for LTL Satisfiability and Model-Checking
- Computer Aided Verification
- Constructing Büchi automata from linear temporal logic using simulation relations for alternating Büchi automata
- scientific article; zbMATH DE number 1670781 (Why is no real title available?)
- scientific article; zbMATH DE number 438994 (Why is no real title available?)
- scientific article; zbMATH DE number 3866588 (Why is no real title available?)
- scientific article; zbMATH DE number 1538040 (Why is no real title available?)
- scientific article; zbMATH DE number 1796123 (Why is no real title available?)
- scientific article; zbMATH DE number 2102710 (Why is no real title available?)
- Improved Algorithms for the Automata-Based Approach to Model-Checking
- Model Checking Software
- NuSMV: A new symbolic model checker
- On complementing nondeterministic Büchi automata
- Reasoning about infinite computations
Cited in
(23)- LTL semantic tableaux and alternating -automata via linear factors
- 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
- A symbolic decision procedure for symbolic alternating finite automata
- SAT-based explicit LTL reasoning and its application to satisfiability checking
- Synthesising succinct strategies in safety games with an application to real-time scheduling
- Extracting unsatisfiable cores for LTL via temporal resolution
- Symbolic model checking in non-Boolean domains
- From LTL and limit-deterministic Büchi automata to deterministic parity automata
- Strategy Construction for Parity Games with Imperfect Information
- An Antichain Algorithm for LTL Realizability
- Fixpoint Guided Abstraction Refinement for Alternating Automata
- Towards a notion of unsatisfiable and unrealizable cores for LTL
- Enhancing unsatisfiable cores for LTL with information on temporal relevance
- Antichains: Alternative Algorithms for LTL Satisfiability and Model-Checking
- scientific article; zbMATH DE number 7327941 (Why is no real title available?)
- Automata terms in a lazy \(\mathrm{WS}k\mathrm{S}\) decision procedure
- Automata terms in a lazy \(\mathrm{WS}k\mathrm{S}\) decision procedure
- From linear temporal logics to Büchi automata: the early and simple principle
- Simplifying Alternating Automata for Emptiness Testing
- Antichain with SAT and tries
- Antiprenexing for WSkS: a little goes a long way
This page was built for publication: Antichains: Alternative Algorithms for LTL Satisfiability and Model-Checking
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5458321)
