Vojtěch Forejt

Marta Kwiatkowska

Gethin Norman

David Parker

Hongyang Qu

Quantitative Multi-Objective Verification for Probabilistic Systems

We present a verification framework for analysing multiple quantitative objectives of systems that exhibit both nondeterministic and stochastic behaviour. These systems are modelled as probabilistic automata, enriched with cost or reward structures that capture, for example, energy usage or performance metrics. Quantitative properties of these models are expressed in a specification language that incorporates probabilistic safety and liveness properties, expected total cost or reward, and supports multiple objectives of these types. We propose and implement an efficient verification framework for such properties and then present two distinct applications of it: firstly, controller synthesis subject to multiple quantitative objectives; and, secondly, quantitative compositional verification. The practical applicability of both approaches is illustrated with experimental results from several large case studies.

Introduction

Automated formal verification techniques such as model checking have proved to be an effective way of establishing rigorous guarantees about the correctness of real-life systems. In many instances, though, it is important to also take stochastic behaviour of these systems into account. This might be because of the presence of components that are prone to failure, because of unpredictable behaviour, e.g. of lossy communication media, or due to the use of randomisation, e.g. in distributed communication protocols such as Bluetooth.

Probabilistic verification offers techniques to automatically check quantitative properties of such systems. Models, typically labelled transition systems augmented with probabilistic information, are verified against properties specified in probabilistic extensions of temporal logics. Examples of such properties include "the probability of both devices failing within 24 hours is less than 0.001" or "with probability at least 0.99, all message packets are sent successfully".

In this paper, we focus on verification techniques for probabilistic automata (PAs) [START_REF] Segala | Modelling and Verification of Randomized Distributed Real Time Systems[END_REF], which model both nondeterministic and probabilistic behaviour. We augment these models with one or more reward structures that assign real values to certain transitions of the model. In fact, these can associate a notion of either cost or reward with the executions of the model and capture a wide range of quantitive measures of system behaviour, for example "number of time steps", "energy usage" or "number of messages successfully sent".

Properties of PAs can be specified using well-known temporal logics such as PCTL, LTL or PCTL* [START_REF] Bianco | Model checking of probabilistic and nondeterministic systems[END_REF] and extensions for reward-based properties [START_REF] De Alfaro | Formal Verification of Probabilistic Systems[END_REF]. The corresponding verification problems can be executed reasonably efficiently and are implemented in tools such as PRISM, LiQuor and RAPTURE.

A natural extension of these techniques is to consider multiple objectives. For example, rather than verifying two separate properties such as "message loss occurs with probability at most 0.001" and "the expected total energy consumption is below 50 units", we might ask whether it is possible to satisfy both properties simultaneously, or to investigate the trade-off between the two objectives as some parameters of the system are varied.

In this paper, we consider verification problems for probabilistic automata on properties with multiple, quantitative objectives. We define a language that expresses Boolean combinations of probabilistic ω-regular properties (which subsumes e.g. LTL) and expected total reward measures. We then present, for properties expressed in this language, techniques both to verify that a property holds for all adversaries (strategies) of a PA and to synthesise an adversary of a PA under which a property holds. We also consider numerical queries, which yield an optimal value for one objective, subject to constraints imposed on one or more other objectives. This is done via reduction to a linear programming problem, which can be solved efficiently. It takes time polynomial in the size of the model and doubly exponential in the size of the property (for LTL objectives), i.e. the same as for the single-objective case [START_REF] Courcoubetis | Markov decision processes and regular events[END_REF].

Multi-criteria optimisation for PAs or, equivalently, Markov decision processes (MDPs) is well studied in operations research [START_REF]Multicriteria Analysis[END_REF]. More recently, the topic has also been considered from a probabilistic verification point of view [START_REF] Chatterjee | Markov decision processes with multiple objectives[END_REF][START_REF] Etessami | Multi-objective model checking of Markov decision processes[END_REF][START_REF] Chatterjee | Markov decision processes with multiple long-run average objectives[END_REF]. In [START_REF] Etessami | Multi-objective model checking of Markov decision processes[END_REF], ω-regular properties are considered, but not rewards which, as illustrated by the examples above, offer an additional range of useful properties. In, [START_REF] Chatterjee | Markov decision processes with multiple objectives[END_REF] discounted reward properties are used. In practice, though, a large class of properties, such as "expected total time for algorithm completion" are not accurately captured when using discounting. Finally, [START_REF] Chatterjee | Markov decision processes with multiple long-run average objectives[END_REF] handles a complementary class of long-run average reward properties. All of [START_REF] Chatterjee | Markov decision processes with multiple objectives[END_REF][START_REF] Etessami | Multi-objective model checking of Markov decision processes[END_REF][START_REF] Chatterjee | Markov decision processes with multiple long-run average objectives[END_REF] present algorithms and complexity results for verifying properties and approximating Pareto curves; however, unlike this paper, they do not consider implementations.

We implement our multi-objective verification techniques and present two distinct applications. Firstly, we illustrate the feasibility of performing controller synthesis. Secondly, we develop compositional verification methods based on assume-guarantee reasoning and quantitative multi-objective properties. Controller synthesis. Synthesis, which aims to build correct-by-construction systems from formal specifications of their intended behaviour, represents a longstanding and challenging goal in the field of formal methods. One area where progress has been made is controller synthesis, a classic problem in control engineering which devises a strategy to control a system such that it meets its specification. We demonstrate the application of our techniques to synthesising controllers under multiple quantitative objectives, illustrating this with experimental results from a realistic model of a disk driver controller.

Compositional verification. Perhaps the biggest challenge to the practical applicability of formal verification is scalability. Compositional verification offers a powerful means to address this challenge. It works by breaking a verification problem down into manageable sub-tasks, based on the structure of the system being analysed. One particularly successful approach is the assume-guarantee paradigm, in which properties (guarantees) of individual system components are verified under assumptions about their environment. Desired properties of the combined system, which is typically too large to verify, are then obtained by combining separate verification results using proof rules. Compositional analysis techniques are of particular importance for probabilistic systems because verification is often more expensive than for non-probabilistic models.

Recent work in [START_REF] Kwiatkowska | Assume-guarantee verification for probabilistic systems[END_REF] presents an assume-guarantee framework for probabilistic automata, based on a reduction to the multi-objective techniques of [START_REF] Etessami | Multi-objective model checking of Markov decision processes[END_REF]. However, the assumptions and guarantees in this framework are restricted to probabilistic safety properties. This limits the range of properties that can be verified and, more importantly, can be too restrictive to express assumptions of the environment. We use our techniques to introduce an alternative framework where assumptions and guarantees are the quantitative multi-objective properties defined in this paper. This adds the ability to reason compositionally about, for example, probabilistic liveness or expected rewards. To facilitate this, we also incorporate a notion of fairness into the framework. We have implemented the techniques and present results from compositional verification of several large case studies, including instances where it is infeasible non-compositionally.

Related work. Existing research on multi-objective analysis of MDPs and its relationship with this work has been discussed above. On the topic of controller synthesis, the problem of synthesising MDP adversaries to satisfy a temporal logic specification has been addressed several times, e.g. [START_REF] Baier | Controller synthesis for probabilistic systems[END_REF][START_REF] Brázdil | Controller synthesis and verification for Markov decision processes with qualitative branching time objectives[END_REF]. Also relevant is [START_REF] Chatterjee | Measuring and synthesizing systems in probabilistic environments[END_REF], which synthesises non-probabilistic automata based on quantitative measures. In terms of compositional verification, the results in this paper significantly extend the recent work in [START_REF] Kwiatkowska | Assume-guarantee verification for probabilistic systems[END_REF]. Other related approaches include: [START_REF] Caillaud | Compositional design methodology with constraint Markov chains[END_REF][START_REF] Delahaye | Probabilistic contracts: A compositional reasoning methodology for the design of stochastic systems[END_REF], which present specification theories for compositional reasoning about probabilistic systems; and [START_REF] Chatterjee | Compositional quantitative reasoning[END_REF], which presents a theoretical framework for compositional verification of quantitative (but not probabilistic) properties. None of [START_REF] Caillaud | Compositional design methodology with constraint Markov chains[END_REF][START_REF] Delahaye | Probabilistic contracts: A compositional reasoning methodology for the design of stochastic systems[END_REF][START_REF] Chatterjee | Compositional quantitative reasoning[END_REF], however, consider practical implementations of their techniques.

Contributions. In summary, the contributions of this paper are as follows:

novel multi-objective verification techniques for probabilistic automata (and MDPs) that include both ω-regular and expected total reward properties; a corresponding method to generate optimal adversaries, with direct applicability to the problem of controller synthesis for these models; new compositional verification techniques for probabilistic automata using expressive quantitative properties for assumptions and guarantees.

An extended version of this paper, with proofs, is available as [START_REF] Forejt | Quantitative multiobjective verification for probabilistic systems[END_REF].

Background

We use Dist(S) for the set of all discrete probability distributions over a set S, η s for the point distribution on s ∈ S, and µ 1 ×µ 2 for the product distribution of µ 1 ∈ Dist(S 1 ) and µ 2 ∈ Dist(S 2 ), defined by µ 1 ×µ 2 ((s 1 , s 2 )) = µ 1 (s 1 ) • µ 2 (s 2 ).

Probabilistic automata (PAs)

Probabilistic automata [START_REF] Segala | Modelling and Verification of Randomized Distributed Real Time Systems[END_REF] are a commonly used model for systems that exhibit both probabilistic and nondeterministic behaviour. PAs are very similar to Markov decision processes (MDPs). 1 For the purposes of verification (as in Section 3), they can often be treated identically; however, for compositional analysis (as in Section 4), the distinction becomes important.

Definition 1 (Probabilistic automata). A probabilistic automaton (PA) is a tuple M=(S, s, α M , δ M ) where S is a set of states, s ∈ S is an initial state, α M is an alphabet and δ M ⊆ S×α M ×Dist(S) is a probabilistic transition relation.

In a state s of a PA M, a transition s a -→ µ, where a is an action and µ is a distribution over states, is available if (s, a, µ) ∈ δ. The selection of an available transition is nondeterministic and the subsequent choice of successor state is probabilistic, according to the distribution of the chosen transition.

A path is a sequence ω = s 0 a0,µ0

---→s 1 a1,µ1

---→ • • • where s 0 =s, s i ai -→ µ i is an available transition and µ i (s i+1 )>0 for all i ∈ N. We denote by IPaths (FPaths) the set of all infinite (finite) paths. If ω is finite, |ω| denotes its length and last(ω) its last state. The trace, tr (ω), of ω is the sequence of actions a 0 a 1 . . . and we use tr (ω) α to indicate the projection of such a trace onto an alphabet α ⊆ α M .

A reward structure for M is a mapping ρ : α ρ → R >0 from some alphabet α ρ ⊆ α M to the positive reals. We sometimes write ρ(a) = 0 to indicate that a ∈ α ρ . For an infinite path ω = s 0 a0,µ0

---→ s 1 a1,µ1 ---→ • • • , the total reward for ω over ρ is ρ(ω) = i∈N,ai∈αρ ρ(a i ).
An adversary of M is a function σ : FPaths→Dist(α M ×Dist(S)) such that, for a finite path ω, σ(ω) only assigns non-zero probabilities to action-distribution pairs (a, µ) for which (last(ω), a, µ) ∈ δ. Employing standard techniques [START_REF] Kemeny | Denumerable Markov Chains[END_REF], an adversary σ induces a probability measure Pr σ M over IPaths. An adversary σ is deterministic if σ(ω) is a point distribution for all ω, memoryless if σ(ω) depends only on last(ω), and finite-memory if there are a finite number of memory configurations such that σ(ω) depends only on last(ω) and the current memory configuration, which is updated (possibly stochastically) when an action is performed. We let Adv M denote the set of all adversaries for M.

If M i = (S i , s i , α Mi , δ Mi ) for i=1, 2, then their parallel composition, denoted M 1 M 2 , is given by the PA (S 1 ×S 2 , (s 1 , s 2 ), α M1 ∪α M2 , δ M1 M2 ) where δ M1 M2 is defined such that (s 1 , s 2 ) a -→ µ 1 ×µ 2 if and only if one of the following holds: (i) s 1 a -→ µ 1 , s 2 a -→ µ 2 and a ∈ α M1 ∩ α M2 ; (ii) s 1 a -→ µ 1 , µ 2 = η s2 and a ∈ α M1 \α M2 ; or (iii) s 2 a -→ µ 2 , µ 1 = η s1 and a ∈ α M2 \α M1 .
1 For MDPs, δM in Definition 1 becomes a partial function S × αM → Dist(S).

When verifying systems of PAs composed in parallel, it is often essential to consider fairness. In this paper, we use a simple but effective notion of fairness called unconditional fairness, in which it is required that each process makes a transition infinitely often. For probabilistic automata, a natural approach to incorporating fairness (as taken in, e.g., [START_REF] Baier | Model checking for a probabilistic branching time logic with fairness[END_REF][START_REF] Baier | Quantitative analysis under fairness constraints[END_REF]) is to restrict analysis of the system to a class of adversaries in which fair behaviour occurs with probability 1.

If M = M 1 . . . M n is a PA comprising n components, then an (unconditionally) fair path of M is an infinite path ω ∈ IPaths in which, for each component M i , there exists an action a ∈ α Mi that appears infinitely often. A fair adversary σ of M is an adversary for which Pr σ M {ω ∈ IPaths | ω is fair} = 1. We let Adv fair M denote the set of fair adversaries of M.

Verification of PAs

Throughout this section, let M = (S, s, α M , δ M ) be a PA.

Definition 2 (Probabilistic predicates). A probabilistic predicate [φ]

∼p comprises an ω-regular property φ ⊆ (α φ ) ω over some alphabet α φ ⊆ α M , a relational operator ∼ ∈ {<, , >, } and a rational probability bound p. Satisfaction of [φ] ∼p by M, under adversary σ, denoted M, σ |= [φ] ∼p , is defined as follows:

M, σ |= [φ] ∼p ⇔ Pr σ M (φ)∼p where Pr σ M (φ) def =Pr σ M ({ω∈IPaths | tr (ω) α φ ∈φ}).

Definition 3 (Reward predicates). A reward predicate [ρ]

∼r comprises a reward structure ρ : α ρ → R >0 over some alphabet α ρ ⊆ α M , a relational operator ∼ ∈ {<, , >, } and a rational reward bound r. Satisfaction of [ρ] ∼r by M, under adversary σ, denoted M, σ |= [ρ] ∼r , is defined as follows:

M, σ |= [ρ] ∼r ⇔ ExpTot σ M (ρ) ∼ r where ExpTot σ M (ρ) def = ω ρ(ω) dPr σ M .
Verification of PAs is based on quantifying over all adversaries. For example, we define satisfaction of probabilistic predicate [φ] ∼p by M, denoted M |= [φ] ∼p , as:

M |= [φ] ∼p ⇔ ∀σ ∈ Adv M . M, σ |= [φ] ∼p .
In similar fashion, we can verify a multi-component PA M 1 . . . M n under fairness by quantifying only over fair adversaries:

M 1 . . . M n |= fair [φ] ∼p ⇔ ∀σ ∈ Adv fair M1 ... Mn . M 1 . . . M n , σ |= [φ] ∼p .
Verifying whether M satisfies a probabilistic predicate [φ] ∼p or reward predicate [ρ] ∼r can be done with, for example, the techniques in [START_REF] Courcoubetis | Markov decision processes and regular events[END_REF][START_REF] De Alfaro | Formal Verification of Probabilistic Systems[END_REF]. In the remainder of this section, we give further details of the case for ω-regular properties, since we need these later in the paper. We follow the approach of [START_REF] De Alfaro | Formal Verification of Probabilistic Systems[END_REF], which is based on the use of deterministic Rabin automata and end components.

An end component (EC) of M is a pair (S , δ ) comprising a subset S ⊆S of states and a probabilistic transition relation δ ⊆δ that is strongly connected when restricted to S and closed under probabilistic branching, i.e., {s ∈ S | ∃(s, a, µ) ∈ δ } ⊆ S and {s ∈ S | µ(s )>0 for some (s, a, µ) ∈ δ} ⊆ S . An EC (S , δ ) is maximal if there is no EC (S , δ ) such that δ δ .

A deterministic Rabin automaton (DRA) is a tuple A = (Q, q, α, δ, Acc) of states Q, initial state q, alphabet α, transition function δ : Q×α → Q, and acceptance condition Acc = {(L i , K i )} k i=1 with L i , K i ⊆ Q. Any infinite word w ∈ (α) ω has a unique corresponding run q q 1 q 2 . . . through A and we say that A accepts w if the run contains, for some 1 i k, finitely many states from L i and infinitely many from K i . For any ω-regular property φ ⊆ (α φ ) ω we can construct a DRA, say A φ , over α φ that accepts precisely φ.

Verification of [φ] ∼p on M is done by constructing the product of M and A φ , and then identifying accepting end components. The product M⊗A φ of M and

DRA A φ = (Q, q, α M , δ, {(L i , K i )} k i=1 ) is the PA (S × Q, (s, q), α M , δ M )
where for all (s, a, µ) ∈ δ M there is ((s, q), a, µ ) ∈ δ M such that µ (s , q ) = µ(s ) for q = δ(q, a) and all s ∈ S. An accepting EC for φ in M⊗A φ is an EC (S , δ ) for which there exists an 1 i k such that the set of states S , when projected onto Q, contains some state from K i , but no states from L i . Verifying, for example, that M |= [φ] ∼p , when ∼ ∈ {<, }, reduces to checking that M⊗A φ |= [♦T ] ∼p , where T is the union of states of accepting ECs for φ in M⊗A φ .

Verification of such properties under fairness, e.g. checking M |= fair [φ] ∼p , can be done by further restricting the set of accepting ECs. For details, see [START_REF] Baier | Quantitative analysis under fairness constraints[END_REF], which describes verification of PAs under strong and weak fairness conditions, of which unconditional fairness is a special case.

Quantitative Multi-Objective Verification

In this section, we define a language for expressing multiple quantitative objectives of a probabilistic automaton. We then describe, for properties expressed in this language, techniques both to verify that the property holds for all adversaries of a PA and to synthesise an adversary of a PA under which the property holds. We also consider numerical queries, which yield an optimal value for one objective, subject to constraints imposed on one or more other objectives.

Definition 4 (Quantitative multi-objective properties). A quantitative multi-objective property (qmo-property) for a PA M is a Boolean combination of probabilistic and reward predicates, i.e. an expression produced by the grammar:

Ψ ::= true | Ψ ∧ Ψ | Ψ ∨ Ψ | ¬Ψ | [φ] ∼p | [ρ] ∼r
where [φ] ∼p and [ρ] ∼r are probabilistic and reward predicates for M, respectively. A simple qmo-property comprises a single conjunction of predicates, i.e. is of the form

(∧ n i=1 [φ i ] ∼ipi ) ∧ ∧ m j=1 [ρ j ] ∼j rj .
We refer to the predicates occurring in a formula as objectives. For property Ψ P , we use α P to denote the set of actions used in Ψ P , i.e. the union of α φ and α ρ over [φ] ∼p and [ρ] ∼r occurring in Ψ P .

A quantitative multi-objective property Ψ is evaluated over a PA M and an adversary σ of M. We say that M satisfies Ψ under σ, denoted M, σ |= Ψ , if Ψ evaluates to true when substituting each predicate x with the result of M, σ |= x. Verification of Ψ over a PA M is defined as follows. Definition 5 (Verification queries). For a PA M and a qmo-property Ψ , a verification query asks whether Ψ is satisfied under all adversaries of M:

M |= Ψ ⇔ ∀σ ∈ Adv M . M, σ |= Ψ.
For a simple qmo-property Ψ , we can verify whether M |= Ψ using standard techniques [START_REF] Courcoubetis | Markov decision processes and regular events[END_REF][START_REF] De Alfaro | Formal Verification of Probabilistic Systems[END_REF] (since each conjunct can be verified separately). To treat the general case, we will use multi-objective model checking, proceeding via a reduction to the dual notion of achievability queries.

Definition 6 (Achievability queries). For a PA M and qmo-property Ψ , an achievability query asks if there exists a satisfying adversary of M, i.e. whether there exists σ ∈ Adv M such that M, σ |= Ψ .

Remark. Since qmo-properties are closed under negation, we can convert any verification query into an equivalent (negated) achievability query. Furthermore, any qmo-property can be translated to an equivalent disjunction of simple qmoproperties (obtained by converting to disjunctive normal form and pushing negation into predicates, e.g.

¬([φ] >p ) ≡ [φ] p ).
In practice, it is also often useful to obtain the minimum/maximum value of an objective, subject to constraints on others. For this, we use numerical queries.

Definition 7 (Numerical queries). For a PA M, qmo-property Ψ and ωregular property φ or reward structure ρ, a (maximising) numerical query is:

Pr max M (φ | Ψ ) def = sup{Pr σ M (φ) | σ ∈ Adv M ∧ M, σ |= Ψ }, or ExpTot max M (ρ | Ψ ) def = sup{ExpTot σ M (ρ) | σ ∈ Adv M ∧ M, σ |= Ψ }.
If the property Ψ is not satisfied by any adversary of M, these queries return ⊥.

A minimising numerical query is defined similarly. Before describing our techniques to check verification, achievability and numerical queries, we first need to discuss some assumptions made about PAs. One of the main complications when introducing rewards into multi-objective queries is the possibility of infinite expected total rewards. For the classical, single-objective case (see e.g. [START_REF] De Alfaro | Formal Verification of Probabilistic Systems[END_REF]), it is usual to impose assumptions so that such behaviour does not occur. For the multi-objective case, the situation is more subtle, and requires careful treatment. We now outline what assumptions should be imposed; later we describe how they can be checked algorithmically.

A key observation is that, if we allow arbitrary reward structures, situations may occur where extremely improbable (but non-zero probability) behaviour still yields infinite expected reward. Consider e.g. the PA ({s 0 , s 1 , s 2 }, s 0 , {a, b}, δ) with δ = {(s 0 , b, η s1 ), (s 0 , b, η s2 ), (s 1 , a, η s1 ), (s 2 , b, η s2 )}, reward structure ρ = {a →1}, and the qmo-property Ψ = [ b] ≥p ∧ [ρ] ≥r . For any p, including values arbitrarily close to 1, there is an adversary satisfying Ψ for any r ∈ R 0 , because it suffices to take action a with non-zero probability. This rather unnatural behaviour would lead to misleading verification results, masking possible errors in the model design.

Motivated by such problems, we enforce the restriction below on multiobjective queries. To match the contents of the next section, we state this for a maximising numerical query on rewards. We describe how to check the restriction holds in the next section.

Assumption 1 Let ExpTot max

M (ρ | Ψ ) be a numerical query for a PA M and qmo-property Ψ which is a disjunction2 of simple qmo-properties Ψ 1 , . . . , Ψ l . For each

Ψ k = (∧ n i=1 [φ i ] ∼ipi ) ∧ ∧ m j=1 [ρ j
] ∼j rj , we require that:

sup{ExpTot σ M (ζ) | M, σ |= n i=1 [φ i ] ∼ipi } < ∞ for all ζ ∈ {ρ} ∪ {ρ j | 1 j m ∧ ∼ j ∈ {>, ≥}}.

Checking Multi-Objective Queries

We now describe techniques for checking the multi-objective queries described previously. For presentational purposes, we focus on numerical queries. It is straightforward to adapt this to achievability queries by introducing, and then ignoring, a dummy property to maximise (with no loss in complexity). As mentioned earlier, verification queries are directly reducible to achievability queries. Let M be a PA and ExpTot max M (ρ | Ψ ) be a maximising numerical query for reward structure ρ (the cases for minimising queries and ω-regular properties are analogous). As discussed earlier, we can convert Ψ to a disjunction of simple qmo-properties. Clearly, we can treat each element of the disjunction separately and then take the maximum. So, without loss of generality, we assume that Ψ is simple, i.e. Ψ = (∧ n i=1 [φ i ] ∼ipi ) ∧ ∧ m j=1 [ρ j ] ∼j rj . Furthermore, we assume that each ∼ i is or > (which we can do by changing e.g. [φ] <p to [¬φ] >1-p ).

Our technique to compute ExpTot max M (ρ | Ψ ) proceeds via a sequence of modifications to M, producing a PA M. From this, we construct a linear program L( M), whose solution yields both the desired numerical result and a corresponding adversary σ of M. Crucially, σ is memoryless and can thus be mapped to a matching finite-memory adversary of M. The structure of L( M) is very similar to the one used in [START_REF] Etessami | Multi-objective model checking of Markov decision processes[END_REF], but many of the steps to construct M and the techniques to establish a memoryless adversary are substantially different. We also remark that, although not discussed here, L( M) can be adapted to a multi-objective linear program, or used to approximate the Pareto curve between objectives.

In the remainder of this section, we describe the process in detail, which comprises 4 steps: 1. checking Assumption 1; 2. building a PA M in which unneccessary actions are removed; 3. converting M to a PA M; 4. building and solving the linear program L( M). The correctness of the procedure is formalised with a corresponding sequence of propositions (see [START_REF] Forejt | Quantitative multiobjective verification for probabilistic systems[END_REF] for proofs).

Step 1. We start by constructing a PA M φ = M⊗A φ1 ⊗ • • • ⊗A φn which is the product of M and a DRA A φi for each ω-regular property φ i appearing in Ψ . We check Assumption 1 by analysing M φ : for each maximising reward structure ζ (i.e. letting ζ=ρ or ζ=ρ j when ∼ j ∈ {>, ≥}) we use the proposition below. This requires a simpler multi-objective achievability query on probabilistic predicates only. In fact, this can be done with the techniques of [START_REF] Etessami | Multi-objective model checking of Markov decision processes[END_REF].

Proposition 1. We have sup{ExpTot σ M (ζ) | M, σ |= n i=1 [φ i ] ∼ipi } = ∞ for a reward structure ζ of M iff there is an adversary σ of M φ such that M φ , σ |= [♦pos] >0 ∧ n i=1 [φ i ] ∼ipi
where "pos" labels any transition (s, a, µ) that satisfies ζ(a)>0 and is contained in an EC.

Step 2. Next, we build the PA M from M φ by removing actions that, thanks to Assumption 1, will not be used by any adversary which satisfies Ψ and maximises the expected value for the reward ρ. Let M φ = (S φ , s, α M , δ φ M ). Then M = ( S, s, α M , δM ) is the PA obtained from M φ as follows. First, we remove (s, a, µ) from δ φ M if it is contained in an EC and ζ(a)>0 for some maximising reward structure ζ. Second, we repeatedly remove states with no outgoing transitions and transitions that lead to non-existent states, until a fixpoint is reached. The following proposition holds whenever Assumption 1 is satisfied. Proposition 2. There is an adversary σ of M φ where ExpTot σ M φ (ρ)=x and M φ , σ |= Ψ iff there is an adversary σ of M where ExpTot σM (ρ)=x and M, σ |= Ψ .

Step 3. Then, we construct PA M from M, by converting the n probabilistic predicates [φ i ] ∼ipi into n reward predicates [λ i ] ∼ipi . For each R ⊆ {1, . . . , n}, we let S R denote the set of states that are contained in an EC (S , δ ) that: (i) is accepting for all {φ i | i ∈ R}; (ii) satisfies ρ j (a) = 0 for all 1 ≤ j ≤ m and (s, a, µ) ∈ δ . Thus, in each S R , no reward is gained and almost all paths satisfy the ω-regular properties φ i for i ∈ R. Note that identifying the sets S R can be done in time polynomial in the size of M (see [START_REF] Forejt | Quantitative multiobjective verification for probabilistic systems[END_REF] for clarification).

We then construct M by adding a new terminal state s dead and adding transitions from states in each S R to s dead , labelled with a new action a R . Intuitively,

Maximise

(s,a,µ)∈ δM ,s =s dead ρ(a) • y (s,a,µ) subject to:

(s,a R ,µ)∈ δM ,s =s dead y (s,a R ,µ) = 1 (s,a,µ)∈ δM ,s =s dead λi(a) • y (s,a,µ) ∼i pi for all 1≤i≤n

(s,a,µ)∈ δM ,s =s dead ρj(a) • y (s,a,µ) ∼j rj for all 1≤j≤m

(s,a,µ)∈ δM y (s,a,µ) -(ŝ,â, μ)∈ δM µ (s) • y (ŝ,â, μ) = init(s) for all s∈ Ŝ\{s dead } y (s,a,µ) ≥ 0 for all (s, a, µ)∈ δM where init(s) is 1 if s = s and 0 otherwise. taking an action a R in M corresponds to electing to remain forever in the corresponding EC of M. Formally, M = ( Ŝ, s, αM , δM ) where Ŝ = S ∪ {s dead },

αM = α M ∪ {a R | R ⊆ {1, . . . , n}}, and δM = δM ∪ {(s, a R , η s dead ) | s ∈ S R }. Fi- nally, we create, for each 1 ≤ i ≤ n, a reward structure λ i : {a R | i ∈ R} → R >0 with λ i (a R ) = 1 whenever λ i is defined. Proposition 3.
There is an adversary σ of M such that ExpTot σM (ρ)=x and M, σ |= Ψ iff there is a memoryless adversary σ of M such that ExpTot σM (ρ)=x

and M, σ |= (∧ n i=1 [λ i ] ∼ipi ) ∧ ∧ m j=1 [ρ j ] ∼j rj ∧ ([♦s dead ] 1 ).
Step 4. Finally, we create a linear program L( M), given in Figure 2, which encodes the structure of M as well as the objectives from Ψ . Intuitively, in a solution of L( M), the variables y (s,a,µ) express the expected number of times that state s is visited and transition s a -→ µ is taken subsequently. The expected total reward w.r.t. ρ i is then captured by (s,a,µ)∈ δM ,s =s dead ρ i (a) • y (s,a,µ) . The result of L( M) yields the desired value for our numerical query. Proposition 4. For x ∈ R 0 , there is a memoryless adversary σ of M where ExpTot σM (ρ)=x and M, σ

|= (∧ n i=1 [λ i ] ∼ipi ) ∧ ∧ m j=1 [ρ j ] ∼j rj ∧ ([♦s dead ] ≥1 ) iff there is a feasible solution (y (s,a,µ) ) (s,a,µ)∈ δM of the linear program L( M) such that (s,a,µ)∈ δM ,s =s dead ρ i (a) • y (s,a,µ) = x.
In addition, a solution to L( M) gives a memoryless adversary σ prod defined by σ prod (s)(a, µ) = y (s,a,µ) a ,µ y (s,a ,µ ) if the denominator is nonzero (and defined arbitrarily otherwise). This can be converted into a finite memory adversary σ for M φ by combining decisions of σ on actions in α M and, instead of taking actions a R , mimicking adversaries witnessing that the state which precedes a R in the history is in S R . Adversary σ can be translated into an adversary σ of M in standard fashion using the fact that every finite path in M φ has a counterpart in M given by projecting states of M φ to their first components. The following is then a direct consequence of Propositions 2, 3 and 4.

Theorem 1. Given a PA M and numerical query ExpTot max M (ρ | Ψ ) satisfying Assumption 1, the result of the query is equal to the solution of the linear program L( M) (see Figure 2). Furthermore, this requires time polynomial in the size of M and doubly exponential in the size of the property (for LTL objectives). An analogous result holds for numerical queries of the form

ExpTot min M (ρ | Ψ ), Pr max M (φ | Ψ ) or Pr min M (φ | Ψ ).
As discussed previously, this also yields a technique to solve both achievability and verification queries in the same manner.

Controller Synthesis

The achievability and numerical queries presented in the previous section are directly applicable to the problem of controller synthesis. We first illustrate these ideas on our simple example, and then apply them to a large case study.

Example 2. Consider the composition M = M c1 M m of PAs from Figure 1; M c1 can be seen as a template for a controller of M m . We synthesise an adversary for M that minimises the expected execution time under the constraints that the machine completes both jobs and the expected power consumption is below some bound r. Thus, we use the minimising numerical query ExpTot min M (ρ time | [ρ pow ] r ∧ [♦done] 1 ). Figure 3 shows the corresponding PA M, dashed lines indicating additions to construct M from M. Solving the LP problem L( M) yields the minimum expected time under these constraints. If r=30, for example, the result is 49 11 . Examining the choices made in the corresponding (memoryless) adversary, we find that, to obtain this time, a controller could schedule the first job fast with probability 5 6 and slow with 1 6 , and the second job slow. Figure 4(a) shows how the result changes as we vary the bound r and use different values for the failure probability of fast (0.1 in Figure 1).

Case study. We have implemented the techniques of Section 3 as an extension of PRISM [START_REF] Hinton | PRISM: A tool for automatic verification of probabilistic systems[END_REF] and using the ECLiPSe LP solver. We applied them to perform controller synthesis on a realistic case study: we build a power manager for an IBM TravelStar VP disk-drive [START_REF] Benini | Policy optimization for dynamic power management[END_REF]. Specific (randomised) power management policies can already be analysed in PRISM [START_REF] Norman | Using probabilistic model checking for dynamic power management[END_REF]; here, we synthesise such policies, subject to constraints specified as qmo-properties. More precisely, we minimise the expected power consumption under restrictions on, for example, the expected job-queue size, expected number of lost jobs, probability that a request waits more than K steps, or probability that N requests are lost. Further details are available from [24]. As an illustration, Figure 4(b) plots the minimal power consumption under restrictions on both the expected queue size and number of lost customers. This shows the familiar power-versus-performance trade-off: policies can offer improved performance, but at the expense of using more power. We now present novel compositional verification techniques for probabilistic automata, based on the quantitative multi-objective properties defined in Section 3.

The key ingredient of this approach is the assume-guarantee triple, whose definition, like in [START_REF] Kwiatkowska | Assume-guarantee verification for probabilistic systems[END_REF], is based on quantification over adversaries. However, whereas [START_REF] Kwiatkowska | Assume-guarantee verification for probabilistic systems[END_REF] uses a single probabilistic safety property as an assumption or guarantee, we permit quantitative multi-objective properties. Another key factor is the incorporation of fairness. Definition 8 (Assume-guarantee triples). If M = (S, s, α M , δ M ) is a PA and Ψ A , Ψ G are qmo-properties such that α G ⊆ α A ∪ α M , then Ψ A M Ψ G is an assume-guarantee triple with the following semantics:

Ψ A M Ψ G ⇔ ∀σ∈Adv M[α A ] . ( M, σ |= Ψ A → M, σ |= Ψ G ) .
where M[α A ] denotes the alphabet extension [START_REF] Kwiatkowska | Assume-guarantee verification for probabilistic systems[END_REF] of M, which adds a-labelled self-loops to all states of M for each a ∈ α A \α M .

Informally, an assume-guarantee triple Ψ A M Ψ G , means "if M is a component of a system such that the environment of M satisfies Ψ A , then the combined system (under fairness) satisfies Ψ G ".

Verification of an assume guarantee triple, i.e. checking whether Ψ A M Ψ G holds, reduces directly to the verification of a qmo-property since:

(M, σ |= Ψ A → M, σ |= Ψ G ) ⇔ M, σ |= (¬Ψ A ∨ Ψ G ) .
Thus, using the techniques of Section 3, we can reduce this to an achievability query, solvable via linear programming. Using these assume-guarantee triples as a basis, we can now formulate several proof rules that permit compositional verification of probabilistic automata. We first state two such rules, then explain their usage, illustrating with an example. Theorem 2. If M 1 and M 2 are PAs, and Ψ A1 , Ψ A2 and Ψ G are quantitative multi-objective properties, then the following proof rules hold:

M 1 |= fair Ψ A1 Ψ A1 M 2 Ψ G M 1 M 2 |= fair Ψ G (ASym) M 2 |= fair Ψ A2 Ψ A2 M 1 Ψ A1 Ψ A1 M 2 Ψ G M 1 M 2 |= fair Ψ G (Circ)
where, for well-formedness, we assume that, if a rule contains an occurrence of the triple Ψ A M Ψ G in a premise, then α G ⊆ α A ∪ α M ; similarly, for a premise that checks Ψ A against M, we assume that α A ⊆ α M Theorem 2 presents two assume-guarantee rules. The simpler, (Asym), uses a single assumption Ψ A1 about M 1 to prove a property Ψ G on M 1 M 2 . This is done compositionally, in two steps. First, we verify M 1 |= fair Ψ A1 . If M 1 comprises just a single PA, the stronger (but easier) check M 1 |= Ψ A1 suffices; the use of fairness in the first premise is to permit recursive application of the rule. Second, we check that Ψ A1 M 2 Ψ G holds. Again, optionally, we can consider fairness here. 3 In total, these two steps have the potential to be significantly cheaper than verifying M 1 M 2 . The other rule, (Circ), operates similarly, but using assumptions about both M 1 and M 2 .

Example 3. We illustrate assume-guarantee verification using the PAs M m and M c2 from Figure 1. Our aim is to verify that M c2 M m |= fair [ρ time ] 19 6 , which does indeed hold. We do so using the proof rule (ASym) of Theorem 2, with M 1 =M c2 and M 2 =M m . We use the assumption A 1 =[ρ slow ] 1 2 where ρ slow ={slow →1}, i.e. we assume the expected number of slow jobs requested is at most 0. . Experimental Results. Using our implementation of the techniques in Section 3, we now demonstrate the application of our quantitative assume-guarantee verification framework to two large case studies: Aspnes & Herlihy's randomised consensus algorithm and the Zeroconf network configuration protocol. For consensus, we check the maximum expected number of steps required in the first R rounds; for zeroconf, we verify that the protocol terminates with probability 1 and the minimum/maximum expected time to do so. In each case, we use the (Circ) rule, with a combination of probabilistic safety and liveness properties for assumptions. All models and properties are available from [24]. In fact, we execute numerical queries to obtain lower/upper bounds for system properties, rather than just verifying a specific bound.

Table 1 summarises the experiments on these case studies, which were run on a 2.66GHz PC with 8GB of RAM, using a time-out of 1 hour. The table shows the (numerical) result obtained and the time taken for verification done both compositionally and non-compositionally (with PRISM). As an indication of problem size, we give the size of the (non-compositional) PA, and the number of variables in the linear programs for multi-objective model checking.

Compositional verification performs very well. For the consensus models, it is almost always faster than the non-compositional case, often significantly so, and is able to scale up to larger models. For zeroconf, times are similar. Encouragingly, though, times for compositional verification grow much more slowly with model size. We therefore anticipate better scalability through improvements to the underlying LP solver. Finally, we note that the numerical results obtained compositionally are very close to the true results (where obtainable).

Conclusions

We have presented techniques for studying multi-objective properties of PAs, using a language that combines ω-regular properties, expected total reward and multiple objectives. We described how to verify a property over all adversaries of a PA, synthesise an adversary that satisfies and/or optimises objectives, and compute the minimum or maximum value of an objective, subject to constraints. We demonstrated direct applicability to controller synthesis, illustrated with a realistic disk-drive controller case study. Finally, we proposed an assumeguarantee framework for PAs that significantly improves existing ones [START_REF] Kwiatkowska | Assume-guarantee verification for probabilistic systems[END_REF], and demonstrated successful compositional verification on several large case studies.

Possible directions for future work include extending our compositional verification approach with learning-based assumption generation, as [START_REF] Feng | Compositional verification of probabilistic systems using learning[END_REF] does for the simpler framework of [START_REF] Kwiatkowska | Assume-guarantee verification for probabilistic systems[END_REF], and investigation of continuous-time models.

Fig. 1 .

 1 Fig. 1. PAs for a machine Mm (left) and two controllers, Mc 1 (centre) and Mc 2 (right)

Example 1 .

 1 Figure1shows the PAs we use as a running example. A machine, M m , executes 2 consecutive jobs, each in 1 of 2 ways: fast, which requires 1 time unit and 20 units of energy, but fails with probability 0.1; or slow , which requires 3 time units and 10 units of energy, and never fails. The reward structures ρ time ={fast →1, slow →3} and ρ pow ={fast →20, slow →10} capture the time elapse and power consumption of the system. The controllers, M c1 and M c2 , can (each) control the machine, when composed in parallel with M m . Using qmoproperty Ψ = [♦done] ≥1 ∧ [ρ pow ] ≤20 , we can write a verification query M m |= Ψ (which is false) or a numerical query ExpTot min Mm (ρ time | Ψ ) (which yields 6).

Fig. 2 .

 2 Fig. 2. The linear program L( M)

Fig. 3 .

 3 Fig. 3. A DRA A φ for the property φ = ♦done and the PA M for M = Mm Mc 1

Fig. 4 .

 4 Fig. 4. Experimental results illustrating controller synthesis 4 Quantitative Assume-Guarantee Verification

  5. We verify M c2 |= [ρ slow ] 1 2 and the triple [ρ slow ] 1

	2	M m [ρ time ] 19 6	.
	The triple is checked by verifying M m |= ¬[ρ slow ] 1 2 ∨[ρ time ] 19 6 or, equivalently,
	that no adversary of M m satisfies [ρ slow ] 1 2 ∧ [ρ time ] > 19 6

Table 1 .

 1 Experimental results for compositional verification

	Case study		Non-compositional		Compositional
	[parameters]		States	Time (s) Result LP size Time (s) Result
		3 2	1,806	0.4 89.00	1,565	1.8 89.65
	consensus	3 20	11,598	27.8 5,057	6,749	10.8 5,057
	(2 processes)	4 2	7,478	1.3 89.00	5,368	3.9 98.42
	(max. steps)	4 20	51,830	155.0 5,057 15,160	16.2 5,120
	[R K]	5 2	30,166	3.1 89.00 10,327	6.5 100.1
		5 20	212,758	552.8 5,057 24,727	21.9 5,121
		3 2	114,559	20.5 212.0 43,712	12.1 214.3
	consensus	3 12	507,919 1,361.6 4,352 92,672	284.9 4,352
	(3 processes)	3 20	822,607 time-out	-131,840	901.8 11,552
	(max. steps)	4 2	3,669,649	728.1 212.0 260,254	118.9 260.3
	[R K]	4 12 29,797,249 mem-out	-351,694	642.2 4,533
		4 20 65,629,249 mem-out	-424,846 1,697.0 11,840
	zeroconf	4	57,960	8.7	1.0 155,458	23.8	1.0
	(termination)	6	125,697	16.6	1.0 156,690	24.5	1.0
	[K]	8	163,229	19.4	1.0 157,922	25.5	1.0
	zeroconf	4	57,960	6.7 13.49 155,600	23.0 16.90
	(min. time)	6	125,697	15.7 17.49 154,632	23.1 12.90
	[K]	8	163,229	22.2 21.49 156,568	23.9 20.90
	zeroconf	4	57,960	5.8 14.28 154,632	23.7 17.33
	(max. time)	6	125,697	13.3 18.28 155,600	24.2 22.67
	[K]	8	163,229	18.9 22.28 156,568	25.1 28.00

This assumption extends to arbitrary properties Ψ by, as described earlier, first reducing to disjunctive normal form.

Adding fairness to checks of both qmo-properties and assume-guarantee triples is achieved by encoding the unconditional fairness constraint as additional objectives.

Acknowledgments. The authors are part supported by ERC Advanced Grant VERIWARE, EU FP7 project CONNECT and EPSRC grant EP/D07956X. Vojtěch Forejt is also supported by a Royal Society Newton Fellowship and the Institute for Theoretical Computer Science, project no. 1M0545.