Characterising Probabilistic Processes Logically

TL;DR

This paper introduces a probabilistic extension of the modal mu-calculus to characterize simulation semantics of finite-state processes with nondeterministic and probabilistic behaviors, enabling logical reasoning about process equivalences.

Contribution

It proposes a new probabilistic mu-calculus and demonstrates how to derive characteristic formulae for simulation preorders without divergence, advancing logical process characterization.

Findings

Derived characteristic formulae for probabilistic simulation preorders

Showed the logic characterizes process equivalences without divergence

Extended mu-calculus to probabilistic processes

Abstract

In this paper we work on (bi)simulation semantics of processes that exhibit both nondeterministic and probabilistic behaviour. We propose a probabilistic extension of the modal mu-calculus and show how to derive characteristic formulae for various simulation-like preorders over finite-state processes without divergence. In addition, we show that even without the fixpoint operators this probabilistic mu-calculus can be used to characterise these behavioural relations in the sense that two states are equivalent if and only if they satisfy the same set of formulae.