Compositional Asymmetric Cooperations for Process Algebras with Probabilities, Priorities, and Time

AbstractThe modeling and analysis experience with process algebras has shown the necessity of extending them with priority, probabilistic internal/external choice, and time in order to be able to faithfully model the behavior of real systems and capture the properties of interest. An important open problem in this scenario is how to obtain semantic compositionality in the presence of all these mechanisms, to allow for an efficient analysis.In this paper we argue that, when abandoning the classical nondeterministic setting by considering the mechanisms above, a natural solution is to break the symmetry of the roles of the processes participating in a synchronization. We accomplish this by distinguishing between master actions – the choice among which is carried out generatively according to their priorities/probabilities or exponentially distributed durations – and slave actions – the choice among which is carried out reactively according to their priorities/probabilities – and by imposing that a master action can synchronize with slave actions only.Technically speaking, in this paper we define a process algebra called EMPAgr including probabilities, priorities, exponentially distributed durations, and the generative master-reactive slaves synchronization mechanism. Then, we prove that the synchronization mechanism in EMPAgr is correct w.r.t. the novel cooperation structure model, we show that the Markovian bisimulation equivalence is a congruence for EMPAgr, and we present a sound and complete axiomatization for finite terms