In: Proceedings of the 12th International Conference on Application and Theory of Petri Nets, 1991, Gjern, Denmark, pages 165-181. June 1991.
Abstract: Place/transition nets are represesnted as sets of formulas in first-order logic and their properties in first-order logic, in propositional dynamic logic, and in quantified dynamic logic. The dynamic logic formulas representing the properties are translated into first-order logic and a resolution theorem prover is used to verify the properties, i.e. to show that they are entailed by the properties of the net. The verification is based on constructing a relevant part of the reachability graph for the net. A detailed example is used to demonstrate the performance of a resolution theorem prover in this task.
Keywords: place/transition net property proving (with)resolution theorem prover; first-order logic; propositional dynamic logic; quantified dynamic logic; reachability graph; resolution theorem prover performance.