License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.FSTTCS.2020.35
URN: urn:nbn:de:0030-drops-132764
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2020/13276/
Go to the corresponding LIPIcs Volume Portal

Almagor, Shaull

Process Symmetry in Probabilistic Transducers

pdf-format:
LIPIcs-FSTTCS-2020-35.pdf (0.6 MB)

Abstract

Model checking is the process of deciding whether a system satisfies a given specification. Often, when the setting comprises multiple processes, the specifications are over sets of input and output signals that correspond to individual processes. Then, many of the properties one wishes to specify are symmetric with respect to the processes identities. In this work, we consider the problem of deciding whether the given system exhibits symmetry with respect to the processes' identities. When the system is symmetric, this gives insight into the behaviour of the system, as well as allows the designer to use only representative specifications, instead of iterating over all possible process identities.
Specifically, we consider probabilistic systems, and we propose several variants of symmetry. We start with precise symmetry, in which, given a permutation π, the system maintains the exact distribution of permuted outputs, given a permuted inputs. We proceed to study approximate versions of symmetry, including symmetry induced by small L_∞ norm, variants of Parikh-image based symmetry, and qualitative symmetry. For each type of symmetry, we consider the problem of deciding whether a given system exhibits this type of symmetry.

BibTeX - Entry

@InProceedings{almagor:LIPIcs:2020:13276,
  author =	{Shaull Almagor},
  title =	{{Process Symmetry in Probabilistic Transducers}},
  booktitle =	{40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020)},
  pages =	{35:1--35:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-174-0},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{182},
  editor =	{Nitin Saxena and Sunil Simon},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2020/13276},
  URN =		{urn:nbn:de:0030-drops-132764},
  doi =		{10.4230/LIPIcs.FSTTCS.2020.35},
  annote =	{Keywords: Symmetry, Probabilistic Transducers, Model Checking, Permutations}
}

Keywords: Symmetry, Probabilistic Transducers, Model Checking, Permutations
Collection: 40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020)
Issue Date: 2020
Date of publication: 04.12.2020

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