2015/08/25 by Pedro R. D’Argenio, Pedro R. D'Argenio, Matias David Lee +1 · 1 citation
Computer Science · Mathematics · #Advanced Algebra and Logic #Artificial intelligence #Bisimulation #Computer science #Congruence (geometry) #Discrete mathematics #Equivalence (formal languages) #Formal Methods in Verification #Logic, programming, and type systems #Mathematics #Nondeterministic algorithm #Probabilistic logic #Theoretical computer science #Transition system #cs.LO #cs.PL
paper · pdf · doi:10.4204/eptcs.190.3
published as EPTCS 190, 2015, pp. 31-45 · In Proceedings EXPRESS/SOS 2015, arXiv:1508.06347
openalex publication_date 2015/08/25 · arxiv created 2015/08/27 · arxiv updated 2015/08/28 · openalex created_date 2021/04/13 · openalex updated_date 2026/08/05
Probabilistic transition system specifications (PTSSs) in the nt μ fθ / ntμ xθ format provide structural operational semantics for Segala-type systems that exhibit both probabilistic and nondeterministic behavior and guarantee that bisimilarity is a congruence for all operator defined in such format. Starting from the nt μ fθ / ntμ xθ format, we obtain restricted formats that guarantee that three coarser bisimulation equivalences are congruences. We focus on (i) Segala's variant of bisimulation that considers combined transitions, which we call here "convex bisimulation"; (ii) the bisimulation equivalence resulting from considering Park & Milner's bisimulation on the usual stripped probabilistic transition system (translated into a labelled transition system), which we call here "probability obliterated bisimulation"; and (iii) a "probability abstracted bisimulation", which, like bisimulation, preserves the structure of the distributions but instead, it ignores the probability values. In addition, we compare these bisimulation equivalences and provide a logic characterization for each of them.