Massimo Bartoletti

Tiziana Cimoli

G Michele Pinna

Lending Petri nets and contracts

Choreography-based approaches to service composition typically assume that, after a set of services has been found which correctly play the roles prescribed by the choreography, each service respects his role. Honest services are not protected against adversaries. We propose a model for contracts based on an extension of Petri nets, which allows services to protect themselves while still realizing the choreography. We relate this model with Propositional Contract Logic, by showing a translation of formulae into our Petri nets which preserves the logical notion of agreement, and allows for compositional verification.

Introduction

Many of today's human activities, from business and financial transactions, to collaborative and social applications, run over complex interorganizational systems, based on service-oriented computing (SOC) and cloud computing technologies. These technologies foster the implementation of complex software systems through the composition of basic building blocks, called services. Ensuring reliable coordination of such components is fundamental to avoid critical, possibly irreparable problems, ranging from economic losses in case of commercial activities, to risks for human life in case of safety-critical applications.

Ideally, in the SOC paradigm an application is constructed by dynamically discovering and composing services published by different organizations. Services have to cooperate to achieve the overall goals, while at the same time they have to compete to achieve the specific goals of their stakeholders. These goals may be conflicting, especially in case of mutually distrusted organizations. Thus, services must play a double role: while cooperating together, they have to protect themselves against other service's misbehavior (either unintentional or malicious).

The lack of precise guarantees about the reliability and security of services is a main deterrent for industries wishing to move their applications and business to the cloud [START_REF] Armbrust | A view of cloud computing[END_REF]. Quoting from [START_REF] Armbrust | A view of cloud computing[END_REF], "absent radical improvements in security technology, we expect that users will use contracts and courts, rather than clever security engineering, to guard against provider malfeasance".

Indeed, contracts are already a key ingredient in the design of SOC applications. A choreography is a specification of the overall behavior of an interorganizational process. This global view of the behavior is projected into a set of local views, which specify the behavior expected from each service involved in the whole process. The local views can be interpreted as the service contracts: if the actual implementation of each service respects its contract, then the overall application must be guaranteed to behave correctly.

There are many proposals of formal models for contracts in the literature, which we may roughly divide into "physical" and "logical" models. Physical contracts take inspiration mainly from formalisms for concurrent systems (e.g. Petri nets [START_REF] Van Der Aalst | Multiparty contracts: Agreeing and implementing interorganizational processes[END_REF], event structures [START_REF] Hildebrandt | Declarative event-based workflow as distributed dynamic condition response graphs[END_REF][START_REF] Bartoletti | An event-based model for contracts[END_REF], and various sorts of process algebras [8-10, 12, 16]), and they allow to describe the interaction of services in terms of response to events, message exchanges, etc. On the other side, logical contracts are typically expressed as formulae of suitable logics, which take inspiration and extend e.g. modal [START_REF] Abadi | A calculus for access control in distributed systems[END_REF][START_REF] Garg | A modal deconstruction of access control logics[END_REF], intuitionistic [START_REF] Abadi | A logical view of composition[END_REF][START_REF] Bartoletti | A calculus of contracting processes[END_REF], linear [START_REF] Abadi | A logical view of composition[END_REF], deontic [START_REF] Prisacariu | A dynamic deontic logic for complex contracts[END_REF] logics to model high-level concepts such as promises, obligations, prohibitions, authorizations, etc.

Even though logical contracts are appealing, since they aim to provide formal models and reasoning tools for real-world Service Level Agreements, existing logical approaches have not had a great impact on the design of SOC applications. A reason is that there is no evidence on how to relate high-level properties of a contract with properties of the services which have to realize it. The situation is decidedly better in the realm of physical contracts, where the gap between contracts and services is narrower. Several papers, e.g. [9-11, 16, 21], address the issue of relating properties of a choreography with properties of the services which implement it (e.g. deadlock freedom, communication error freedom, session fidelity), in some cases providing automatic tools to project the choreography to a set services which correctly implements it.

A common assumption of most of these approaches is that services are honest, i.e. their behavior always adheres to the local view. For instance, if the local view takes the form of a behavioral type, it is assumed that the service is typeable, and that its type is a subtype of the local view. Contracts are only used in the "matchmaking" phase: once, for each local view projected from the choreography, a compliant service has been found, then all the contracts can be discarded.

We argue that the honesty assumption is not suitable in the case of interorganizational processes, where services may pursue their providers goals to the detriment to the other ones. For instance, consider a choreography which prescribes that a participant A performs action a (modeling e.g. "pay $100 to B"), and that B performs b (e.g. "provide A with 5GB disk storage"). If both A and B are honest, then each one will perform its due action, so leading to a correct execution of the choreography. However, since providers have full control of the services they run, there is no authority which can force services to be honest. So, a malicious provider can replace a service validated w.r.t. its contract, with another one: e.g., B could wait until A has done a, and then "forget" to do b. Note that B may perform his scam while not being liable for a contract violation, since contracts have been discarded after validation.

In such competitive scenarios, the role of contracts is twofold. On the one hand, they must guarantee that their composition complies with the choreography: hence, in contexts where services are honest, the overall execution is correct. On the other hand, contracts must protect services from malicious ones: in the example above, the contract of A must ensure that, if A performs a, then B will either do b, or he will be considered culpable of a contract violation.

In this paper, we consider physical contracts modeled as Petri nets, along the lines of [START_REF] Van Der Aalst | Multiparty contracts: Agreeing and implementing interorganizational processes[END_REF]. In our approach we can both start from a choreography (modeled as a Petri net) and then obtain the local views by projection, as in [START_REF] Van Der Aalst | Multiparty contracts: Agreeing and implementing interorganizational processes[END_REF], or start from the local views, i.e. the contracts published by each participant, to construct a choreography which satisfies the goals of everybody. Intuitively, when this happens the contracts admit an agreement.

A crucial observation of [START_REF] Bartoletti | A theory of agreements and protection[END_REF] is that if contracts admit an agreement, then some participant is not protected, and vice-versa. The archetypical example is the one outlined above. Intuitively, if each participant waits until someone else has performed her action, then everyone is protected, but the contracts do not admit an agreement because of the deadlock. Otherwise, if a participant does her action without waiting, then the contracts admit an agreement, but the participant who makes the first step is not protected. This is similar to the proof of impossibility of fair exchange protocols without a trusted third party [START_REF] Even | Relations among public key signature systems[END_REF].

To overcome this problem, we introduce lending Petri nets (in short, LPN). Roughly, an LPN is a Petri net where some places may give tokens "on credit". Technically, when a place gives a token on credit its marking will become negative. This differs from standard Petri nets, where markings are always nonnegative. The intuition is that if a participant takes a token on credit, then she is obliged to honour it -otherwise she is culpable of a contract violation.

Differently from the Petri nets used in [START_REF] Van Der Aalst | Multiparty contracts: Agreeing and implementing interorganizational processes[END_REF], LPNs allow for modeling contracts which, at the same time, admit an agreement (more formally, weakly terminate) and protect their participants. LPNs preserve one of the main results of [START_REF] Van Der Aalst | Multiparty contracts: Agreeing and implementing interorganizational processes[END_REF], i.e. the possibility of proving that an application respects a choreography, by only locally verifying the services which compose it. More precisely, we project a choreography to a set of local views, independently refine each of them, and be guaranteed then the composition of all refinements respects the choreography. This is stated formally in Theorem 8.

The other main contribution is a relation between the logical contracts of [START_REF] Bartoletti | A calculus of contracting processes[END_REF] and LPN contracts. More precisely, we consider contracts expressed in (a fragment of) Propositional Contract Logic (PCL), and we compile them into LPNs. Theorem 23 states that a PCL contract admits an agreement if and only if its compilation weakly terminates. Summing up, Theorem 24 states that one can start from a choreography represented as a logical contract, compile it to a physical one, and then use Theorem 8 to project it to a set services which correctly implement it, and which are protected against adversaries. Finally, Theorem 25 relates logical and physical characterizations of urgent actions, i.e. those actions which must be performed in a given state of the contract.

Nets

We briefly review Petri nets [START_REF] Reisig | Petri Nets: An Introduction[END_REF] and the token game. We consider Petri nets labeled on a set T, and (perhaps a bit unusually) the labeling is also on places.

A labeled Petri net is a 5-tuple S, T, F, Γ, Λ , where S is a set of places, and T is a set of transitions (with S ∩ T = ∅), F ⊆ (S × T ) ∪ (T × S) is the flow relation, and Γ : S → T, Λ : T → T are partial labeling function for places and transitions, respectively. Ordinary (non labeled) Petri nets are those where the two labeling functions are always undefined (i.e. equal to ⊥). We require that for each t ∈ T , F (t, s) > 0 for some place s ∈ S, i.e. a transition cannot happen spontaneously. Subscripts on the net name carry over the names of the net components. As usual, we define the pre-set and post-set of a transition/place:

• x = {y ∈ T ∪ S | F (y, x) > 0} and x • = {y ∈ T ∪ S | F (x,
y) > 0}, respectively. These are extended to subsets of transitions/places in the obvious way.

A marking is a function m from places to natural numbers (i.e. a multiset over places), which represents the state of the system modeled by the net. A marked Petri net is a pair N = ( S, T, F, Γ, Λ , m 0 ), where S, T, F, Γ, Λ is a labelled Petri net, and m 0 : S → N is the initial marking.

The dynamic of a net is described by the execution of transitions at markings. Let N be a marked net (hereafter we will just call net a marked net). A transition t is enabled at a marking m if the places in the pre-set of t contains enough tokens (i.e. if m contains the pre-set of t). Formally, t ∈ T is enabled at m if m(s) ≥ F (s, t) for all s ∈ • t. In this case, to indicate that the execution of t in m produces the new marking m (s) = m(s) -F (s, t) + F (t, s), we write m [t m , and we call it a step1 . This notion is lifted, as usual, to multisets of transitions.

The notion of step leads to that of execution of a net. Let N = ( S, T, F, Γ, Λ , m 0 ) be a net, and let m be a marking. The firing sequences starting at m are defined as follows: (a) m is a firing sequence, and (b

) if m [t 1 m 1 • • • m n-1 [t n m n is a firing sequence and m n [t m is a step, then m [t 1 m 1 • • • m n-1 [t n m n [t m
is a firing sequence. A marking m is reachable iff there exists a firing sequence starting at m 0 leading to it. The set of reachable markings of a net N is denoted with M(N ). A net N = ( S, T, F, Γ, Λ , m 0 ) is safe when each marking m ∈ M(N ) is such that m(s) ≤ 1 for all s ∈ S.

A trace can be associated to each firing sequence, which is the word on T * obtained by the firing sequence considering just the (labels of the) transitions and forgetting the markings

: if m 0 [t 1 m 1 • • • m n-1 [t n m n is a firing sequence of N , the associated trace is Λ(t 1 t 2 . . . t n ).
The trace associated to m 0 is the empty word ε. If the label of a transition is undefined then the associated word is the empty one. The traces of a net N are denoted with Traces(N ).

A subnet is a net obtained by restricting places and transitions of a net, and correspondingly the flow relation and the initial marking. Let N = ( S, T, F, Γ, Λ , m 0 ) be a net, and let T ⊆ T . We define the subnet generated by T as the net

N | T = ( S , T , F , Γ , Λ , m 0 ), where S = {s ∈ S | F (t, s) > 0 or F (s, t) > 0 for t ∈ T } ∪ {s ∈ S | m 0 (s) > 0}, F
is the flow relation restricted to S and T , Γ is obtained by Γ restricting to places in S , Λ is obtained by Λ restricting to transitions in T , and m 0 is obtained by m 0 restricting to places in S A net property (intuitively, a property of the system modeled as a Petri net) can be characterized in several ways, e.g. as a set of markings (states of the system). The following captures the intuition that, notwithstanding the state (marking) reached by the system, it is always possible to reach a state satisfying the property. A net N weakly terminates in a set of markings M iff ∀m ∈ M(N ), there is a firing sequence starting at m and leading to a marking in M. Hereafter, we shall sometimes say that N weakly terminates (without referring to any M) when the property is not relevant or clear from the context.

We now introduce occurrence nets. The intuition behind this notion is the following: regardless how tokens are produced or consumed, an occurrence net guarantees that each transition can occur only once (hence the reason for calling them occurrence nets). We adopt the notion proposed by van Glabbeek and Plotkin in [START_REF] Van Glabbeek | Configuration structures[END_REF], namely 1-occurrence nets. For a multiset M , we denote by

[[M ]] the multiset defined as [[M ]](a) = 1 if M (a) > 0 and [[M ]](a) = 0 otherwise. A state of a net N = ( S, T, F, Γ, Λ , m 0 ) is any finite multiset X of T such that the function m X : S → Z given by m X (s) = m 0 (s) + t∈T X(t) • (F (t, s) -F (s, t)),
for all s ∈ S, is a reachable marking of the net. We denote by St(N ) the states of N . A state contains (in no order) all the occurrence of the transitions that have been fired to reach a marking. Observe that a trace of a net is a suitable linearization of the elements of a state X. We use the notion of state to formalize occurrence nets. An

occurrence net O = ( S, T, F, Γ, Λ , m 0 ) is a net where each state is a set, i.e. ∀X ∈ St(N ). X = [[X]]. A net is correctly labeled iff ∀s.∀t, t ∈ • s. Γ (s) = ⊥ =⇒ Λ(t) = Λ(t ) = Γ (s).
Intuitively, this requires that all the transitions putting a token in a labeled place represent the same action.

Nets with lending places

We now relax the conditions under which transitions may be executed, by allowing a transition to consume tokens from a place s even if the s does not contain enough tokens. Consequently, we allow markings with negative numbers. When the number of tokens associated to a place becomes negative, we say that they have been done on credit. We do not permit this to happen in all places, but only in the lending places (a subset L of S). Lending places are depicted with a double circle. The notion of step is adapted to take into account this new kind of places. Let N be an LPN, let t be a transition in T , and let m be a marking. We say that t is enabled at m iff ∀s ∈ • t. m(s) ≤ 0 =⇒ s ∈ L. The evolution of N is defined as before, with the difference that the obtained marking is now a function from places to Z (instead of N). This notion matches the intuition behind of lending places: we allow a transition to be executed even when some of the transitions that are a pre-requisite have not been executed yet.

Definition 2. Let m be a reachable marking of an LPN N . We say that m is honored iff m(s) ≥ 0 for all places s of N .

An honored firing sequence is a firing sequence where the final marking is honored. Note that if the net has no lending places, then all the reachable markings are honored.

Example 2. In the net of Ex. 1, the transition c is enabled even though there are no tokens in the places p 2 and p 4 in its pre-set, as they are lending places. The other transitions are not enabled, hence at the initial marking only c may be executed (on credit). After firing c, only b can be executed. This results in putting one token in p 3 and one in p 4 , hence giving back the one taken on credit. After this, only a can be executed. Upon firing c, b and a, the marking is honored. The net is clearly a (correctly labeled) occurrence net.

We now introduce a notion of composition of LPNs. The idea is that the places with a label are places in an interface of the net (though we do not put any limitation on such places, as done instead e.g. in [START_REF] Van Der Aalst | Multiparty contracts: Agreeing and implementing interorganizational processes[END_REF]) and they never are initially marked. The labelled transitions of a net are connected with the places bearing the same label of the other. Definition 3. Let N = ( S, T, F, Γ, Λ , m 0 , L) and N = ( S , T , F , Γ , Λ , m 0 , L ) be two LPNs. We say that N, N are compatible whenever (a) they have the same set of labels, (b)

S ∩ S = ∅, (c) T ∩ T = ∅, (d) m 0 (s) = 1 implies Γ (s) = ⊥, and (e) m 0 (s ) = 1 implies Γ (s ) = ⊥. If N and N are compatible, their composition N ⊕ N is the LPN ( Ŝ, T ∪ T , F , Γ , Λ , m0 , L) in Fig. 2.
The underlying idea of LPN composition is rather simple: the sink places in a net bearing a label of a transition of the other net are removed, and places and transitions with the same label are connected accordingly (the removed sink places have places with the same label in the other net). All the other ingredients of the compound net are trivially inherited from the components. Observe that,

Ŝ = (S \ {s ∈ S | Γ (s) ∈ Λ (T ) and s • = ∅}) ∪ (S \ {s ∈ S | Γ (s ) ∈ Λ(T ) and s • = ∅}) F (ŝ, t) ⇐⇒ ŝ = s1 ∈ S ∧ t = t1 ∈ T ∧ F (s1, t1) ∨ ŝ = s2 ∈ S ∧ t = t2 ∈ T ∧ F (s2, t2) F ( t, ŝ) ⇐⇒ ŝ = s1 ∈ S ∧ t = t1 ∈ T ∧ F (t1, s1) ∨ ŝ = s2 ∈ S ∧ t = t2 ∈ T ∧ F (t2, s2) ∨ ŝ = s ∈ S ∧ t = t ∈ T ∧ Λ (t ) = Γ (s) = ⊥ ∨ ŝ = s ∈ S ∧ t = t ∈ T ∧ Λ(t) = Γ (s ) = ⊥ Γ (ŝ) = Γ (s1) if ŝ = s1 ∈ S Γ (s2) if ŝ = s2 ∈ S Λ( t) = Λ(t1) if t = t1 ∈ T Λ (t2) if t = t2 ∈ T m0(ŝ) = 1 if ŝ = s1 ∈ S and m0(s1) = 1, or ŝ = s2 ∈ S and m 0 (s2) = 1 0 otherwise L = (L ∪ L ) ∩ Ŝ Fig. 2. Composition of two LPNs.
when composing two compatible nets N and N such that Γ (S) ∩ Γ (S ) = ∅, we obtain the disjoint union of the two nets. Further, if the common label a ∈ Γ (S) ∩ Γ (S ) is associated in N to a place s with empty post-set and in N to a place s with empty post-set (or vice versa) and the labelings are injective, we obtain precisely the composition defined in [START_REF] Van Der Aalst | Multiparty contracts: Agreeing and implementing interorganizational processes[END_REF]. If the components N and N may satisfy some properties (sets of markings M and M ), the compound net N ⊕ N may satisfy the compound property (which is the set of markings M obtained obviously from M and M ).

Example 3. Consider the nets in Fig. 3. Net N fires a after b has been performed; dually, net N waits for b before firing a. These nets model two participants which protect themselves by waiting the other one to make the first step (the properties being that places p 3 and p 3 , respectively, are not marked). Clearly, no agreement is possible in this scenario. This is modelled by the deadlock in the composition N ⊕ N , where neither transitions a nor b can be fired. Consider now the LPN N , which differs from N only for the lending place p 1 . This models a participant which may fire a on credit, under the guarantee that the credit will be eventually honoured by the other participant performing b (hence, the participant modeled by N is still protected), and the property is then place p 3 unmarked and p 1 with a non negative marking. The composition N ⊕ N weakly terminates wrt the above properties, because transition a can take a token on credit from p 1 , and then transition b can be fired, so honouring the debit in p 1 . The operation ⊕ is clearly associative and commutative.

Proposition 4 Let N 1 , N 2 and N 3 be three compatible LPNs. Then,

N 1 ⊕ N 2 = N 2 ⊕ N 1 and N 1 ⊕ (N 2 ⊕ N 3 ) = (N 1 ⊕ N 2 ) ⊕ N 3 .
The composition ⊕ does not have the property that, in general, considering only the transitions of one of the components, we obtain the LPN we started with, i.e. (N 1 ⊕ N 2 )| Ti = N i . This is because the number of places with labels increases and new arcs may be added, and these places are not forgotten when considering the subnet generated by T i . However these added places are not initially marked, hence it may be that the nets have the same traces. Definition 5. Let N and N two LPNs on the same sets of labels. We say that N approximates N (N N ) iff Traces(N ) ⊆ Traces(N ). We write N ∼ N when N N and N N .

Proposition 6 For two compatible LPNs N 1 , N 2 , N i ∼ (N 1 ⊕ N 2 )| Ti , i = 1, 2.
Following [START_REF] Van Der Aalst | Multiparty contracts: Agreeing and implementing interorganizational processes[END_REF] we introduce a notion of refinement (called accordance in [START_REF] Van Der Aalst | Multiparty contracts: Agreeing and implementing interorganizational processes[END_REF]) between two LPNs. We say that M (with a property M M ) is a strategy for an LPN N (with a property M) if N ⊕ M is weakly terminating. With S(N ) we denote the set of all strategies for N . In the rest of the paper we assume that properties are always specified, even when not done explicitly.

Definition 7. An LPN N refines N if S(N ) ⊇ S(N ).
Observe that if N refines N and N weakly terminates, then N weakly terminates as well.

If a weakly terminating LPN N is obtained by composition of several nets, i.e. N = i N i , we can ask what happens if there is an N i which refines N i , for each i. The following theorem gives the desired answer. Theorem 8 Let N = i N i be a weakly terminating LPN, and assume that N i refines N i , for all i. Then, N = i N i is a weakly terminating LPN.

The theorem above gives a compositional criterion to check weak termination of a SOC application. One starts from an abstract specification (e.g. a choreography), projects it into a set of local views, and then refines each of them into a service implementation. These services can be verified independently (for refinement), and it is guaranteed that their composition still enjoys weak termination.

We now define, starting from a marking m, which actions may be performed immediately after, while preserving the ability to reach an honored marking. We call these actions urgent. Example 4. Consider the nets in Ex. 3. In N ⊕ N the only urgent action at the initial marking is a, while b is urgent at the marking where p 1 is marked. In N there are no urgent actions at the initial marking, since no honored marking is reachable. In the other nets (N , N , N ⊕ N ) no actions are urgent in the initial marking, since these nets are deadlocked.

Physical contracts

We now present a model for physical contracts based on LPNs. Let a, b, . . . ∈ T be actions, performed by participants A, B, . . . ∈ Part. We assume that actions may only be performed once. Hence, we consider a subclass of LPNs, namely occurrence nets, where all the transitions with the same label are mutually exclusive. A physical contract is an LPN, together with a set A of participants bound by the contract, a mapping π from actions to participants, and a set Ω modeling the states where all the participant in A are satisfied.

(s) = 1 =⇒ • s = ∅ ∧ Γ (s) = ⊥) ∧ (s ∈ L =⇒ Γ (s) ∈ T), (b) ∀t ∈ T. (∀s ∈ t • . Λ(t) = Γ (s)) ∧ (∃s ∈ • t. s ∈ L), (c) ∀t, t ∈ T . Λ(t) = Λ(t ) =⇒ ∃s ∈ • t ∩ • t . m 0 (s) = 1, (d) π(Λ(T )) ⊆ A.
The last constraint models the fact that only the participants in A may perform actions in D.

Given a state X of the component O of D, the reached marking m tells us which actions have been performed, and which tokens have been taken on credit. The configuration µ(m) associated to a marking m is the pair (C, Y ) defined as: The first component is the set of the labels of the transitions in X. The marking m is honored whenever the second component of µ(m) is empty.

-C = {a ∈ T | ∃s ∈ S. {s} = t∈T { • t | Λ(t) =
We now state the conditions under which two contract nets can be composed. We require that an action can be performed only by one of the components (the other may use the tokens produced by the execution of such action).

⊕ D = (O ⊕ O , A ∪ A , π • π , Ω ) where Ω = {X ∪ X | X ∈ Ω, X ∈ Ω }.
We lift the notion of weak termination to contract nets D = (O, A, π, ok , Ω).

The set of markings obtained by

Ω is M Ω = {m ∈ M(O) | µ(m) = (C, ∅), C ∈ Ω}.
We say that D weakly terminates w.r.t. Ω when O weakly terminates w.r.t. M Ω .

We also extend to contract nets the notion of urgent actions given for LPNs (Def. 9). Here, the set of urgent actions U C D is parameterized by the set C of actions already performed. Definition 13. Let D be a contract net, and let C ⊆ T. We define:

U C D = {a ∈ T | ∃Y ⊆ T. ∃m. µ(m) = (C, Y ) ∧ a is urgent at m} Example 5.
Interpret the LPN N 1 in Fig. 1 as a contract net where the actions a, b, c are associated, respectively, to participants A, B, and C, and Ω is immaterial. Then, a and c are urgent at the initial marking, whereas b is not (the token borrowed from p 1 cannot be given back). In the state where a has been fired, only b is urgent; in the state where c has been fired, no actions are urgent.

Logical contracts

In this section we briefly review Propositional Contract Logic (PCL [START_REF] Bartoletti | A calculus of contracting processes[END_REF]), and we exploit it to model contracts. PCL extends intuitionistic propositional logic IPC with a connective , called contractual implication. Intuitively, a formula b a implies a not only when b is true, like IPC implication, but also in the case that a "compatible" formula, e.g. a b, holds. PCL allows for a sort of "circular" assume-guarantee reasoning, hinted by (b a) ∧ (a b) → a ∧ b, which is a theorem in PCL . We assume that the prime formulae of PCL coincide with the atoms in T. PCL formulae, ranged over greek letters ϕ, ϕ , . . ., are defined as:

ϕ ::= ⊥ | | a | ¬ϕ | ϕ ∨ ϕ | ϕ ∧ ϕ | ϕ → ϕ | ϕ ϕ
Two proof systems have been presented for PCL : a sequent calculus [START_REF] Bartoletti | A calculus of contracting processes[END_REF], and an equivalent natural deduction system [START_REF] Bartoletti | Contract agreements via logic[END_REF], the main rules of which are shown in Fig. 4. Provable formulae are contractually implied, according to rule ( I1).

∆ ψ ∆ ϕ ψ ( I1) ∆ ϕ ψ ∆, ϕ ϕ ∆, ψ ϕ ψ ∆ ϕ ψ ( I2) ∆ ϕ ψ ∆, ψ ϕ ∆ ψ ( E)
Fig. 4. Natural deduction for PCL (rules for ).

Rule ( I2) provides with the same weakening properties of →. The crucial rule is ( E), which allows for the elimination of . Compared to the rule for elimination of → in IPC, the only difference is that in the context used to deduce the antecedent ϕ, rule ( E) also allows for using as hypothesis the consequence ψ. The decidability of the provability relation of PCL has been proved in [START_REF] Bartoletti | A calculus of contracting processes[END_REF], by exploiting the cut elimination property enjoyed by the sequent calculus.

To model contracts, we consider the Horn fragment of PCL , which comprises atoms, conjunctions, and non-nested (intuitionistic/contractual) implications. Definition 14. A PCL contract is a tuple ∆, A, π, Ω , where ∆ is a Horn PCL theory, A ⊆ Part, π : T → Part associates each atom with a participant, and Ω ⊆ ℘(T) is the set of goals of the participants.

The component A of C contains the participants which can promise to do something in C. Consequently, we shall only consider PCL contracts such that if α • a ∈ ∆, for • ∈ {→, }, then π(a) ∈ A. Example 6. Suppose three kids want to play together. Alice has a toy airplane, Bob has a bike, and Carl has a toy car. Each of the kids is willing to share his toy, but they have different constraints: Alice will lend her airplane only after Bob has allowed her ride his bike; Bob will lend his bike after he has played with Carl's car; Carl will lend his car if the other two kids promise to eventually let him play with their toys. Let π = {a → A, b → B, c → C}. The kids contracts are modeled as follows: b → a, {A}, π, {{b}} , c → b, {B}, π, {{c}} , and (a ∧ b) c, {C}, π, {{a, b}} .

A contract admits an agreement when all the involved participants can reach their goals. This is formalized in Def. 15 below. Definition 15. A PCL contract admits an agreement iff ∃X ∈ Ω. ∆ X.

We now define composition of PCL contracts. If C is the contract of an adversary of C, then a naïve composition of the two contracts could easily lead to an attack, e.g. when Mallory's contract says that Alice is obliged to give him her airplane. To prevent from such kinds of attacks, contract composition is a partial operation. We do not compose contracts which bind the same participant, or which disagree on the association between atoms and participants. We now recap from [START_REF] Bartoletti | Contract agreements via logic[END_REF] the notion of proof traces, i.e. the sequences of atoms respecting the order imposed by proofs in PCL . Consider e.g. rule (→E):

Definition 16. Two PCL contracts C = ∆, A, π, Ω and C = ∆ , A , π , Ω are compatible whenever A ∩ A = ∅, and ∀A ∈ A ∪ A . π -1 (A) = π -1 (A). If C, C are compatible, the contract C | C = ∆ ∪ ∆ , A ∪ A , π • π , Ω | Ω , where Ω | Ω = {X ∪ X | X ∈ Ω, X ∈ Ω }, is their composition. ε ∈ ∆ (ε) α → a ∈ ∆ σ ∈ ∆ α ⊆ σ σ a ∈ ∆ (→) α a ∈ ∆ σ ∈ ∆, a α ⊆ σ σ | a ⊆ ∆ ( )
∆ α → a ∆ α ∆ a (→E)
The rule requires a proof of all the atoms in α in order to construct a proof of a. Accordingly, if σ is a proof trace of ∆, then σa if a proof trace of ∆. Instead, in the rule ( E), the antecedent α needs not necessarily be proved before a: it suffices to prove α by taking a as hypothesis.

Definition 17 (Proof traces [START_REF] Bartoletti | Contract agreements via logic[END_REF]). For a Horn PCL theory ∆, we define the set of proof traces ∆ by the rules in Fig. 5, where for σ, η ∈ E * we denote with σ the set of atoms in σ, with ση the concatenation of σ and η, and with σ | η the interleavings of σ and η. We assume that both concatenation and interleaving remove duplicates from the right, e.g. aba | ca = ab | ca = {abc, acb, cab}.

The set U X C in Def. 18 contains, given a set X of atoms, the atoms which may be proved immediately after, following some proof trace of C. Definition 18 (Urgent actions [START_REF] Bartoletti | Contract agreements via logic[END_REF]). For a contract C = ∆, . . . and a set of atoms X, we define 6 From logical to physical contracts

U X C = {a ∈ X | ∃σ, σ . σ = X ∧ σ a σ ∈ ∆, X }.
In this section we show, starting from a logical contract, how to construct a physical one which preserves the agreement property. Technically, we shall relate provability in PCL to reachability of suitable configurations in the associated LPN. The idea of our construction is to translate each Horn clause of a PCL formula into a transition of an LPN, labelled with the action in the conclusion of the clause. Definition 19. Let C = ∆, A, π, Ω be a PCL contract. We define the contract net P(C) as (( S, T, F, Γ, Λ , m 0 , L), A, π, Ω) in Fig. 6.

S = (T × T ) ∪ ({a | X → a ∈ ∆} ∪ {a | X a ∈ ∆} ∪ {a | a ∈ ∆}) × { * } T = {(X, a, ) | X → a ∈ ∆} ∪ {(X, a, ) | X a ∈ ∆} F = {(s, t) | s = (a, * ), t = (X, a, z)} ∪ {(s, t) | s = (a, t), t = (X, c, z), a ∈ X} ∪ {(t, s) | s = (a, x), t = (X, a, z), x = * } Γ (s) = if s = (a, x) with x ∈ T then a else ⊥ Λ(t) = if t = (X
The transitions associated to C are a subset T of ℘(T) × T × { , }. For each intuitionistic/contractual implication, we introduce a transition as follows. A clause X a maps to (X, a, ) ∈ T , while X → a maps to (X, a, ) ∈ T . A formula a is dealt with as the clause ∅ → a. Places in S carry the information on which transition may actually put/consume a token from them (even on credit). The lending places are those places (a, t) where t = (X, c, ). Observe that a transition t = (X, a, z) puts a token in each place (a, x) with x = * , and all the transitions bearing the same labels, say a, are mutually excluding each other, as they share the unique input place (a, * ). The initial marking will contains all the places in T × { * }, and if a token is consumed from one of these places then the place will be never marked again. Furthermore the lending places are never initially marked.

Example 9. Consider the PCL contract with formula a a (the other components are immaterial for the sake of the example). The associated LPN is in Fig. 7, left. The transition ({a}, a, )), labeled a, can be executed at the initial marking, as the unmarked place in the preset is a lending place. The reached marking contains no tokens, hence it is honored. This is coherent with the fact that a a a holds in PCL . The associated LPN is the one on the right depicted in Fig. 7. The transitions are t 1 = ({b}, a, ), t 2 = ({a}, c, ) and t 3 = ({a}, b, ). Initially only t 1 is enabled, lending a token from place (b, t 1 ). This leads to a marking where both t 2 and t 3 are enabled, but only the execution of t 3 ends up with an honored marking. The marking reached after executing all the actions is honored. This is coherent with the fact that ∆ a ∧ b ∧ c holds in PCL .

(b, t1) (a, t3) (a, t2) (c, t1) (c, t2) (c, * ) (c, t3) (b, t3) (b, t2) (b, * )
Since all the transitions consume the token from the places (a, * ) (where a is the label of the transition), and these places cannot be marked again, it is easy to see that each transition may occur only once. Hence, the net associated to a contract is an occurrence net. If two transitions t, t have the same label (say a), then they cannot belong to the same state of the net. In fact, transitions with the same label share the same input place (a, * ). This place is not a lending one, and has no ingoing arcs, hence only one of the transitions with the same label may happen. The notion of correctly labeled net lifts obviously to contract nets.

Proposition 20 For all PCL contracts C, the net P(C) is correctly labeled.

A relevant property of P is that it is an homomorphism with respect to contracts composition. Thus, since both | and ⊕ are associative and commutative, we can construct a physical contract from a set of logical contracts In Theorem 23 below we state the main result of this section, namely that our construction maps the agreement property of PCL contracts into weak termination of the associated contract nets. To prove Theorem 23, we exploit the fact that C is a set of provable atoms in the logic iff (C, ∅) is a configuration of the associated contract net. Theorem 23 C admits an agreement iff P(C) weakly terminates in Ω.

We now specialize Theorem 8, which allows for compositional verification of choreographies. Assuming a choreography specified as a PCL contract C, we can (i) project it into the contracts C 1 • • • C n of its participants, (ii) construct the corresponding LPN contracts P(C 1 ) • • • P(C n ), and (iii) individually refine each of them into a service implementation. If the original choreography admits an agreement, then the composition of the services weakly terminates, i.e. it is correct w.r.t. the choreography. The notion of urgency in contract nets correspond to that in the associated PCL contracts (Theorem 25).

Theorem 25 For all PCL contracts C, and for all X ⊆ T, U X C = U X P(C) .

Example 11. Recall from Ex. 8 that, for C = {a → b, b a}, . . . , we have:

U ∅ C = {a} U {a} C = {b} U {b} C = {a} U {a,b} C = ∅
This is coherent with the fact that, in the corresponding contract net N ⊕ N in Fig. 3, only a is urgent at the initial marking, while b becomes urgent after a has been fired.

Related work and conclusions

We have investigated how to compile logical into physical contracts. The source of the compilation is the Horn fragment of Propositional Contract Logic [START_REF] Bartoletti | A calculus of contracting processes[END_REF], while the target is a contract model based on lending Petri nets (LPNs). Our compilation preserves agreements (Theorem 23), as well as the possibility of protecting services against misbehavior of malevolent services. LPN contracts can be used to reason compositionally about the realization of a choreography (Theorem 24), so extending a result of [START_REF] Van Der Aalst | Multiparty contracts: Agreeing and implementing interorganizational processes[END_REF]. Furthermore, we have given a logical characterization of those urgent actions which have to be performed in a given state. This notion, which was only intuitively outlined in [START_REF] Bartoletti | A calculus of contracting processes[END_REF], is now made formal through our compilation into LPNs (Theorem 25). Contract nets seem a promising model for reasoning on contracts: while having a clear relation with PCL contracts, they may inherit as well the whole realm of tools that are already available for Petri nets.

The notion of places with a negative marking is not a new one in the Petri nets community, though very few papers tackle this notion, as the interpretation of negative tokens does not match the intuition of Petri nets, where tokens are generally intended as resources. In this paper we have used negative tokens to model situations where actions are in a circular dependency, like the ones arising in PCL contracts. Lending places model the intuition that an action can be performed on a promise, and a negative token in a place can be interpreted as the promise made, which must be, sooner or later, honored. Indeed, the net obtained from a PCL contract is an occurrence net which may contain cycles, e.g. in the net of Ex. 10 the transition t 1 depends on t 3 , which in turn depends on t 1 (and to execute t 1 we required to lend a token which is after supplied by t 3 ). In [START_REF] Stotts | Place/transition nets with debit arcs[END_REF] the idea of places with negative marking is realized using a new kind of arc, called debit arcs. Under suitable conditions, these nets are Turing powerful, whereas our contract nets do not add expressiveness (while for LPNs the issue has to be investigated). In [START_REF] Martí-Oliet | An algebraic axiomatization of linear logic models[END_REF] negative tokens arise as the result of certain linear assumptions. The relations with LPNs have to be investigated.

Definition 1 .

 1 A lending Petri net (LPN) is a triple ( S, T, F, Γ, Λ , m 0 , L) where ( S, T, F, Γ, Λ , m 0 ) is a marked Petri net, and L ⊆ S is the set of lending places. Example 1. Consider the LPN N 1 in Fig. 1. The places p 2 and p 4 are lending places. The set of labels of the transitions is T = {a, b, c}, and the set of labels of the places is G = T. The labeling is Γ (p 1 ) = c, Γ (p 2 ) = a and Γ (p 4 ) = Γ (p 3 ) = b (the place p 0 is unlabeled).

1 Fig. 1 .

 11 Fig. 1. Two lending Petri nets.

Fig. 3 .

 3 Fig. 3. Three LPNs (top) and their pairwise compositions (bottom).

Definition 9 .

 9 For an LPN N and marking m, we say a urgent at m iff there exists a firing sequence m [t 1 • • • [t n m n with Λ(t 1 ) = a and m n honored.

Definition 10 .

 10 A contract net D is a tuple (O, A, π, Ω), where O is an occurrence LPN ( S, T, F, Γ, Λ , m 0 , L) labeled on T, A ⊆ Part, π : T → Part, Ω ⊆ ℘(T) is the set of goals of the participants, and where: (a) ∀s ∈ S. (m 0

  a} and m(s) = 0}, and -Y = {a ∈ T | ∃s ∈ S. a = Γ (s) and m(s) < 0}

Definition 11 .

 11 Two contracts nets D = (O, A, π, Ω) and D = (O , A , π , Ω ) are compatible whenever O ⊕ O is defined and A ∩ A = ∅. The composition of D and D is then the obvious extension of the one on LPNs: Definition 12. Let D = (O, A, π, Ω) and D = (O , A , π , Ω ) be two compatible contract nets. Then D

Fig. 5 .Example 7 .

 57 Fig. 5. Proof traces of Horn PCL .

Example 8 .

 8 For the contract C specified by the theory ∆ = a → b, b a, we have ∆ = {ε, ab}, and U ∅ ∆ = {a}, U {a} ∆ = {b}, U {b} ∆ = {a}, and U {a,b} ∆ = ∅.

Fig. 6 .

 6 Fig. 6. Translation from logical to physical contracts.

Fig. 7 .

 7 Fig. 7. Two contract nets constructed from PCL contracts.

  C 1 • • • C n componentwise, i.e. by composing the contract nets P(C 1 ) • • • P(C n ). Proposition 21 For all C 1 , C 2 , we have that P(C 1 | C 2 ) ∼ P(C 1 ) ⊕ P(C 2 ).

Lemma 22

 22 Let C = ∆, A, π, Ω be a PCL contract, and let P(C) = (O, A, π, Ω). For all C ⊆ T, ∆ C iff there exists m ∈ M(O) such that µ(m) = (C, ∅).

Theorem 24

 24 Let C = C 1 | • • • | C n admit an agreement, with Ω i goals of C i . If D i refines P(C i ) for i ∈ 1..n, then D 1 ⊕• • •⊕D n weakly terminates in Ω 1 ∪• • •∪ Ω n .

The word step is usually reserved to the execution of a subset of transitions, but here we prefer to stress the computational interpretation.

Acknowledgments. We thank Philippe Darondeau, Eric Fabre and Roberto Zunino for useful discussions and suggestions. This work has been partially supported by Aut. Reg. of Sardinia grants L.R.7/2007 CRP2-120 (TESLA) CRP-17285 (TRICS) and P.I.A. 2010 ("Social Glue"), and by MIUR PRIN 2010-11 project "Security Horizons".


Hassan Hatefi
email: hhatefi@depend.cs.uni-saarland.de

Holger Hermanns
email: hermanns@cs.uni-saarland.de

Improving Time Bounded Reachability Computations in Interactive Markov Chains

Interactive Markov Chains (IMCs) are compositional behaviour models extending both Continuous Time Markov Chain (CTMC) and Labeled Transition System (LTS). They are used as semantic models in different engineering contexts ranging from ultramodern satellite designs to industrial system-on-chip manufacturing. Different approximation algorithms have been proposed for model checking of IMC, with time bounded reachability probabilities playing a pivotal role. This paper addresses the accuracy and efficiency of approximating time bounded reachability probabilities in IMC, improving over the state-of-the-art in both efficiency of computation and tightness of approximation. Experimental evidence is provided by applying the new method on a case study.

Introduction

Why IMCs? Over the last decade, a formal approach to quantitative performance and dependability evaluation of concurrent systems has gained maturity. At its root are continuous-time Markov chains for which efficient and quantifiably precise solution methods exist [START_REF] Baier | Efficient computation of time-bounded reachability probabilities in uniform continuous-time Markov decision processes[END_REF]. On the specification side, continuous stochastic logic (CSL) [START_REF] Aziz | Towards Performance Prediction of Verifying Continuous Time Markov Chains[END_REF][START_REF] Baier | Efficient computation of time-bounded reachability probabilities in uniform continuous-time Markov decision processes[END_REF] enables the specification of a large spectrum of performance and dependability measures. A CTMC can be viewed as a labelled transition system (LTS) whose transitions are delayed according to exponential distributions. Opposed to classical concurrency theory models, CTMCs neither support compositional modelling [START_REF] Hermanns | Automated compositional Markov chain generation for a plain-old telephone system[END_REF] nor do they allow nondeterminism in the model. Among several formalisms that overcome these limitations [START_REF] Böde | Compositional Dependability Evaluation for STATEMATE[END_REF][START_REF] Hermanns | Interactive Markov Chains: The Quest for Quantified Quality[END_REF][START_REF] Hillston | A Compositional Approach to Performance Modelling[END_REF][START_REF] Macià | sPBC: A Markovian Extension of Petri Box Calculus with Immediate Multiactions[END_REF], interactive Markov chains (IMCs) [START_REF] Hermanns | Process algebra for performance evaluation[END_REF] stand out. IMCs conservatively extend classical concurrency theory with exponentially distributed delays, and this induces several further benefits [START_REF] Bravetti | YMCA -Why Markov Chain Algebra ?[END_REF]. In particular, it enables compositional modelling with intermittent weak bisimulation minimisation [START_REF] Hermanns | Interactive Markov Chains: The Quest for Quantified Quality[END_REF] and allows to augment existing untimed process algebra specifications with random timing [START_REF] Böde | Compositional Dependability Evaluation for STATEMATE[END_REF]. Moreover, the IMC formalism is not restricted to exponential delays but allows to encode arbitrary phase-type distributions such as hyper-and hypoexponentials [START_REF] Pulungan | Reduction of Acyclic Phase-Type Representations[END_REF]. Since IMCs smoothly extend classical LTSs, the model has received attention in academic as well as in industrial settings [START_REF] Boudali | Mariëlle Stoelinga: Architectural dependability evaluation with Arcade[END_REF][START_REF] Coste | Quantitative Evaluation in Embedded System Design: Validation of Multiprocessor Multithreaded Architectures[END_REF][START_REF] Coste | Towards Performance Prediction of Compositional Models in Industrial GALS Designs[END_REF][START_REF] Esteve | Formal correctness, safety, dependability and performance analysis of a satellite[END_REF].

Why time bounded reachability? The principles of model checking IMCs are by now well understood. One analysis strand, implemented for instance in CADP [START_REF] Garavel | CADP 2010: A Toolbox for the Construction and Analysis of Distributed Processes[END_REF], resorts to CSL model checking of CTMCs. But this is only applicable if the weak bisimulation quotient of the model is indeed a CTMC, which cannot be always guaranteed. This is therefore a partial solution technique, albeit it integrates well with compositional construction and minimisation approaches, and is the one used in industrial applications. The approximate CSL model checking problem for IMCs has been solved by Neuhäusser and Zhang [START_REF] Martin | Neuhäusser: Model Checking Nondeterministic and Randomly Timed Systems[END_REF][START_REF] Zhang | Neuhäusser: Model Checking Interactive Markov Chains[END_REF]. Most of the solution resorts to untimed model checking [START_REF] Bianco | Model checking of probabilistic and nondeterministic systems[END_REF]. The core innovation lies in the solution of the time bounded model checking problem, that is needed to quantify a bounded until formula subject to a (real-valued) time interval. The problem is solved by splitting the time interval into equally sized digitisation steps, each small enough such that with high probability at most one Markov transition occurs in any step.

However, the practical efficiency and accuracy of this approach to evaluate time bounded reachability probabilities turns out substantially inferior to the one known for CTMCs, and this limits applicability to real industrial cases. As a consequence, model checking algorithms for other, less precise, but still highly relevant properties have been coined [START_REF] Guck | Neuhäusser: Quantitative Timed Analysis of Interactive Markov Chains[END_REF], including expected reachability and long run average properties.

Our contribution. We revisit the approximation of time bounded reachability probabilities so as to arrive at an improved computational approach. For this, we generalise the digitisation approach of Neuhäusser and Zhang [START_REF] Martin | Neuhäusser: Model Checking Nondeterministic and Randomly Timed Systems[END_REF][START_REF] Zhang | Neuhäusser: Model Checking Interactive Markov Chains[END_REF] by considering the effect of multiple Markov transition firings in a time interval of length δ. We show that this can be exploited by a tighter error bound, and thus a more accurate computation. We put the theoretical improvement into practice by proposing a new algorithm to solve time bounded reachability in IMCs. Empirical results demonstrate that the improved algorithm can gain more than one order of magnitude speedups.

Interactive Markov Chain

An Interactive Markov Chain (IMC) is a model that generalises both CTMC and LTS. In this section, we provide the definition of IMC and the necessary concepts relating to it.

Definition 1 (IMC).

An IMC [START_REF] Hermanns | Interactive Markov Chains: The Quest for Quantified Quality[END_REF] is a tuple M = (S, Act, -→, , s 0 ), where -S is a finite set of states, -Act is a set of actions, including τ , representing the internal invisible action,

--→⊂ S × Act × S is a set of interactive transitions, - ⊂ S × R ≥0 × S is a set of Markov transitions, -s 0 is the initial state.
Maximum progress vs. urgency. States of an IMC are partitioned into interactive, Markov and hybrid. Interactive (Markov) states have only interactive (Markov) outgoing transitions, while hybrid states have transitions of both types. Let S I , S M and S H be the set of interactive, Markov and hybrid states respectively. An IMC might have states without any outgoing transition. For the purpose of this paper, any such state is turned into a Markov state by adding a self loop with an arbitrary rate. We distinguish between closed and open IMCs. An open IMC can interact with the environment and in particular, can be composed with other IMCs, e.g. via parallel composition. For such models, a maximum progress assumption [START_REF] Hermanns | Interactive Markov Chains: The Quest for Quantified Quality[END_REF] is imposed which implies that τ -transitions take precedence over Markov transitions whenever both are enabled in a state. In contrast, a closed IMC is not subject to any further communication and composition. In this paper, we assume that the models we are going to analyse are closed, and impose the stronger urgency assumption which means that any interactive transition has precedence over Markov transitions, i.e. interactive transitions are taken immediately whenever enabled in a state, leaving no chance for enabled Markov transitions. Consequently, in a closed IMC, hybrid states can be regarded as interactive states.

Branching probabilities. A (probability) distribution µ over a discrete set S is a function µ : S [0, 1] such that s∈S µ(s) = 1. If µ(s) = 1 for some s ∈ S, µ is a Dirac distribution denoted by µ s . Let Dist(S) be the set of all distributions over set S. For uniformity of notations, we use a distinguished action ⊥ / ∈ Act to indicate Markov transitions and extend the set of actions to Act ⊥ = Act • ∪ {⊥}. For s ∈ S, we define Act ⊥ (s) as the set of enabled actions in state s. If s is a Markov state, Act ⊥ (s) = {⊥}, otherwise Act ⊥ (s) = {α | (s, α, s ) ∈ -→}. The rate between state s and s is defined by rate(s, s ) = (s,λ,s )∈ λ. Then E(s) = s ∈S rate(s, s ) denotes the sum of outgoing rates of state s. Using these concepts, we define the branching probability matrix for both interactive and Markov states by Let M be the IMC in Figure 1. s 1 and s 3 are Markov states, while s 2 is an interactive state. Initial state s 0 is a hybrid state, since it has both interactive and Markov transitions enabled. Considering M as a closed IMC, the urgency assumption allows us to ignore (s 0 , 0.5, s 2 ) ∈ and consider s 0 as an interactive state. Under this assumption, interactive transitions are instantaneously fired after zero time delay. Conversely, the sojourn time in a Markov state s is exponentially distributed with rate E(s). For example, the probability to leave s 1 within δ time unit is 1-e -5δ (E(s 1 ) = 2+3 = 5). At this point, branching probabilities determine the distribution of evolving to next states. For s 1 , P(s 1 , ⊥, s 0 ) = 2 and P(s 1 , ⊥, s 3 ) = 3 5 , as a result the probabilities to go to s 0 and s 3 after spending at most δ time unit in s 1 are 2 5 (1e -5δ ) and 3 5 (1e -5δ ) respectively.

P(s, α, s ) =      1 s ∈ S I ∧ (s, α, s ) ∈-→ rate(s,s ) E(s) s ∈ S M ∧ α = ⊥ 0 otherwise s 0 s 1 s 2 s 3 τ b 0.5
Behavioural aspects. Like in other transition systems, an execution in an IMC is described by a path. Formally, a finite path is a finite sequence π = s 0 t0,α0

---→

s 1 • • • s n-1 tn-1,αn-1 -------→ s n with α i ∈ Act ⊥ , t i ∈ R ≥0 , i = 0 • • • n -1.
We use |π| = n as the length of π and last(π) = s n as the last state of π. Each step of a path π describes how the IMC evolves from one state to the next, with what action and after spending what state sojourn time. For example, when the IMC is in an interactive state s ∈ S I , it must immediately (in zero time) choose some action α ∈ Act ⊥ (s) and go to state s . This gives rise to the finite path s 0,α --→ s . On the other hand, if s ∈ S M , the IMC can stay for t > 0 time units and then choose the next state s based on the distribution P(s, ⊥, •) by s t,⊥ --→ s . An infinite path specifies an infinite execution of an IMC. We use Paths * and Paths ω to denote the set of finite and infinite paths, respectively. By dropping the sojourn times from a path, we obtain the time-abstract path. We use subscript ta to refer to the set of time-abstract finite and infinite paths (i.e. Paths * ta and Paths ω ta ).

Resolving nondeterminism. In states with more than one interactive transitions, the resolution of the transition to take is nondeterministic, just as in the LTS setting. This nondeterminism is resolved by schedulers. The most general scheduler class maps a finite and possibly timed path to a distribution over the set of interactive transitions enabled in the last state of the path:

Definition 2 (Generic Scheduler). A generic scheduler over IMC M = (S, Act, -→, , s 0 ) is a function, A : Paths * Dist(-→), where the support of A(π) is a subset of ({last(π)} × Act × S)∩ -→ and last(π) ∈ S I .

For a finite path π, a scheduler specifies how to resolve nondeterminism on the last state of π which is an interactive state. It gives a distribution over the set of enabled transitions of last(π). We use the term Gen to refer to the set of all generic schedulers. Following the definition of schedules, the probability measure can be uniquely defined over the σ-algebra on Paths ω , given scheduler A and initial state s, denoted by Pr ω A,s [START_REF] Martin | Neuhäusser: Model Checking Nondeterministic and Randomly Timed Systems[END_REF].

Non-zenoness. Owing to the presence of immediate state changes, an IMC might exhibit Zeno behaviour, where infinitely many interactive transitions are taken in finite or zero time. This is an unrealistic phenomenon, characterised by an infinite path π, where the time spent on π does not diverge, called a Zeno path. To exclude such unrealistic phenomena, we restrict our attention to models where the probability of Zeno behaviour is zero. This means that ∀A ∈ Gen, ∀s ∈ S. Pr ω A,s (Π <∞ ) = 0, where Π <∞ is the set of all Zeno paths. This condition implies that starting from any interactive states, we must reach the set of Markov states with probability one. In the remainder of this paper, we therefore restrict to such models.

Time Bounded Reachability

CSL model checking of time bounded until properties plays a pivotal role in quantitative evaluation of IMCs. It can be reduced to time bounded reachability analysis, by a well-known technique [START_REF] Baier | Modelchecking algorithms for continuous-time Markov chains[END_REF] of making target states absorbing. This section reviews the current state-of-the-art [START_REF] Martin | Neuhäusser: Model Checking Nondeterministic and Randomly Timed Systems[END_REF][START_REF] Zhang | Neuhäusser: Model Checking Interactive Markov Chains[END_REF] of solving time bounded reachability problems in IMC. Section 4 will discuss how can we improve upon that.

Fixed point characterisation. We first discuss the fixed point characterisation for the maximum probability to reach a set of goal states within an interval of time. For this, let I and Q be the set of all nonempty nonnegative real intervals with real and rational bounds respectively. For I ∈ I and t ∈ R ≥0 , we define

I t = {x -t | x ∈ I ∧ x ≥ t}. If I ∈ Q and t ∈ Q ≥0 , then I t ∈ Q. Given IMC M,
a time interval I ∈ I and a set of goal states G ⊆ S, the set of all paths that reach the goal states within interval I is denoted by ♦ I G. Let p M max (s, ♦ I G) be the maximum probability of reaching the goal states within interval I if starting in state s at time 0. In formal terms, it is the supremum ranging over all possible Gen schedulers, of the probability measures on the induced paths:

p M max (s, ♦ I G) = sup A∈Gen Pr ω A,s (♦ I G). The next lemma recalls a characterisation of p M max (s, ♦ I G) as a fixed point. That of p M min (s, ♦ I G) is dealt with similarly.
1. For s ∈ S M Ω(F )(s, I) = b 0 E(s)e -E(s)t s ∈S P(s, ⊥, s )F (s , I t) dt s / ∈ G e -E(s)a + a 0 E(s)e -E(s)t s ∈S P(s, ⊥, s )F (s , I t) dt s ∈ G 2. For s ∈ S I Ω(F )(s, I) = 1 s ∈ G ∧ 0 ∈ I max (s,α,s )∈-→ F (s , I) otherwise
Interactive Probabilistic Chain. The above characterisation provides an integral equation system of the maximum time interval bounded reachability probability. But this system is in general not directly tractable algorithmically [START_REF] Baier | Modelchecking algorithms for continuous-time Markov chains[END_REF]. To circumvent this problem, the fixed point characterisation can be approximated by a digitisation [START_REF] Martin | Neuhäusser: Model Checking Nondeterministic and Randomly Timed Systems[END_REF][START_REF] Zhang | Neuhäusser: Model Checking Interactive Markov Chains[END_REF] approach. Intuitively, the time interval is split into equally sized intervals, which we call digitisation steps. It is assumed that the digitisation constant δ is small enough such that with high probability it carries at most one Markov transition firing. This assumption reduces an IMC to an Interactive Probabilistic Chain (IPC) [START_REF] Coste | Towards Performance Prediction of Compositional Models in Industrial GALS Designs[END_REF]. An IPC is a digitised version of IMC, obtained by summarising the behaviour of an IMC at equidistant time points. A digitised Markov transition specifies with which probability a state evolves to its successors after taking one time step. The notion of digitised Markov transition resembles the one-step transition matrix in DTMC. The concepts of closed and open models carry over to IPC. As we do not have the notion of continuous time, paths in IPC can be seen as time-abstract paths in IMC, implicitly still counting digitisation steps, and thus discrete time.

Digitisation from IMC to IPC. We now recall the digitisation that turns an IMC into an IPC. Afterwards, we explain how reachability computation in an IMC can be approximated by analysis on IPC, for which there exists a proved error bound.

Definition 4 (Digitisation [START_REF] Martin | Neuhäusser: Model Checking Nondeterministic and Randomly Timed Systems[END_REF]). Given IMC M = (S, Act, -→, , s 0 ) and a digitisation constant δ, M δ = (S, Act, -→, δ , s 0 ) is an IPC constructed from digitisation of M with respect to digitisation constant δ and δ = {(s, µ s )|s ∈ S M }, where

µ s (s ) = (1 -e -E(s)δ )P(s, ⊥, s ) s = s (1 -e -E(s)δ )P(s, ⊥, s ) + e -E(s)δ s = s
The digitisation in Definition 4 approximates the original model by assuming that at most one Markov transition in M can fire in each step of length δ. It is specified by distribution µ s , which contains the probability of having either one or no Markov transition in M from state s within a time interval of length δ. Using the fixed point characterisation above, it is possible to relate reachability analysis in an IMC to reachability analysis in its associated IPC [START_REF] Martin | Neuhäusser: Model Checking Nondeterministic and Randomly Timed Systems[END_REF], together with an error bound. We recall the result here:

Theorem 1 (Error Bound [START_REF] Martin | Neuhäusser: Model Checking Nondeterministic and Randomly Timed Systems[END_REF]). Given IMC M = (S, Act, -→, , s 0 ), a set of goal states G ⊆ S, a time interval I ∈ Q such that a = inf I and b = sup I with 0 ≤ a < b. and λ = max s∈S M E(s). Assume digitisation step δ > 0 is selected such that b = k b δ and a = k a δ for some k b , k a ∈ N. For all s ∈ S it holds

p M δ max (s, ♦ (ka,k b ] G) -k a (λδ) 2 2 ≤ p M max (s, ♦ I G) ≤ p M δ max (s, ♦ (ka,k b ] G) + k b (λδ) 2 2 + λδ
For the proof of Theorem 1 see [26, Theorem 6.5].

Time bounded computation in IPC. We briefly review the maximum time bounded reachability computation in IPC [START_REF] Zhang | Neuhäusser: Model Checking Interactive Markov Chains[END_REF]. At its core, a modified value iteration algorithm is carried out. Given an IPC, a set of goal states and a step interval, the algorithm iteratively proceeds by taking two different phases. In the first phase, reachability probabilities starting from all interactive states are updated. This is done by selecting the maximum from reachability probabilities of Markov states that are reachable from each interactive state. The second phase updates the reachability probabilities from Markov states by taking a digitised time step. The algorithm iterates until the last digitised time step is processed. For more details about the algorithm we refer to [START_REF] Zhang | Neuhäusser: Model Checking Interactive Markov Chains[END_REF].

Improving Time Bounded Reachability Computation

In this section, we generalise the previously discussed technique for computing maximum time bounded reachability. As before, we approximate the fixed point characterisation of IMC using a digitisation technique. However instead of considering at most one, we consider at most n Markov transition firing(s) in a digitisation step, for n being an arbitrary natural number. This enables us to establish a tighter error bound. Alternatively, an increased n lets us to choose a larger digitisation constant δ, without compromising the original error bound. A larger digitisation constant implies fewer iterations, thus speeding up the overall runtime of the algorithm.

Higher-order approximation. When developing an approximation of n-th order of the maximum reachability probability, we first restrict ourselves to intervals with zero lower bounds.

Definition 5. Given IMC M = (S, Act, -→, , s 0 ), a set of goal states G ⊆ S, an interval I ∈ Q such that inf I = 0 and sup

I = b. Assume digitisation step δ > 0 is selected such that b = k b δ for some k b ∈ N. We define p M δ (n) max (s, ♦ I G) = 1 if s ∈ G, and for s ∈ S \ G: p M δ (n) max (s, ♦ I G) = A n I,n (s, δ) s ∈ S M \ G max (s,α,s )∈-→ p M δ (n) max (s , ♦ I G) s ∈ S I \ G and for 0 ≤ k ≤ n and 0 ≤ ∆ ≤ δ: A k I,n (s, ∆) =          ∆ 0 E(s)e -E(s)t s ∈S P(s, ⊥, s )A k-1 I,n (s , ∆ -t) dt + e -E(s)∆ p M δ (n) max (s, ♦ I δ G) s ∈ S M \ G ∧ k > 0 p M δ (n) max (s, ♦ I δ G) s ∈ S M \ G ∧ k = 0 max (s,α,s )∈-→ A k I,n (s, ∆) s ∈ S I \ G Intuitively A k I,n (s, ∆)
is the maximum probability to reach G from state s inside I (δ -∆) by having up to k Markov transition(s) in the first ∆ time unit and up to n Markov transition(s) in each digitisation step δ afterwards. This approximation represents the behaviour of the original model more faithfully, thus leading to a better error bound. Theorem 2 quantifies the quality of this approximation.

Theorem 2. Given IMC M = (S, Act, -→, , s 0 ), a set of goal states G ⊆ S, an interval I ∈ Q with inf I = 0, sup I = b and λ = max s∈S M E(s). Assume digitisation step δ > 0 is selected such that b = k b δ for some k b ∈ N and n > 0 is the order of approximation. For all s ∈ S it holds

p M δ (n) max (s, ♦ I G) ≤ p M max (s, ♦ I G) ≤ p M δ (n) max (s, ♦ I G) + 1 -e -λb n i=0 (λδ) i i! k b
The proof of Theorem 2 is tedious, basically following and generalising the proof of [START_REF] Martin | Neuhäusser: Model Checking Nondeterministic and Randomly Timed Systems[END_REF]Theorem 6.3]. We provide the proof for the case n = 2 in the appendix and discuss how it can be extended to the general case. The core insight is, intuitively speaking, as follows. We can view the error as the probability of more than n Markov transition(s) firing in at least one digitisation step. Due to independence of the number of Markov transition occurrences in digitisation steps, this probability can be upper bounded by k b independent Poisson processes, all parametrised with the maximum exit rate exhibited in the IMC. In each Poisson process the probability of at most n Markov transition(s) firing in one digitisation step is e -λδ n i=0 (λδ) i i! , therefore the probability of a violation of this assumption in at least one digitisation step is 1e -λb n i=0

(λδ) i i! k b .
It is worthwhile to note that open and closed intervals of type (0, b] and [0, b] are treated in the same manner based on Theorem 2. They lead to the same fixed point computation of time bounded reachability, in contrast to bounded until [START_REF] Zhang | Automata-Based CSL Model Checking[END_REF]. We can directly extend Definition 5 to intervals with non-zero lower bounds and adapt Theorem 2 accordingly. Theorem 3. Given IMC M = (S, Act, -→, , s 0 ), a set of goal states G ⊆ S, an interval I ∈ Q with inf I = a > 0, sup I = b > a and λ = max s∈S M E(s). Assume digitisation step δ > 0 is selected such that a = k a δ and b = k b δ for some k a , k b ∈ N and n > 0 is the order of approximation. For all s ∈ S it holds

p M δ (n) max (s, ♦ I G) -1 -e -λa n i=0 (λδ) i i! ka ≤ p M max (s, ♦ I G) ≤ p M δ (n) max (s, ♦ I G) + 1 -e -λb n i=0 (λδ) i i! k b
The proof of Theorem 3 combines the one of Theorem 2 and of [START_REF] Martin | Neuhäusser: Model Checking Nondeterministic and Randomly Timed Systems[END_REF]Theorem 6.4].

It is worth noting that the digitisation error decreases by decreasing digitisation step δ or increasing the order of approximation n. Further, the error vanishes as n goes to infinity or δ goes to zero.

Improved algorithm. In this section we describe how the result of Theorem 2 and 3 can improve the original time bounded reachability approximation [START_REF] Zhang | Neuhäusser: Model Checking Interactive Markov Chains[END_REF]. The structure of the algorithm remains unchanged, but is parametrised with natural n. It computes p

M δ (n) max
as the approximation of the maximum reachability probability. Our objective is to compute maximum probability to reach a set of goal states within a given step interval. First we restrict ourselves to the case that the lower bound of the step interval is zero. Afterwards, we extend it to the general case. Let M be an IMC, G ⊆ S be a set of goal state and I ∈ Q be a nonempty interval with inf I = 0 and sup

I = b. Assume digitisation step δ > 0 is selected such that b = k b δ for some k b ∈ N. We use p M δ (n)
max (s, ♦ I G) to denote the approximate maximum probability of reaching the goal states inside I where we only consider up to n Markov transition firing(s) within each digitisation step. Let Reach i (s) be the set of states that can be reached from s by only using interactive transitions.

The overall algorithm is depicted in Algorithm 1. It proceeds by backwards unfolding the IMC in an iterative manner, starting from the goal states. At the beginning, all goal states are made absorbing: all of their transitions are removed, Input : M is the given IMC, G ⊆ S is the set of goal state, I is the interval with inf I = 0 and sup I = b, δ > 0 such that b = k b δ for some k b ∈ N Output: Maximum reachability probabilities starting from all states begin make all s ∈ G in M absorbing ;

foreach s ∈ G do p M δ (n) max (s, ♦ [0,0] G) := 1 ; foreach s ∈ S \ G do p M δ (n) max (s, ♦ [0,0] G) := 0; foreach s ∈ SI do p M δ (n) max (s, ♦ [0,0] G) := max s ∈Reach i (s)∩S M p M δ (n) max (s , ♦ [0,0] G); for j := k b -1 to 0 do // m-phase ; foreach s ∈ SM do calculate p M δ (n) max (s, ♦ I jδ G) as in Definition 5 ; // i * -phase ; foreach s ∈ SI do p M δ (n) max (s, ♦ I jδ G) := max s ∈Reach i (s)∩S M p M δ (n) max (s , ♦ I jδ G) ; end end
Algorithm 1: Computing maximum step bounded reachability and replaced by a digitised Markov self loop (a transition to a Dirac distribution over the source state). The initial value of probability vector is set to one for goal states and to zero otherwise. The algorithm then proceeds by intertwining m-phases and i * -phases consecutively for k b steps. In each iteration, i * -phase and m-phase update reachability probabilities from interactive and Markov states to the set of goal states respectively. After completing i * -phase and m-phase at the end of an iteration, the elements of p M δ (n) max (•, ♦ I jδ G) are updated for both interactive and Markov states.

Phases of an iteration. In the following we explain the functioning of i * -phase and m-phase in more details. An i * -phase maximises the reachability probabilities starting from interactive states to the set of goal states. By the law of total probability, this can split into two parts: (1) the probability of reaching Markov states from interactive states in zero time and (2) the probability of reaching goal states from Markov states. The latter has been computed by the m-phase directly preceding the i * -phase under consideration. The former can be computed by a backward search in the interactive reachability graph underlying the IMC [START_REF] Zhang | Neuhäusser: Model Checking Interactive Markov Chains[END_REF]. The number of transitions taken does not matter in this case, because they take zero time each. This step thus needs the set of all Markov states that are reachable from each interactive state s via an arbitrary number of interactive transitions. That set, Reach i (s) ∩ S M , can be precomputed prior to the algorithm. From these sets, the i * -phase selects states with maximum reachability probability. In an m-phase, we update the reachability probabilities starting from Markov states by taking at most n Markov transitions. This step is performed by solving the integral equation in Definition 5 for case s ∈ S M \ G. Restricting the number n of Markov transitions in a digitisation step makes the integral equation in Definition 5 tractable, in contrast to Lemma 1. For instance, in the first-order approximation (n = 1) it is enough to consider zero or one Markov transition starting from a Markov state. Owing to this assumption the resulting model (M δ (1)) is equivalent to the induced IPC (M δ ) from the original model with respect to digitisation step δ. For the second-order approximation we need to consider up to two Markov transitions starting from a Markov state.

Example 2. We now discuss by example how i * -and m-phases are performed for n = 2. Assume Figure 2 is a fragment of an IMC C with a set of goal states G. Given time interval I = [0, b] with b > 0 and digitisation step δ, the vector p

C δ (2) max (•, ♦ I δ G) has been computed for all states of C. The aim is to compute p C δ (2)
max (s 0 , ♦ I G). From Definition 5 we have:

p C δ (2) max (s 0 , ♦ I G) = A 2 I,2 (s 0 , ∆) = δ 0 2e -2t A 1 I,2 (s 1 , δ -t) dt + e -2δ p C δ (2) max (s 0 , ♦ I δ G)
For s 1 we have

A 1 I,2 (s 1 , δ-t) = max{A 1 I,2 (s 3 , δ-t), A 1 I,2 (s 5 , δ-t)}, since Reach i (s 1 )∩ S M = {s 3 , s 5 }.
From Definition 5 for s 3 and s 5 we have:

A 1 I,2 (s 3 , δ -t) = δ-t 0 3e -3t A 0 I,2 (s 4 , δ -t -t ) dt + e -3(δ-t) p C δ (2) max (s 3 , ♦ I δ G) = (1 -e -3(δ-t) )p C δ (2) max (s 4 , ♦ I δ G) + e -3(δ-t) p C δ (2) max (s 3 , ♦ I δ G)
Similar calculations give:

A 1 I,2 (s 5 , δ -t) = (1 -e -5(δ-t) )p C δ (2) max (s 6 , ♦ I δ G) + e -5(δ-t) p C δ (2) max (s 5 , ♦ I δ G). s 0 s 1 s 2 s 3 s 5 s 4 • • • s 6 • • • 2 τ τ τ 3 5

Fig. 2. An exemplary IMC fragment

Generalisation to intervals with nonzero lower bound. We can generalise time bounded reachability computation just discussed to intervals with non-zero error bound, following a recipe discussed in [START_REF] Baier | Modelchecking algorithms for continuous-time Markov chains[END_REF]. Assume we choose interval I such that inf I = a > 0 and sup I = b > a. We break the interval into two parts, first from b down to a and second from a down to zero. Within the first, we are interested in reaching one of the goal states, as a result we make the goal states absorbing. Nevertheless, within the second, it does not matter that the model is in one of the goal states, which consequently leads us to ignore goal states and reintroduce them as before.

Accordingly the algorithm proceeds as follows. In the first part ([0, ba]), goal states are made absorbing and reachability probabilities are computed by running Algorithm 1. The result will be used as the initial vector of the next step. Then, goal states are treated as normal states, so we undo absorbing of goal states and set G = ∅. However other calculations remain the same as before.

Complexity and efficiency. The key innovation of this approach lies in both the precision and the efficiency of the computation. Following Theorems 2 and 3, the number of iterations required to guarantee accuracy level can be calculated by determining the least k b such that 1e -λb n i=0

(λδ) i i! k b ≤ . The inequality however does not have closed-form solution with respect to k b . Routine calculus allows us to derive that 1e -λb n i=0

(λδ) i i! k b ≤ k b (λδ) n+1
(n+1)! which is tight in our setting, since λδ is very small. Thus, we instead consider inequality k b

(λδ) n+1 (n+1)! ≤ which leads to k b ≥ λb λb (n+1)! 1 n
. This shows how the number of iterations required to achieve a predefined accuracy level decreases by increasing the order of approximation n. In other words, using higher-order approximations gives the same error bound in less iterations.

To shed some light on this, we compare the complexity of the original firstorder and the second-order instance of the novel approximation.

O N 2.376 + M 2 + M N + N 2 (bλ) 3 , while the complexity of the first-order approximation is O N 2.376 + (M + N 2 ) (bλ) 2 [29]
. We observe that the per iteration complexity of the second-order approximation is higher, but since in almost all cases M is at least N this is a negligible disadvantage. At the same time, the number of iterations (the respective last terms) is much less. Therefore the efficiency of the second-order approximation compares favourably to the original first-order approximation, at least in theory. In the next section we compare the complexity of both algorithms in practice.

A Simplified Empirical Evaluation

This section reports on empirical results with an implementation that harvests the theoretical advances established, but is simplified in one dimension: Our current implementation keeps the scheduler decisions constant over each time interval of length δ, even though a timed scheduler may perform slightly better by adjusting the decision during the interval, and not at interval boundaries only. We do not yet have an error bound for the deviation introduced by this simplification. In light of the above discussion, we consider n = 2, thus we use a second-order approximation, and compare with the original first-order approximation.

Case study. As a case study we consider a replicated file system as it is used as part of the Google search engine [START_REF] Cloth | Haverkort: Model Checking for Survivability[END_REF]. The IMC specification is available as an example of IMCA tool [START_REF] Guck | Quantitative Analysis of Markov Automata Master Thesis[END_REF]. The Google File System (GFS) splits files into chunks of equal size maintained by several chunk servers. If a user wants to access a chunk, it asks a master server which store the address of all chunks. Then the user can directly access the appropriate chunk server to read/write the chunk. The model contains three parameters, N cs is the number of chunk server, C s is the number of chunks a server may store, and C t is the total number of chunks.

Evaluation. We set C s = 5000 and C t = 100000 and change the number of chunk servers N cs . The set of goal states G is defined as states in which the master server is up and there is at least one copy of each chunk available. We compute minimum and maximum time bounded reachability with respect to the set of goal states G using both the first-and the second-order approximations on different intervals of time. The former has been implemented in the IMCA tool [START_REF] Guck | Quantitative Analysis of Markov Automata Master Thesis[END_REF], and our implementation is derived from that. All experiments were conducted on a single core of a 2.5 GHz Intel Core i5 processor with 4GB RAM running on Linux. The computation times of both algorithm under different parameter settings are reported in Table 1.

As stated before, the second-order algorithm takes less iterations for computing reachability to guarantee accuracy . The computation times reported apparently show a beneficial effect, with the speedup depending on different parameters. Table 1 indicates that the speedup gets higher with increasing λ and with increasing interval upper bounds.

Conclusions

This paper has presented an improvement of time bounded reachability computations in IMC, based on previous work [START_REF] Zhang | Neuhäusser: Model Checking Interactive Markov Chains[END_REF], which has established a digitisation approach for IMC, together with a stable error bound. We have extended this theoretical result by assuming at most n Markov transitions to fire in each digitisation step, where previously n = 1 was assumed. In practice, setting n = 2 already provides a much tighter error bound, and thus saves considerable computation time. We have demonstrated the effectiveness of the approach in our empirical evaluation with speedups of more than one order of magnitude, albeit for a simplified scheduler scenario.

Lately, model checking of open IMC has been studied, where the IMC is considered to be placed in an unknown environment that may delay or influence the IMC behaviour via synchronisation [START_REF] Brázdil | Verification of Open Interactive Markov Chains[END_REF]. The approach resorts to the approximation scheme laid out in [START_REF] Zhang | Neuhäusser: Model Checking Interactive Markov Chains[END_REF], which we have improved upon in the present paper. Therefore, our improvement directly carries over to the open setting. As a future work, we intend to further generalise the proposed algorithm to Markov Automata [START_REF] Eisentraut | On Probabilistic Automata in Continuous Time[END_REF][START_REF] Deng | On the Semantics of Markov Automata[END_REF][START_REF] Hatefi | Model Checking Algorithms for Markov Automata[END_REF].

We have to prove that: (2) max (s, ♦ I G) ≤ p M max (s, ♦ I G) ≤ p M δ (2) max (s, ♦ I G) + 1e -λb 2 i=0

p M δ
(λδ

) i i! k b
In the following, we prove the upper bound of the approximation. For the proof of lower bound see [START_REF] Martin | Neuhäusser: Model Checking Nondeterministic and Randomly Timed Systems[END_REF]Lemma 6.6].

Proof. The proof is by induction over k b : 1. k b = 1: We consider two cases:

a. s ∈ S M \ G: Let Π δ be the set of paths that reach G within δ time unit. In the approximation we measure the set of paths that have at most two Markovian jumps and then reach G. Let this set be denoted by Π δ ≤2 . Since we have Π δ = Π δ ≤2 ∪ Π δ >2 and Π δ ≤2 and Π δ >2 are disjoint, we have: Pr ω A,s (Π δ ) -Pr ω A,s (Π δ ≤2 ) = Pr ω A,s (Π δ >2 ). The probability Pr ω A,s (Π δ >2 ) can be bounded by the probability of more than two arrivals in a Poisson process with the largest exit rate appearing in the IMC within a time interval of length δ. For the Poisson process, this probability is 1e -λδ

Fig. 1 .

 1 Fig. 1. An exemplary IMC Example 1.Let M be the IMC in Figure1. s 1 and s 3 are Markov states, while s 2 is an interactive state. Initial state s 0 is a hybrid state, since it has both interactive and Markov transitions enabled. Considering M as a closed IMC, the urgency assumption allows us to ignore (s 0 , 0.5, s 2 ) ∈ and consider s 0 as an interactive state. Under this assumption, interactive transitions are instantaneously fired after zero time delay. Conversely, the sojourn time in a Markov state s is exponentially distributed with rate E(s). For example, the probability to leave s 1 within δ time unit is 1-e -5δ (E(s 1 ) = 2+3 = 5). At this point, branching probabilities determine the distribution of evolving to next states. For s 1 , P(s 1 , ⊥, s 0 ) = 2

Lemma 1 (

 1 Fixed Point Characterisation for IMCs [26, Theorem 6.1]). Let M be an IMC, G ⊆ S be a set of goal states and I ∈ I with inf I = a and sup I = b. p M max : S × I [0, 1] is the least fixed point of the higher-order operator Ω : (S × I [0, 1]) (S × I [0, 1]), which is:

Definition 3 .

 3 An IPC is a tuple D = (S, Act, -→, d , s 0 ), where S, Act, -→ and s 0 are as Definition 1 and d ⊂ S × Dist(S) is the set of digitised Markov transitions.

  Given accuracy level and IMC M as before, assume N = |S| and M = | -→ | + | |. The best known complexity for the precomputation of set Reach i (•) for all interactive states and hence of Reach i (•) ∩ S M is O(N 2.376 ) [11]. Instantiating the inequality above for n = 2 gives O (bλ) 3 as the complexity of the iteration count. Since the size of Reach i (s) ∩ S M for a given state s is at most N , the complexity of the i * -phase is O(N 2 ). m-phase contains one step reachability computations from Markov states by considering zero, one or two Markov transitions which has the respective complexities O(N ), O(M N ) and O(M 2 ). Thus the resulting complexity is

Table 1 .

 1 Reachability computation time in the Google file system. M δ time(s) M δ (2) time(s)

	Ncs |S| |G|		I	min max min	max
		10 -3	[0, 0.1]	124.8 115.0 18.6	21.4
	10 1796 408	10 -3 10 -4	[0, 0.4] [0, 0.1]	2021.0 1823.6 145.0 165.1 1308.9 1188.1 56.7 66.0
		10 -4 [0.01, 0.04] 232.8 214.0 17.1	21.9
	20 7176 1713	10 -4 10 -5 [0.005, 0.015] 5564.9 6413.0 179.4 219.1 [0, 0.01] 319.9 308.5 52.2 54.0

i=0 (λδ) i i!

Acknowledgement. We thank Lijun Zhang for helpful discussions and comments, and Dennis Guck for developing and sharing the original implementation of the algorithm and the case study as a part of IMCA.

This work has been supported by the DFG as part of SFB/TR 14 AVACS, by the DFG/NWO bilateral project ROCKS, and by the European Union FP7-ICT projects MEALS, grant agreement no. 295261, and SENSATION, grant agreement no. 318490.

Appendix

Proof of Theorem 2

We present the proof of Theorem 2 in a restricted setting and afterwards briefly discuss how to extend it to cover the entirety of the theorem. We assume that I = [0, b] and focus on the case n = 2. Lemma 1 for s ∈ S M \G can be rewritten [START_REF] Martin | Neuhäusser: Model Checking Nondeterministic and Randomly Timed Systems[END_REF]Section 6

The following holds from Definition 5 for s ∈ S M \ G and n = 2:

. b. s ∈ S I \ G: This case reduces to case 1.a as follows. We have

From the above equations there exists s ∈ S M such that p M max (s,

Because s is a Markov state, the upper bound for s is deployed to s.

max (s, ♦ I δ G). We consider two cases: a. s ∈ S M \ G: From Eq. 1 and 2 we have:

We try to find an upper bound for B 1 (s , t) for s ∈ S M :

Now we find an upper bound for B 0 (s , t + τ ). For s ∈ S M we have:

We know that:

Plugging the above inequality and 3 into 6 gives:

Plugging 3 and 7 into 5 gives:

Note that Eq. 7 and 8 are still valid for s , s ∈ S I \ G with the same argument described in 1.b. Finally plugging 3 and 8 into 4 gives:

In this case the proof is similar to 1.a. This proof can directly be extended to intervals with open bounds and to intervals with nonzero lower bounds. Furthermore it can be embedded into an induction on n, thereby showing the theorem for any natural n. We need to skip these cases because of space limitations.