Self-independent Petri Nets (or a dead-lock-free paradigm)

Sun, Yong

Abstract: The work presented comes from the following three considerations:(a) hand-shaking has implementation problems, especially synchronization in distributed systems;(b) dead-lock detection is generally undecidable;(c) a non-interleaving and denotational model for CCS.

Technically, the model is constructed from labelled Petri Nets with emphasis on self-independency which resolves the above three problems at the same time. Also, our result can be regarded as an improvement of (a) Winskel's event structures [Winskel 83] which semantics is non-symmetricity to non-determinism (i.e. the semantics of B1 + B2 is not equal to semantics of B2 + B1; of (b) Goltz and Mycroft's labelled Petri-nets [Goltz 84] which cannot systematically deal with recursive processes (i.e. they have trouble in giving a semantics to B2 in {B1 \Leftarrow alpha.Nil | gamma.B1,B2 \Leftarrow B1 | beta.B2}, although isomorphic nets are treated as identical; and of (c) the work of Boudol and Castellani in [Boudol 87] which follows Winskel's approach and solves the problem of non-symmetricity of non-determinism, but can only discuss finite structures. Therefore, this paper provides an appropriate and sufficiently abstract domain of Petri Nets for solving fixpoints of semantic equations when isomorphic nets are regarded as identical.


Previous | Index | Next