Skip to Main content Skip to Navigation
Journal articles

SOS-based Modal Decomposition on Nondeterministic Probabilistic Processes

Valentina Castiglioni 1 Daniel Gebler 2 Simone Tini 3
1 COMETE - Concurrency, Mobility and Transactions
Inria Saclay - Ile de France, LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau]
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.
Document type :
Journal articles
Complete list of metadata
Contributor : Valentina Castiglioni <>
Submitted on : Sunday, December 30, 2018 - 9:57:43 AM
Last modification on : Friday, April 30, 2021 - 10:04:18 AM




Valentina Castiglioni, Daniel Gebler, Simone Tini. SOS-based Modal Decomposition on Nondeterministic Probabilistic Processes. Logical Methods in Computer Science, Logical Methods in Computer Science Association, 2018, 14 (2), ⟨10.23638/LMCS-14(2:18)2018⟩. ⟨hal-01966954⟩



Record views