Search

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.

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.

An interactive system is a system that allows communication with the users. This communi- cation is modeled through input and output actions. Input actions are controllable by a user of the system, while output actions are controllable by the system. Standard semantics for sequen- tial system [1, 2] are not suitable in this context because they do not distinguish between the different kinds of actions. Applying a similar approach to the one used in [2] we define seman- tics for interactive systems. In this setting, a particular semantic is associated with a notion of observability. These notions of observability are used as parameters of a general definition of non-interference. We show that some previous versions of the non-interference property based on traces semantic, weak bisimulation and refinement, are actually instances of the observability- based non-interference property presented here. Moreover, this allows us to show some results in a general way and to provide a better understanding of the security properties.