Metric Denotational Semantics For Probabilistic Process Algebra

During the last decade many studies focus on functional analysis of systems using process algebra, almost no work deals with performance evaluation. Process algebra without probability can only describe functional aspects, but not performance aspects of such systems. Therefore it is necessary to add performance evaluation parameters (such as probability) on process algebra. As a result we get probabilistic process algebra. Event structures are important true concurrent models and are well-suited to provide a true concurrent semantics for process algebra in a compositional way. But the related work is insufficient. In this paper, we take probabilistic event structures as our semantic model and provide a metric denotational semantics for probabilistic process algebra.Each action in probabilistic process algebra can be assigned a fixed probability, which can eliminate the non-deterministic of choice. In order to define semantics for probabilistic process algebra, we take probabilistic event structures as our semantic models. In these structures, internal events can be assigned a fixed probability. In this way, probabilistic event structures can specify probabilistic behaviour of systems. Since it is hard to specify recursive processes using probabilistic event structures directly, we use a metric approach on probabilistic event structures. The distance function of the metric is based on the length of the longest bundle chain in probabilistic event structures. But this intuitive notion of distance is a pseudo metric, but not a metric. In order to get a metric, we constitute the equivalence classes of probabilistic event structures and obtain the set of finitely approximable probabilistic event structures, which is shown to be a complete ultra-metric space. Due to Banach's fixed point theorem, we can define a metric semantics for the contractive process expressions on this complete metric space. This work is important for formal verification and systems optimization.