Completing the temporal picture

DOI10.1016/0304-3975(91)90041-YzbMath0795.68133OpenAlexW2065353132WikidataQ126352126 ScholiaQ126352126MaRDI QIDQ1176248

Amir Pnueli, Zohar Manna

Publication date: 25 June 1992

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/0304-3975(91)90041-y

zbMATH Keywords

Borel hierarchycomplete proof systemtemporal properties of reactive programs

Mathematics Subject Classification ID

Modes of computation (nondeterministic, parallel, interactive, probabilistic, etc.) (68Q10) Modal logic (including the logic of norms) (03B45) Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60)

Related Items

Efficient Runtime Verification of First-Order Temporal Properties ⋮ Hybrid diagrams: A deductive-algorithmic approach to hybrid system verification ⋮ Safety, liveness and fairness in temporal logic ⋮ Selectively-amortized resource bounding ⋮ Liveness Reasoning with Isabelle/HOL ⋮ Monitorability for the Hennessy-Milner logic with recursion ⋮ Verifying a signature architecture: a comparative case study ⋮ A simple rewrite system for the normalization of linear temporal logic ⋮ Using Patterns and Composite Propositions to Automate the Generation of LTL Specifications ⋮ A sound and complete proof system for a unified temporal logic ⋮ A dynamic logic for deductive verification of multi-threaded programs ⋮ First-order temporal logic monitoring with BDDs ⋮ A formal definition of hierarchical predicate transition nets ⋮ A decision procedure and complete axiomatization for projection temporal logic ⋮ Computer says no: verdict explainability for runtime monitors using a local proof system ⋮ A compositional approach to CTL\(^*\) verification ⋮ Verification by augmented abstraction: The automata-theoretic view ⋮ Proving the Refuted: Symbolic Model Checkers as Proof Generators ⋮ Model checking with strong fairness ⋮ Automatically verifying temporal properties of pointer programs with cyclic proof ⋮ On the refinement of liveness properties of distributed systems ⋮ Past is for Free: on the Complexity of Verifying Linear Temporal Properties with Past ⋮ Developing topology discovery in Event-B ⋮ MODULAR RANKING ABSTRACTION ⋮ Hybrid diagrams ⋮ Verification by augmented finitary abstraction ⋮ Models for reactivity ⋮ Back to the future: a fresh look at linear temporal logic

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• 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