Adrián Puerto Aubel, PhD Student at DISCO (Computer Science Dpt.), Universitá degli Studi di Milano-Bicocca, Italy,

Abstract:

Elementary Net Systems represent a suitable paradigm to study the logical structure of observable properties of distributed systems. As a class of Petri Nets, they explicitly represent concurrency, and as elementary systems, their local states are interpretable as Boolean variables. Unlike in the sequential case, on a system depicting concurrency, these properties do not interact according to the classical Boolean logic. We study such logical variables, and their interactions. This is done by looking at the partial order of regions of the case graph of the net system. In particular, we focus on the sets of their potential events, or labels on the transitions, providing them with a structure so as to reason about concurrency from the perspective of the observable properties of these systems. This is achieved by introducing the notion of minimal events, as the generators of such a structure of labels. We show that these events are sufficient to synthesize a transition system, such that its Regional Partial Order is isomorphic to the one obtained with the full set of events.