scientific article; zbMATH DE number 3800906

zbMath0507.68005MaRDI QIDQ4745241

Zohar Manna, Amir Pnueli

Publication date: 1983

Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.

zbMATH Keywords

invariancelivenessprecedencefirst-order temporal logicshared-variables computation model

Mathematics Subject Classification ID

Modal logic (including the logic of norms) (03B45) Specification and verification (program logics, model checking, etc.) (68Q60)

Related Items (16)

Verification of multiprocess probabilistic protocols ⋮ A principle for sequential reasoning about distributed algorithms ⋮ Proving entailment between conceptual state specifications ⋮ A new algebraic semantic approach and some adequate connectives for computation with temporal logic over discrete time ⋮ The temporal boolean derivative applied to verification of extended finite state machines ⋮ The power of temporal proofs ⋮ Completing the temporal picture ⋮ A temporal logic approach to discrete event control for the safety canonical class ⋮ On using temporal logic for refinement and compositional verification of concurrent systems ⋮ The \({\mathcal NU}\) system as a development system for concurrent programs: \(\delta{\mathcal NU}\) ⋮ Transformation of programs for fault-tolerance ⋮ ``A la Burstall intermittent assertions induction principles for proving inevitability properties of programs ⋮ Decidability for a temporal logic used in discrete-event system analysis ⋮ A structured temporal logic language: XYZ/SE ⋮ Real-time refinement in Manna and Pnueli's temporal logic ⋮ On the strength of temporal proofs

This page was built for publication: