Temporal predicate transition nets—a new formalism for specifying and verifying concurrent systems

DOI10.1080/00207169208804127MaRDI QIDQ4032915zbMATH OpenOpenAlexFDO

Authors Xudong He

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

zbMATH Keywords

dining philosophers problemhigh-level Petri netspredicate transition netsspecificationtemporal logicverification

Mathematics Subject Classification ID

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)

Recommendations

• Integrating predicate transition nets with first order temporal logic in the specification and verification of concurrent systems
• Formal Specification of Concurrent Systems: A Structured Approach
• A formal definition of hierarchical predicate transition nets
• ITL semantics of composite Petri nets
• scientific article; zbMATH DE number 749804

Cites work

• A Proof System for Communicating Sequential Processes
• A theorem on atomicity in distributed algorithms
• Adequate proof principles for invariance and liveness properties of concurrent programs
• First-order modal tableaux
• Integrating predicate transition nets with first order temporal logic in the specification and verification of concurrent systems
• Nonclausal deduction in first-order temporal logic
• Proving Liveness Properties of Concurrent Programs
• System modelling with high-level Petri nets
• The ``Hoare Logic of CSP, and All That

Cited in

(5)

• scientific article; zbMATH DE number 15894 (Why is no real title available?)
• Formal Specification of Concurrent Systems: A Structured Approach
• scientific article; zbMATH DE number 1556864 (Why is no real title available?)
• A formal definition of hierarchical predicate transition nets
• Integrating predicate transition nets with first order temporal logic in the specification and verification of concurrent systems

This page was built for publication: Temporal predicate transition nets—a new formalism for specifying and verifying concurrent systems

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4032915)