For the most recent entries see the Petri Nets Newsletter.

Integrating Predicate Transition Nets with First Order Temporal Logic in the Specification and Verification of Concurrent Systems.

He, Xudong; Lee, John A.N.

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.

Do you need a refined search? Try our search engine which allows complex field-based queries.

Back to the Petri Nets Bibliography