Process algebras for Petri nets. The alphabetization of distributed systems (Q2406167)

Labeled transition systems are presented as a suitable interleaving semantic model for distributed systems. Some notions of behavioral equivalence are discussed, such as isomorphism equivalence, trace equivalence, and bisimulation equivalence. The non-interleaving model of step transition system is also introduced. Finite place/transition Petri nets are introduced as a suitable semantic model for distributed systems. As this semantic model is not Turing-complete, properties such as reachability, boundedness and liveness are decidable. Also, some behavioral equivalences, such as interleaving bisimulation equivalence and step bisimulation equivalence, are presented. A decidable behavioral equivalence based on the structure of finite nets, i.e., net isomorphism is discussed. A Turing-complete class of finite Petri nets, called non-permissive Petri nets, is introduced. The sequential calculus of sequential finite-state machines (SFM) is equipped with an operational labeled transition systems semantics and operational Petri net semantics. It is proved that all and only the sequential finite-state machines are the models of the Petri net semantics for SFM. SFM is extended with the operator of asynchronous parallel composition in two steps: first by adding parallel composition at top level only, thus obtaining concurrent finite-step machines (CFM); then by additionally extending the definition of action prefixing to parallel processes, thus yielding basic parallel processes (BPP). The parallel composition operator is enhanced to allow for synchronous, point-to-point communication; moreover, in order to force communications, also the calculus of communicating systems (CCS) operator of restriction is added to BPP, but at the top level only. The resulting calculus is a subset of CCS that is expressive enough to model the class of finite CCS nets. Finite-net CCS is enhanced with an operator for atomicity, called strong prefixing, so that action sequences can be used as labels for transitions. Multi-party communication is implemented by means of atomic sequences of binary, CCS-like synchronizations. Hence, the parallel operator has a richer synchronization discipline dealing also with action sequences. The resulting calculus is a subset of multi-CCS, called finite-net multi-CCS (FNM). FNM is extended with a construct for atomic tests, which is exploited to check the absence of those parallel processes whose presence may impede the executability of the current transition. The effect is that parallel composition is no longer a permissive operator, as different parallel contexts may enable or disable the transitions performable by some component. The resulting language, called non-permissive Petri net language, is Turing-complete and represents the class of finite non-permissive Petri nets. A few possible extensions and variant semantics are discussed.