From complementation to certification
From MaRDI portal
Publication:2575735
DOI10.1016/j.tcs.2005.07.021zbMath1079.68060MaRDI QIDQ2575735
Moshe Y. Vardi, Orna Kupferman
Publication date: 6 December 2005
Published in: Theoretical Computer Science (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/j.tcs.2005.07.021
68Q45: Formal languages and automata
68Q60: Specification and verification (program logics, model checking, etc.)
Cites Work
- Alternating finite automata on \(\omega\)-words
- The complementation problem for Büchi automata with applications to temporal logic
- Symbolic model checking: \(10^{20}\) states and beyond
- Theories of automata on \(\omega\)-tapes: a simplified approach
- Reasoning about infinite computations
- Safety, liveness and fairness in temporal logic
- An algorithm for strongly connected component analysis in \(n \log n\) symbolic steps
- The complexity of verification
- Temporal logic can be more expressive
- Weak alternating automata are not that weak
- Synthesis of Communicating Processes from Temporal Logic Specifications
- Correct Hardware Design and Verification Methods
- A new heuristic for bad cycle detection using BDDs
- Model checking of safety properties
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item