Completing the temporal picture
From MaRDI portal
Publication:1176248
DOI10.1016/0304-3975(91)90041-YzbMath0795.68133WikidataQ126352126 ScholiaQ126352126MaRDI QIDQ1176248
Publication date: 25 June 1992
Published in: Theoretical Computer Science (Search for Journal in Brave)
68Q10: Modes of computation (nondeterministic, parallel, interactive, probabilistic, etc.)
03B45: Modal logic (including the logic of norms)
03B70: Logic in computer science
68Q60: Specification and verification (program logics, model checking, etc.)
Related Items
Proving the Refuted: Symbolic Model Checkers as Proof Generators, Verification by augmented abstraction: The automata-theoretic view, On the refinement of liveness properties of distributed systems, Verifying a signature architecture: a comparative case study, Developing topology discovery in Event-B, Models for reactivity, Safety, liveness and fairness in temporal logic, A compositional approach to CTL\(^*\) verification, Hybrid diagrams, Verification by augmented finitary abstraction, Model checking with strong fairness, Liveness Reasoning with Isabelle/HOL, MODULAR RANKING ABSTRACTION, Using Patterns and Composite Propositions to Automate the Generation of LTL Specifications
Cites Work
- Adequate proof principles for invariance and liveness properties of concurrent programs
- The \(\mu\)-calculus as an assertion-language for fairness arguments
- A calculus of communicating systems
- First-order dynamic logic
- A proof rule for fair termination of guarded commands
- Countable nondeterminism and random assignment
- Verifying temporal properties without temporal logic
- Ten Years of Hoare's Logic: A Survey—Part I
- A combinatorial approach to the theory of ω-automata
- Proving Liveness Properties of Concurrent Programs
- Soundness and Completeness of an Axiom System for Program Verification
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
