Paolo Baldan
email: baldan@math.unipd.it

Alessandro Beggiato
email: alessandro.beggiato@imtlucca.it

Multilevel Transitive and Intransitive Non-Interference, Causally

We develop a theory of non-interference for multilevel security domains based on causality, with Petri nets as a reference model. We first focus on transitive non-interference, where the relation representing the admitted flow is transitive. Then we extend the approach to intransitive non-interference, where the transitivity assumption is dismissed, leading to a framework which is suited to model a controlled disclosure of information. Efficient verification algorithms based on the unfolding semantics of Petri nets stem out of the theory.

Introduction

Starting with [START_REF] Goguen | Security policies and security models[END_REF], the notion of non-interference has been widely used in the study of information flow security. In the simplest scenario, entities are classified according to two levels, a confidential level High and a public level Low . Information is allowed to flow from Low to High, but not vice-versa. When dealing with formalisms describing concurrent components that can interact and synchronize, like process calculi and Petri nets, a popular formulation of non-interference is Non-Deducibility on Composition (NDC). It states that a component S is free of interference whenever S running in isolation, seen from the low level, is behaviorally equivalent to S interacting with any parallel high level component [START_REF] Focardi | Classification of security properties (Part I: Information flow)[END_REF][START_REF] Ryan | Process algebra and non-interference[END_REF][START_REF] Mantel | Possibilistic definitions of security -an assembly kit[END_REF][START_REF] Busi | Structural non-interference in elementary and trace nets[END_REF][START_REF] Best | On the decidability of non interference over unbounded Petri nets[END_REF][START_REF] Baldan | A causal view on non-intereference[END_REF][START_REF] Mccullough | Noninterference and the composability of security properties[END_REF][START_REF] Wittbold | Information flow in nondeterministic systems[END_REF]. Intuitively, the behavior of the High part of the system is required not to cause any modification in the behavior of the Low part.

This informal reference to causality is made formal in [START_REF] Baldan | A causal view on non-intereference[END_REF] that, relying on some previous work [START_REF] Busi | Structural non-interference in elementary and trace nets[END_REF], provides a causal characterization of BNDC (Bisimulationbased NDC) on Petri nets, in terms of the unfolding semantics [START_REF] Nielsen | Petri nets, event structures and domains, part 1[END_REF]. The interest for a causal characterization is not only of theoretical nature. On the pragmatic side the use of a true concurrent semantics, like the unfolding, which represents interleaving only implicitly, is helpful to face the state explosion problem which affects the verification of concurrent systems.

The approach in [START_REF] Baldan | A causal view on non-intereference[END_REF] works in a two-level setting, possibly with downgrading [START_REF] Baldan | Intransitive non-interference by unfolding[END_REF], while since its infancy (see, e.g., [START_REF] Denning | A lattice model of secure information flow[END_REF]) information flow security has Supported by MIUR project CINA and the Padua University project ANCORE.

recognized the usefulness of dealing with multilevel security domains where a relation between levels, referred as a security policy, specifies the admitted flows. The transitive nature of information flow -if information flows from level A to level B and from B to C then it necessarily flows from A to C -naturally leads to work in domains where the security policy is a partial order, only allowing a flow of information from lower to higher levels (no read-up, no write-down). The order can be total, expressing a hierarchy of confidentiality degrees (e.g., top secret, secret, confidential and unclassified in a military setting). It can also be partial, typically when various confidentiality criteria are combined into a single domain. E.g., an administration could keep public and sensitive citizen data concerning taxes and civil status. Independent access rights to sensitive tax and civil status data naturally leads to a lattice of security levels.

As argued, e.g., in [START_REF] Rushby | Design and verification of secure systems[END_REF] it can also be natural to consider intransitive policies, in a way that a direct flow between two levels, say from A to B, can be forbidden, while a flow mediated through a third level, say D, is admitted. Intransitive policies are suited, for instance, for representing downgrading of confidential information. This allows for a controlled form of leakage, making such policies more realistic than pure non-interference policies that require the complete isolation of confidential levels. More generally, intransitive policies allow one to describe the (possibly cyclic) paths on which information is allowed to flow in a system.

In this paper the approach of [START_REF] Baldan | A causal view on non-intereference[END_REF], providing a causal characterization of the BNDC (Bisimulation-based NDC) property for (safe) Petri nets based on the unfolding semantics, is extended to deal with multilevel transitive policies. Generalizing [START_REF] Baldan | Intransitive non-interference by unfolding[END_REF] we also treat the intransitive case, namely we develop a multilevel theory for BINI [START_REF] Best | On the decidability of non interference over unbounded Petri nets[END_REF], an adaptation of BNDC to intransitive domains. The noninterference properties of interest are characterized in terms of the absence of suitable causal dependencies in the unfolding, witnessed by places where illegal interactions occur. This enables the definition of algorithms that checks the noninterference properties on a suitably defined complete prefix of the unfolding.

The unfolding-based algorithms are implemented in a tool MultiUBIC [START_REF] Beggiato | MultiUBIC[END_REF]. Compared to tools that exploit the reachability graph of the net, like ANICA (Automated Non-Interference Check Assistant) [START_REF]ANICA: Automated Non-Interference Check Assistant[END_REF] and PNSC (Petri Net Security Checker) [START_REF] Gorrieri | On intransitive non-interference in some models of concurrency[END_REF], thanks to the partial order representation of concurrency, MultiUBIC -as its predecessor UBIC -leads to a gain of efficiency for highly concurrent systems where the unfolding prefix can be exponentially smaller than the complete state space (see e.g. [START_REF] Esparza | Unfoldings -A Partial order Approach to Model Checking[END_REF]). The verification of multilevel policies can be also reduced to a number of problems on two-level security domains (enriched with a downgrading level in the intransitive case). MultiUBIC comes equipped with facilities for performing the reduction. The experiments suggest that, in general, a direct multilevel verification is more efficient when the number of levels increases, but situations are singled out where the reduction is convenient.

Synopsis.

In § 2 we define multilevel security domains and we review some Petri net notions. In § 3 we focus on transitive policies, providing a causal characterization of the BNDC property and a verification algorithm. In § 4 we extend the results to intransitive policies. In § 5 we describe the tool MultiUBIC. In § 6 we draw some conclusions.

Multilevel Security Domains and Petri Nets

In this section, after introducing multilevel security domains, we review some basic notions about Petri nets, with special attention to their unfolding semantics, later used to provide a causal characterization of the non-interference properties.

Multilevel Security Domains

Definition 1 (multilevel security domain). A multilevel security domain (MSD) (L , ) is a finite set of security levels L , endowed with a reflexive relation ⊆ L × L called a security policy. When is transitive we call (L , ) a transitive multilevel security domain.

The security policy specifies the legal information flows. It is reflexive because entities at the same level should be able to freely exchange information. Without loss of generality, a transitive MSD will be assumed to be a partial order. In fact, if is a proper preorder (i.e, not antisymmetric), we can equivalently consider the partial order obtained as its quotient under the equivalence ∩ -1 . Since equivalent levels can communicate in either direction, they can be safely collapsed. Examples of MSD will be discussed later, after introducing also net systems. Given S ⊆ L we write S for its complement L \ S.

Definition 2 (upper sets and targets). Let (L , ) be a MSD. An upper set is a subset U ⊆ L such that if L ∈ U and L L then L ∈ U . Given a security level L ∈ L its set of targets is ↑ L = {L ∈ L | L L }, while the strict targets are ↑ ↑ L = ↑ L \ {L}.

An entity (user, program, variable, instruction) with associated security level L has permission to influence, or to write, or to pass information only to entities with security level in ↑ L. Any other information flow is a violation of the policy. Targets are defined on sets U ⊆ L by letting ↑ U = L∈U ↑ L and ↑ ↑ U = ↑ U \ U .

Petri Nets and Net Systems

A (Petri) net is a tuple N = (P, T, F ) where P , T are disjoint sets of places and transitions, respectively, and F : (P × T ) ∪ (T × P ) → {0, 1} is the flow function. Graphically places and transitions are drawn as circles and rectangles, respectively, while the flow function is rendered by means of directed arcs connecting places and transitions. For x ∈ P ∪ T we define its pre-set • x = {y ∈ P ∪T : F (y, x) = 1} and its post-set x • = {y ∈ P ∪T : In order to formalize information flow properties in the setting of Petri nets, an MSD L is fixed and, as in [START_REF] Busi | Structural non-interference in elementary and trace nets[END_REF][START_REF] Best | On the decidability of non interference over unbounded Petri nets[END_REF], transitions are associated with security levels.

F (x, y) = 1}. A marking of N is a function m : P → N. A transition t ∈ T is enabled at a marking m, denoted m[t , if m(p) ≥ F (p,
Definition 3 (net system). A net system is a tuple N = (P, T, F, λ) where (P, T, F ) is a Petri net and λ : T → L is a function that assigns a security level to each transition. For S ⊆ L we define T S = {t ∈ T | λ(t) ∈ S}, the set of transitions whose security level is in S. An S-system is a net system such that T = T S , i.e. a system only capable of performing actions whose security level belongs to S. Consider the net system and security domain in Fig. 1. It represents a device consisting of two independent sensors getting new measures for a processor, that, in turn, can poll them to acquire more recent data. Each sensor has a cyclic behavior. For instance, the left sensor is capable to get a measure (get A ). Such measure can be exposed at its interface (show A ) and then removed after a while (rem A ), restarting the cycle. Alternatively, the measure can be sent to a shared cache (send A ) which is thus updated (upd i C ). Note that when a place is both in the pre-and post-set of a transition (like cache for upd i C ) instead of an ingoing and an outgoing arrow, we draw a single double arrow. The presence or absence of a datum at the interface is represented by a token in place a or ¬a, respectively. The access to the cache by the two sensors via transitions upd i C is mutually exclusive (the cache stores a single measure), as guaranteed by the use of place Free, consumed by transitions send X and produced by upd i C . The processor cyclically gets some value for the measure. If a value is exposed at the interfaces of the sensors (places a or b marked) then one of such values is taken (poll i P ), otherwise (places ¬a and ¬b marked) the cached value is read (read P ).

The security level of transitions is given by their subscript (namely, λ(t L ) → L). Transitions modeling the left and right sensors have security level A and B. The processor and the cache have security levels P and C, respectively. The intuition is that the two sensors should not interfere with each other, and they can send information to the processor directly or through the cache. The processor and the cache should not affect the behavior of the sensors.

In order to formalize the non-interference notions we will need some operations on net systems, specifically (parallel) composition and restriction [START_REF] Best | On the decidability of non interference over unbounded Petri nets[END_REF].

Definition 4 (composition). Let N and N be two net systems such that P ∩ P = ∅ and for all t ∈ T ∩ T it holds λt = λ t. The composition of N and N is the net system N|N = (

P ∪ P , T ∪ T , λ ∪ λ , F ∪ F ). The composition of N = (N, m 0 ) and N = (N , m 0 ) is the marked net system N|N = (N|N , m 0 ∪ m 0 ).
Definition 5 (restriction). Given a net system N and a subset T 1 ⊆ T , the restriction of N by T 1 is the net system N \ T 1 = (P, T -T 1 , λ , F ) where λ and F are the obvious restrictions of λ and F . For a marked net system N, the restriction

N \ T 1 is (N \ T 1 , m 0 ).
Intuitively N |N is the parallel composition of N and N , synchronized on the common transitions. Restriction simply removes the restricted transitions.

Unfolding semantics and related notions

The behavior of a Petri net can be represented by its unfolding U(N) [START_REF] Nielsen | Petri nets, event structures and domains, part 1[END_REF], an acyclic net constructed inductively starting from the initial marking of N and then adding, at each step, an occurrence of each enabled transition of N. In what follows we indicate by π 1 the projection over the first component of pairs. Definition 6 (unfolding). Let N = ((P, T, F ), m 0 ) be a marked net. Define the net U (0) = (P (0) , T (0) , F (0) ) as

T (0) = ∅, P (0) = {(p, ⊥) : p ∈ m 0 } and F (0) = ∅,
where ⊥ is an element not belonging to P , T or F . The unfolding is the least net U(N) = (P (ω) , T (ω) , F (ω) ) containing U (0) and such that

-if t ∈ T and X ⊆ P (ω) with X reachable, and π 1 (X) = • t, then (t, X) ∈ T (ω) ; -for any e = (t, X) ∈ T (ω) , the set Z = {(p, e) : p ∈ π 1 (e) • } ⊆ P (ω) ; moreover • e = X and e • = Z.
Places and transitions in the unfolding represent tokens and firing of transitions, respectively, of the original net. Each place in the unfolding is a tuple recording the place in the original net and the "history" of the token. For historical reasons transitions and places in the unfolding are also called events and

get 1 A a1 send 1 A show 1 A l a upd 1 C rem 1 A a0 a0 ¬a get 2 A get 3 A a1 a1 send 2 A show 2 A send 3 A show 3 A • • • • • • • • • • • • U(N) L A B C P Fig. 2.
A net system and the initial part of its unfolding.

conditions, respectively. The projection π 1 over the first component maps places and transitions of the unfolding to the corresponding items of the original net N. The initial marking is implicitly identified as the set of minimal places.

As an example, consider the net system in Fig. 2 (top left), a slightly simplified version of the subnet of Fig. 1 modeling one of the sensors. A fragment of its unfolding is provided in Fig. 2(right). Conditions and events are labeled with the name of the corresponding place and transition in the original net. Different occurrences of a transition are distinguished using a numeric superscript. The conditions labeled by a 0 and ¬a on the top, according to Definition 6, are (a 0 , ⊥) and (¬a, ⊥), respectively. Event get 1 A is (get A , {(a 0 , ⊥)}) and the condition a 1 in its post-set is (a 1 , get 1 A ). Similarly, event

show 1 A is (show A , {(a 1 , get 1 A ), (¬a, ⊥)}).
Definition 7 (causality, conflict). Causality < is the least transitive binary relation on P (ω) ∪ T (ω) such that x < y if x ∈ • y. By ≤ we denote the reflexive closure of <. Conflict is the least symmetric binary relation on P ∪ T such that if t, t ∈ T , t = t and • t ∩ • t = ∅ then t t and if x < x and x y then x y.

In the running example,

get 1 A ≤ show 1 A and get 1 A ≤ send 1 A , while send 1 A show 1 A and show 1 A rem 1 A .
The runs of N are represented by the configurations of U(N), i.e., subsets of T (ω) that are causally closed and conflict-free. For a transition t ∈ T (ω) we define its causes [t] = {t ∈ T (ω) : t ≤ t} and its strict causes

[t) = [t] -{t}. Definition 8 (configuration). A configuration of U(N) is a finite subset C ⊆ T (ω) such that (C × C) ∩ = ∅ and [e] ⊆ C for all e ∈ C. The set of all configurations of U(N) is denoted by C(U(N)).
The transitions of a configuration C can be fired in any order compatible with causality, producing a marking called the frontier

C • = (P (0) ∪ t∈C t • ) - ( t∈C • t); in turn, this corresponds to a marking of N given by M(C) = π 1 (C • ).
For instance, in Fig. 2, the set

{get 1 A , show 1 A , rem 1 A } is a configuration, while {show 1 A , rem 1 A } and {get 1 A , show 1 A , rem 1 A , show 2 A } are not since the first is not causally closed (get 1 A < show 1 A )
and the second has a conflict ( show 1 A #show 2 A ). The unfolding has been shown to be marking complete in the sense that m ∈ [m 0 iff there exists C ∈ C(U(N)) such that M(C) = m (see [START_REF] Nielsen | Petri nets, event structures and domains, part 1[END_REF][START_REF] Mcmillan | A technique of state space search based on unfolding[END_REF]).

Transitive Multilevel Non-Interference

In this section we focus on transitive multilevel security domains and we define the reference security property in the paper as an instance of (Bisimulationbased) Non-Deducibility on Composition (BNDC) [START_REF] Busi | Structural non-interference in elementary and trace nets[END_REF].

Bisimilarity-based Non-Deducibility on Composition

Let (L , ) be a transitive MSD, fixed throughout the section. The definition of BNDC can be obtained by adapting that in [START_REF] Busi | Structural non-interference in elementary and trace nets[END_REF][START_REF] Baldan | A causal view on non-intereference[END_REF] to the multilevel setting. First, in order to formalize the idea of variations of the behavior which are visible at a given security level we introduce a view function (or purge function [START_REF] Rushby | Noninterference, transitivity, and channel-control security policies[END_REF]).

Definition 9 (view function). Given a subset of the domain S ⊆ L and a net system N , the view function S(•) : T * → T * S , is defined inductively by S( ) = , S(tσ ) = tS(σ ) if λ(t) ∈ S and S(tσ ) = S(σ ) otherwise.

The view function filters out transitions whose level is not in S. It is used to define a bisimulation capturing the observation power of a user able to observe only events with security level in a given set.

Definition 10 (S-view bisimulation). Let N, N be marked systems and In a two-level setting, i.e., in the domain {Low High}, a system is noninterferent when the low level behavior is not influenced by high level interactions. Formally, a net system N is BNDC when N ≈ Low (N|N ) \ (T High -T ) for any {High}-net N , i.e., the "low level" view of the behavior of N remains unchanged when the net interacts with any high level net system [START_REF] Best | On the decidability of non interference over unbounded Petri nets[END_REF].

S ⊆ L . An S-view simulation of N by N is a relation R ⊆ [m 0 × [m 0 such that: -(m 0 , m 0 ) ∈ R ; -if (m, m ) ∈ R
The generalization to the multilevel setting considers any partition of the security domain in an upper set U ⊆ L and its complement U , and requires that U does not influence the view of U .

Definition 11 (BNDC). Let N be a marked net system. For an upper set

U ⊆ L , we say that N is U -BNDC if N ≈ U (N|N ) \ (T U -T ) for all marked U -systems N . The system is BNDC if it is U -BNDC for any upper set U ⊆ L .
The definition can be understood as follows. Given an upper set U , if the system is not U -BNDC then there is a flow from some level L ∈ U to L ∈ U . This is a security violation since L L otherwise L would be in U . Vice versa, if there is a security violation, it will consist of a flow from some security level L to a level L which cannot be influenced by L, namely L L . This is captured by the definition above when considering the upper set U = ↑ L, since L ∈ U .

Note that the BNDC property for a multilevel domain reduces to the validity of BNDC in a number of two-level domains, one for each upper set, with U and its complement U playing the role of the high and low part of the system, respectively. Actually, as suggested by the considerations above, any security violation can be detected by analyzing upper sets of the kind U = ↑ L for L ∈ L . Proposition 1. A net system N is BNDC iff N is ↑ L-BNDC for every L ∈ L .

BNDC through Causal and Conflict Places

The characterization of BNDC based on causal and conflict places for the twolevel case in [START_REF] Busi | Structural non-interference in elementary and trace nets[END_REF][START_REF] Baldan | A causal view on non-intereference[END_REF], can be generalized to multilevel security domains. Roughly, a net system is BNDC when transitions with different security levels are never in conflict and there is no causal flow which is not allowed by the security policy.

Hereafter we focus on safe nets, which admit simpler and more effective notions of causal and conflict place (a weakening of those for general nets, whence the qualification "weak").

Notation. Given a net system N and a transition t ∈ T , we denote by t -= • t\t • and, dually, t + = t • \ • t the sets of places where the firing of t decrease and increase, respectively, the number of tokens.

Definition 12 (weak causal place).

A weak causal place in a net system N is any place p ∈ • l ∩ h + , for some l, h ∈ T such that λh λl, and some marking m ∈ [m 0 such that m[hτ l , with τ ∈ T * .

Intuitively, the firing sequence hτ l and the place p ∈ • l ∩ h + witness a firing of l that depends on a token produced by the firing of h, representing an illegal flow from level λh to level λl. Conflict places are defined along the same lines.

Definition 13 (weak conflict place). A weak conflict place in a net system N is any place p ∈ • l ∩ h -, for some l, h ∈ T such that λh λl, and some reachable marking m ∈ [m 0 such that m[h and m[τ l , with τ ∈ T * .

The presence of weak causal or conflict places witnesses the failure of BNDC.

Theorem 1 (BNDC through weak causal/conflict places). A safe net system N is BNDC iff N contains no weak causal nor weak conflict place.

Consider the running example in Fig. 1. The system is not BNDC. In fact place a 0 is causal, as witnessed by the firing sequence get

A send A upd1 C get A , with a 0 ∈ upd1 C + ∩ • get A and λ(upd1 C ) = C A = λ(get A ).
Analogously, place b 0 is causal and place Free, is both causal and conflict. The interference seems unavoidable given that the cache is accessed in mutual exclusion and a value sent to the cache must determine an update. In § 4 we will show how these occurrences of interference can be amended with the use of intransitive policies.

Non-Interference in the Unfolding

Occurrences of causal and conflict places in the unfolding of safe net systems can be given a structural characterization, which, thanks to Theorem 1, leads to a unfolding-based characterization of the BNDC property.

Notation. For a condition b and an event t in the unfolding U(N) we set t + = {b ∈ P (ω) : π 1 (b) ∈ π 1 (t) + } and t -= {b ∈ P (ω) : π 1 (b) ∈ π 1 (t) -}.

Proposition 2 (BNDC in the unfolding). A safe net system N is not BNDC iff there are events h , l such that λh λl and a condition b in U(N) such that either (i) b ∈

• l ∩ h + or (ii) b ∈ • l ∩ h -and [h ) ∪ [l ] ∈ C(U(N)).
Note that condition (ii) is harder to check than (i), as it involves an exploration of the history of the interacting transitions. In the verification procedure it is convenient to look only for causal interference. This can be done, thanks to the fact that for safe nets all occurrences of interference can be reduced to causal ones. We omit the details which largely overlap with those for the twolevel case [START_REF] Baldan | A causal view on non-intereference[END_REF]. We only remark that the causal reduction causes an expansion of the size of the net that is at most quadratic in the number of transitions.

Proposition 3 (BNDC in the causal reduct). Let N be a safe net system. It is possible to build a safe net γ(N), called causal reduct of N, such that N is BNDC iff γ(N) has no weak causal places.

Unfolding-based Algorithm for BNDC

The unfolding of a net can be infinite (when it includes a cycle). Starting with [START_REF] Mcmillan | A technique of state space search based on unfolding[END_REF] techniques have been developed for efficiently constructing finite prefixes of the unfolding which are complete with respect to properties of interest [START_REF] Khomenko | Canonical prefixes of Petri net unfoldings[END_REF].

Here, as a first step, we identify a completeness criterion ensuring that an unfolding prefix includes at least a representative for a causal interference, when a net system is not BNDC. This is used for developing an algorithm for checking BNDC for a safe net. Interestingly, while Definition 11 reduces multilevel noninterference to a number of checks in a two-level setting, here the verification is performed by constructing a single unfolding prefix.

As discussed in the two-level case [START_REF] Baldan | A causal view on non-intereference[END_REF], a prefix complete for reachability could omit information relevant for interference. In order to capture all occurrences of interference, in the two-level case, markings were enriched by recording which tokens were generated by high transitions. Here we record the level of transitions generating the tokens, adapting the notion of completeness accordingly.

Definition 14 (c-marking, c-complete prefix). Let N be a safe net system and let C ∈ C(U(N)). The confidentiality marking (c-marking

) of C is M * (C) = M(C), Λ C , where Λ C : M(C) → L is a partial function defined as follows. For any b ∈ C • , if • b = {t } then Λ C (π 1 (b)) = λt , otherwise, if • b = ∅ then Λ C (π 1 (b)) is undefined. A prefix U of U(N) is complete for c-marking reachability, or simply c-complete, when for any configuration C ∈ C(U(N)) there exists C ∈ C(U ) such that M * (C) = M * (C ).
In words, Λ C maps each marked place to the level of the transition that generated the corresponding token. It is undefined on tokens of the initial marking.

When checking BNDC on a complete prefix U , we need to consider also events at the "border" of U , i.e., events that are enabled by configurations of U and which could be could be added by a further unfolding step. In the procedure for generating the prefix these transitions will be added and marked as cut-offs. The prefix obtained from U by adding such transitions is denoted U .

We can now show that a c-complete prefix U of U(N), includes sufficient information for deciding whether or not N contains a weak causal place.

Theorem 2 (weak causal places in c-complete prefixes). Let N be a safe net system and let U be a c-complete prefix of U(N). Then p is a weak causal place in N iff there exists in U a condition b and events h , l such that π 1 (b) = p, b ∈ • l ∩ h + and λh λl .

The above result and Proposition 3 implies that, given a safe net system, one can check for BNDC on a c-complete prefix of the unfolding of its causal reduct.

Corollary 1 (BNDC on c-complete prefixes).

Let N be a safe net system and let U be a c-complete prefix of U(γ(N)). Then N is not BNDC iff there exist events h , l ∈ U such that λh λl and • l ∩ h + = ∅.

Corollary 1 leads to an algorithm for checking BNDC on safe net systems. Given N first it computes its causal reduct γ(N). Then it builds a c-complete prefix of the unfolding U(γ(N)) by adding, at each step, a transition occurrence and checking if its direct causalities satisfy the conditions in Corollary 1.

Corollary 2 (correctness of the algorithm for BNDC). Let N be a safe net system. The algorithm outlined above always terminates and answers 'yes' iff N is BNDC.

Intransitive Multilevel Non-Interference

In this section we focus on intransitive policies. The idea is that some information flows between levels that cannot communicate directly become allowed if they are mediated by a chain of trusted intermediaries.

Bisimilarity-based Intransitive Non-Interference

Inspired by the idea of separability in [START_REF] Rushby | Noninterference, transitivity, and channel-control security policies[END_REF], in order to check whether there are illegal flows from a set of levels U , we artificially isolate that set by removing from the system all of its legal targets in ↑ ↑ U . If, afterwards, the levels in U can still influence other levels in the rest of the system, the influence is certainly illegal. In fact, it cannot be mediated by a chain of legal intermediaries since any such chain has been certainly broken by the construction. This leads to a multilevel generalization of BINI (Bisimulation-based Intransitive Non-Interference) [START_REF] Best | On the decidability of non interference over unbounded Petri nets[END_REF].

Definition 15 (BINI). Given U ⊆ L , a net system N is U -BINI if for all reachable markings m ∈ [m 0 the system (N \T ↑ ↑ U , m) is U -BNDC in the domain L = (L \ ↑ ↑ U, * ). The system N is BINI if it is U -BINI for all U ⊆ L .
As explained above, for each set of levels U we consider the net N \ T ↑ ↑ U , obtained by pruning the transitions with level in ↑ ↑ U , to which a flow from U is admitted. The presence of an illegal flow from U is thus reduced to the presence of any flow from U in the pruned subsystem. In turn, the presence of a flow from U is formalized by resorting to the notion of BNDC previously introduced (Definition 11). It is easy to see that the definition is well-given, i.e., U is an upper set in L = (L \ ↑ ↑ U, * ). Note that an illegal flow from U could occur at any reachable marking m of the original system, but clearly the pruning operation can make m unreachable. This is the reason why the pruned net N \ T ↑ ↑ U is checked with any marking reachable in the original net system N.

Consider the running example in Fig. 1, which is not BNDC due to an interference between the cache and the sensors, and between the sensors themselves. In both cases the interference stem out from the mutually exclusive access to the cache. If this mode of access is an hardware constraint, it might be the case that the designer intends to ignore such occurrences of interference, deeming them inevitable and not problematic. This can be modeled by adding a number of "downgrading" levels to the domain, and modifying the net adding downgrading transitions. In Fig. 3 we show how this can be done in order to make the old net BINI (we only show a part of the system: the processor is unchanged and the second sensor is symmetric to the first one). Note, e.g., that C

A but transition upd1 C can obviously influence get A , since we can have a causal chain upd1 C d3 D get A . However, this is not a violation of BINI because the interference occurs through d3 D , which is a legitimate intermediary (C D A). More formally, if we take U = {C}, according to Definition 15, we have to consider the net N \ T ↑ ↑ U , where legal intermediaries for C, namely transitions with level in ↑ ↑ {C} = {D, P } are pruned. In particular, the pruned net does not include transition d3 D and thus the interference of upd1 C on get A is correctly hidden. Similarly, transitions d1 D and d2 D mediate the conflict between send A and send B .

Although not immediate, as a sanity check, it can be proved that BINI and BNDC coincide on transitive domains.

Proposition 4 (BINI is BNDC on transitive domains). In a transitive MSD L , a net system N is BINI if and only if N is BNDC.

Additionally, BINI can be characterized by replacing the quantification over all subsets U ⊆ L of Definition 15 with a quantification over single levels.

Proposition 5 (multilevel BINI on single levels). A net system N is BINI iff N is {L}-BINI for each L ∈ L .

BINI through Causal and Conflict Places

A characterization of BINI amenable of effective verification in the unfolding of safe nets, relies on intransitive variants of weak causal and conflict places.

Definition 16 (intransitive weak causal/conflict place). Let N be a safe net system. An intransitive weak causal place is p ∈ The difference with respect to the notions of weak causal and conflict place in § 3.2 for transitive policies is that here τ is required not to contain any transition to which information can could legally flow from h. Intuitively, the reason is that, otherwise, the flow from h to l would be mediated by such transition, possibly amending the violation represented by p. As an example, in Fig. 3 place Free is not an intransitive conflict place, despite the fact that Free ∈ • send A ∩ send B and B

• l ∩ h + ,
A. The reason is that, in any firing sequence starting from place Free marked, an occurrence of send A is necessarily preceded by d1 D .

Theorem 3 (BINI through intransitive weak places). A safe net system N is BINI iff it contains no intransitive weak causal or conflict place.

BINI in the Unfolding

Occurrences of intransitive weak causal places can be characterized in the unfolding of safe nets.

Theorem 4 (intransitive weak causal places in the unfolding). Let N be a safe net system. A place p in N is an intransitive weak causal place iff there exists a condition b in U(N) such that π 1 (b) = p and there are events h , l such that (i) b ∈ • l ∩ h + and (ii) ∀t : h < t ≤ l . λh λt .

The above, together with the possibility of resorting, as in the intransitive case, to the causal reduct, leads to the following characterization of BINI.

Proposition 6 (BINI in the causal reduct). Let N be a net system. Then N is BINI iff the causal reduct γ(N) contains no intransitive causal places.

For building a complete prefix, we still need to enrich the marking associated with a configuration C with a function Λ C , mapping each token to the security level of the generating transition. However, due to the intransitivity of the policy, this is no longer sufficient to detect a violation. In fact, assume that an event l of level L consumes a token of level H such that H L. Apparently this is a violation of the policy since the presence of a token of level H reveals that an event, say h, of the same level has been executed before, and this fact is visible at level L. However, this might not be a problem, since it could be that a token of a level D such that H D L, is also in the pre-set of l, produced by an event d such that h < d < l. In this case, the flow of information from L to H is legitimately mediated by D. Roughly, we can think that the token of level D absorbs the token of level H to its level. We then enrich the markings with an absorbing relation δ over the conditions in the frontier of a configuration.

Definition 17 (i-marking, i-complete prefix). Let N be a safe net system and let C ∈ C(U(N)). The intransitive confidentiality marking (i-marking

) of C is M * i (C) = M(C), Λ C , δ C , where Λ C : P → L is as in Definition 14 and δ C : π 1 (C • ) × π 1 (C • ) is the relation: {(π 1 (p), π 1 (q)) | ∃t, t ∈ C . q ∈ t • ∧ λ(t ) λt ∧ t < t ≤ p} A prefix U of U(N) is complete for i-marking reachability ( i-complete), when for any configuration C ∈ C(U(N)) there is C ∈ C(U ) such that M * i (C) = M * i (C ).
Intuitively, whenever δ(p, q) the token in p absorbs the token in q to its level, if they are used in the same pre-set.

It can be proved that an i-complete prefix U of U(N) includes sufficient information for deciding whether N contains a weak intransitive causal place. This fact, with Theorem 4 and Proposition 6, implies that one can check BINI for a net system on an i-complete prefix of the unfolding of its causal reduct. Corollary 3 (BINI on i-complete prefixes). Let N be a safe net system and let U be a i-complete prefix of U(γ(N)). Then N is not BINI iff there exists in U a condition b and events h , l such that b ∈ • l ∩ h + , λh λl , and furthermore ∀b ∈

• l . ¬(b δ [l ) b).
In words, an interference is witnessed by an event l that uses a token b of a non accessible level such that b is not absorbed. As in the transitive case, this result is used for designing an algorithm that checks BINI on safe net systems.

The tool MultiUBIC

The unfolding-based algorithms outlined in the previous sections are implemented in MultiUBIC [START_REF] Beggiato | MultiUBIC[END_REF]. It extends a previous tool UBIC, which was limited to two level security domains (possibly with downgrading). MultiUBIC inputs a security policy (transitive or intransitive) and a safe net system, and it checks whether BNDC (transitive policies) or BINI (intransitive policies) is satisfied.

Compared to PNSC [START_REF] Frau | Petri net security checker: Structural noninterference at work[END_REF] and ANICA [START_REF] Accorsi | Automatic information flow analysis of business process models[END_REF], "interleaving competitors" based on the work [START_REF] Busi | Structural non-interference in elementary and trace nets[END_REF], MultiUBIC inherits the good performance of its ancestor UBIC: the use of a partial order semantics leads to a gain of efficiency especially for highly concurrent systems, where the state explosion problem is more serious.

The verification of multi-level security policies can be reduced to a number of checks in a two-level setting (possibly with downgrading, in the intransitive case). MultiUBIC comes equipped with facilities for performing such reduction. The definition of BNDC suggests that such reduction can be expensive, since the two-levels problems arise from partitions of the security domain whose number can be exponential in the number of levels. For net systems it can be actually shown that we can limit to a linear number of two-level checks, one for each level (see Proposition 1 for the transitive case and Proposition 5 for the intransitive case). Still, some preliminary experiments reveal that solving directly the original multi-level problem, typically provides a linear gain of efficiency at the price of an increase of memory usage. The performances of MultiUBIC can degrade for net systems where a relevant number of places have input transitions of different levels, a fact that potentially causes an exponential blow of the number of enriched markings. A precise characterization of this pathological situations is under investigation. Due to space limitations, a presentation of the experimental results and a more extensive discussion are deferred to the full version.

Conclusions

We studied non-interference in a multilevel setting, for transitive and intransitive security domains, focusing on Petri nets. Generalizing [START_REF] Baldan | A causal view on non-intereference[END_REF][START_REF] Baldan | Intransitive non-interference by unfolding[END_REF], we showed that Bisimilarity-based Non-Deducibility on Composition (BNDC) and its intransitive extension BINI [START_REF] Best | On the decidability of non interference over unbounded Petri nets[END_REF], admit a causal characterizations in the unfolding of safe net systems. This led to verification algorithms for BNDC and BINI on safe net systems with multilevel policies, implemented in the tool MultiUBIC.

Causal semantics have been used in [START_REF] Haar | Types of asynchronous diagnosability and the reveals-relation in occurrence nets[END_REF] for deducing the occurrence of nonobservable transitions in the diagnosis of discrete event systems. There is a clear conceptual relation relation between diagnosability properties and noninterference, despite the fact that the former are trace-based while our noninterference is bisimulation-based. The work on intransitive non-interference in [START_REF] Hadj-Alouane | On the verification of intransitive noninterference in multilevel security[END_REF], that relies on automata models and language theory could be helpful for establishing a formal relation.

In the setting of Petri nets other classes of information flow properties have been studied, like opacity properties [START_REF] Bryans | Modelling dynamic opacity using Petri nets with silent actions[END_REF] (which include non-interference) and selective non-interference [START_REF] Best | Deciding selective declassification of Petri nets[END_REF]. Exploring the use of causal semantics in this general setting appears as an interesting and challenging venue of future research.

A huge literature exists on non-interference for various formalisms, including process calculi and imperative languages (see, e.g., [START_REF] Focardi | Classification of security properties (Part I: Information flow)[END_REF][START_REF] Mantel | Controlled declassification based on intransitive noninterference[END_REF] for surveys). Fruitful connections could emerge investigating a causal characterizations of noninterference in these settings, possibly through encodings into Petri nets.

We also plan to consider formalizations of non-interference obtained from the classical ones, by replacing interleaving observational semantics with trueconcurrent ones [START_REF] Van Glabbeek | Refinement of actions and equivalence notions for concurrent systems[END_REF]. The higher distinguishing power of such semantics could allow to identify new forms of interference which cannot be captured in an interleaving setting. Interesting reflections in this directions are reported in [START_REF] Fröschle | Causality, behavioural equivalences, and the security of cyberphysical systems[END_REF].

  and m[σ then there exists σ such that S(σ) = S(σ ), m [σ and ( m[σ , m [σ ) ∈ R. An S-view bisimulation between N and N is a relation R ⊆ [m 0 ×[m 0 such that R and R -1 are S-view simulations. If there exists an S-view bisimulation between N and N , we say that they are S-view bisimilar and write N ≈ S N .

Fig. 3 .

 3 Fig.3. A fix for the sensor net that makes it BINI. Only part of the system is shown, and as usual λ(xL) = L. The downgrading transitions are highlighted in green.

.

  all places p ∈ P . The enabling and firing relations are extended to σ ∈ T * (finite sequences of elements of T ) by defining m[ε m (where ε is the empty sequence) and m[σ m [t m imply m[σt m . Markings are represented as black dots, called tokens, inside places. A marked net is a pair N = (N, m 0 ) where N is a net and m 0 is a marking of N . A marking m is reachable if there exists σ ∈ T * such that m 0 [σ m . The set of reachable markings of N is denoted by [m 0 . When m[t m , the marking m , uniquely determined by m and t, is denoted by m[t . Analogously, for σ ∈ T * , if m[σ we can define the marking m[σ . A net N is safe if for every p ∈ P and every m ∈ [m 0 we have m(p) ≤ 1.

	A	L		processP
	C	P	R		W
	B	poll1P		readP	poll2P
	a	¬a				¬b	b
	remA	showA	upd1C	cache	upd2C	showB	remB
	a0	lA		lB		b0
	getA		sendA		sendB		getB
		a1		F ree		b1
	Fig. 1. A non-BNDC net system under the security domain L (top left).
				t) for all p ∈ P . If m[t then t can be fired leading
	to a new marking m , written m[t m , defined by m (p) = m(p)+F (t, p)-F (p, t)

for

  for l, h ∈ T such that λh λl, and there is a reachable m ∈ [m 0 such that m[hτ l , with τ ∈ T * ↑ ↑ λh .An intransitive weak conflict place is p ∈ • l ∩ h -, for l, h ∈ t such that λh λl, and there is a reachable m ∈ [m 0 such that m[h and m[τ l , with τ ∈ t *

	↑ ↑ λh


Herbert Wiklicky
email: herbert@doc.ic.ac.uk

On Dynamical Probabilities, or: How to learn to shoot straight

In order to support, for example, a quantitative analysis of various algorithms, protocols etc. probabilistic features have been introduced into a number of programming languages and calculi. It is by now quite standard to define the formal semantics of (various) probabilistic languages, for example, in terms of Discrete Time Markov Chains (DTMCs). In most cases however the probabilities involved are represented by constants, i.e. one deals with static probabilities. In this paper we investigate a semantical framework which allows for changing, i.e. dynamic probabilities which is still based on time-homogenous DTMCs, i.e. the transition matrix representing the semantics of a program does not change over time.

Introduction

Over the last 20 years or so probabilistic programming languages, model checking, programming, semantics etc. have become more and more popular. It appears now to be rather straight forward to add probabilities to any language, formalism, calculus, etc. one might be interested in. Most "probabilistic" programming languages, etc. however use constant probabilities [START_REF] Kozen | Semantics of probabilistic programs[END_REF][START_REF] Gretz | Operational versus weakest pre-expectation semantics for the probabilistic guarded command language[END_REF] etc., as we also did in our own work [START_REF] Di Pierro | A systematic approach to probabilistic pointer analysis[END_REF][START_REF] Di Pierro | Semantics of probabilistic programs: A weak limit approach[END_REF], especially when anything beyond a simple operational semantics is considered.

One of the motivations for introducing probabilities, as a form of quantified non-determinism, into a programming language is to allow for the formulation and analysis of so-called "randomised algorithms" [START_REF] Motwani | Randomized Algorithms[END_REF], i.e. algorithms where chance is exploited in order to obtain a certain result, may it be probabilistic primality tests, Monte Carlo integration, etc.

However, there is a large class of randomised algorithms in the area of stochastic programming which have dynamic probabilities at their core, such a stimulated annealing, the Metropolis algorithm, Boltzmann machines, etc. [START_REF] Aarts | Simulated Annealing and Boltzmann Machines[END_REF][START_REF] Schneider | Stochastic Optimization[END_REF]. All of these try to find global optimal solutions and in order to avoid getting trapped into a local minima (as might, for example, be the effect of a steepest gradient method) there are random perturbations. The effect of these perturbations is decreasing over time, i.e. during optimisation the chances of a perturbation changes slowly to become zero. Without going into the details of such "cooling" schemes or schedules we are in this paper interested in how to formalise dynamically changing probabilities in an appropriate semantical model. Probabilistic features, e.g. choices, introduce also a subtle, nevertheless extremely important form of coordination. Probabilities have to be normalised, not as a formal requirement but quasi because of the fundamental laws of nature: Something must happen, so the probabilities of all possibilities at any moment must add up to one. Thus, whatever model we employ in order to describe probabilistic choices, assignments, etc. the different options or possibilities are "communicating" in some form via their probabilities: if one option becomes more likely, another one must give up its chances to be executed/realised.

A Probabilistic Language

In the following we will denote by Var = {x 1 , . . . , x v } the set of all variables of a program P and by Value(x) the range of possible values of a variable x.

Technical restriction: In this paper we assume that Value(x) is finite for all x ∈ Var. We will allow below for variables as probabilities which thus also will have to come from a finite set of (possible) values. From a computational point of view probabilities should in any case perhaps be modeled as rational numbers in [0, 1]. Using real numbers can, as always, create a number of fundamental problems related to computability etc., e.g. [START_REF] Stannett | X-machines and the halting problem: Building a super-turing machine[END_REF].

To simplify the presentation we will go even a step further and only consider positive integers in Z + as "weights" 1 : Given several options with "weights" w i these correspond to probabilities p i = w i / j w j . As we have to (re)normalise probabilities in any case (even for static probabilities as constants, unless we can trust the programmer that all probabilities in a choice or a probability distribution always add up to one) this does not imply any restriction. It only means that in effect we consider proportions or ratios rather than rational values.

Conceptual restriction:

We do not allow for any kind of pure "non-determinism" as part of the actual execution of the program. The reasons for this are: (i) From a conceptual point of view it seems to be a contradiction to the notions like that of a Turing machine as an unambiguous procedure ("Entscheidungsproblem") to allow for (e.g. angelic) "non-determinism"; (ii) we also do not believe that any physical implementation of a purely "non-deterministic" choice exists (e.g. one could use quantum devices to realise probabilistic but never "non-deterministic" choices); and (iii) there are several mathematical (pseudo-)problems which disappear when one eliminates " non-determinism" during the execution of a program (e.g. related to boundedness, etc. [START_REF] Di Pierro | Semantics of probabilistic programs: A weak limit approach[END_REF]).

However, our semantical model still accommodates "non-determinism" in several aspects such as "non-determinism" as "under-specification" and "openness". Concretely, the semantical model provides for our language (pure) "nondeterminism" in two ways: (i) We leave it open which initial configuration will be used, as we have no further interaction with the environment this can also be seen as allowing for an "open" system; and (ii) we also allow for parameters as

S ::= skip | x := f (x1, . . . , xn) | S1; S2 | choose p1 : S1 or p2 : S2 ro | if b then S1 else S2 fi | while b do S od S ::= [skip] | [x := f (x1, . . . , xn)] | S1; S2 | [choose] p1 : S1 or p2 : S2 ro | if [b] then S1 else S2 fi | while [b] do S od
Table 1. The syntax of pWhile probabilities, i.e. our semantics allows for "under-specification" in the sense that the concrete probabilities are only determined in a concrete implementation.

Syntax

The syntax of statements in our language pWhile is given in Table 1. We also provide a labelled version of this syntax (cf. [START_REF] Nielson | Principles of Program Analysis[END_REF]) in order to be able to refer to certain program points in a program analysis context, see also Table 1. We will denote by Label the set of all labels of a program. For details on expressions f (x 1 , . . . , x n ) (also sometimes denoted simply by e) etc. we refer to e.g. [START_REF] Nielson | Principles of Program Analysis[END_REF][START_REF] Di Pierro | Probabilistic semantics and analysis[END_REF].

For this language we have the usual intuitive semantics: We have an "empty" skip statement, assignment to variables, sequential composition as well as if statements and while loops. The only probabilistic construct is the choose statement which executes S 1 or S 2 according to the probabilities p 1 and p 2 (which we assume to be normalised, i.e. p 1 + p 2 = 1, or which will be (re)normalised as part of the execution of the program, mor below). The choose statement can also be extended from its binary version to an n-ary one. We will not consider in this core language random assignments -as in some of our other papers or, e.g., [START_REF] Kozen | Semantics of probabilistic programs[END_REF] -but just note that obviously one can implement a random assignment (involving finite values) using the choose construct.

Operational Semantics

The SOS semantics for pWhile is given in Table 2. We use the (additional) statement stop to indicate successful termination and (re)normalise probabilities in R7, otherwise these are the usual SOS rules for procedural languages. The operational (SOS) semantics of pWhile is defined in terms of a probabilistic transition system on configurations. A configuration is a pair S, s ∈ Conf with S a statement in pWhile and s ∈ State a (classical) state, i.e. a function Var → Value. The SOS semantics is essentially also the same for the labelled version of the language, in this case we can however simplify the presentation by identifying each statement S with the label of the initial block of S, i.e. a configuration S, s is identified with the pair s, init(S) ∈ State × Label (for a formal definition of init see e.g. [START_REF] Di Pierro | Probabilistic semantics and analysis[END_REF]). Most transitions are in fact deterministic (i.e. the associated probability is 1) just for choices, i.e. rules R7 do we use the normalised probabilities pi (more on the actual normalisation procedure below).

R1 stop, s -→1 stop, s R2 skip, s -→1 stop, s R3 v := e, s -→1 stop, s[v → E(e)s] R41 S1, s -→p S 1 , s S1; S2, s -→p S 1 ; S2, s R42 S1, s -→p stop, s S1; S2, s -→p S2, s R51 if b then S1 else S2 fi, s -→1 S1, s if E(b)s = true R52 if b then S1 else S2 fi, s -→1 S2, s if E(b)s = false R61 while b do S od, s -→1 S; while b do S od, s if E(b)s = true R62 while b do S od, s -→1 stop, s if E(b)s = false R71 choose p1 : S1 or p2 : S2 ro, s -→p 1 S1, s with p1 = p 1[p 1 ,p 2 ] R72 choose p1 : S1 or p2 : S2 ro, s -→p 2 S2, s with p2 = p 2[p 1 ,p 2 ]
Table 2. The rules of the SOS semantics of pWhile (static)

The probabilistic transition system defined in Table 2 describes a Discrete Time Markov Chain (DTMC) (cf. e.g. [START_REF] Norris | Markov Chains. Cambidge Series in Statistical and Probabilistic Mathematics[END_REF][START_REF] Seneta | Non-negative Matrices and Markov Chains[END_REF]) as we obviously have a memoryless process: the transitions in Rules R1 to R7 depend only on the current configuration and not on the sequence of the configurations that preceded it. One can also easy to show that the probabilities of out-going transitions from each state sum up to one. It is well-known that the matrix of transition probabilities of a DTMC on a countable state space is a stochastic matrix, i.e. a square (possibly infinite) matrix P = (p ij ) whose elements are real numbers in the closed interval [0, 1], for which j p ij = 1 for all i [START_REF] Seneta | Non-negative Matrices and Markov Chains[END_REF][START_REF] Woess | Denumerable Markov Chains[END_REF]. We can therefore represent the SOS semantics for a pWhile program P by the stochastic matrix on the vector space over the set Conf of all configurations of a program P defined by the rules in Table 2.

States and Observables

For our language we also allow for the specification of the range of possible values of variables, i.e. Value(x), via declarations. Without going into the details of the formal syntax, we distinguish between parameters, indicated by para, and proper variables for which we specify their Value as a subset of the integers. This allows us (also because Value(x) are assumed to be finite) to describe the space of probabilistic states σ (of a program) as (probability) distributions over classical states, i.e. σ ∈ D(State). We can also see σ simply as a vector in the so-called free vector space V(State) over State (distributions correspond to positive vectors with 1-norm 1) cf. [START_REF] Di Pierro | Probabilistic semantics and analysis[END_REF][START_REF] Di Pierro | Semantics of probabilistic programs: A weak limit approach[END_REF].

For a single variable x we have (the isomorphism) State = Value(x) and when we consider several variables we can identify a classical state s with an element in the Cartesian product Value(x i ) × . . . × Value(x v ). When we consider probabilistic states of a single variable x then we have σ ∈ D(State) ⊆ V(Value(x)). But for more than one variable we have σ ∈ v i=1 V(Value(x i )), i.e. the so-called tensor product, rather than the Cartesian product of V(Value). This unfortunately leads to a form of combinatorial explosion but is needed accommodate all possible joint probability distributions as we have (the isomor-

phism) V(X 1 × . . . × X v ) = V(X 1 ) ⊗ . . . ⊗ V(X v ).
Concretely, the tensor product -more precisely, the Kronecker product, i.e. the coordinate based version of the abstract concept of a tensor product -of two vectors (x 1 , . . . , x n ) and (y 1 , . . . , y m ) is (x 1 y 1 , . . . , x 1 y m , . . . , x n y 1 , . . . , x n y m ) i.e. an nm dimensional vector. For an n × m matrix A = (A ij ) and an n × m matrix B = (B kl ) we construct similarly an nn × mm matrix A ⊗ B = (A ij B), i.e. each entry A ij in A is multiplied with a copy of the matrix or block B, for further details we refer e.g to [START_REF] Roman | Advanced Linear Algebra[END_REF]Chap. 14].

In the following we also will use the notion of an observable which describes properties a program or system might have (for further details see [START_REF] Di Pierro | Semantics of probabilistic programs: A weak limit approach[END_REF]). Formally, an observable is a linear functional on the probabilistic state space, i.e. an element of its dual space. For finite dimensional spaces, as we have them here, we can identify state and observable space. States and observables are related to each other by the notion of expected value, E(x, σ), which gives the probability that we will observe a certain property x when the state of the system is described by σ. In our finite setting (and by Riesz's representation theorem) we can utilise an inner product ., . in order to to obtain E(x, σ) = x, σ .

Static Probabilities

If the probabilities in the choose statement are required to be constants (or parameters) then we can us a simple (re)normalisation procedure (at compile time) in order to obtain the effective probabilities that a certain alternative is executed, i.e. we (re) normalise probabilities in the SOS in Table 2 via:

p = p [p1...pn] = p p 1 + . . . + p n .
Not least because we will allow later also variable values p i we have to address the issue whether p [p1...pn] is always well-defined. We will exclude negative weights (if the nevertheless appear we could consider the absolute values). However, one problem remains, namely whether or not we allow for p i = 0. One argument -which we will adopt -would be to allow this to indicate "blocked" alternatives, especially when we consider (below) dynamical probabilities. This implies another issue we need to consider, namely the case where all p i = 0. In this case, normalisation would imply a division by zero. To overcome this we set p = p [p1...pn] = 0 if we have for all p i = 0.

Linear Operator Semantics (LOS)

The Linear Operator Semantics (LOS) in [START_REF] Di Pierro | A systematic approach to probabilistic pointer analysis[END_REF][START_REF] Di Pierro | Semantics of probabilistic programs: A weak limit approach[END_REF] constructs the generator of the DTMC which represents the dymanics of a program (executions) in a syntax directed fashion. Like Kozen's semantics [START_REF] Kozen | Semantics of probabilistic programs[END_REF] we can represent the LOS as an operator on the vector space of probabilistic states, i.e. in the finite case as a matrix.

{ {[skip] } }LOS = { I, } { {[x := e] } }LOS = { U(x ← e), } { {S1; S2} }LOS = ([[S1]] £ init(S2)) ∪ [[S2]] { {[choose] p1 : S1 or p2 : S2 ro} }LOS = {p 1[p 1 ,p 2 ] • I ⊗ E( , init(S1))} ∪ { {S1} }LOS ∪ {p 2[p 1 ,p 2 ] • I ⊗ E( , init(S2))} ∪ { {S2} }LOS { {if [b] then S1 else S2 fi} }LOS = { P(b), } £ init(S1)} ∪ { {S1} }LOS ∪ { P(b) ⊥ , } £ init(S2)} ∪ { {S2} }LOS { {while [b] do S od} }LOS = { P(b), } £ init(S)} ∪ { {S} }LOS £ ∪{ P(b) ⊥ , } Table 3. The LOS semantics of pWhile (static)
The LOS, [[P ]] LOS , of a program P is constructed by means of a set, { {P } } LOS which associated to a program P is a set of linear operators which describe local changes (at individual labels). From { {P } } LOS we can construct the DTMC generator [[P ]] LOS then as a linear operator on V(Conf)

[[P ]] LOS : V(Value n ) ⊗ V(Label) → V(Value n ) ⊗ V(Label) or simply [[P ]] LOS ∈ L(V(Conf)
). We obtain it by combining all the individual effects which are described in { {P } } LOS :

[[P ]] LOS = { {P } } LOS = {G | G ∈ { {P } } LOS }.
The { {S} } LOS associated to a statement S is given by a set of global and local operators, i.e. { {.} } LOS : Stmt → P(Γ ∪Λ), cf Table3. Global operators are linear operators on

V(Conf) i.e. Γ = L(V(Value n ) ⊗ V(Label)) = L(V(Conf))
, and local operators are pairs of operators on V(State) and labels ∈ Label, i.e.

Λ = L(V(Value n )) × Label.
Global operators are providing information about how the computational state changes at a label as well as the control flow, i.e. what is the label of the next statement to be executed. Local operators are representing statements for which the "continuation" is not yet known. In order to transform local operators into global ones (once the "continuation" is known) we define a "continuation" operation F, £ = F ⊗ E( , ) which we extend in the obvious way to sets of operators as { F i , i }} £ = {F i ⊗ E( i , )} (for global operators we have G £ = G). We denote by E(i, j) matrix units: (E(i, j)) ij = 1 and 0 otherwise.

We use elementary update and test operators U and P (and its complement P ⊥ = I -P) as in Kozen's semantics. However, the tensor product structure allows us to define these operators in a different (but equivalent) way.

For a single variable the assignment to a constant value v ∈ Value is represented by the operator on V(Value) given by U(v) = 1 if v = i and 0 otherwise.

Testing if a single variable satisfies a boolean test b is achieved by a (diagonal) projection operator on V(Value) with (P(b)) ii = 1 if b(i) holds and 0 otherwise. We extend these to the multivariable case, i.e. for |Var| = n > 1. For testing if we are in a classical state s ∈ Value n or if an expression e evaluates to a constant v (assuming an appropriate evaluation function E : Expr → State → Value) we have operators on V(Value) ⊗n :

P(s) = n i=1 P(x i = s(x i )) P(e = v) = E(e)s=v

P(s).

We also have operators on V(Value) ⊗n for updating a variable x k in the context of other variables to a constant v or to the value of an expression e:

U(x k ← v) = k-1 i=1 I ⊗ U(v) ⊗ n i=k+1 I U(x k ← e) = v P(e = v)U(x k ← v)
As we model the semantics of a program as DTMCs we are also adding a final loop * (for * a fresh label not appearing already in P ) when we consider a complete program (DTMC never terminate and thus we have to simulate termination by an infinite repetition of the final state), i.

A Small Example

The LOS semantics specifies the semantics of a program as the generator of a DTMC. We use a simple experimental toolpwc -which "compiles" a pWhile program into an octave [START_REF] Eaton | GNU Octave -A high-level interactive language for numerical computations[END_REF] script which defines the different matrices/operators. To illustrate this let us look at a simple example involving a probabilistic choice.

Example 1. The concrete program P we consider, for which we also provide the labelling (which is in fact produced by the pwc tool) is given by: Here we deal with one parameter p, the value of this can be set to any (integer) value before the program is actually executed, and one variable x which can take two values in {0, 1}. The state space is thus given just by V({0, 1}) = R 2 (as the parameter p does not change we do not record its value as part of the state). The program is made up from 5 blocks:

[choose] 1 , [x := 0] 2 , [x := 1] 3 , [skip] 4 , [skip] 5 .
We thus have as the (probabilistic) space of configurations on which the LOS operator acts

V({0, 1} × V({ 1 , 2 , 3 , 4 , 5 }) = R 2 ⊗ R 5 = R 10 , i.e.

[[P ]]

LOS is a 10 × 10 matrix which represents the generator of a DTMC on a space of 10 elements. Each dimension corresponds to a possible configuration, i.e. a tuple s i , j with s a (classical) state s : {x} → {0, 1} and a statement or block identified by its label ∈ { 1 , 2 , 3 , 4 , 5 }. Concretely we have the following base vectors e i in R 10 for the state spaces of the DTMC: e 1 = x → 0, 1 , e 2 = x → 0, 2 , . . . , e 5 = x → 0, 5 , e 6 = x → 1, 1 , . . . , e 10 = x → 1, 5 .

For each of the 5 blocks we have a local transfer operator F 1 , . . . F 5 which are (stochastic) 2 × 2 matrices, i.e. linear operators on our state space R 2 . For blocks 4 and 5 these F i are trivial, i.e. the identity 2 × 2 matrix, for label 2 and 3 the transfer operators are slightly more interesting:

F 1 = F 4 = F 5 = 1 0 0 1 , F 2 = 1 0 1 0 , F 3 = 0 1 0 1 .
This allows us to specify the local LOS operators for each basic block:

{ {[x := 0] 2 } } LOS = { F 1 , 2 }, { {[x := 1] 3 } } LOS = { F 1 , 3 }, { {[skip] 4 } } LOS = { F 4 , 4 }, { {[skip] 5 } } LOS = { F 5 , 5 }.
We could also consider explicitely { {[choose] 1 } } LOS = { F 1 , 1 }, however this will be covered when we consider the global operators.

The control flow of P is made up from 7 control-flow step triples i, p, j , where i is the initial label, p the transition probability and j the final label:

1 -1, 1, 2 , 2 -1, 1, 3 , 3 -1, p, 4 , 4 -2, 1, 5 , 5 -3, 1, 5 , 6 -4, 1, 5 , 7 -5, 1, 5 .
For each of these control-flow steps we construct a global operator, typically the tensor product of the local transfer operator F i at the initial label i and a controlflow step given by the matrix unit E(i, j), eventually weighted by a probability. Here we have to consider the (global) operators: [START_REF] Di Pierro | Probabilistic semantics and analysis[END_REF][START_REF] Di Pierro | Probabilistic semantics and analysis[END_REF]. The first three operators allow us to define the LOS of the choices statement. For this we have to specify a particular value for the parameter p. For example, for p = 0 we get after renormalisation:

T 1 = F 1 ⊗ E(1, 2), T 2 = F 1 ⊗ E(1, 3), T 3 = F 1 ⊗ E(1, 4), T 4 = F 2 ⊗ E(2, 5), T 5 = F 3 ⊗ E(3, 5), T 5 = F 4 ⊗ E(4, 5), T 7 = F 5 ⊗ E
{ {[choose] 1 . . . ro} } LOS = { 1 2 T 1 , 1 2 T 2 } ∪ { {[x := 0] 2 } } LOS ∪ { {[x := 1] 3 } } LOS .
If we instead take p = 1 we get after renormalisation:

= { 1 3 T 1 , 1 3 T 2 , 1 3 T 3 , } ∪ { {[x := 0] 2 } } LOS ∪ { {[x := 1] 3 } } LOS ∪ { {[skip] 4 } } LOS .
The LOS { {[choose] 1 . . . ro} } LOS contains global as well as local operators: The global ones represent control-flow steps where the destination is already known, while the local ones (here for the labels 2 , 3 and 4 are still unresolved. However, when we consider the whole program then the operation £ resolves the destinations of local operators and turns them into global ones, e.g.

{ {[x := 0] 2 } } LOS £ 5 = {T 4 } = {F 2 ⊗ E(2, 5)} { {[x := 1] 3 } } LOS £ 5 = {T 5 } = {F 3 ⊗ E(3, 5)} { {[skip] 4 } } LOS £ 5 = {T 6 } = {F 4 ⊗ E(4, 5)}
Resolving the self-loop for label 5 using T 7 we get the semantics for p = 0 as:

{ {P } } LOS = { 1 2 T 1 , 1 2 T 2 , T 4 , T 5 , T 6 , T 7 }
and for p = 1 we have (similarly also for other values of p):

{ {P } } LOS = { 1 3 T 1 , 1 3 T 2 , 1 3 T 3 , T 4 , T 5 , T 6 , T 7 }
The DTMC generator in both case is

[[P ]] LOS = {T | T ∈ { {P } } LOS } .

Dynamical Probabilities

The main purpose of this work is to allow for "dynamical" probabilities in programs. That is we would like to allow for variables in choice constructs which allow a change of their values in the course of a computation. Given that our LOS semantics constructs a single operator [[P ]] LOS for every program P which does not change during the execution, i.e. represents a (time) homogenous DTMC, this seems to be a hopeless task. On the other hand, the state of the system does obviously contain all the information which could influence how the execution of a program should continue, so if it encodes the values of variables in choices, then this information should somehow be exploitable.

For the SOS semantics it is still relatively easy to extend it towards variable probabilities: We have to replace the normalisation condition in rules R7 in Tablle 2 by referrence to the current state s, i.e. pi = s(p i )/s(p 1 ) + s(p 2 ) rather than constant values of p i . The way to introduce dynamical or variable probabilities into the LOS semantics of the choice construct is to test or check whether we are in a certain state where variables have certain concrete values, if this is the case then the corresponding normalisation is applied.

Linear Operator Semantics (LOS)

In order to extend the LOS semantics as to allow for variable probabilities we have to consider the way we construct the LOS operator for the choice statement with static, i.e. constant, probabilities:

{ {[choose] p 1 : S 1 or p 2 : S 2 ro} } LOS = {p 1 • I ⊗ E( , init(S 1 ))} ∪ { {S 1 } } LOS ∪ {p 2 • I ⊗ E( , init(S 2 ))} ∪ { {S 2 } } LOS ,
or more general for n alternatives in a choice statement:

{ {[choose] p 1 : S 1 or . . . or p n : S n ro} } LOS = = n i=1 {p i • I ⊗ E( , init(S i ))} ∪ { {S i } } LOS .
In these rules all p i are known, either because they are constants or because they are constant parameters. We thus can compute the normalised probabilities pi or, when we need to explicitely record the context in which we normalise, pi = p i[p 1...pn] in exactly the same way as in the operational semantics.

When it comes to dynamical probabilities then we need to consider all possible contexts, i.e. all possible values p 1 , . . . , p n could take, in which we might need to normalise a probability. Formally we define a context for probabilities p 1 , . . . , p n where each p i can be a constant value (incl. a parameter) or a variable (name) as a set of sequences i 1 , . . . , i n of integers:

C[p 1 , p 2 , . . . , p n ] =        ∅ if n = 0 {[p 1 ]} if n = 1 and p i constant {[c] | c ∈ Value(p 1 )} if n = 1 and p i a variable [i]∈C[p1] {[i] • C[p 2 , . . . , p n ]} otherwise, i.e. n > 1.
where "•" denotes the concatenation of integer sequences [i 1 , . . . , i m ] defined and extended to sets of sequences in the obvious way.

Example 2. Assume we have a variable x with Value(x) = {0, 1} and a parameter p = 0 or p = 1 then contexts are given by:

C[x, 1, p] = {[0, 1, 0], [1, 1, 0]} and C[x, 1, p] = {[0, 1, 1], [1, 1, 1]}
With this we can now define an extended version of the LOS which also allows for variables as choice probabilities:

{ {[choose] p 1 : S 1 or . . . or p n : S n ro} } LOS = = n i=1    cj ∈pi [d1,...,dn]∈C[p1...pn] c j [d1...dn] • P pi[p1...pn] cj [d1...dn] ⊗ E( , init(S i ))    ∪ { {S i } } LOS .
To explain this construction: The LOS of the choices is given -as in the static case -as the union of all (global) operators which implement the control-flow step from label to one of the alternatives i = 1 . . . n together with the LOS semantics of each of these alternatives defined by { {S i } } LOS . However, in the case of static probabilities we have to weight the operator E( , init(S i )) not just with a normalised probability but instead we test if the values of the probabilities (which can be variables, after all) are described by a particular context and then apply the corresponding normalised weight c j [d1...dn] . This test operator P pi[p1...pn] cj [d1...dn] is very similar to the test we apply in order to identify a particular state, i.e. P(σ), except that in a context the same variable can appear several times:

P pi[p1...pn] cj [d1...dn] = P(p i = c j ) •   k=1,...,n P(p k = d k )   .
The first sum is over all possible values of the guard probability p i , where we use the short-hand notation c j ∈ p i for c j ∈ Value(p i ) which for constants and parameters reduces to a single term c j = p i . The second sum is over all possible values of all probabilities in all possible contexts. It might be interesting to note that if a variable appears twice it has to have the same value (as diag(e i ) ⊗ diag(e j ) = diag(e i ) if and only if i = j and the zero matrix otherwise). For constant values we can also omit the tests (as e i T = e i diag(e i )T for all T).

It is simple to show that the LOS semantics for choice with variable probabilities is equivalent to the SOS semantics, for the other construct things are unchanged [START_REF] Di Pierro | Semantics of probabilistic programs: A weak limit approach[END_REF].

A Small Example

In order to illustrate the LOS for dynamical variables let us again first consider a very simple example, similar to Example 1. As we have the same declarations, we have exactly the same state spaces as in Example 1. Furthermore, we also have the same 5 blocks as in the previous example and therefore the DTMC state space of configurations is again R 10 . We also have the same transfer operators F i (and local LOS operators for the basic blocks). However, though the control flow has again 7 control-flow steps and it is nearly identical, except for the step from 1 to 2 which here is guarded by a variable probability x:

1 -1, x, 2 , 2 -1, 1, 3 , 3 -1, p, 4 , 4 -2, 1, 5 , 5 -3, 1, 5 , 6 -4, 1, 5 , 7 -5, 1, 5 .
We can still use the same operators T i from Example 1 but the complete LOS semantics now looks slightly different. For p = 0 or p = 1 we need to work with the contexts given in Example 2. For p = 0 we have

C[x, 1, p] = {[0, 1, 0], [1, 1, 0]} and thus get { {Q} } LOS = { (P(x = 0) + 1 2 P(x = 1)) ⊗ E(1, 3), ( 1 2 P(x = 1)) ⊗ E(1, 4), T 4 , T 5 , T 6 , T 7 }.
and for the parameter value p = 1 we have C[x, 1, p] = {[0, 1, 1], [1, 1, 1]} and:

{ {Q} } LOS = { ( 1 3 P(x = 1)) ⊗ E(1, 2), ( 1 2 P(x = 0) + 1 3 P(x = 1)) ⊗ E(1, 3), ( 1 2 P(x = 0) + 1 3 P(x = 1)) ⊗ E(1, 4), T 4 , T 5 , T 6 , T 7 }.
Note that test operators like P(x = 1) should actually be expressed as, for example: P(x = 1)P(x = 1)P(1 = 1)P(p = 1). However, as said before, in the case of constants (and parameters) these tests are redundant and as projections are always idempotents we also have: P(x = 1) = P(x = 1)P(x = 1).

Example: Duel at High Noon

We illustrate the generation of the LOS semantics -i.e. the DTMC generator of a probabilistic program -by considering an example given in [START_REF] Gretz | Operational versus weakest precondition semantics for the probabilistic guarded command language[END_REF][START_REF] Gretz | Operational versus weakest pre-expectation semantics for the probabilistic guarded command language[END_REF], see also [12, p211], which concerns the kind of "duel" between two "cowboys" A and B. We first reproduce essentially the results of [START_REF] Gretz | Operational versus weakest precondition semantics for the probabilistic guarded command language[END_REF][START_REF] Gretz | Operational versus weakest pre-expectation semantics for the probabilistic guarded command language[END_REF] regarding the chances that A (or B) will win/survive the "duel" with static probabilities. We then also consider the case where one the two duellists (here A) improves his hitting chances during the contest. This situation obviously requires dynamical/changing probabilities.

Static Probabilities

The idea is that two "cowboys", A (Adam) and B (Boris), have a duel. At each turn one of them is allowed to shoot at the other, if he misses the other one can try, if he also misses it is the first ones turn again until one is "successful".

That is, at the beginning one of the two -either Adam or Boris -is allowed to shoot at the other one. Which of the two starts is left open, i.e. decided nondeterministically. We assume that there is a probability a for A hitting B and a probability b that B manages to shoot A. More precisely, we have a = ak ak+am for a "killing" and a "missing" weight ak and bk, respectively (and similar for b).

In the original version it is non-deterministically decided whether A or B starts, but in order to get simple numerical results we will flip a fair coin to determine who has the first attempt. The concrete pWhile program is given on the left hand side in Table 4.

The variable c determines whether the duel should be continued, if c = 1 the duel continues, otherwise it is over. This is essentially to simulate a until statement using the while construct. The variable t determines which of the two duellists is allowed to try to shoot, for t = 0 it is A's turn, otherwise it is B's turn. As long as the duel is continued (i.e. c = 1) it is either A which gets a try (if t = 0) or B (for t = 1). If it is A's turn he will hit B with probability a -in this case the duel is over and c is set to 0; and with probability 1 -a it might be a miss -in this case the next round it will be B's turn. Similarly, for t = 1 the duellist B gets his chance.

At the end of the duel the value of t determines who has lost/won -i.e whoes turn it was when the loop terminated, i.e. c was set to zero. In order to extract akl:=@inc(akl); aml:=@dec(aml); od; stop; # terminal loop end Table 4. pWhile programs for the Duel at High Noon information about the probability distribution describing a particular variablein our case t -at a given label , i.e. program point , we can use an abstraction operator A . This operator/matrix leaves the first variable (i.e. t) unchanged and "forgets" about all other variables in a particular label :

A = I ⊗ A f ⊗ . . . ⊗ A f ⊗ (e ) t
with I the identity matrix for the first variable (for t it is a 2 × 2 matrix), A f a so-called "forgetfull abstraction" for the remaining variables and e t the transposed (column) base vector in V(Label) which selects or projects the state at label . The operators A f are given by column vectors (or n × 1 matrices) which only contain 1s, i.e. A f = (1, 1, 1, . . . , 1) t with n = dim(V(Value(x)) = |Value(x)|. This is an instance of a more general framework of Probabilistic Abstract Interpretation (PAI), cf. e.g. [START_REF] Di Pierro | Relational analysis and precision via probabilistic abstract interpretation[END_REF][START_REF] Di Pierro | Semantics of probabilistic programs: A weak limit approach[END_REF][START_REF] Di Pierro | Probabilistic semantics and analysis[END_REF].

With this abstraction A we can extract the probabilities that t is 0 or 1, i.e. who has won the duel, if we take = * , i.e. the final label 8 of the program once the program has "terminated". For this we have to consider the (long-run) input/output behaviour for an initial configuration c 0 = s 0 ⊗ e 0 , i.e. an initial state s 0 which determines the initial values of all variables at the initial label 0 . We then have to apply the LOS operator [[P ]] LOS until we reach a limit lim n→∞ (s 0 ⊗ e 0 )[[P ]] n LOS . This essentially gives Kozen's input/output semantics [START_REF] Kozen | Semantics of probabilistic programs[END_REF] of the program, cf. [START_REF] Di Pierro | Semantics of probabilistic programs: A weak limit approach[END_REF].

To obtain numerical results we can stop this iteration for a finite value of n, in our case n = 100 is sufficient. Finally, we have to extract the state of t using A * and the observable w = (1, 0) which gives the probability that t = 0, i.e. that the winner is A. In other words, the aim of the analysis is to determine:

ω = lim n→∞ w, (s 0 ⊗ e 0 ) • [[P ]] n LOS • A * .
or a numerical approximation (for n = 100). In our case t and c are both initialised, so ω is idependent of the initial state s 0 . If we consider the "nondeterministic" version, i.e. dropping 'choose 1: t:=0 or 1: t:=1 ro', the value of ω would depend on s 0 . We use our tool pwc to construct [[P ]] LOS . The program has 13 labels or elementary blocks (with * = 13). The dimension of the DTMC is then 2 × 2 × 13 = 52 as t and c take two possible values. With this we can compute ω for different values of the parameters ak, am, etc. The top left diagram in Figure 1 depicts the chances of A surviving the duel depending on a = ak/(ak + am) and b = bk/(bk + bm).

Dynamic Probabilities

If we assume that probabilities (of hitting) are not constant, but that for example one of the duellists is getting better during the shoot-out we have to consider a different model as in the following pWhile program as on the right in Table 4.

Here we use the same parameters ak, etc. as in the static case. However for A these are only the initial values. During the duel A will improve his shooting skills (while B's abilities do not change). The (learned) chances of A hitting is given by akl and the chances of missing aml. These are changed using "external" functions @inc and @dec which depend on a learning rate r defined directly in octave as min(max(x+r,0),10) and min(max(x-r,0),10), respectively.

For different values of the parameters ak, am, etc. we can again construct the LOS operator [[P ]] LOS . In this case we have 17 lables/blocks and two additional variables akl and akm which each can have 11 possible values, thus we have to consider a DTMC on 2 × 2 × 11 × 11 × 17 = 8228 states.

The survival chances for A can be computed in the same way as in the static case, using the corresponding abstraction A 17 , the same w and based on a numeric approximation based on n = 100 iterations of [[P ]] LOS . For different learning rates r we depict the survival rate for A in Figure 1. For r = 0 we get exactly the same as in the static case -after all, A is stuck with his initial shooting abilities and does not improve at all.

Conclusions

We presented a model for probabilistic programs which essentially encodes the semantics of a program in terms of time homogenous DTMCs, i.e. the operator representing the semantics is given by a time invariant, "eternal" stochastic operator/matrix. Nevertheless, within this static model it is possible to also realise changing probabilities.

The language we based this on is a simple procedural language. Nevertheless, it is obvious that this model also applies to (proper) coordination languages like pKLAIM [START_REF] Di Pierro | Probabilistic KLAIM[END_REF][START_REF] Di Pierro | Continuous-time probabilistic KLAIM[END_REF]. This concerns in particular concurrency aspects: The rules of the duel in the cowboy example essentially implement an explicit round robin scheduler and the extension to more general schedulers seems not to be difficult. Surviving the duel itself can also be seen as an ultimate coordination problem in which the role of probability normalisation is essential: Ones survival depends not only on ones own (shooting) abilities but also on the one of the opponent. A hit rate of 50% for A means almost sure survival for A if B is a bad shooter with a 2% hit rate, but if B a perfect duelist with 100% hit rate then this will give the same A no chance of survival if B begins the duel.

It seems also feasible to extend this "probability testing" approach to continuous time models, continuous probabilities and hybrid systems, although this will require more careful considerations of the underlying measure theoretic structure (Borel structure, σ-algebras, measures instead of distributions, integrals in place of sums, etc.).

  e. we actually have to use ({ {P } } LOS £ * ) ∪ {I ⊗ E( * , * )} when we construct [[P ]] LOS . In this way we also resolve all open or dangling control flow steps, i.e. we deal ultimately with a set containing only global operators.As said, the operator [[P ]] LOS is the generator of a DTMC which implements the dynamic behaviour or executions of the program P . In particular, we can take any (initial) configuration c 0 , represented by a (point) distribution in V(Conf) and compute the distribution over all configurations we will have after n steps as c n = c 0 • [[P ]] n LOS (using post-multiplication as our convention).

  var p :para; x :{0,1}; begin [choose]^1 1: [x:=0]^2 or 1: [x:=1]^3 or p: [skip]^4 ro; [stop]^5 end

Example 3 .

 3 The program Q we consider is given by: var p :para; x :{0,1}; begin [choose]^1 x: [x:=0]^2 or 1:[x:=1]^3 or p:[skip]^4 ro; [stop]^5 end

Fig. 1 .

 1 Fig. 1. Survival probabilities ω for A with learning rates 0, 1, 2 and 4