In: Proc. of the Fifteenth Manitoba Conf. on Numerical Mathematics and Computing, pages 211-227. 1986.
Abstract: Petri nets are often used as a formal tool for representing distributed systems. It is shown that the reachable markings of a Petri net form a branching tense structure, thereby permitting the use of the temporal logic to define properties of the distributed system.