Temporal predicate transition nets—a new formalism for specifying and verifying concurrent systems
From MaRDI portal
Publication:4032915
DOI10.1080/00207169208804127zbMath0796.68163OpenAlexW2017513308MaRDI QIDQ4032915
Publication date: 16 May 1993
Published in: International Journal of Computer Mathematics (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1080/00207169208804127
verificationtemporal logicspecificationhigh-level Petri netsdining philosophers problempredicate transition nets
Modes of computation (nondeterministic, parallel, interactive, probabilistic, etc.) (68Q10) Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85) Distributed algorithms (68W15)
Cites Work
- Adequate proof principles for invariance and liveness properties of concurrent programs
- A theorem on atomicity in distributed algorithms
- Integrating predicate transition nets with first order temporal logic in the specification and verification of concurrent systems
- First-order modal tableaux
- System modelling with high-level Petri nets
- The ``Hoare Logic of CSP, and All That
- Nonclausal deduction in first-order temporal logic
- A Proof System for Communicating Sequential Processes
- Proving Liveness Properties of Concurrent Programs
