Verification by augmented abstraction: The automata-theoretic view
From MaRDI portal
Publication:5946060
DOI10.1006/jcss.2000.1744zbMath0983.68109MaRDI QIDQ5946060
Moshe Y. Vardi, Yonit Kesten, Amir Pnueli
Publication date: 28 April 2002
Published in: Journal of Computer and System Sciences (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1006/jcss.2000.1744
68Q45: Formal languages and automata
Related Items
On the refinement of liveness properties of distributed systems, MODULAR RANKING ABSTRACTION, On-the-fly Emptiness Check of Transition-Based Streett Automata
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- On verifying that a concurrent program satisfies a nondeterministic specification
- The \(\mu\)-calculus as an assertion-language for fairness arguments
- Completing the temporal picture
- Symbolic model checking: \(10^{20}\) states and beyond
- Theories of automata on \(\omega\)-tapes: a simplified approach
- Reasoning about infinite computations
- Property preserving abstractions for the verification of concurrent systems
- Verification by augmented finitary abstraction
- Verification of concurrent programs: The automata-theoretic framework
- Generalized temporal verification diagrams
- Temporal logic can be more expressive
- A new solution of Dijkstra's concurrent programming problem
