2012/08/12 by Matias David Lee, Daniel Gebler, Pedro R. D’Argenio +1 · 17 citations
Computer Science · Mathematics · #Advanced Software Engineering Methodologies #Artificial intelligence #Computer science #Congruence (geometry) #Formal Methods in Verification #Mathematics #Nondeterministic algorithm #Operational semantics #Probabilistic logic #Programming language #Semantics (computer science) #Software Reliability and Analysis Research #Theoretical computer science #Transition system #cs.PL
paper · pdf · doi:10.4204/eptcs.89.9
published in Electronic Proceedings in Theoretical Computer Science 89, 115-130 (Open Publishing Association) · In Proceedings EXPRESS/SOS 2012, arXiv:1208.2440
openalex publication_date 2012/08/12 · arxiv created 2012/08/14 · arxiv updated 2012/08/15 · openalex created_date 2016/06/24 · openalex updated_date 2026/08/05
Probabilistic transition system specifications (PTSSs) in the ntmufnu/ntmuxnu format provide structural operational semantics for Segala-type systems that exhibit both probabilistic and nondeterministic behavior and guarantee that isimilarity is a congruence.Similar to the nondeterministic case of rule format tyft/tyxt, we show that the well-foundedness requirement is unnecessary in the probabilistic setting. To achieve this, we first define an extended version of the ntmufnu/ntmuxnu format in which quantitative premises and conclusions include nested convex combinations of distributions. This format also guarantees that bisimilarity is a congruence. Then, for a given (possibly non-well-founded) PTSS in the new format, we construct an equivalent well-founded transition system consisting of only rules of the simpler (well-founded) probabilistic ntree format. Furthermore, we develop a proof-theoretic notion for these PTSSs that coincides with the existing stratification-based meaning in case the PTSS is stratifiable. This continues the line of research lifting structural operational semantic results from the nondeterministic setting to systems with both probabilistic and nondeterministic behavior.