|
Abstract: |
Development of complex concurrent systems with Petri nets is very often performed in a top-down or bottom-up approach depending on design circumstances. In this process, some vertical structuring techniques are needed to reduce the amount of work in specification, modeling, analysis and verification. Petri net morphisms will be useful in this process as long as desired structural and/or behavioral properties are preserved.
This thesis is a study of structural and behavioral properties of concurrent system models related to Petri net morphisms.
Three types of Petri net morphisms: vicinity respecting morphisms, Winskel???s morphisms and general morphisms are considered and their purposes and relations are presented. Different structural and behavioral properties of Petri net morphisms, including connectivity, path, strong connectedness, pre/post vicinity of place/transition, subnet, strongly connected place/transition bordered subnet, S/T component, covering by S/T components, siphon, trap, free-choice property, initial marking, reachable marking, boundedness, safety, liveness, case graph, are examined. The roles of Petri net morphisms in the development of concurrent systems are discussed. An example of Petri net morphisms??? application in the development of concurrent systems is given too.
This thesis shows that Petri net morphisms are very useful in formal specification, conceptual modeling, analysis and verification of concurrent systems with respect to system refinement and abstraction.
|
