# SOS-based Modal Decomposition on Nondeterministic Probabilistic Processes

## TL;DR

This paper introduces a SOS-based method for decomposing modal formulas on nondeterministic probabilistic processes, simplifying the verification of process properties by reducing satisfaction checks to subprocesses.

## Contribution

It presents a novel SOS-like framework for decomposing modal formulae in probabilistic processes, enabling the derivation of congruence formats for probabilistic behavioral equivalences.

## Key findings

- Provides a decomposition method for modal formulae in probabilistic processes.
- Establishes (pre)congruence formats for probabilistic bisimilarity and similarity.
- Introduces a SOS-like machinery for open distribution terms.

## Abstract

We propose a method for the decomposition of modal formulae on processes with nondeterminism and probability with respect to Structural Operational Semantics. The purpose is to reduce the satisfaction problem of a formula for a process to verifying whether its subprocesses satisfy certain formulae obtained from the decomposition. To deal with the probabilistic behavior of processes, and thus with the decomposition of formulae characterizing it, we introduce a SOS-like machinery allowing for the specification of the behavior of open distribution terms. By our decomposition, we obtain (pre)congruence formats for probabilistic bisimilarity, ready similarity and similarity.