DROPS

Document

DOI: 10.4230/LIPIcs.CONCUR.2016.36

Modal Decomposition on Nondeterministic Probabilistic Processes

Authors: Valentina Castiglioni, Daniel Gebler, and Simone Tini

Published in: LIPIcs, Volume 59, 27th International Conference on Concurrency Theory (CONCUR 2016)

Abstract

We propose a SOS-based method for decomposing modal formulae for nondeterministic probabilistic processes. The purpose is to reduce the satisfaction problem of a formula for a process to verifying whether its subprocesses satisfy certain formulae obtained from its decomposition. By our decomposition, we obtain (pre)congruence formats for probabilistic bisimilarity, ready similarity and similarity.

Cite as

Valentina Castiglioni, Daniel Gebler, and Simone Tini. Modal Decomposition on Nondeterministic Probabilistic Processes. In 27th International Conference on Concurrency Theory (CONCUR 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 59, pp. 36:1-36:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{castiglioni_et_al:LIPIcs.CONCUR.2016.36,
  author =	{Castiglioni, Valentina and Gebler, Daniel and Tini, Simone},
  title =	{{Modal Decomposition on Nondeterministic Probabilistic Processes}},
  booktitle =	{27th International Conference on Concurrency Theory (CONCUR 2016)},
  pages =	{36:1--36:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-017-0},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{59},
  editor =	{Desharnais, Jos\'{e}e and Jagadeesan, Radha},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2016.36},
  URN =		{urn:nbn:de:0030-drops-61665},
  doi =		{10.4230/LIPIcs.CONCUR.2016.36},
  annote =	{Keywords: SOS, nondeterministic probabilistic process algebras, logical characterization, decomposition of modal formulae}
}

Document

DOI: 10.4230/LIPIcs.CONCUR.2015.155

SOS Specifications of Probabilistic Systems by Uniformly Continuous Operators

Authors: Daniel Gebler and Simone Tini

Published in: LIPIcs, Volume 42, 26th International Conference on Concurrency Theory (CONCUR 2015)

Abstract

Compositional reasoning over probabilistic systems wrt. behavioral metric semantics requires the language operators to be uniformly continuous. We study which SOS specifications define uniformly continuous operators wrt. bisimulation metric semantics. We propose an expressive specification format that allows us to specify operators of any given modulus of continuity. Moreover, we provide a method that allows to derive from any given specification the modulus of continuity of its operators.

Cite as

Daniel Gebler and Simone Tini. SOS Specifications of Probabilistic Systems by Uniformly Continuous Operators. In 26th International Conference on Concurrency Theory (CONCUR 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 42, pp. 155-168, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{gebler_et_al:LIPIcs.CONCUR.2015.155,
  author =	{Gebler, Daniel and Tini, Simone},
  title =	{{SOS Specifications of Probabilistic Systems by Uniformly Continuous Operators}},
  booktitle =	{26th International Conference on Concurrency Theory (CONCUR 2015)},
  pages =	{155--168},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-91-0},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{42},
  editor =	{Aceto, Luca and de Frutos Escrig, David},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2015.155},
  URN =		{urn:nbn:de:0030-drops-53876},
  doi =		{10.4230/LIPIcs.CONCUR.2015.155},
  annote =	{Keywords: SOS, probabilistic process algebra, bisimulation metric semantics, compositional metric reasoning, uniform continuity}
}

Search Results

Documents authored by Gebler, Daniel

Modal Decomposition on Nondeterministic Probabilistic Processes

Abstract

Cite as

SOS Specifications of Probabilistic Systems by Uniformly Continuous Operators

Abstract

Cite as

Thanks for your feedback!

Could not send message