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 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.

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

Bernardo, Marco
2000

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 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.
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11576/1891863
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 41
  • ???jsp.display-item.citation.isi??? ND
social impact