In: Formal Aspects of Computing, Vol. 2, No. 3, pages 226-246. July 1990.
Abstract: This paper presents some results of integrating predicte transition nets with first order temporal logic; the intention is to use predicte transition nets as a specification method and first order temporal logic as a verification method. A theoretical relationship between the computation models of theses two formalisms is presented; an algorithm for systematically translating a predicate transition net into a corresponding temporal logic system is outlined; a special temporal refutation proof technique is prososed and illustrated in verifying various properties of the predicate transition net specification of the dining philosophers problem.
Keywords: (integrating) predicate transition net(s) (with) first order temporal logic; specification, verification (of) concurrent system(s); dining philosophers problem.