English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Tools annual

Global: Zendy Free Plan

Global: Zendy Tools monthly

Global: Zendy Plus monthly

Probabilistic transition system specifications (PTSSs) in the ntmufnu/ntmuxnuformat provide structural operational semantics for Segala-type systems thatexhibit both probabilistic and nondeterministic behavior and guarantee thatisimilarity is a congruence.Similar to the nondeterministic case of rule formattyft/tyxt, we show that the well-foundedness requirement is unnecessary in theprobabilistic setting. To achieve this, we first define an extended version ofthe ntmufnu/ntmuxnu format in which quantitative premises and conclusionsinclude nested convex combinations of distributions. This format alsoguarantees that bisimilarity is a congruence. Then, for a given (possiblynon-well-founded) PTSS in the new format, we construct an equivalentwell-founded transition system consisting of only rules of the simpler(well-founded) probabilistic ntree format. Furthermore, we develop aproof-theoretic notion for these PTSSs that coincides with the existingstratification-based meaning in case the PTSS is stratifiable. This continuesthe line of research lifting structural operational semantic results from thenondeterministic setting to systems with both probabilistic andnondeterministic behavior.

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