Affordable Access

Publisher Website

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

Electronic Notes in Theoretical Computer Science
Publication Date
DOI: 10.1016/s1571-0661(05)80749-2
  • Linguistics
  • Mathematics


Abstract The 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 EMPA gr including probabilities, priorities, exponentially distributed durations, and the generative master-reactive slaves synchronization mechanism. Then, we prove that the synchronization mechanism in EMPA gr is correct w.r.t. the novel cooperation structure model, we show that the Markovian bisimulation equivalence is a congruence for EMPA gr, and we present a sound and complete axiomatization for finite terms.

There are no comments yet on this publication. Be the first to share your thoughts.