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

He, X, Lee, JAN. (1990). Integrating predicate transition nets with first order temporal logic in the specification and verification of concurrent systems . 2(1), 226-246. 10.1007/BF01888226

cited authors

  • He, X; Lee, JAN

authors

abstract

  • This paper presents some results of integrating predicate transition nets with first order temporal logic in the specification and verification of concurrent systems. The intention of this research is to use predicate transition nets as a specification method and to use first order temporal logic as a verification method so that their strengths - the easy comprehension of predicate transition nets and the reasoning power of first order temporal logic can be combined. In this paper, a theoretical relationship between the computation models of these two formalisms is presented; an algorithm for systematically translating a predicate transition net into a corresponding temporal logic system is outlined; and a special temporal refutation proof technique is proposed and illustrated in verifying various concurrent properties of the predicate transition net specification of the five dining philosophers problem. © 1990 BCS.

publication date

  • March 1, 1990

Digital Object Identifier (DOI)

start page

  • 226

end page

  • 246

volume

  • 2

issue

  • 1