For the most recent entries see the Petri Nets Newsletter.

Modular Verification of Petri Nets: The Temporal Logic Approach.

Damm, Werner; Döhmen, Gert; Gerstner, Volker; Josko, Bernhard

In: J.W. de Bakker, et al.: Lecture Notes in Computer Science, Vol. 430; Proceedings of the REX Workshop on Stepwise Refinement, 1989, Mook, The Netherlands, pages 180-207. Berin, Germany: Springer-Verlag, 1990.

Abstract: In the paper, the questions of reactive behaviour decomposition and stepwise refinement are considered using a particular class of Petri nets as models for open reactive systems. The paper presents an assumption/commitment style temporal logic for specifying the behaviour of such systems, an automatic proof method for verifying the correctness of an implementation of such a specification in terms of the considered class of Petri nets based on modelchecking of MCTL formula, and presents a proof method for infering the behaviour of a compound reactive system from the behaviour of its constituents.

Keywords: modular verification; temporal logic; refinement; reactive system.

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

Back to the Petri Nets Bibliography