SOS-based Modal Decomposition on Nondeterministic Probabilistic Processes

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.

References in corpus (5)

• Revisiting Trace and Testing Equivalences for Nondeterministic and Probabilistic Processes
• Logical, Metric, and Algorithmic Characterisations of Probabilistic Bisimulation
• Logical Characterization of Bisimulation Metrics
• Logical Characterization of Trace Metrics
• Divide and Congruence II: From Decomposition of Modal Formulas to Preservation of Delay and Weak Bisimilarity

Cited by in corpus (1)

• Trace and Testing Metrics on Nondeterministic Probabilistic Processes