Temporal predicate transition nets—a new formalism for specifying and verifying concurrent systems

References

• Brauer , W. and Reisig , W. 1987 . Petri Nets: I—Central Models and Their Properties and II—Applications and Relationships to Other Models of Concurrency, LNCS , Edited by: Rozenberg , G. Vol. 254 and 255 , Springer-Verlag .
   Google Scholar
• Murata , T. 1989 . Petri nets: properties, analysis and applications . Proc. of The IEEE , 77 ( 4 ) : 541 – 580 .
   Web of Science ®Google Scholar
• Pnueli , A. 1986 . Applications of temporal logic to the specification and verification of reactive systems: a survey of current trends . LNCS , 224 : 510 – 584 .
   Google Scholar
• Anttila , M. , Eriksson , H. and Ikonen , J. 1983 . “ Tools and studies of formal techniques—Petri nets and temporal logic ” . In Protocol Specification, Testing, and Verification, III , Edited by: Rudin , H. and West , C. H. 139 – 148 . Elsevier Science Publishers . IFIP
   Google Scholar
• Diaz , M. and Guidacci Da Silverira , G. 1983 . Proceeding of IFIP83 Congress . Information Processing 83 . 1983 . pp. 47 – 52 . Paris On the specification and validation of protocols by temporal logic and nets
   Google Scholar
• Queille , J. P. and Sifakis , J. 1982 . Specification and verification of concurrent systems in CESAR . LNCS , 137 337 – 351 .
   Google Scholar
• Suzuki , I. and Lu , H. 1989 . Temporal Petri nets and their application to modeling and analysis of a handshake daisy chain arbiter . IEEE Trans. Computer , 38 ( 5 ) 696 – 704 .
   Web of Science ®Google Scholar
• Suzuki , I. 1990 . Formal analysis of the alternating bit protocol by temporal Petri nets . IEEE Trans. Software Engineering , 16 ( 11 ) 1273 – 1281 .
   Web of Science ®Google Scholar
• He , X. 1990 . Proc. of the 14th International Computer Software and Application Conference (COMPSAC'90) . Temporal predicate transition nets and their applications . 1990 , Chicago. pp. 261 – 266 .
   Google Scholar
• He , X. and Lee , J. A. N. 1990 . Integrating predicate transition nets with first order temporal logic in the specification and verification of concurrent systems . Formal Aspect of Computing , 2 ( 3 ) 226 – 246 .
   Google Scholar
• Genrich , H. J. and Lautenbach , K. 1981 . System modelling with high level Petri nets . Theoretical Computer Science , 13 109 – 136 .
   Web of Science ®Google Scholar
• Rescher , N. and Urquhart , A. 1971 . Temporal Logic , Springer-Verlag .
   Google Scholar
• Manna , Z. and Pnueli , A. 1981 . “ Verification of concurrent programs: the temporal framework ” . In The Correctness Problem in Computer Science , Edited by: Boyer , R. S. and Moore , J. S. 215 – 274 . Academic Press .
   Google Scholar
• Vardi , M. Y. and Wolper , P. 1986 . Proc. of IEEE Symposium on Logic in Computer Science . An automata-theoretic approach to automatic program verification . 1986 . pp. 332 – 344 .
   Google Scholar
• Garson , J. W. 1984 . “ Quantification in modal logic ” . In Handbook of Philosophical Logic , Vol. II , D. Reidel Publishing Company .
   Google Scholar
• Apt , K. R. , Francez , N. and De Roever , W. P. 1980 . A proof system for communicating sequential processes . ACM TOPLAS , 2 ( 3 ) : 359 – 385 .
   Google Scholar
• Lamport , L. 1989 . A simple approach to specifying concurrent systems . CACM , 32 ( 1 ) : 32 – 45 .
   Web of Science ®Google Scholar
• Abadi , M. and Manna , Z. Nonclausal deduction in first-order temporal logic . JACM , 37 ( 2 ) 279 – 317 .
   Google Scholar
• Fitting , M. C. 1988 . First-order modal tableaux . J. of Automated Reasoning , 4 : 191 – 213 .
   Google Scholar
• Wallen , L. A. 1990 . Automated Deduction in Nonclassical Logics , MIT Press .
   Google Scholar
• Owicki , S. and Lamport , L. 1982 . Proving liveness properties of concurrent programs . ACM TOPLAS , 4 ( 3 ) : 455 – 495 .
   Web of Science ®Google Scholar
• Lamport , L. and Schneider , F. B. 1984 . The Hoare Logic of CSP . ACM TOPLAS , 6 ( 2 ) : 281 – 296 . and all that
   Google Scholar
• Manna , Z. and Pnueli , A. 1984 . Adequate proof principles for invariance and liveness properties of concurrent programs . Science of Computer Programming , 4 ( 3 ) : 257 – 289 .
   Web of Science ®Google Scholar
• Lamport L. A temporal logic of actions 1990 SRC Report #57
   Google Scholar