License: Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.CONCUR.2023.15
URN: urn:nbn:de:0030-drops-190090
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2023/19009/
Go to the corresponding LIPIcs Volume Portal

Schmitt, Anna ; Peters, Kirstin

Probabilistic Operational Correspondence

pdf-format:
LIPIcs-CONCUR-2023-15.pdf (0.9 MB)

Abstract

Encodings are the main way to compare process calculi. By applying quality criteria to encodings we analyse their quality and rule out trivial or meaningless encodings. Thereby, operational correspondence is one of the most common and most important quality criteria. It ensures that processes and their translations have the same abstract behaviour. We analyse probabilistic versions of operational correspondence to enable such a verification for probabilistic systems.
Concretely, we present three versions of probabilistic operational correspondence: weak, middle, and strong. We show the relevance of the weaker version using an encoding from a sublanguage of probabilistic CCS into the probabilistic π-calculus. Moreover, we map this version of probabilistic operational correspondence onto a probabilistic behavioural relation that directly relates source and target terms. Then we can analyse the quality of the criterion by analysing the relation it induces between a source term and its translation. For the second version of probabilistic operational correspondence we proceed in the opposite direction. We start with a standard simulation relation for probabilistic systems and map it onto a probabilistic operational correspondence criterion.

BibTeX - Entry

@InProceedings{schmitt_et_al:LIPIcs.CONCUR.2023.15,
  author =	{Schmitt, Anna and Peters, Kirstin},
  title =	{{Probabilistic Operational Correspondence}},
  booktitle =	{34th International Conference on Concurrency Theory (CONCUR 2023)},
  pages =	{15:1--15:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-299-0},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{279},
  editor =	{P\'{e}rez, Guillermo A. and Raskin, Jean-Fran\c{c}ois},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2023/19009},
  URN =		{urn:nbn:de:0030-drops-190090},
  doi =		{10.4230/LIPIcs.CONCUR.2023.15},
  annote =	{Keywords: Probabilistic Process Calculi, Encodings, Operational Correspondence}
}

Keywords: Probabilistic Process Calculi, Encodings, Operational Correspondence
Collection: 34th International Conference on Concurrency Theory (CONCUR 2023)
Issue Date: 2023
Date of publication: 07.09.2023

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI