Integrating predicate transition nets with first order temporal logic in the specification and verification of concurrent systems

DOI10.1007/BF01888226zbMath0703.68078MaRDI QIDQ916414

John A. N. Lee, Xudong He

Publication date: 1990

Published in: Formal Aspects of Computing (Search for Journal in Brave)

zbMATH Keywords

Petri netsformal verificationformal specificationtemporal logic

Mathematics Subject Classification ID

Modes of computation (nondeterministic, parallel, interactive, probabilistic, etc.) (68Q10) Modal logic (including the logic of norms) (03B45) Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Related Items (1)

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

Uses Software

• ETPS
• CESAR

Cites Work

• System modelling with high-level Petri nets
• Tableau methods of proof for modal logics
• Specifying Concurrent Program Modules
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Integrating predicate transition nets with first order temporal logic in the specification and verification of concurrent systems