SOS-based modal decomposition on nondeterministic probabilistic processes

Valentina Castiglioni, Daniel Gebler, Simone Tini

Research output: Contribution to JournalArticleAcademicpeer-review

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.

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

Fingerprint

Decomposition
Decompose
Structural Operational Semantics
Nondeterminism
Congruence
Machinery
Semantics
Specification
Specifications
Term
Similarity

Keywords

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

Cite this

Castiglioni, Valentina ; Gebler, Daniel ; Tini, Simone. / SOS-based modal decomposition on nondeterministic probabilistic processes. In: Logical Methods in Computer Science. 2018 ; Vol. 14, No. 2. pp. 1-51.
@article{7a92450432c74c3b9bbb2998aa4337c7,
title = "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.",
keywords = "Decomposition of modal formulae, Logical characterization, Nondeterministic probabilistic process algebras, SOS",
author = "Valentina Castiglioni and Daniel Gebler and Simone Tini",
year = "2018",
month = "6",
day = "25",
doi = "10.23638/LMCS-14(2:18)2018",
language = "English",
volume = "14",
pages = "1--51",
journal = "Logical Methods in Computer Science",
issn = "1860-5974",
publisher = "Technischen Universitat Braunschweig",
number = "2",

}

SOS-based modal decomposition on nondeterministic probabilistic processes. / Castiglioni, Valentina; Gebler, Daniel; Tini, Simone.

In: Logical Methods in Computer Science, Vol. 14, No. 2, 18, 25.06.2018, p. 1-51.

Research output: Contribution to JournalArticleAcademicpeer-review

TY - JOUR

T1 - SOS-based modal decomposition on nondeterministic probabilistic processes

AU - Castiglioni, Valentina

AU - Gebler, Daniel

AU - Tini, Simone

PY - 2018/6/25

Y1 - 2018/6/25

N2 - 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.

AB - 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.

KW - Decomposition of modal formulae

KW - Logical characterization

KW - Nondeterministic probabilistic process algebras

KW - SOS

UR - http://www.scopus.com/inward/record.url?scp=85055834923&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=85055834923&partnerID=8YFLogxK

U2 - 10.23638/LMCS-14(2:18)2018

DO - 10.23638/LMCS-14(2:18)2018

M3 - Article

VL - 14

SP - 1

EP - 51

JO - Logical Methods in Computer Science

JF - Logical Methods in Computer Science

SN - 1860-5974

IS - 2

M1 - 18

ER -