Expressing Priorities and External Probabilities in Process Algebra
via Mixed Open/Closed Systems

Mario Bravetti

Abstract.

Defining operational semantics for a process algebra is often based
either on labeled transition systems that account for interaction with
a context or on the so-called reduction semantics: we assume to have a
representation of the whole system and we compute unlabeled reduction
transitions (leading to a distribution over states in the
probabilistic case). In this paper we consider mixed models with
states where the system is still open (towards interaction with a
context) and states where the system is already closed. The idea is
that (open) parts of a system $P$ can be closed via an operator ``$P
\uparrow G$'' that turns synchronized actions whose ``handle'' is
specified inside ``$G$'' into prioritized reduction transitions (and,
therefore, states performing them into closed states). We show that we
can use the operator ``$P \uparrow G$'' to express multi-level
priorities and external probabilistic choices, and that, by
considering reduction transitions as the only unobservable $\tau$
transitions, the proposed technique is compatible, for process algebra
with general recursion, with both standard (probabilistic)
observational congruence and a notion of equivalence which aggregates
reduction transitions in a (much more aggregating) trace based
manner. Finally, we observe that the trace-based aggregated transition
system can be obtained directly in operational semantics.  Time: