Tree rules in probabilistic transition system specifications with negative and quantitative premises

Abstract

Probabilistic transition system specifications (PTSSs) in the ntμ;fv/ntμxv format provide structural operational semantics for Segala-type systems that exhibit both probabilistic and nondeterministic behavior and guarantee that bisimilarity is a congruence. Similar to the nondeterministic case of the rule format tyft/tyxt, we show that the well-foundedness requirement is unnecessary in the probabilistic setting. To achieve this, we first define a generalized version of the ntμ;fv/ntμxv format in which quantitative premises and conclusions include nested convex combinations of distributions. Also this format 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 PTSS 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.