SOS-based modal decomposition on nondeterministic probabilistic processes

Valentina Castiglioni, Daniel Gebler, Simone Tini

Research output: Contribution to JournalArticleAcademicpeer-review


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.

Original languageEnglish
Article number18
Pages (from-to)1-51
Number of pages51
JournalLogical Methods in Computer Science
Issue number2
Publication statusPublished - 25 Jun 2018


  • Decomposition of modal formulae
  • Logical characterization
  • Nondeterministic probabilistic process algebras
  • SOS


Dive into the research topics of 'SOS-based modal decomposition on nondeterministic probabilistic processes'. Together they form a unique fingerprint.

Cite this