Radu Mateescu

José Ignacio Requeno

On-the-Fly Model Checking for Extended Action-Based Probabilistic Operators

The quantitative analysis of concurrent systems requires expressive and user-friendly property languages combining temporal, data handling, and quantitative aspects. In this paper, we aim at facilitating the quantitative analysis of systems modeled as PTSs (Probabilistic Transition Systems) labeled by actions containing data values and probabilities. We propose a new regular probabilistic operator that specifies the probability measure of a path described by a generalized regular formula involving arbitrary computations on data values. This operator, which subsumes the Until operators of PCTL and their action-based counterparts, can provide useful quantitative information about paths having certain (e.g., peak) cost values. We integrated the regular probabilistic operator into MCL (Model Checking Language) and we devised an associated on-the-fly model checking method, based on a combined local resolution of linear and Boolean equation systems. We implemented the method in the EVALUATOR model checker of the CADP toolbox and experimented it on realistic PTSs modeling concurrent systems.

Introduction

Concurrent systems, which are becoming ubiquitous nowadays, are complex software artifacts involving qualitative aspects (e.g., concurrent behaviour, synchronization, data communication) as well as quantitative aspects (e.g., costs, probabilities, timing information). The rigorous design of such systems based on formal methods and model checking techniques requires versatile temporal logics able to specify properties about qualitative and quantitative aspects in a uniform, user-friendly way. During the past two decades, a wealth of temporal logics dealing with one or several of these aspects were defined and equipped with analysis tools [START_REF] Clarke | Model Checking[END_REF][START_REF] Baier | Principles of model checking[END_REF]. One of the first logics capturing behavioral, discrete time, and probabilistic information is PCTL (Probabilistic Computation Tree Logic) [START_REF] Hansson | A logic for reasoning about time and reliability[END_REF].

In this paper, we propose a framework for specifying and checking temporal logic properties combining actions, data, probabilities, and discrete time on PTSs (Probabilistic Transition Systems) [START_REF] Larsen | Bisimulation through probabilistic testing[END_REF], which are suitable action-based models for representing value-passing concurrent systems with interleaving semantics. We consider here the class of generative (also called fully probabilitistic) PTSs [START_REF] Van Glabbeek | Reactive, generative and stratified models of probabilistic processes[END_REF], in which transition probability distributions implicitly assign probabilities to the occurrences of actions. These PTSs can be viewed as DTMCs (Discrete-Time Markov Chains) in which transitions are labeled by actions carrying probabilities, channel names, and data values sent between concurrent processes during handshake communication. We are interested mainly in action-based properties, in contrast with standard DTMCs [START_REF] Baier | Principles of model checking[END_REF]Chap. 10], where atomic propositions are attached to states. Our contributions are twofold.

Regarding the specification of properties, we propose a new regular probabilistic operator, which specifies the probability measure of a path (specified as a regular formula on actions) in a PTS. Several probabilistic logics have been proposed in the action-based setting. PML (Probabilistic Modal Logic) [START_REF] Larsen | Bisimulation through probabilistic testing[END_REF] is a variant of HML (Hennessy-Milner Logic) [START_REF] Hennessy | Algebraic Laws for Nondeterminism and Concurrency[END_REF] with modalities indexed by probabilities, and was introduced as a modal characterization of probabilistic bisimulation on (generative) PTSs. GPL (Generalized Probabilistic Logic) [START_REF] Cleaveland | Probabilistic temporal logics via the modal mu-calculus[END_REF] is a probabilistic variant of the alternationfree modal µ-calculus, able to reason about execution trees, and equipped with a model checking algorithm relying on the resolution of non-linear equation systems. Compared to these logics, our probabilistic operator is a natural (action-based) extension of the Until operator of PCTL: besides paths of the form a * .b (the action-based counterpart of Until operators), we consider more general paths, specified by regular formulas similar to those of PDL (Propositional Dynamic Logic) [START_REF] Fischer | Propositional dynamic logic of regular programs[END_REF]. To handle the data values present on PTS actions, we rely on the regular formulas with counters of MCL (Model Checking Language) [START_REF] Mateescu | A model checking language for concurrent value-passing systems[END_REF], an extension of first-order µcalculus with programming language constructs. Moreover, we enhance the MCL regular formulas with a generalized iteration operator parameterized by data values, thus making possible the specification of complex (Turing computable) paths in a PTS.

Regarding the evaluation of regular probabilistic formulas on PTSs, we devise an on-the-fly model checking method based on translating the problem into the simultaneous local resolution of a linear equation system (LES) and a Boolean equation system (BES). For probabilistic operators containing dataless MCL regular formulas, the sizes of the LES and BES are linear in the size of the PTS and linear (resp. exponential) in the size of the regular formula, depending whether it is deterministic or not. In the action-based setting, the determinism of formulas is essential for a sound translation of the verification problem to a LES. For general data handling MCL regular formulas, the termination of the model checking procedure is guaranteed for a large class of formulas (e.g., counting, bounded iteration, aggregation of values, computation of costs over paths, etc.) and the sizes of the equation systems depend on the data parameters occurring in formulas. It is worth noticing that on-the-fly verification algorithms for PCTL were proposed only recently [START_REF] Latella | On-the-fly fast mean-field model-checking[END_REF], all previous implementations, e.g., in PRISM [START_REF] Kwiatkowska | PRISM 4.0: Verification of probabilistic real-time systems[END_REF] having focused on global algorithms. Our method provides on-the-fly verification for PCTL and its action-based variant PACTL, and also for PPDL (Probabilistic PDL) [START_REF] Kozen | A probabilistic PDL[END_REF], which are subsumed by the regular probabilistic operator of MCL. We implemented the method in the EVALUATOR [START_REF] Mateescu | A model checking language for concurrent value-passing systems[END_REF] on-the-fly model checker of the CADP toolbox [START_REF] Garavel | CADP 2011: A Toolbox for the Construction and Analysis of Distributed Processes[END_REF] and experimented it on various examples of value-passing concurrent systems.

Related work. Most of the works on action-based logics for quantitative analysis have concentrated on continuous-time models. CSL (Continuous Stochastic Logic) [START_REF] Aziz | Verifying continuous time Markov chains[END_REF][START_REF] Baier | Model-checking algorithms for continuous-time Markov chains[END_REF] is a continuous-time variant of PCTL interpreted on CTMCs (Continuous-Time Markov Chains). aCSL (action-based CSL) [START_REF] Hermanns | Towards model checking stochastic process algebra[END_REF], interpreted on actionlabeled CTMCs, is the action-based counterpart of CSL suitable for action-oriented modeling formalisms, such as stochastic process algebras. aCSL was defined in a way similar to ACTL (Action-based CTL) [START_REF] De Nicola | Action versus State Based Logics for Transition Systems[END_REF], which is the action-based counterpart of CTL [START_REF] Clarke | Automatic verification of finite-state concurrent systems using temporal logic specifications[END_REF]. In our setting, we can encode probabilistic versions of the ACTL operators, which are discrete-time counterparts of the time-bounded probability operators of aCSL. This logic was subsequently extended with regular operators similar to those of PDL, leading to the strictly more expressive logic asCSL [START_REF] Baier | Model checking Markov chains with actions and state labels[END_REF] interpreted on state-and action-labeled CTMCs. The purpose of asCSL was to enable the specification of complex properties of finite computations with real-time constraints. We had a similar motivation for our regular probabilistic operator on PTSs, and we extended its expressiveness further by adding data-handling mechanisms.

In the state-based setting, the logic closest to ours is QuaTEx (Quantitative Temporal Expressions) [START_REF] Agha | PMaude: rewritebased specification language for probabilistic object systems[END_REF], which combines constructs from PCTL and the rule-based query language EAGLE [START_REF] Barringer | Rulebased runtime verification[END_REF]. In QuaTEx, paths are described using recursive temporal operators with data parameters, built over a next-time operator and conditional path expressions. QuaTEx queries are evaluated using statistical model checking on GSMPs (Generalized Semi-Markov Processes) produced from actor-based probabilistic programs written in the PMaude language [START_REF] Agha | PMaude: rewritebased specification language for probabilistic object systems[END_REF]. Instead of recursive path formulas, our data-handling probabilistic operator extends the regular expressions over paths with a generalized iteration operator, yielding more concise specifications of step-bounded properties.

Organization of the paper. This paper is an extended version of a conference paper [START_REF] Mateescu | On-the-fly model checking for extended action-based probabilistic operators[END_REF], to which it adds the following material: (i) an enhanced review of related work; (ii) an in-depth presentation of the proposed logic, with more examples of properties, and of the proposed on-the-fly model checking procedure; (iii) further experimental validation on three probabilistic systems (BRP protocol and two randomized protocols) and a comparison with the PRISM model checker.

The rest of the paper is organized as follows. Section 2 defines the dataless regular probabilistic operator and Section 3 presents the on-the-fly model checking method. Section 4 is devoted to the data handling extensions. Section 5 briefly describes the implementation of the method within CADP and Section 6 illustrates it for the quantitative analysis of several protocols. Finally, Section 7 gives concluding remarks and directions of future work.

Dataless regular probabilistic operator

As interpretation models, we consider generative PTSs (Probabilistic Transition Systems) [START_REF] Larsen | Bisimulation through probabilistic testing[END_REF], in which transitions between states carry both action and probabilistic information. A PTS M = S, A, T, P, s i comprises a set of states S, a set of actions A, a transition relation T ⊆ S ×A×S, a probability labeling P : T → (0, 1], and an initial state s i ∈ S. A transition (s, a, s ) ∈ T (also written s a → s ) indicates that the system can move from state s to state s by performing action a with probability P(s, a, s ). For each state s ∈ S, the probability sum s a →s P(s, a, s ) = 1. These PTS models do not contain nondeterminism, but probabilistic choice, i.e., a transition s a → s assigns implicitly the same probability P(s, a, s ) to the occurrence of a.

Action formulas:

α ::= a | false | ¬α1 | α1 ∨ α2 b |=A a b |=A false b |=A ¬α1 b |=A α1 ∨ α2 iff b = a iff false iff b |=A α1 iff b |=A α1 or b |=A α2
Regular formulas:

β ::= α | ϕ? | β1.β2 | β1|β2 | β * 1 σ[i, j] |=M α σ[i, j] |=M ϕ? σ[i, j] |=M β1.β2 σ[i, j] |=M β1|β2 σ[i, j] |=M β * 1 iff i + 1 = j and σa[i] |=A α iff i = j and σ[i] |=M ϕ iff ∃k ∈ [i, j].σ[i, k] |=M β1 and σ[k, j] |=M β2 iff σ[i, j] |=M β1 or σ[i, j] |=M β2 iff i = j or ∃k > 0.σ[i, j] |=M β k 1 State formulas: ϕ ::= false | ¬ϕ1 | ϕ1 ∨ ϕ2 | β ϕ1 | {β} ≥p | {β}>p s |=M false s |=M ¬ϕ1 s |=M ϕ1 ∨ ϕ2 s |=M β ϕ1 s |=M {β} ≥p s |=M {β}>p iff false iff s |=M ϕ1 iff s |=M ϕ1 or s |=M ϕ2 iff ∃σ ∈ PathsM (s).∃i ≥ 0.σ[0, i] |=M β and σ[i] |=M ϕ1 iff PrM ({σ ∈ PathsM (s) | ∃i ≥ 0.σ[0, i] |=M β}) ≥ p iff PrM ({σ ∈ PathsM (s) | ∃i ≥ 0.σ[0, i] |=M β}) > p
Fig. 1: Modal and probabilistic operators over regular paths

A path σ = s(= s 0 ) a0 → s 1 a1 → • • • an-1 → s n • • • going out of a state s is an infinite sequence of transitions in M . The i-th state and i-th action of a path σ are noted σ[i] and σ a [i], respectively. An interval σ[i, j] with 0 ≤ i ≤ j is the path fragment σ[i] ai → • • • aj-1 → σ[j],
which reduces to the single-state path σ[i] if i = j. The suffix of a path σ starting at state σ[i] is noted σ i . The set of paths going out of s is noted Paths M (s).

The probability space associated to a PTS M is defined similarly to DTMCs: the outcomes are paths and the basic events are the cylinder sets defined as

Cyl(s 0 a0 → • • • an-1 → s n ) = {σ ∈ Paths M (s 0 ) | σ[0, n] = s 0 a0 → • • • an-1 → s n }, i.e.
, sets of paths sharing a common prefix. The σ-algebra associated to M is the smallest one containing all cylinder sets, and the probability measure of cylinder sets is defined as Pr M (Cyl(s

0 a0 → • • • an-1 → s n )) = Π 0≤i<n P(s i , a i , s i+1 )
. By Caratheodory's extension theorem in classical measure theory [START_REF] Feller | An Introduction to Probability Theory and Its Applications[END_REF], this probability measure uniquely extends to the σ-algebra, i.e., to all events (sets of paths) defined as countable unions of cylinder sets.

The regular probabilistic operator that we propose specifies the probability measure of paths characterized by regular formulas. For the dataless version of the operator, we use the regular formulas of PDL (Propositional Dynamic Logic) [START_REF] Fischer | Propositional dynamic logic of regular programs[END_REF], defined over the action formulas of ACTL (Action-based CTL) [START_REF] De Nicola | Action versus State Based Logics for Transition Systems[END_REF]. Figure 1 shows the syntax and semantics of the operators.

Action formulas α are built over the set of actions by using standard Boolean connectors. Derived action operators can be defined as usual: true = ¬false, α 1 ∧ α 2 = ¬(¬α 1 ∨ ¬α 2 ), etc. Regular formulas β are built from action formulas by using the testing (?), concatenation (.), choice (|), and transitive reflexive closure ( * ) operators. Derived regular operators can be defined as usual: nil = false * is the empty path operator, β + = β.β * is the transitive closure operator, etc. State formulas ϕ are built from Boolean connectors, the possibility modality ( ) and the probabilistic operators ({ } ≥p and { } >p ) containing regular formulas. In line with the original definition of PCTL [START_REF] Hansson | A logic for reasoning about time and reliability[END_REF], we considered both strict (> p) and non strict (≥ p) conditions on the probability. Derived state operators can be defined as usual: true = ¬false, ϕ 1 ∧ ϕ 2 = ¬(¬ϕ 1 ∨ ¬ϕ 2 ), and [β] ϕ = ¬ β ¬ϕ is the necessity modality.

Action formulas are interpreted on the set of actions A in the usual way, as propositional formulas denoting subsets of actions [START_REF] De Nicola | Action versus State Based Logics for Transition Systems[END_REF]. A path σ satisfies a regular formula

β, noted σ |= M β, if ∃i ≥ 0.σ[0, i] |= M β, i.e.
, it has a prefix belonging to the regular language defined by β. The testing operator ϕ? of PDL specifies state formulas ϕ that must hold in the intermediate states of a path. Concatenation, choice, and transitive reflexive closure on regular formulas are defined in the standard way (β k denotes the concatenation of β with itself k times). Boolean connectors on states are defined as usual. A state s satisfies the possibility modality β ϕ 1 (resp. the necessity modality [β] ϕ 1 ) iff some (resp. all) of the paths in Paths M (s) have a prefix satisfying β and leading to a state satisfying ϕ 1 . A state s satisfies the probabilistic operator {β} ≥p iff the probability measure of the paths in Paths M (s) with a prefix satisfying β is greater or equal to p (and similarly for the strict version of the operator). A PTS M = S, A, T, P, s i satisfies a formula ϕ, denoted by M |= ϕ, iff s i |= M ϕ (the subscript M will be omitted when it is clear from the context).

We show below some examples of properties expressible in the logic. Safety properties, which express that "something bad never happens" [START_REF] Manna | The temporal logic of reactive and concurrent systems[END_REF], can be specified using the modality [β] false, where the regular formula β denotes the undesirable paths and the box modality forbids their occurrence. Thus, mutual exclusion between two processes can be expressed as:

[true * .access 1 .(¬release 1 ) * .access 2 ] false meaning that all paths containing an access of process 1 to a shared resource followed by an access of process 2 before process 1 has released the resource lead necessarily to states satisfying false, i.e., never occur.

The absence of deadlocks (sink states), a necessary condition for a well-defined PTS, can be specified by forbidding the paths leading to a deadlock (denoted by the modality [true] false), or alternatively by imposing that all reachable states have at least one successor (denoted by the modality true true):

¬ true * [true] false = [true * ] true true
The existential Until operator of CTL can be specified using a diamond modality as follows:

E [ϕ 1 U ϕ 2 ] = (ϕ 1 ?.true) * ϕ 2
expressing that the current state has an outgoing path leading to a state satisfying ϕ 2 after zero or more transitions whose source states satisfy ϕ 1 (denoted by the regular subformula ϕ 1 ?.true). Similarly, the existential Until operators of ACTL are specified as follows:

E ϕ 1α 1 U ϕ 2 = (ϕ 1 ?.α 1 ) * ϕ 2 E ϕ 1α 1 U α2 ϕ 2 = (ϕ 1 ?.α 1 ) * .ϕ 1 ?.α 2 ϕ 2
These action-based operators specify properties about both source states and actions of the intermediate transitions (denoted by the regular subformulas ϕ 1 ?.α 1 ) and -for the second Until operator -also the last transition of the path fragment (denoted by the regular subformula ϕ 1 ?.α 2 ).

The probabilistic operator expresses constraints on the probability of occurrence of certain paths described using regular formulas. The formula below specifies that the probability to send a message along an unreliable channel and receive it finally (possibly after a finite number of retries) is at least 90%: {send .(true * .retry) * .recv } ≥0.9

By combining the modalities of PDL and the probabilistic operator, one can express quantitative response properties. The formula below specifies that every request of accessing a resource will be granted with probability 1 (i.e., almost surely):

[true * .request] {true * .grant} ≥1
The operator {β} ≥p generalizes naturally the Until operators of classical probabilistic branching-time logics.

The Until operator of PCTL [START_REF] Hansson | A logic for reasoning about time and reliability[END_REF] without discrete time (i.e., without the step-bounding clause U ≤t ), and probabilistic versions of the two Until operators of ACTL are expressed as follows:

[ϕ 1 U ϕ 2 ] ≥p = {(ϕ 1 ?.true) * .ϕ 2 ?} ≥p ϕ 1α 1 U ϕ 2 ≥p = {(ϕ 1 ?.α 1 ) * .ϕ 2 ?} ≥p ϕ 1α 1 U α2 ϕ 2 ≥p = {(ϕ 1 ?.α 1 ) * .ϕ 1 ?.α 2 .ϕ 2 ?} ≥p
These encodings consider the Until operators as a means of describing path fragments, and reformulate them using regular operators, which are strictly more expressive: for instance, the regular formula (true.true.ϕ?) + denoting the path fragments in which ϕ holds at even states is not expressible using Until operators [START_REF] Wolper | Temporal logic can be more expressive[END_REF]. Our extension of regular formulas with data handling (see Section 4) will enable to express also the step-bounded Until operators, and therefore to subsume full P(A)CTL.

Measurability of β-events. The probabilistic operator {β} ≥p interpreted on a state s refers to the probability measure of the set of paths going out of s and having a prefix satisfying β, defined as Paths(s, β) = {σ ∈ Paths(s) | σ |= M β}. For this semantics to be welldefined, the set Paths(s, β) must be measurable, i.e., it must be an event of the σ-algebra associated to the PTS M . This follows directly from the definition of {β} ≥p in Figure 1, because Paths(s, β) can be considered as a countable union of cylinder sets:

Paths(s, β) = {σ ∈ Paths(s) | σ |= M β} = {σ ∈ Paths(s) | ∃i ≥ 0.σ[0, i] |= M β} = i ≥ 0 σ[0, i] ∈ Paths fin (s) σ[0, i] |= M β Cyl(σ[0, i])
where Paths fin (s) is the set of finite paths going out of s. The countable union above can be computed by enumerating, for each i ≥ 0, all finite path fragments σ[0, i] ∈ Paths fin (s) of length i and checking whether they satisfy β. This last check can be done by verifying the PDL formula β [true] false on s in the LTS consisting solely of the finite path fragment σ[0, i] by using, e.g., the model checking procedure given in [START_REF] Emerson | Efficient model checking in fragments of the propositional mu-calculus[END_REF].

Model checking method

We propose below a method for checking a regular probabilistic formula on a PTS on the fly, by reformulating the problem as the simultaneous resolution of a linear equation system (LES) and a Boolean equation system (BES). The method consists of five steps, each one translating the problem into an increasingly concrete intermediate formalism. The first four steps operate syntactically on formulas and their intermediate representations, whereas the fifth step makes use of semantic information contained in the PTS. A detailed formalization of the first two steps can be found in [START_REF] Mateescu | Efficient on-the-fly model-checking for regular alternation-free mu-calculus[END_REF], and of the third and fourth steps (in a state-based setting) in [START_REF] Mateescu | CTRL: Extension of CTL with regular expressions and fairness operators to verify genetic regulatory networks[END_REF]. We illustrate the model checking method using the classical example of a six-sided dice emulated using a fair coin [START_REF] Knuth | The complexity of nonuniform random number generation[END_REF]. First, we consider a dataless version of the system (i.e., in which actions are simply names), represented as a PTS in Figure 2(a). The actions of tossing a head or tail of the coin are denoted by head and tail, each one having 0.5 probability. The actions corresponding to the dice faces are denoted by dice i for 1 ≤ i ≤ 6, each one occurring with probability 1. We will check on this PTS the formula Ψ 1 , stating that the probability of reaching the dice side marked with four directly after tossing the last head (if any) is at least 1/6:

Ψ 1 = {(true * .head ) * .dice 4 } ≥0.16
Strictly speaking, this formula could be verified using a PACTL model checker, since the regular subformula can be expressed equivalently without nested star operators as dice 4 |(true * .head .dice 4 ). The existence of a path matching it can be specified in ACTL using two Until operators:

E [true false U dice4 true]∨ E [true true U head E [true false U dice4 true]]
. This would require the model checker to compute the probability measures of each Until operator, then check that their sum is at least 0.16. However, we use formula Ψ 1 for the sake of simplicity to illustrate our model checking procedure. Examples of more complex properties, most of them unexpressible in PACTL, can be found in Section 6.

Translation to PDL with recursion.

To evaluate an operator {β} ≥p on a PTS M = S, A, T, P, s i on the fly, one needs to determine the set of paths going out of s i and satisfying β, to compute the probability measure of this set, and to compare it with p. For this purpose, it is more appropriate to use an equational representation of β, namely PDLR (PDL with recursion), which was introduced in [START_REF] Mateescu | Efficient on-the-fly model-checking for regular alternation-free mu-calculus[END_REF] for model checking PDL formulas. A PDLR specification is a system of fixed point equations having propositional variables X ∈ X in their left hand side and PDL formulas ϕ in their right hand side:

{X i = ϕ i } 1≤i≤n
where ϕ i are modal state formulas (see Fig. 1) and X 1 is the variable of interest corresponding to the desired property. Since formulas ϕ i may be open (i.e., contain occurrences of variables X j ), their interpretation is defined w.r.t. a propositional context ρ : X → 2 S , which assigns state sets to all variables occurring in ϕ i . The interpretation of a PDLR specification is the value of X 1 in the least fixed point µΦ of the functional Φ : (2 S ) n → (2 S ) n defined by:

Φ(U 1 , ..., U n ) = [[ϕ i ]] ρ [U 1 /X 1 , ..., U n /X n ] 1≤i≤n
where [[ϕ i ]] ρ = {s ∈ S | s |= ρ ϕ i }, and the interpretation of ϕ i (see Fig. 1) is extended with the rule "s |= ρ X iff s ∈ ρ(X)". The notation ρ [U 1 /X 1 , ..., U n /X n ] stands for the context ρ in which X i were assigned U i .

In the sequel, we consider PDLR specifications in derivative normal form (RNF), which are the modal logic counterparts of Brzozowski's (generalized) derivatives of regular expressions [START_REF] Brzozowski | Derivatives of regular expressions[END_REF]:

X i = ni j=1 (ϕ ij ∧ β ij X ij ) ∨ ϕ i 1≤i≤n
where ϕ ij and ϕ i are closed state formulas. Note that, in the right hand side of equation i, the same variable X ij ∈ {X 1 , ..., X n } may occur several times in the first disjunct. Intuitively, a variable X i denotes the set of states from which there exists a path with a prefix satisfying some of the regular formulas β ij and whose last state satisfies X ij . This is formalized using path predicates P i : Paths M → bool, defined by the following system of equations:

       P i (σ) = ni j=1 ∃l ij ≥ 0.(σ[0] |= ϕ ij ∧ σ[0, l ij ] |= β ij ∧ P ij (σ lij )) ∨ σ[0] |= ϕ i        1≤i≤n More precisely, (µΦ) i = {s ∈ S | ∃σ ∈ Paths M (s).P i (σ)}.
The PDLR specification in RNF associated to a formula β is defined below:

{X 1 = β X 2 X 2 = true}
in which the variable of interest X 1 denotes the PDL formula β true, expressing the existence of a path with a prefix satisfying β and leading to some final state denoted by X 2 . The corresponding path predicates are:

{P 1 (σ) = ∃l ≥ 0.(σ[0, l] |= β ∧ P 2 (σ l )) P 2 (σ) = true}
According to the interpretation of regular formulas (see Fig. 1), the path predicate P 1 (σ) holds iff σ |= β, and also (µΦ

) 1 = {s ∈ S | ∃σ ∈ Paths M (s).σ |= β}.

Translation to HML with recursion.

To bring the PDLR specification closer to an equation system suitable for verification, one must simplify it by removing the regular operators occurring in modalities. This yields a HMLR (HML with recursion) specification [START_REF] Larsen | Proof systems for Hennessy-Milner logic with recursion[END_REF], which contains only HML modalities on action formulas. Regular operators can be eliminated by applying the following substitutions, which are valid equalities in PDL [START_REF] Fischer | Propositional dynamic logic of regular programs[END_REF]:

ϕ? X = ϕ ∧ nil X β 1 .β 2 X = β 1 X where X = β 2 X β 1 |β 2 X = β 1 X ∨ β 2 X β * X = nil X where X = nil X ∨ β X
The rules for the '.' and '*' operators create new equations, necessary for maintaining the PDLR specification in RNF (the insertion of nil X modalities, which are

X1 = (true * .head ) * .dice4 X2 X2 = true                    X1 = nil X4 X2 = true X3 = dice4 X2 X4 = nil X3 ∨ nil X5 X5 = nil X7 X6 = head X4 X7 = nil X6 ∨ true X7                       X1 = dice4 X2 ∨ head X1 ∨ true X7 X2 = true X7 = head X1 ∨ true X7    (b) PDLR (c) HMLR (d) guarded HMLR        X1 = dice4 X2 ∨ head X1 ∨ ¬(head ∨ dice4) X7 X2 = true X7 = head X1 ∨ ¬head X7                           Z1,0 = 0.5 • Z1,1 + 0.5 • Z7,2 Z7,2 = 0.5 • Z1,5 + 0.5 • Z7,6 Z1,5 = 0.5 • Z1,10 + 0.5 • Z7,11 Z1,10 = 1.0 Z7,6 = 0.5 • Z1,2 + 0.5 • Z7,12 Z1,2 = 0.5 • Z1,5 + 0.5 • Z7,6                                                       X1,1 = X1,3 ∨ X7,4 X1,3 = X1,7 X1,7 = X7,7 X7,4 = X1,8 ∨ X7,9 X1,8 = X7,8 X7,7 = X7,7 X7,8 = X7,8 X7,9 = X7,9 X7,11 = X7,11 X7,12 = X7,12                                    (e) deterministic HMLR (f) LES (g) BES (excerpt)
Fig. 2: Model checking formula Ψ 1 = {(true * .head ) * .dice 4 } ≥0.16 on the PTS simulating the six-sided dice using a coin equivalent to X, serves the same purpose). The rule for the '|' operator creates two occurrences of the same variable X, reflecting that a same state can be reached by two different paths. These rules preserve the path predicates P i associated to the PDLR specification, and in particular P 1 (σ), which specifies that a path σ satisfies the initial formula β.

The size of the resulting HMLR specification (number of variables and operators) is linear w.r.t. the size of β (number of operators and action formulas). Besides pure HML modalities, the HMLR specification may also contain occurrences of nil X modalities, which will be eliminated in the next step.

3.

Transformation to guarded form. The right hand side of an equation i of the HMLR specification may contain modalities of the form α ij X ij and nil X ij (equivalent to X ij ), which correspond to guarded and unguarded occurrences of variables X ij , respectively. To facilitate the formulation of the verification problem in terms of equation systems, it is useful to remove unguarded occurrences of variables. The general procedure for transforming arbitrary µ-calculus formulas to guarded form [START_REF] Kozen | Results on the propositional µ-calculus[END_REF] can be specialized for HMLR specifications by applying the following actions for each equation defining X i :

-Remove the unguarded occurrences of X i in the right hand side of the equation defining X i by replacing them with false, which amounts to apply the µcalculus equality µX.(X ∨ ϕ) = µX.ϕ. -Substitute all unguarded occurrences of X i in other equations with the right hand side formula of equa-tion i, and rearrange the right hand sides to maintain the equations in RNF.

This produces a guarded HMLR specification:

X i = ni j=1 (ϕ ij ∧ α ij X ij ) ∨ ϕ i 1≤i≤n
which is the exact modal logic counterpart of Brzozowski's derivatives of regular expressions [START_REF] Brzozowski | Derivatives of regular expressions[END_REF] defined on the alphabet of action formulas. The transformation to guarded form generally decreases the number of equations in the HMLR specification (by producing unreachable and/or duplicate equations, which are eliminated), but may increase the number of operators in the right hand sides.

Determinization.

A guarded HMLR specification may contain, in the right hand side of an equation i, several alternatives ϕ ij ∧ α ij X ij whose guards ϕ ij and/or action formulas α ij are not disjoint, i.e., they can match the same transition going out of the current state. This is a form of nondeterminism, meaning that the same transition s a → s can start a path σ satisfying the path predicate P i (σ) in several ways, corresponding to alternative suffixes of the initial regular formula β. To ensure a correct translation of the verification problem into a LES, it is necessary to determinize the equations. This can be done by applying the classical subset construction, which produces a deterministic HMLR specification defined on meta-variables (i.e., sets of propositional variables):

                   X I = ∅⊂J⊆alt(I) ∅⊂L⊆J ij∈J ϕ ij ∧ i j ∈alt(I)\J ¬ ϕ i j ∧ kl∈L α kl ∧ k l ∈J\L ¬ α k l X L ∨ i∈I ϕ i                    I⊆[1,n]
where I ⊆ [1, n] is a subset of the variable indices and X I is a shorthand notation for the meta-variable

{X i | i ∈ I}. Given a subset I, the set of indices of al- ternatives contained in the equations defining variables in X I is alt(I) = {ij | i ∈ I ∧ j ∈ [1, n i ]}. A transition s a → s matches an alternative ϕ ij ∧ α ij X ij if s |= ϕ ij , a |= α ij ,
and s |= X ij . Intuitively, the right hand side of the meta-equation defining X I is obtained by considering all situations when a transition s a → s matches a subset of the alternatives alt(I) and requiring that the target state s satisfies the meta-variable induced by the matching alternatives. For a transition s a → s to match a subset of alternatives J ⊆ alt(I), state s must satisfy all guards ϕ ij of alternatives in J, and none of the guards of alternatives in alt(I) \ J. Then, for all modalities α ij X ij contained in the alternatives in J, it may be the case that a satisfies only the action formulas contained in a subset L ⊆ J of alternatives (and none of the action formulas of the alternatives in J \L), and therefore s must satisfy the meta-variable X L . As shown in [START_REF] Mateescu | CTRL: Extension of CTL with regular expressions and fairness operators to verify genetic regulatory networks[END_REF] for a similar construction in the state-based setting, the determinization preserves the path predicate associated to the variables of interest X 1 and X {1} in the HMLR before and after determinization, i.e., P 1 (σ) = P {1} (σ) for any path σ ∈ Paths M .

In the worst case, determinization may yield an exponential increase in the size of the HMLR specification. However, this happens on pathological examples of regular formulas, which rarely occur in practice; most of the time, the nondeterminism contained in a formula β is caused by a lack of precision regarding the iteration operators, which can be corrected by constraining the action formulas corresponding to iteration "exits". For example, the regular formula contained in Ψ 1 can be made deterministic by specifying precisely that the occurrences of the head action are separated by actions other than head and by taking into account that, in the PTS of Figure 2(a), a dice action cannot occur before a head : ((¬head ) * .head ) * .dice 4 . In practice, the size of the determinized HMLR specification can be reduced by eliminating duplicate equations and by identifying contradictory combinations and absorptions of action formulas (α 1 ∧ α 2 = false and α 1 ∧ ¬α 2 = α 1 when α 1 , α 2 are disjoint).

Translation to linear and Boolean equation systems.

Consider a determinized HMLR specification in RNF (in which the meta-variables have been renamed into ordinary propositional variables) corresponding to a regular formula β:

X i = ni j=1 (ϕ ij ∧ α ij X ij ) ∨ ϕ i 1≤i≤n
where α ij ∧α ik = false for each i ∈ [1, n] and j, k ∈ [1, n i ] with j = k. The associated path predicates are defined as follows:

       P i (σ) = ni j=1 (σ[0] |= ϕ ij ∧ σ a [0] |= α ij ∧ P ij (σ 1 )) ∨ σ[0] |= ϕ i        1≤i≤n
They are related to the HMLR specification by (µΦ) i = {s ∈ S | ∃σ ∈ Paths M (s).P i (σ)}, and to the initial regular formula β by P 1 (σ) = σ |= β.

The last step of the model checking method reformulates the problem of verifying the determinized HMLR specification on a PTS in terms of solving a LES ( * ) and a BES ( * * ) defined as follows:

                                 Z i,s = if s |= X i then 0 else if s |= ϕ i then 1 else ni j=1 if s |= ϕ ij then 0 else s a → s a |= αij P(s, a, s ) • Z ij,s                                  1 ≤ i ≤ n s ∈ S ( * )            X i,s = ni j=1 s |= ϕ ij ∧ s a →s a |= α ij ∧ X ij,s ∨ s |= ϕ i            1 ≤ i ≤ n s ∈ S ( * * )
The LES ( * ) is obtained by a translation similar to the classical one defined originally for PCTL [START_REF] Hansson | A logic for reasoning about time and reliability[END_REF]. A numerical variable Z i,s denotes the probability measure of the paths going out of state s and satisfying the path predicate P i . The BES ( * * ), with minimal fixed point semantics, is produced by the classical translation employed for model checking modal µ-calculus formulas on LTSs [START_REF] Cleaveland | A linear-time modelchecking algorithm for the alternation-free modal mucalculus[END_REF][START_REF] Andersen | Model checking and boolean graphs[END_REF]. A Boolean variable X i,s is true iff state s satisfies the propositional variable X i of the HMLR specification. The on-the-fly model checking consists in solving the variable Z 1,s i , which denotes the probability measure of the set of paths going out of the initial state s i of the PTS and satisfying the initial regular formula β. This is carried out using local LES and BES resolution algorithms, as will be explained in Section 5. The conditions s |= X i occurring in the LES ( * ) and the conditions s |= ϕ ij , s |= ϕ i occurring in both equation systems are checked by applying the on-the-fly model checking method for solving the variable X s i of the BES ( * * ) and for evaluating the closed state formulas ϕ ij , ϕ i on state s.

The determinization of the HMLR specification guarantees that the sum of coefficients in the right hand side of each equation of the LES is at most 1. If the HMLR specification is not determinized, such as the one shown in Figure 3(c), the LES encoding the interpretation of the formula on the PTS in Figure 3(a) has the wrong solution Z 1,0 = 2.0 (variable Z 1,2 = 0 since s 2 |= X 1 , and variables Z 2,1 = Z 2,2 = 1 since X 2 = true). This is because the nondeterministic equation defining X 1 in the HMLR specification matches twice the suffix of the path going out of s 0 . Note that determinization ensures a sound LES translation also if some states have several outgoing transitions labeled by the same action a.

The condition s |= X i surrounded in the LES (*) has the role of pruning the exploration of the PTS if the current state s does not have any outgoing path matching the suffix of β denoted by X i . As explained in [START_REF] Baier | Principles of model checking[END_REF]Chap. 10], this is necessary to avoid singularities in the

a 1.0 a 1.0 b 1.0 s0 s1 s2 X1 = a X2 ∨ true X1 X2 = true (a) PTS (c) guarded HMLR {true * .a} ≥0 Z1,0 = 1.0 • Z2,1 + 1.0 • Z1,1 Z1,1 = 1.0 • Z2,2 + 1.0 • Z1,2 (b) formula (d) LES
Fig. 3: Nondeterministic regular formula

a 0.5 s0 s1 c 1.0 b 0.5 X1 = a X2 ∨ ¬a X1 X2 = true (a) PTS (c) deterministic HMLR {(¬a) * .a} ≥0 Z1,0 = 0.5 • Z2,0 + 0.5 • Z1,1 Z1,1 = 1.0 • Z1,1 (b) formula (d) LES
Fig. 4: Unreachable path suffix LES and ensure a unique solution. For example, if we neglect the condition s |= X i when checking the deterministic HMLR specification shown in Figure 4(c) on the PTS shown in Figure 4(a), the resulting LES contains the singular equation Z 1,1 = Z 1,1 . This is precisely because s 1 |= X 1 , meaning that from s 1 there is no path matching the regular formula suffix denoted by X 1 . By solving the LES obtained in Figure 2(f), we obtain Z 1,0 = 1/6, meaning that tossing the head of the coin an (arbitrarily large) number of times corresponds to rolling the four-side of the dice with 1/6 probability, and therefore the formula Ψ 1 is valid on the PTS. The numerical variables Z 1,1 , Z 7,11 , and Z 7,12 surrounded by boxes in Figure 2(f) are equal to 0, since the path suffixes denoted by the propositional variables X 1 and X 7 are not reachable from states s 1 , s 11 , and s 12 of the PTS; this is checked by solving the Boolean variables X 1,1 , X 7,11 , and X 7,12 of the BES in Figure 2(g), which are equal to false. If we evaluate the Ψ 1 formula for every dice i action, we obtain a probability equal to 1/6 for i ∈ {1, 2, 4} and to 0 for i ∈ {3, 5, 6}, the latter sides of the dice being not directly reachable after a head action.

Extension with data handling

The regular formulas that we used so far belong to the dataless fragment [START_REF] Mateescu | Efficient on-the-fly model-checking for regular alternation-free mu-calculus[END_REF] of MCL, which considers actions simply as names of communication channels. In practice, the analysis of value-passing concurrent systems, whose actions typically consist of channel names and data values, requires the ability to extract and manipulate these elements. For this purpose, MCL [START_REF] Mateescu | A model checking language for concurrent value-passing systems[END_REF] provides action predicates extracting and/or matching data values, regular formulas involving data variables, and parameterized fixed point operators. The regular probabilistic operator {β} ≥p can be naturally extended with the data handling regular formulas of MCL, which enable to characterize complex paths in a PTS modeling a value-passing concurrent system.

To improve versatility, we extend the regular formulas of MCL with a general iteration operator "loop", which subsumes the classical regular operators with counters, and can also specify paths having a certain cost calculated from the data values carried by its actions. After briefly recalling the main data handling operators of MCL, we define the "loop" operator, illustrate its expressiveness, and show how the on-the-fly model checking procedure previously described is generalized to deal with the data handling probabilistic operator.

Overview of data handling MCL operators

In the PTSs modeling value-passing systems, actions are of the form "c v 1 . . . v n ", where c is a channel name and v 1 , ..., v n are the data values exchanged during the rendezvous on c. To handle the data values contained in actions, MCL provides several basic constructs, defined in Figure 5. Data expressions e are built over data variables x and functions f (restricted, for simplicity, to a single argument in Fig. 5). The interpretation of e is defined w.r.t. a data context δ assigning values to all data variables occurring in e.

Actions containing data are specified using action predicates of the form "{c !e}" (value matching) or "{c ?x:T }" (value extraction). The former predicate matches an action c v with v equal to the value of e, whereas the latter predicate also captures the value v (which must be of type T ) and stores it in the variable x. The successful evaluation of a predicate "{c ?x:T }" on an action a also produces a data context env a ({c ?x:T }) where x is assigned the value extracted from a. The action predicates of MCL are slightly more involved than those shown in Figure 5: several clauses "!e" and "?x:T " can be freely combined (the variables defined in the extraction clauses are visible inside the action predicate and also in the enclosing formula), the "..." wildcard can be used to match zero or more values, and an optional clause "where b" can be used to specify a Boolean condition b over the extracted variables. An action satisfies an action predicate if its structure is compatible with the clauses of the predicate and the "where" guard (if present) evaluates to true in the context of the data variables extracted from that action.

Expressions:

e ::= x | f (e) [[x]] δ = δ(x) [[f (e)]] δ = f ([[e]] δ)
Action patterns:

α ::= {c !e} | {c ?x:T } [[{c !e}]] δ = {c [[e]] δ} [[{c ?x:T }]] δ = {c v | v ∈ T } env c v ({c ?x:T }) = [v/x] if v ∈ T env a(α) = [ ] otherwise
State formulas:

ϕ ::= α ϕ | Y (e) | µY (x:T :=e).ϕ [[ α ϕ]] ρδ = {s ∈ S | ∃s a → s .a ∈ [[α]] δ ∧ s ∈ [[ϕ]] ρ(δ env a(α))} [[Y (e)]] ρδ = ρ(Y )([[e]] δ) [[µY (x:T :=e).ϕ]] ρδ = µΦ ρδ ([[e]] δ)
where

Φ ρδ : (T → 2 S ) → (T → 2 S ), (Φ ρδ (F ))(v) = [[ϕ]] (ρ [F/Y ])(δ [v/x])
Fig. 5: Syntax and semantics of basic MCL operators

The basic state formulas of MCL are built from Boolean connectors, modalities, and parameterized fixed point operators (restricted, for simplicity, to a single parameter in Fig. 5). A fixed point formula µY (x:T :=e).ϕ denotes both the definition and the call in situ of a propositional variable Y parameterized by x. Its interpretation w.r.t. a propositional context ρ and a data context δ is the call of µΦ ρδ with the value of e in the context δ, µΦ ρδ being the minimal solution of the equation Y (x) = ϕ interpreted w.r.t. the contexts ρ and δ.

Regular formulas in MCL are built over action predicates using the classical operators shown in Section 2, as well as constructs inspired from sequential programming languages: conditional ("if-then-else"), counting, iteration ("for" and "loop", described in Subsection 4.2), and definition of variables ("let"). Finally, the state formulas of MCL also provide modalities containing regular formulas, quantifiers over finite domains, and programming language constructs ("if" and "let") [START_REF] Mateescu | A model checking language for concurrent value-passing systems[END_REF].

Generalized iteration on regular formulas

The general iteration mechanism that we propose on regular formulas consists of three operators having the following syntax:

β ::= loop (x:T :=e 0 ) : (x :T ) in β end loop | continue (e) | exit (e )
The "loop" operator denotes a path made by concatenation of (zero or more) path fragments satisfying β, each one corresponding to an iteration of the loop with the current value of variable x. The iteration variable x, which is visible inside the loop body β, is initialized with the value of expression e 0 at the first loop iteration and can be updated to the value of e by using the operator "continue (e)", which starts a new iteration of the loop. The loop is terminated by means of the "exit (e )" operator, which sets the return variable x , visible outside the "loop" formula, to the value of e .

The iteration and return variables (x and x ) are both optional; if they are absent, the "in" keyword is also omitted. For simplicity, we used only one variable x and x , but several variables of each kind are allowed. The arguments of the operators "continue" and "exit" invoked in the loop body β must be compatible with the declarations of iteration and return variables, respectively. Every occurrence of "continue" and "exit" refers to the immediately enclosing "loop", which enforces a specification style similar to structured programming.

For conciseness, we define the semantics of the "loop" operator by translating it to basic MCL in the context of an enclosing diamond modality (a dual translation holds for an enclosing box modality). The translation loop2mcl Z/x:T /x :T (ϕ) is defined in Figure 6, where x and x are the iteration and return data variables of the immediately enclosing "loop", and Z is the propositional variable associated to it. Basically, a possibility modality enclosing a "loop" operator is translated into a minimal fixed point operator parameterized by the iteration variable(s). The occurrences of "continue" in the body of the loop are translated into calls of the propositional variable with the corresponding arguments, and the occurrences of "exit" are translated into "let" state formulas defining the return variables and assigning them the corresponding return values. The rules for the other regular operators generalize those of the translation from PDL to modal µ-calculus [START_REF] Emerson | Efficient model checking in fragments of the propositional mu-calculus[END_REF].

All iteration operators on MCL regular formulas can be expressed in terms of the "loop" operator, as shown in Table 1. For simplicity, we omitted the definition of β * , β + , β{e} (iteration e times), and β{... e} (iteration at most e times), which are equivalent to β{0 ...}, β{1 ...}, β{e ... e}, and β{0 ... e}, respectively.

To illustrate the semantics of general iteration, consider the formula β{e} true stating the existence of a path made of e path fragments satisfying β. By encoding bounded iteration as a "loop" and applying the translation rules of general iteration, we obtain:

:= e2 -e1) times in if c1 > 0 then β . continue (c1 -1, c2) elsif c2 > 0 then exit | β . continue (c1, c2 -
:= e). if c > 0 then β Z(c -1) else true end if
The bounded iteration operators β{e}, β{e ...}, and β{e 1 ... e 2 } are natural means for counting actions (ticks), and hence describing discrete-time properties. The full Until operator of PCTL, and its action-based counterparts derived from ACTL, can be expressed as follows (where t ≥ 0 is the number of ticks until ϕ 2 ): Besides counting, the "loop" operator can characterize complex paths in a PTS, by collecting the data values (costs) present on actions and using them in arbitrary computations, as it will be illustrated in Section 6.

ϕ 1 U ≤t ϕ 2 ≥p = {(ϕ 1 ?.true){0 ... t}.ϕ 2 ?} ≥p ϕ 1α 1 U ≤t ϕ 2 ≥p = {(ϕ 1 ?.α 1 ){0 ... t}.ϕ 2 ?} ≥p ϕ 1α 1 U ≤t α2 ϕ 2 ≥p = {(ϕ 1 ?.α 1 ){0 ... t}.ϕ 1 ?.α 2 .ϕ 2 ?} ≥p

Model checking method with data handling

The on-the-fly model checking method described in Section 3 can be generalized to deal with the data handling constructs of MCL by adding data parameters to the various equation systems used as intermediate forms.

We illustrate the complete method on a data handling version of the PTS modeling the six-sided dice using a fair coin, shown on Figure 7(a). The actions of tossing the head and tail of the coin are denoted by "toss 1" and "toss 0", and the actions corresponding to the dice faces are denoted by "dice i" for 1 ≤ i ≤ 6. We will check on this PTS the formula Ψ 2 , stating that the probability of reaching the dice side marked with one by tossing first a side of the coin and then tossing the same side at most n times (where n is a parameter to be instantiated) is at least 10%:

Ψ 2 = { {toss ?v:nat}. ((¬{toss !v}) * .{toss !v}){... n}. {dice !1} } ≥0.1
The various translation phases are illustrated on Figure 7. The translation rules for standard regular operators given in Section 3, extended with data handling, are applied for eliminating the "." operators in the PDLR specification. To facilitate the subsequent model checking steps, the new equations introduced by these rules are data-closed, i.e., the propositional variables in their left hand sides are parameterized by the data variables occurring in their right hand side formulas. For example, when translating the right hand side of the equation defining X 1 , the extended rule applied is {toss ?v:nat}.β X 2 = {toss ?v:nat} X 3 (v), where X 3 (v) = β X 2 , ensuring that data variable v occurring in β is a parameter of X 3 . Then, the iteration at most n times is translated into a "loop" operator, and the corresponding modality is further refined using the semantics of "loop" defined in Section 4.2, yielding a HMLR specification parameterized by a counter c and by the value v of the coin side captured by the first action of the regular formula (Fig. 7(c)).

This HMLR specification is then brought to guarded form (Fig. 7(d)) by carrying out systematically the appropriate substitutions and keeping track of the data parameters. For example, variable X 3 (v) is replaced by X 5 (v, n) in the equation of X 1 , and X 6 (v, c) is replaced by {toss !v} X 5 (v, c-1) in the equation defining

X 7 (v, c).
The guarded HMLR specification is determinized by ensuring that the alternatives in the right hand side of equation defining X 5 (v, c) are mutually exclusive (all the other equations being already deterministic). This produces the alternatives {dice !1} ∧ ¬{toss !v} {X 2 , X 7 (v, c)} and ¬{toss !v} ∧ ¬{dice !1} {X 7 (v, c)}. The former alternative is equivalent to {dice !1} {X 2 } because {dice !1} ⇒ ¬{toss !v} and X 2 denotes the final states of the paths satisfying the initial regular formula. The other alternatives present in the equations led to singleton meta-variables, which are replaced by the variables themselves (Fig. 7(e)).

Next, a parameterized LES is produced (Fig. 7(f)) by the translation scheme given in Section 3, extended to handle data parameters. For instance, variable Z 5,1 (1, n) in the LES denotes the probability measure of the paths starting from state s 1 and satisfying the path predicate denoted by X 5 with the parameters v and c set to 1 and n, respectively. The numerical variables Z 5,2 (0, n) and Z 7,4 (1, c) surrounded by boxes in Figure 7(f) are equal to 0, since the path suffixes denoted by the propositional variables X 5 (0, n) and X 7 (1, c) are not reachable from states s 2 and s 4 of the PTS (this is checked by solving the corresponding Boolean variables of the BES, not shown in Figure 7). Finally, a plain LES is generated (Fig. 7(g)) by instantiating n = 2 in the parameterized LES. By solving this LES (e.g., using substitution), we obtain Z 1,0 = 0.125, which is the probability measure of the paths starting from the initial state s 0 of the PTS and satisfying the regular formula specified in Ψ 2 . In other words, tossing first a side of the coin, then tossing again the same side at most n = 2 times corresponds with 12.5% probability to rolling the one-side of the dice, and therefore the Ψ 2 formula is valid on the PTS in Figure 7(a). If we evaluate the Ψ 2 formula with n = 2 for every action "dice i", we obtain a probability equal to 0.125 for i ∈ {1, 6}, to 0.156 for i ∈ {2, 5}, and to 0 for i ∈ {3, 4}, the latter sides of the dice being not reachable after tossing once, then at most n = 2 times the same side of the coin.

Soundness and termination of the method

The presence of data parameters (with infinite domains) in the regular formulas β makes necessary two additional hypotheses about the structure of β in order to ensure the feasibility of our model checking method for the probabilistic operator {β} ≥p .

Soundness of the translation to guarded form. The translation of (parameterized) HMLR specifications to guarded form relies on the absorption property for µcalculus formulas with data parameters:

µX(u).(X(u) ∨ ϕ) = µX(u).ϕ
where ϕ may contain occurrences of the propositional variable X with arbitrary data arguments. The above equality does not hold anymore if the unguarded occurrence of X in the left hand side has an argument e different from the parameter u. Typically, such cases correspond to regular formulas that perform pure computations on data without exploring any transition in the PTS. For example, the following regular modality specifies the classical primality testing of a natural number n (odd and greater than 3) by checking that n is not divided by any of the odd numbers from 3 to √ n:

loop (k:nat:=3) : (r:bool) in if k * k > n then exit (true) elsif n%k = 0 then exit (false) else continue (k + 2) end if end loop r
The corresponding HMLR specification, shown below, contains the unguarded occurrence X 2 (k+2), which cannot be eliminated by absorption:

                       X 1 = X 2 (3) X 2 (k) = if k * k > n then true elsif n%k = 0 then false else X 2 (k + 2) end if                       
In practice, we forbid such kind of regular formulas purely operating on data, since they can be replaced by functions, and we reserve regular formulas for the specification of (non empty) paths in the PTS.

Termination of the LES and BES construction. After translating the regular formula into a (parameterized) deterministic HMLR specification, the last phase of the model checking procedure consists in generating and solving on the fly the LES and BES. These systems depend not only on the (finite) information contained in the PTS, but also on the values of the data parameters (with infinite domains) created during instantiation. Therefore, the convergence of the whole procedure relies on the termination of the instantiation phase, which must create finite LES and BES. This is in general undecidable, similarly to the termination of term rewriting [START_REF] Dershowitz | Termination of rewriting[END_REF]. Typically, such situations happen for "pathological" formulas, which carry on divergent computations unrelated to the data values contained in the PTS actions. For example, the following modality: loop (k:nat:=0) in a . continue (k + 1) end loop true will not converge on the PTS consisting of a single loop s a 1.0 → s, since it will entail the construction of an infinite LES {Z s (0) = Z s (1), Z s (1) = Z s (2), ...}. In practice, for such divergent formulas, the instantiation phase will attempt to generate an infinite LES, eventually causing the whole model checking procedure to abort when the available memory is exhausted.

The regular formulas β used in the probabilistic operator are meant to characterize finite paths in the PTS.

           X1 = {toss ?v:nat}. ((¬{toss !v}) * . {toss !v}){... n}. {dice !1} X2 X2 = true
Ensuring this becomes undecidable in the presence of the generalized iteration operator "loop", which enables the specification of arbitrary (Turing computable) paths in a PTS. However, the model checking procedure terminates for most practical cases of data handling regular formulas denoting finite paths (counting, accumulating or aggregating values, computing costs over paths).

Tool support

We implemented the on-the-fly model checking method described in Sections 3 and 4 within the CADP toolbox [START_REF] Garavel | CADP 2011: A Toolbox for the Construction and Analysis of Distributed Processes[END_REF]. We briefly present here the extension of the existing on-the-fly model checker of MCL with the regular probabilistic operator, and the representations of PTS and DTMC models suitable for probabilistic analysis.

Extension of MCL and its model checker. We extended MCL with the general iteration operator "loop" on regular formulas and the regular probabilistic operator {β} p , where ∈ {<, ≤, >, ≥, =}. Temporal and probabilistic operators can be freely combined, e.g., [β 1 ] {β 2 } ≥p specifies that, from all states reached after a path satisfying β 1 , the probability measure of an outgoing path satisfying β 2 is at least p. Also, using the MCL quantifiers on finite data domains, one can succinctly describe data handling probabilistic properties, such as the fact that after zero or more coin tosses, each side of the dice is reached with 1/6 probability: forall i:nat among {1...6}.{ {toss ...} * .{dice !i} } ≥1/6 .

We also enhanced the EVALUATOR [START_REF] Mateescu | A model checking language for concurrent value-passing systems[END_REF] on-the-fly model checker with the translation of {β} p formulas into BESs (for checking the existence of path suffixes) and LESs (for computing probability measures) as described in Sections 3 and 4. The on-the-fly resolution of BESs is carried out by the algorithms of the CAE-SAR SOLVE library [START_REF] Mateescu | Caesar solve: A generic library for on-thefly resolution of alternation-free boolean equation systems[END_REF], which already serves as verification back-end for (non-probabilistic) MCL formulas. The resolution algorithms work in a systolic manner: several subsequent invocations of an algorithm for solving different variables of a BES have a linear overall complexity in the size of the BES (number of variables and operators), obtained by keeping the values of all variables computed during intermediate resolutions.

For the on-the-fly resolution of LESs, we designed a local algorithm operating on the associated Signal Flow Graphs (SFG) [START_REF] Chua | Computer Aided Analysis of Electronic Circuits[END_REF], in a way similar to the BES resolution algorithms, which operate on the associated Boolean graphs [START_REF] Andersen | Model checking and boolean graphs[END_REF]. Figure 8 illustrates the SFG of the LES corresponding to the evaluation of property Ψ 1 on the PTS of the six-sided dice, shown in Figure 2(f). In the SFG, each vertex corresponds to a variable of the LES and each edge Z i,s q → Z j,r denotes a dependency of Z i,s upon Z j,r , i.e., the fact that the term q • Z j,r occurs in the right hand side of the equation defining Z i,s (e.g., edges Z 1,0 0.5

→ Z 1,1 and Z 1,0 0.5 → Z 7,2 represent the equation Z 1,0 = 0.5 • Z 1,1 + 0.5 • Z 7,2
). Constants are represented as sink vertices (e.g., Z 1,1 or Z 1,10 ). Self-loops Z i,s q → Z i,s are deleted during the construction of the SFG by updating the coefficients on the edges going out

of Z i,s (an edge Z i,s qij → Z j,r becomes Z i,s qij /(1-q) → Z j,r
). The on-the-fly LES resolution algorithm carries out a forward DFS (depth-first search) exploration of the SFG with detection of SCCs (strongly connected components), starting at the vertex of interest. The SFG is constructed on demand in the following way. For each vertex Z i,s , the BES solver is invoked on the Boolean variable X i,s to determine whether s has an outgoing sequence matching the suffix of the regular formula β denoted by the propositional variable X i of the determinized HMLR specification (see Fig. 2(e)). If variable X i,s is false, the vertex Z i,s denotes a constant 0, like the boxed vertices Z 1,1 , Z 7,11 , and Z 7,12 in Figure 8. When a constant vertex Z j,r is encountered, its value is propagated backwards to its predecessor vertex Z i,s on the DFS stack, which amounts to perform the substitution of Z j,r in the right-hand side of the equation defining Z i,s . If the vertex Z i,s on top of the stack becomes stable (i.e., the values of all its successor vertices have been computed), its value is stored for possible later reuse and is propagated backwards as if Z i,s was a constant.

If variable X i,s is true, then the SFG edges going out of Z i,s are constructed by scanning the right hand side of the corresponding equation in the LES, and the DFS exploration can proceed further. When a non-trivial SCC (i.e., containing at least two vertices) is encountered, the corresponding LES fragment induced by the vertices of the SCC is solved using either Gaussian elimination (for LES fragments with less than 1, 000 variables) or the Gauss-Seidel iterative method (for larger LES fragments). For the SFG in Figure 8, the DFS traversal will propagate backwards the values of vertices Z 1,1 , Z 1,10 , and Z 7,11 , stabilizing the vertex Z 1,5 at 0.5. Then, after propagating backwards the vertex Z 7,12 , the SCC {Z 7,6 , Z 1,2 } is detected and solved, stabilizing the vertices Z 7,6 and Z 1,2 at 1/6 and 1/3, respectively. Finally, vertex Z 7,6 is propagated and stabilizes vertex Z 7,2 at 1/3, and then the vertex of interest Z 1,0 at 1/6.

For the acyclic parts of the SFG, this algorithm amounts to a resolution by substitution, and stores in memory only the vertices (corresponding to LES variables). For each non-trivial SCC, the algorithm stores the vertices and the edges (corresponding to the operands in the right-hand sides of the LES equations) until the SCC has been solved. Therefore, the peak memory consumption is determined by the largest SCC contained in the SFG. In practice, it is often the case that the evaluation of probabilistic operators on PTSs produces LESs with SFGs that are not strongly connected (this is the case, e.g., for the SFG in Figure 8 and also for all properties shown in Section 6). In these situations, the SFG-based on-the-fly LES resolution can be Representation of PTSs. The concurrent systems under analysis in CADP are described formally using the LNT language [START_REF] Champelovier | Reference Manual of the LNT to LOTOS Translator (Version 6.2)[END_REF], inspired from value-passing process algebras and classical programming languages. An LNT description is compiled into an LTS represented implicitly as a C program implementing the successor function according to the OPEN/CAESAR application programming interface [START_REF] Garavel | OPEN/CAESAR: An Open Software Architecture for Verification, Simulation, and Testing[END_REF] for on-the-fly graph exploration. This LTS is converted on the fly into a PTS by adding probabilities to its actions (transition labels) using the label renaming feature of EVALUATOR. By default, all transitions going out of a state are equiprobable, in which case there is no need to specify any probability distribution (this happens, e.g., for the PTSs modeling the dice, shown in Fig. 2(a) and 7(a)). If one assigns a specific probability p to some action a, then for each state s having an outgoing transition s a → s , the remaining probability 1 -p is equally distributed on the actions labeling the neighbour transitions s b → s . In this way, an LNT description can be converted on the fly (without any additional annotation) into a PTS during the verification of a probabilistic MCL formula.

Representation of DTMCs. Although the modeling and verification approach of CADP is action-based, the underlying models can be adapted to accomodate for statebased analysis, by encoding the relevant information on actions instead of states. Thus, a DTMC having atomic propositions on states can be converted into a PTS by "pushing" all state information on the actions labeling the outgoing transitions. For example, if a set of atomic propositions q 1 , ..., q n hold on a state s of a DTMC, then the transitions going out of s in the corresponding PTS will be labeled by actions of the form "A q 1 . . . q n " and will keep the same probabilities as in the DTMC. This scheme, which does not change the structure of the graph, relies on the data handling modalities of MCL for expressing atomic propositions on states: a state satisfying q i in the DTMC satisfies the diamond modality {A ?any ... ?any !q i ...} true in the PTS, where "?any" is a wildcard matching a value of any type. Using the macro-definition mechanism of MCL, the atomic propositions can be encoded as macros with symbolic names and reused in state-based formulas.

In this way, one can check state-based properties using the PCTL operators encoded in terms of {β} ≥p as shown in Section 4.2. Moreover, the regular operators of MCL enable one to specify properties more expressive than Until operators, such as {send ?.true.(retry?.true * ) * .recv ?} ≥0.9 , where the atomic propositions like send are macro-definition names for the modalities {A !send } true and they are checked on states using the testing operator "?" of PDL.

Case studies

We illustrate the application of the regular probabilistic operator by carrying out a probabilistic analysis of several concurrent systems. First, we consider several shared-memory mutual exclusion protocols (Sec. 6.1), and corroborate the results of the probabilistic analysis with those previously obtained by a steady-state analysis using CTMCs in [START_REF] Mateescu | Model Checking and Performance Evaluation with CADP Illustrated on Shared-Memory Mutual Exclusion Protocols[END_REF]. Then, we compare our on-thefly model checker procedure with the explicit-state algorithms of the probabilistic model checker PRISM [START_REF] Kwiatkowska | PRISM 4.0: Verification of probabilistic real-time systems[END_REF], by analyzing the Bounded Retransmission Protocol (Sec. 6.2) and two randomized protocols (Sec. 6.3). All model checking experiments have been carried out on a single core of an Intel(R) Xeon(R) E5-2630v3 @2.4GHz with 128 GBytes of RAM and Linux Debian 7.9 within a cluster of Grid'5000 [START_REF] Bolze | Grid'5000: A large scale and highly reconfigurable experimental grid testbed[END_REF].

We considered the explicit-state engine of PRISM in order to achieve a consistent comparison with our onthe-fly verification algorithms, which operate on explicitstate PTSs; however, some of the performance figures reported below (e.g., in Sec. 6.2) are close to those of the PRISM benchmarks1 , which were conducted using the symbolic engine of PRISM. The time and memory consumption measured for the two tools include the time of constructing the model (i.e., launching the Java virtual machine and building the DTMC by PRISM, compiling the LNT description and converting the state space on the fly into a PTS by CADP). Given that PRISM and CADP are very different in their architecture, algorithms, and implementation, the experimental measures presented in this section are not meant to provide an absolutely precise comparison of the tools performance, but rather to give general tendencies for various sizes of the models considered.

Mutual exclusion protocols

We focus here on a subset of the 27 protocols specified in LNT and studied in [START_REF] Mateescu | Model Checking and Performance Evaluation with CADP Illustrated on Shared-Memory Mutual Exclusion Protocols[END_REF], namely the CLH, MCS, Burns&Lynch (BL), Lamport, Peterson, TAS and TTAS protocols, by considering configurations of N ≤ 5 concurrent processes competing to access the critical section. Each process executes cyclically a sequence of four sections: non critical, entry, critical, and exit. The entry and exit sections represent the algorithm specific to each protocol for demanding and releasing the access to the critical section, respectively. During these sections, each protocol carries out various operations (read, write, test-and-set, etc.) on the shared variables.

In the PTS models of the protocols, all transitions going out of each state have equal probabilities, meaning that each process has the same chances to execute. This kind of analysis by introducing probabilities may seem artificial in the case of mutual exclusion protocols. However, it provides a simple way to compare the performance of different protocols by estimating their respective "speed" in reaching certain actions, and also enabling to simulate particular situations of system load (e.g., for the contention property studied at the end of this section) by varying the probabilities assigned to the actions of certain processes. We found that this probabilistic analysis corroborates, and also complements, a stochastic analysis using IMCs (Interactive Markov Chains) previously carried out in [START_REF] Mateescu | Model Checking and Performance Evaluation with CADP Illustrated on Shared-Memory Mutual Exclusion Protocols[END_REF].

We formulate four probabilistic properties using MCL and evaluate them on the fly on each LNT protocol description. Since we are interested in the probability measures, we use the syntax {β} ? p instructing the model checker to display the probability measure computed for β in addition to the Boolean verdict. For each property requiring several invocations of the model checker with different values for the data parameters in the MCL formula, we automate the analysis using SVL scripts [START_REF] Garavel | SVL: a Scripting Language for Compositional Verification[END_REF].

Critical section. First of all, for each i ∈ [0, N -1], we compute the probability that process P i is the first one to enter its critical section. For this purpose, we use the following MCL formula:

{ (¬{CS !"ENTER"...}) * .{CS !"ENTER" !i} } ≥ ? 0
which computes the probability that, from the initial state, process P i accesses its critical section before any (other) process. Symmetric protocols guarantee that this probability is equal to 1/N for all processes, while asymmetric protocols (such as BL) may favor certain processes w.r.t. the others. This is indeed reflected by checking the above formula for N = 5: for the BL protocol, which gives higher priority to processes of lower index, the probabilities computed are 71.01% for P 0 , 21.33% for P 1 , 5.68% for P 2 , 1.53% for P 3 , and 0.43% for P 4 , whereas they are equal to 20% for all processes of the other, symmetric, protocols. This corroborates the results obtained by steady-state analysis using IMCs [START_REF] Mateescu | Model Checking and Performance Evaluation with CADP Illustrated on Shared-Memory Mutual Exclusion Protocols[END_REF], which pointed out the asymmetry of the BL protocol.

The SFGs of the LESs produced by EVALUATOR when checking this formula are not strongly connected, being even acyclic as e.g., the SFG obtained for the TAS protocol.

Memory latency. The analysis of critical section reachability can be refined by taking into account the cost of memory accesses (e.g., read, write, test-and-set operations on shared variables) that a process P i must perform before entering its critical section. The protocol modeling provided in [START_REF] Mateescu | Model Checking and Performance Evaluation with CADP Illustrated on Shared-Memory Mutual Exclusion Protocols[END_REF] also considers non-uniform memory accesses, assuming that concurrent processes execute on a cache-coherent multiprocessor architecture. The cost c (or latency) of a memory access performed by P i depends on the placement of the memory in the hierarchy (local caches, shared RAM, remote disks) and is represented in the PTS by actions of the form "MU ... c i" [START_REF] Mateescu | Model Checking and Performance Evaluation with CADP Illustrated on Shared-Memory Mutual Exclusion Protocols[END_REF].

The MCL formula below computes the probability that a process P i performs memory accesses of a total cost max before entering its critical section. The regular formula expresses that, after executing its non critical section for the first time, process P i begins its entry section and, after a number of memory accesses, enters its critical section:

{ (¬{NCS !i}) The "loop" subformula denotes the entry section of P i and requires that it terminates when the cost of all memory accesses performed by P i (accumulated in the iteration variable total cost) exceeds a given value max. The costs present on transitions are captured by the action pattern "{MU ... ?c:nat !i}" and used in the "continue" subformula to update the value of total cost. The other processes can execute freely during the entry section of P i , in particular they can overtake P i by accessing their critical sections before it.

Figure 9(a) shows the probability of entering the critical section for various values of max. Since the entry section contains waiting loops, the number of memory accesses of P i before entering its critical section is unbounded (and hence, also the cost max). However, the probability that a process waits indefinitely before entering its critical section tends to zero in long-term runs of starvation-free protocols. This explains the asymptotic probability 1.0 observed in Figure 9(a): a process has better chances to reach its critical section when the memory cost of its entry section increases. Moreover, the variation of probabilities shown in Figure 9(a) provides a comparison of the protocols w.r.t. the "speed" of reaching the critical section: the CLH protocol has the fastest increase of the probability, and therefore it uses most efficiently its accesses to shared variables. We can further refine the MCL formula above to infer the steady-state behavior by imposing a number of protocol executions before the entry section of P i (i.e., start accumulating the memory access cost after the r-th "NCS !i" action). For the TAS protocol, we observed a convergence of the probability when r = 5 for values of max between 5 (steady-state probability of 42.66%) and 30 (steady-state probability of 96.41%). The SFGs of the LESs produced by EVALUATOR for this MCL formula contain several SCCs, e.g., for the TAS protocol with 2 processes the SFG contains up to 32 SCCs, of which the largest one has 9 variables and was solved in 7 iterations. Other properties involving the memory latency can be expressed similarly, e.g., compute the probability to enter the critical section after executing an entry section that maximizes the ratio of local versus remote memory accesses.

Overtaking. Even if a mutual exclusion protocol is starvation-free, a process P i that begins its entry section (and hence, starts requesting the access to the crit-ical section) may be overtaken one or several times by another process P j that accesses its own critical section before P i does so. A qualitative measure of a starvationfree protocol is given by its overtaking degree, which is the maximum number of overtakes per couple of processes. This number should be as small as possible, and may vary among process couples for asymmetric protocols. A qualitative study of the overtaking degree was carried out in [START_REF] Mateescu | Model Checking and Performance Evaluation with CADP Illustrated on Shared-Memory Mutual Exclusion Protocols[END_REF] using MCL regular formulas with counters. Here we use the same property in the probabilistic setting, which enables to compute the probability that process P j overtakes P i a given number of times. Figure 9(b) shows the results for the BL protocol, which outline its intrinsic asymmetry: lower index processes, with higher priority, also have better chances to overtake the other processes. The SFGs of the LESs produced by EVALUATOR contain several SCCs, e.g., for the TAS protocol with 2 processes the SFG contains up to 6 SCCs, of which the largest one has 5 variables and was solved in 7 iterations.

Standalone execution. As opposed to overtaking, it is also interesting to examine the dual situation, in which a process P i executes its cycle in standalone, i.e., without any interference with the other processes. This was explicitly formulated in [START_REF] Dijkstra | Solution of a problem in concurrent programming control[END_REF] as the independent progress requirement, which should be satisfied by any mutual exclusion protocol. We can analyze this situation by computing the probability measure of a complete execution of process P i without any other action being performed meanwhile by other processes. The MCL formula below specifies such kind of execution, where max denotes the number of consecutive executions of P i : { ((¬{CS ... ?j:nat where j = i}) * .{NCS !i}.

(¬{... ?j:nat where j = i}) * .{CS !"ENTER" !i}. (¬{... ?j:nat where j = i}) * .{CS !"LEAVE" !i} ) {max} } ≥ ? 0

Figure 9(c) shows that the probability of standalone execution of P i decreases with max, which reflects the starvation-free nature of the protocols. The SFGs of the LESs produced by EVALUATOR for this formula contain several SCCs, e.g., for the TAS protocol with 2 processes the SFG contains up to 27 SCCs, of which the largest one has 5 variables and was solved in 7 iterations.

Contention. The last property we consider regards the access of a process P i to its critical section when the other processes attempt (with different probabilities) to access their own critical sections. Lamport's protocol [START_REF] Lamport | A fast mutual exclusion algorithm[END_REF] was designed to ensure a fast access, consisting of only a few operations on the shared variables, of a process to its critical section when the other processes do not attempt similar accesses. This was motivated by the observation that contention of accesses to critical sections is a rare phenomenon in well-designed concurrent systems.

We consider the same MCL formula used for analyzing the memory latency, and evaluate it for the process P 2 in Lamport's protocol with N = 3 in presence of different degrees of contention, modeled by assigning on the fly different probabilities to the memory operations performed by the other processes P 0 and P 1 .

The results are shown in Figure 9(d), where the curve marked with a '-' represents the normal situation (all processes compete for the critical section with equal probabilities). The plots confirm the characteristic of the fast access protocol: for low contention (1%) from the other processes, P 2 reaches its critical section with almost 100% probability after a small amount of memory operations, whereas this probability decreases for higher degrees of contention.

Performance of analysis. The sizes of the PTSs including the additional transitions of memory access costs (available in [START_REF] Mateescu | Model Checking and Performance Evaluation with CADP Illustrated on Shared-Memory Mutual Exclusion Protocols[END_REF]Tab. 4]), range from 3 252 states and 6 444 transitions (for the TAS protocol) to 18 317 849 states and 31 849 616 transitions (for the CLH protocol).

The computing resources needed for on-the-fly verification depend on the complexity of the MCL regular formulas, and in particular the number and domains of their data parameters. For example, the analysis of the first access to the critical section takes between 3.25-5.5 seconds and 36.5-77 MBytes for all protocol configurations considered. For other properties, such as those concerning the memory latency or the overtaking, some peaks arrive up to 2-3 hours and 12-14 GBytes because of the manipulation of data (cost of memory accesses) and iterations (number of overtakes). The analysis of the standalone execution of P i may take up to 285 seconds and 1 230 MBytes for the BL protocol because of the complex cycles present in the PTS, while the same analysis takes less than 100 seconds (or even 10 seconds) for the other protocols.

Analysis of peak cost paths. The combination of data handling and probabilistic on-the-fly model checking using MCL enables the analysis of paths having peak cost values in a PTS. Assuming that the paths of interest are characterized by a regular formula β(cost) with a parameter cost, two cases must be considered:

-If the paths of interest are finite, the peak value of cost can be computed by checking the modality β(cost) true with various values of cost, using dichotomic search to reduce the number of invocations of EVALUATOR. Then, the probability of the peak cost sequence is obtained by checking the formula {β(peak )} ≥?0 . -If the paths of interest are infinite, the analysis can be done by checking the formula {β(cost)} ≥?0 for various values of cost and observing the variation of the probability.

These analyses can be easily automated in CADP using SVL scripts.

Bounded Retransmission Protocol

We consider here an action-based specification of Philips' Bounded Retransmission Protocol (BRP) developed initially in LOTOS and analyzed by model checking using a data-handling version of ACTL [START_REF] Mateescu | Formal description and analysis of a bounded retransmission protocol[END_REF]. The BRP protocol is designed to transmit large data packets over an unreliable medium by splitting them in small chunks, which are sent sequentially. After each chunk transmission, the sender waits for an acknowledgment from the receiver before sending the next chunk. If the acknowledgment does not arrive because of a communication failure, the sender times out and retransmits the chunk. In case of repeated failures, only a bounded number of retransmissions are allowed, after which the protocol aborts the transmission of the packet. The protocol informs the sender and the receiver about the outcome of each packet transmission by sending OK, NOK, or DK indications, denoting success, failure, or uncertainty (loss of the last acknowledgment) of the transmission, respectively.

To carry out a probabilistic analysis of the BRP protocol, we resorted to a state-based probabilistic modeling initially proposed in [START_REF] D'argenio | Reachability analysis of probabilistic systems by successive refinements[END_REF] and also available as a PRISM benchmark 2 . Starting from an LNT description of the BRP protocol (strongly bisimilar to the initial LOTOS description in [START_REF] Mateescu | Formal description and analysis of a bounded retransmission protocol[END_REF]) available as a CADP demo example 3 , we converted it on the fly into a PTS by setting a 2% probability for chunk losses and a 1% probability for acknowledgment losses, keeping all the other actions equiprobable, and considering the transmission of a single data packet as in [START_REF] D'argenio | Reachability analysis of probabilistic systems by successive refinements[END_REF]. We specified in MCL the action-based counterparts of the six PCTL properties given in [START_REF] D'argenio | Reachability analysis of probabilistic systems by successive refinements[END_REF], of which we illustrate below only the properties P a and P 3 , the other ones having similar shapes. P a evaluates the probability that the sender reports an unsuccessful transmission after the complete packet was received (this should never occur!):

{ (¬{OUTPUT !OK}) * .{OUTPUT !OK}. (¬{INPUT !NOK}) * .{INPUT !NOK} } =0
This MCL formula requires a zero probability measure for the sequences containing a successful indication delivered to the receiver (action "OUTPUT !OK") followed by an unsuccessful indication to the sender (action "INPUT !NOK"). P 3 evaluates the probability that the sender reports an unsuccessful transmission after more than eight chunks of the packet have been transmitted: This MCL formula asks for the probability measure of a sequence containing eight chunk acknowledgments received by the sender (action "REC L") followed by an unsuccessful indication to the sender (action "INPUT !NOK").

{ ((¬REC L) * .REC L) {8 ...}. (¬(REC L ∨ {INPUT !NOK})) * .{INPUT !NOK} } ≥?0
We checked the six properties using explicit-state PRISM and EVALUATOR on the corresponding BRP models for five retransmissions and packet lengths between 16 and 256 chunks. The probability values for all six properties obtained using CADP and PRISM are identical to the ones reported in [START_REF] D'argenio | Reachability analysis of probabilistic systems by successive refinements[END_REF], which suggests that the action-based model in [START_REF] Mateescu | Formal description and analysis of a bounded retransmission protocol[END_REF] and the state-based model in [START_REF] D'argenio | Reachability analysis of probabilistic systems by successive refinements[END_REF] are consistent, even if they are quite different in structure. The performance measures of CADP and PRISM are shown in Figure 10. We observe that CADP consumes up to one order of magnitude less memory than PRISM, which is in turn faster on small configurations but becomes slower for properties P 1 , P 2 , and P 3 on larger configurations (packets with more than 150 chunks). For all six MCL formulas, the LESs produced by EVALUATOR have acyclic SFGs.

Probability of successful packet transmission. In addition to the six probabilistic properties of the BRP analyzed in [START_REF] D'argenio | Reachability analysis of probabilistic systems by successive refinements[END_REF], we also studied how the total number of retries during a packet transmission influences the probability of the packet being successfully received. The MCL formula below computes the probability of a successful packet transmission (initiated by an action "INPUT PACKET" and concluded by an action "INPUT !OK") when the total number of retries occurring when sending the chunks is equal to retries. The outer "loop" subformula counts the total number of retries in the iteration variable r by summing up the retries that occur for every chunk c, i.e., the number of retransmissions (actions "SEND K ... !c") occurring after Fig. 10: Execution time and memory consumption of CADP and PRISM for checking the six probabilistic properties in [START_REF] D'argenio | Reachability analysis of probabilistic systems by successive refinements[END_REF] on the BRP model for five retries and a packet size k between 16 and 256 data chunks. the chunk was sent for the first time and before it was received (action "OUTPUT !c ?any"). These retries are counted by the inner "loop" in the iteration variable nc and provided as result in the return variable rc.

Figure 11 shows the variation of the probability of successfully transmitting a packet of length k = 32 with maximum two retries per chunk, when the total number of retries varies between 0 and 64. This probability is high (99, 9%) when no retries occur, and decreases very fast with the total number of retries (0, 05% for five retries). This indicates that with a 2% chunk loss probability and a 1% acknowledgment loss probability, the BRP protocol is already quasi-reliable, the probability of a successful packet transmission such that the retransmission bound was reached for each chunk being negligible (10 -110 for 64 retries).

Of course, this analysis can be carried out with PRISM as well, by introducing an additional variable in the PRISM model of the BRP for counting the total number of retries; on the other hand, the action-based analysis using the MCL formula above (which is independent of the packet length and retransmission bound parameters of the BRP) does not require to change the PTS model.

Randomized Protocols

We consider here two randomized protocols taken from the PRISM benchmarks suite. The first one is the Israeli-Jalfon (IJ) self-stabilizing protocol [START_REF] Israeli | Token management schemes and random walks yield self-stabilizating mutual exclusion[END_REF], which operates on a set of k concurrent processes P 0 , ..., P k-1 connected on a ring topology and brings them after a finite number of steps to a stable configuration, where only one process is privileged (i.e., has a token). The IJ protocol is asynchronous and communication on the ring is bidirectional. When a process has a token, it can be scheduled for exe-cution and it must pass the token with equal probability to its left or right neighbor process on the ring. If two tokens reach the same process, they are merged into a single one.

The fundamental property of self-stabilisation protocols is that starting from any configuration, a stable configuration is reached with probability one. This can be expressed in MCL as follows: { (¬ϕ stable ? . true) * . ϕ stable ? } =1 where ϕ stable = exists i:nat among {0 ... n -1} .

( {EXE !i} true ∧ [{EXE ?j:Nat where j = i}] false)

The state formula ϕ stable expresses that a single process P i can execute an action in the current state (action "{EXE !i}").

Figure 12 shows the time and memory consumed by EVALUATOR and explicit-state PRISM for checking the self-stabilisation property on the corresponding LNT and DTMC descriptions of the IJ protocol. Both tools exhibit similar performance on medium-sized configurations (k ≤ 15 processes), PRISM becoming more efficient for larger configurations. The SFGs of the LESs produced by EVALUATOR contain several SCCs, e.g., for k = 10 the SFG contains 8 SCCs, of which the largest one has 756 variables and was solved in 22 iterations.

The second example considered is a version of the randomized Lehmann-Rabin (LR) dining philosophers protocol without fairness assumptions [START_REF] Duflot | Randomized dining philosophers without fairness assumption[END_REF]. Each of the k philosophers picks his forks in a random order if they are both available, and releases them in any order after eating and before returning to thinking. We modeled the system in LNT and checked the basic property stating that a hungry philosopher will be able to eat with probability one: This MCL formula combines a regular box modality searching all states in which a philosopher p becomes hungry (i.e., immediately after performing an action "{THINK !p}"), and a regular probabilistic operator checking the reachability of an action "{EAT !p}" with probability one. The value extraction mechanism, which captures the value of p present on a transition label in the box modality and reuses it in the probabilistic operator, enables to check configurations of the system with different values of k without changing the formula.

Figure 13 shows the performance of CADP and explicit-state PRISM for checking the above property on their respective models of the LR protocol. On this example, PRISM is increasingly faster but also increasingly demanding in memory (one order of magnitude difference with CADP for six philosophers). Also on this example, the SFGs of the LESs produced by EVALU-ATOR contain several SCCs, e.g., for k = 4 the SFG contains 180 SCCs, of which the largest one has 3016 variables and was solved in 25 iterations.

Conclusion and future work

We proposed a regular probabilistic operator for computing the probability measure of complex paths in a PTS whose actions contain data values. Paths are specified using the action-based, data handling regular formulas of MCL [START_REF] Mateescu | A model checking language for concurrent value-passing systems[END_REF] that we extended with a general iteration operator "loop" enabling the specification of complex (Turing computable) paths. These new operators subsume those of P(A)CTL, and make possible the study of paths whose associated cost, calculated from the data values present on their actions, has a given value. We defined an on-the-fly model checking method based on reformulating the problem as the resolution of a linear equation system (LES) and a Boolean equation system (BES), and implemented it in the EVALUATOR model checker of the CADP toolbox. Several experiments showed that this on-the-fly verification procedure exhibits a performance comparable to the explicit-state algorithms of the PRISM model checker.

Since the PTS is explored on the fly by annotating the transitions of the original LTS with probabilities, the high-level description of the concurrent system under analysis (written, in our case, in the LNT language) remains unchanged, and can serve therefore as unique model for both functional and quantitative analysis, the details of which can be encapsulated in SVL scripts.

The on-the-fly analysis back-end (which is currently sequential) can be enhanced with distributed capabilities by connecting it with the MUMPS distributed solver [START_REF] Amestoy | MUMPS: A general purpose distributed memory sparse solver[END_REF] for sparse LESs. We also plan to investigate the adequacy of MCL fragments w.r.t. probabilistic branching bisimulation, which would enable the (property-preserving) compositional construction and minimization of PTSs described as Interactive Probabilistic Chains [START_REF] Coste | Towards performance prediction of compositional models in industrial gals designs[END_REF]. Finally, we will seek to extend our approach (which deals only with finite paths described using data handling regular formulas) to handle infinite paths satisfying ω-regular properties, along the lines of [START_REF] Baier | Principles of model checking[END_REF]Chap. 10].

Fig. 6 :

 6 Fig. 6: Translation of the general iteration operators in basic MCL

  PTS (data handling version)

Fig. 8 :

 8 Fig. 8: Signal Flow Graph of the LES in Figure 2(f)

Fig. 9 :

 9 Fig. 9: Probabilities computed using on-the-fly model checking. (a) Accessing the critical section after memory accesses of cost MAX. (b) Overtaking of P i by P j (P j P i ) in the BL protocol. (c) Standalone execution of P i . (d) Execution of P 2 (in Lamport's protocol) for different degrees of contention from the other processes.

Fig. 11 :

 11 Fig. 11: Probability of successful packet transmission for the BRP model with two retries and packet size k = 32, depending on the total number of retries

[

  true * .{THINK ?p:nat}] { (¬{EAT !p}) * .{EAT !p} } =1

Fig. 12 :

 12 Fig. 12: Execution time and memory consumption of CADP and PRISM for computing the probability of reaching a stable state on the self-stabilising protocol with 3 ≤ k ≤ 20 concurrent processes.

Fig. 13 :

 13 Fig. 13: Execution time and memory consumption of CADP and PRISM for computing the probability that a hungry philosopher eats on the LR dining philosophers protocol with 3 ≤ k ≤ 6 philosophers.

Table 1 :

 1 Encoding MCL iteration operators using "loop"

	Syntax	Meaning	Encoding using "loop"
	β{e ...}	≥ e times loop (c:nat := e) in
			if c > 0 then
			β . continue (c -1)
			else
			exit | β . continue (c)
			end if
			end loop
	β{e1 ... e2} between	loop (c1:nat := e1,
		e1 and e2	c2:nat

http://www.prismmodelchecker.org/casestudies/

Acknowledgments

This work was partially supported by the European project SENSATION (Self Energy-Supporting Autonomous Computation) FP7-318490. We are grateful to the anonymous referees for their constructive criticism and their valuable suggestions for improving the

manuscript. We also thank Wendelin Serwe for providing the LNT descriptions of the mutual exclusion protocols.