Laure Petrucci

Jaco Van De Pol

Parameter Synthesis Algorithms for Parametric Interval Markov Chains

ou non, émanant des établissements d'enseignement et de recherche français ou étrangers, des laboratoires publics ou privés.

Introduction

Markov Chains (MC) are widely used to model stochastic systems, like randomized protocols, failure and risk analysis, and phenomena in molecular biology. Here we focus on discrete time MCs, where transitions between states are governed by a state probability distribution, denoted by µ : S × S → [0, 1]. Practical applications are often hindered by the fact that the probabilities µ(s, t), to go from state s to t, are unknown. Several solutions have been proposed, for instance Parametric Markov Chains (PMC) [START_REF] Daws | Symbolic and Parametric Model Checking of Discrete-Time Markov Chains[END_REF] and Interval Markov Chains (IMC) [START_REF] Jonsson | Specification and refinement of probabilistic processes[END_REF], in which unknown probabilities are replaced by parameters or intervals, respectively, see Figs. 1a and1b. Following [START_REF] Delahaye | Consistency for Parametric Interval Markov Chains[END_REF], we study their common generalization, Parametric Interval Markov Chains (PIMC, Fig. 1c), which allow intervals with parametric bounds. PIMCs are more expressive than IMCs and PMCs [START_REF] Bart | Reachability in Parametric Interval Markov Chains Using Constraints[END_REF]. PIMCs allow to study the boundaries of admissible probability intervals, which is useful in the design exploration phase. This leads to the study of parameter synthesis for PIMCs, started in [START_REF] Delahaye | Parameter Synthesis for Parametric Interval Markov Chains[END_REF].

IMCs can be viewed as specifications of MCs. An IMC is consistent if there exists an MC that implements it. The main requirements on the implementation are: [START_REF] Bagnara | The Parma Polyhedra Library: Toward a complete set of numerical abstractions for the analysis and verification of hardware and software systems[END_REF] all behaviour of the MC can be simulated by the IMC, preserving probabilistic information; [0, 1 4 ] [ 1 4 , 1]

(b) an IMC 0 1 2 3 4 5

[p, p]

[q, q]

[0, r] [ 1 4 , r] [p + q, 4 5 ]

(c) a PIMC We drop self-loops with probability 1 (or [START_REF] Bagnara | The Parma Polyhedra Library: Toward a complete set of numerical abstractions for the analysis and verification of hardware and software systems[END_REF][START_REF] Bagnara | The Parma Polyhedra Library: Toward a complete set of numerical abstractions for the analysis and verification of hardware and software systems[END_REF]) in all terminal nodes. and (2) the outgoing transition probabilities for each state sum up to 1. The consistency synthesis problem for PIMCs is to compute all parameter values leading to a consistent IMC. E.g., PIMC in Fig. 1c 2 is consistent when q = 0, p = 1, or when p+q = 1, r = 1.

The witness MC of Fig. 1d corresponds to p = 1 4 , q = 3 4 , r = 1.

Contribution. This paper studies the consistency synthesis problem for PIMCs. We improve the theory in [START_REF] Delahaye | Parameter Synthesis for Parametric Interval Markov Chains[END_REF], which gave an inductive definition of n-consistency. Basically, a state is n-consistent if it has a locally consistent subset of successors, which are in turn all (n -1)-consistent. Here local consistency checks that there is a solution within the specified bounds that sums up to 1. That paper provided an expression for n-consistency. There are two drawbacks from an algorithmic perspective: all possible subsets of successors must be enumerated, and a sufficiently large upper bound for n must be provided. It has been shown that taking the number of states for n is sufficient.

We address both problems. First we simplify the inductive definition and show that for IMCs, the enumeration over the subset of successors is not necessary. Instead, we can restrict to a single candidate: the set of all (n -1)-consistent successors. Second, we provide a smaller upper bound for n. We show that it is sufficient to take the length of the longest simple path in the IMC. However, the length of the longest simple path cannot be efficiently computed (this would solve the Hamiltonian path problem, which is NP-complete).

Our main contribution is to provide an alternative, co-inductive definition of consistency, dropping the need to reason about n altogether. Instead, we define consistency as the largest set, such that a state is consistent if the set of its consistent successors is locally consistent. We have formally proved the equivalence between all these definitions in the interactive theorem prover PVS [START_REF] Owre | PVS: A prototype verification system[END_REF]. The complete PVS proof development is available online.

Based on the simplified inductive definition, we provide a polynomial time forward algorithm to check that an IMC is consistent. Based on the new co-inductive defini-tion, we provide a polynomial backward algorithm. Again, the number of iterations is bounded by the length of the longest simple path, without having to compute it.

Finally, we provide algorithms to compute an expression for all parameters for which a PIMC is consistent. Unfortunately, to obtain an expression we must fall back on subset enumeration. The forward algorithm can be implemented as a Constraint Logic Program, so Prolog + CLP(Q) can be used directly to compute a list of all solutions, basically as a disjunction of conjunctions of linear inequations over the parameters. We introduce two optimizations: caching intermediate results and suppressing subsumed solutions. The backward algorithm for IMCs can be viewed as computing the maximal solution of a Boolean Equation System. Generalizing this to PIMCs, we now compute the maximal solution of an equation system over disjunctions of conjunctions of constraints. Such equation systems can be solved by standard iteration, representing the intermediate solutions as powerdomains over convex closed polyhedra. We implemented this using the Parma Polyhedra Library [START_REF] Bagnara | The Parma Polyhedra Library: Toward a complete set of numerical abstractions for the analysis and verification of hardware and software systems[END_REF].

Related Work. One of the first results on synthesis for PMCs [START_REF] Daws | Symbolic and Parametric Model Checking of Discrete-Time Markov Chains[END_REF] computes the probability of path formulas in PCTL as an expression over the parameters. Since then, the efficiency and numeric stability has been improved considerably [START_REF] Quatmann | Parameter synthesis for Markov models: Faster than ever[END_REF][START_REF] Dehnert | Prophesy: A probabilistic parameter synthesis tool[END_REF]. On such models, the realizability (or well-defined) property is considered [START_REF] Lanotte | Parametric probabilistic transition systems for system design and analysis[END_REF][START_REF] Moritz Hahn | Probabilistic reachability for parametric markov models[END_REF] which mainly differs from the consistency we address in that they consider consistency of all states, while we have the option to avoid some states (and their successors) by assigning nullprobability to some edges. Model checking for IMCs is studied, for instance in [START_REF] Chakraborty | Model checking of open Interval Markov Chains[END_REF][START_REF] Chen | On the complexity of model checking interval-valued discrete time Markov chains[END_REF]. For continuous-time Markov Chains, precise parameter synthesis is studied as well [START_REF] Ceska | PRISM-PSY: precise GPU-accelerated parameter synthesis for stochastic systems[END_REF]. However, PIMCs are more expressive (concise) than PMCs and IMCs, as shown in [START_REF] Bart | Reachability in Parametric Interval Markov Chains Using Constraints[END_REF]. As far as we know, besides reachability, there are no model checking results for PIMCs.

Other specification formalisms include Constraint Markov Chains [START_REF] Delahaye | New results for Constraint Markov Chains[END_REF], with arbitrary constraints on transitions, and Abstract Probabilistic Automata [START_REF] Delahaye | Abstract probabilistic automata[END_REF], which add non-deterministic transitions. We believe that our work can be extended in a straightforward manner to CMCs with linear constraints. For APA the situation is probably quite different. Another branch of research has investigated the synthesis of parameters for timed systems, but that is out of the scope of this paper.

PIMCs, and the related consistency problem, have been introduced in [START_REF] Delahaye | Consistency for Parametric Interval Markov Chains[END_REF]. Our backward algorithm for IMCs is somewhat similar in spirit to the pruning operator of [START_REF] Delahaye | Consistency for Parametric Interval Markov Chains[END_REF]. We provide a sharper upper bound on the number of required iterations. That paper addresses the existence of a consistent parameter valuation for a restricted subclass of PIMCs, where parameters occur only locally. The parameter synthesis problem for the full class of PIMCs was considered in [START_REF] Delahaye | Parameter Synthesis for Parametric Interval Markov Chains[END_REF]. We improved on their theory, as explained before. Our experiments (Section 6) show that our algorithms and optimizations are more efficient than the approach in [START_REF] Delahaye | Parameter Synthesis for Parametric Interval Markov Chains[END_REF].

Very recently, [START_REF] Bart | Reachability in Parametric Interval Markov Chains Using Constraints[END_REF] also introduced a CLP approach for checking the existence of a consistent parameter valuation. Their contribution is a CLP program of linear size in the PIMC. Their CLP is quite different from ours: basically, they introduce a Boolean variable for each state and a real variable for each transition probability of the Markov Chain that implements the PIMC. So solving the CLP corresponds to searching for a satisfying implementation.

Parametric Interval Markov Chains

As Parametric Interval Markov Chains allow for describing a family of Markov Chains, we first define these.

Definition 1 (Markov Chain). A Markov Chain (MC) is a tuple (S, s 0 , µ, A, V ), where:

-S is a set of states and s 0 ∈ S is the initial state; µ : S × S → [0, 1] is the transition probability distribution s.t.:

∀s ∈ S : s ∈S µ(s, s ) = 1; -A is a set of labels and V : S → A is the labelling function.

Notation 2. Let P be a set of parameters, i.e. variable names. We denote by Int[0, 1](P ) the set of pairs [a, b] with a, b ∈ [0, 1] ∪ P . Given x ∈ Int[0, 1](P ), we denote by x and x u its left and right components. If x is an interval, this corresponds to its lower and upper bounds. The same notation is used for functions which result in an interval.

Example 3. [0.3, 0.7], [0, 1], [0.5, 0.5], [p, 0.8], [0.99, q], [p, q] are all in Int[0, 1]({p, q}).

Definition 4 ((Parametric) Interval Markov Chain). A Parametric Interval Markov

Chain (PIMC) is a tuple (P, S, s 0 , ϕ, A, V ) where:

-P is a set of parameters; -S is a set of states and s 0 ∈ S is the initial state; ϕ : S × S → Int[0, 1](P ) is the parametric transition probability constraint; -A is a set of labels and V : S → A is the labelling function.

An Interval Markov Chain (IMC) is a PIMC with P = ∅ (we drop P everywhere).

Note that Def. 4 and 1 are very similar, but for PIMCs and IMCs the well-formedness of the intervals and of the probability distribution will be part of the consistency property to be checked (see Def. 11).

When ambiguity is possible, we will use a subscript to distinguish the models, e.g. S M , S I and S P will denote the set of states of respectively a MC, an IMC and a PIMC.

If all intervals are point intervals of the form [p, p], this PIMC is actually a Parametric Markov Chain [START_REF] Daws | Symbolic and Parametric Model Checking of Discrete-Time Markov Chains[END_REF].

Example 5. Fig. 2a shows our running example of a PIMC with two parameters p and q (taken from [START_REF] Delahaye | Parameter Synthesis for Parametric Interval Markov Chains[END_REF]). Fig. 2b shows a particular IMC. Definition 6 (Support). The support of a probability distribution µ at a state s ∈ S M is the set: sup(µ, s)

:= {s ∈ S M | µ(s, s ) > 0}.
Similarly, for a parametric transition probability constraint ϕ at a state s ∈ S P the support is the set: sup(ϕ, s) := {s ∈ S P | ϕ u (s, s ) > 0}.

Assumption: From now on, we will assume that I is finitely branching, i.e. for all s ∈ S, sup(ϕ, s) is a finite set. For the algorithms in Section 4 we will even assume that S is finite.

PIMCs and IMCs can be viewed as specifications of MCs. Definition 7 (A MC implements an IMC). Let M = (S M , s M0 , µ, A, V M ) be a MC and I = (S I , s I 0 , ϕ, A, V I ) an IMC. M implements I (M I) if there exists a simulation relation R ⊆ S M × S I , s.t. ∀s M ∈ S M and s I ∈ S I , if s M Rs I , then:

1. V M (s M ) = V I (s I ) (the source and target states have the same label) 2. There exists a probabilistic correspondence δ :

S M × S I → [0, 1], s.t.: (a) ∀s I ∈ S I : s M ∈S M µ(s M , s M ) • δ(s M , s I ) ∈ ϕ(s I , s I )
(the total contribution of implementing transitions satisfies the specification)

(b) ∀s M ∈ S M : µ(s M , s M ) > 0 ⇒ s I ∈S I δ(s M , s I ) = 1 (the implementing transitions yield a probability distribution) (c) ∀s M ∈ S M , s I ∈ S I : δ(s M , s I ) > 0 ⇒ s M Rs I (corresponding successors are in the simulation relation) (d) ∀s M ∈ S M , s I ∈ S I : δ(s M , s I ) > 0 ⇒ µ(s M , s M ) > 0 ∧ ϕ u (s I , s I ) > 0
(δ is only defined on the support of µ and ϕ)

Definition 8 (Consistency).

An IMC I is consistent if for some MC M, we have M I.

A PIMC is consistent if there exist parameter values such that the corresponding IMC is consistent.

Intuitively, this definition states that the implementation is an MC, whose behaviour is allowed by the specification IMC, i.e., the IMC can simulate the MC. Clause (2d) was not present in the original definition [START_REF] Delahaye | Consistency for Parametric Interval Markov Chains[END_REF], but it is convenient in proofs. We first show that limiting δ to the support of µ and ϕ does not alter the implementation relation. Proof. Assume, there exist R, s M Rs I and δ that satisfy conditions (2a)-(2c) of Def. 7. Define:

δ (s M , s I ) := δ(s M , s I ) if µ(s M , s M ) > 0 and ϕ u (s I , s I ) > 0; 0 otherwise. 0 1 2 3 4 [0, 1] [0, 1] [q, 1] [0.3, q] [0, q] [0, p] [0, 0.5] [p, 0.3] 1 [0.5, p] (a) A Parametric Interval Markov Chain 0 1 2 3 4 [0, 1] [0, 1] [0.5, 1] [0.3, 0.5] [0, 0.4] [0, 0.5] [0, 0.5] 0.6 1 [0.5, 1] (b) An Interval Markov Chain

Consistency of Interval Markov Chains

In this section we study consistency of Interval Markov Chains; we will return to Parametric IMCs in Section 5. Intuitively, an IMC is consistent if it can be implemented by at least one MC. From now on, we will drop the labelling V , since it plays no role in the discussion on consistency, and thus consider an arbitrary IMC I = (S, s 0 , ϕ).

Local Consistency

Local consistency of a state s ∈ S is defined with respect to a set X ⊆ S of its successors, and its probability constraint ϕ(s, •). It ensures the existence of some probability distribution satisfying the interval constraints on transitions from s to X: the collective upper bound should be greater than or equal to 1 (condition up(ϕ, s, X)), the collective lower bound less than or equal to 1 (low (ϕ, s, X)). Moreover, each lower bound should be smaller than the corresponding upper bound, and the states outside X should be avoidable, in the sense that they admit probability 0 (local (ϕ, s, X)).

Definition 11 (Local consistency).

The local consistency constraints for a state s ∈ S and a set X ⊆ S is LC (ϕ, s, X) s.t.:

LC (ϕ, s, X) := up(ϕ, s, X) ∧ low (ϕ, s, X) ∧ local (ϕ, s, X), where up(ϕ, s, X) We obtain the following facts, which can be directly checked from the definitions. Note that from Lemma 12(1) and ( 2) it follows that we may always restrict attention to the support of (ϕ, s): LC (ϕ, s, X) ≡ LC (ϕ, s, X ∩ sup(ϕ, s)).

:= s ∈X ϕ u (s, s ) ≥ 1 low (ϕ, s, X) := s ∈X ϕ (s, s ) ≤ 1 local (ϕ, s, X) := (∀s ∈ X : ϕ (s, s ) ≤ ϕ u (s, s )) ∧ (∀s ∈ X : ϕ (s, s ) = 0)
Lemma 12. For X, Y ⊆ S:

1. If X ⊆ Y and LC (ϕ, s, X) then LC (ϕ, s, Y ). 2. If LC (ϕ, s, X) then also LC (ϕ, s, X ∩ sup(ϕ, s)).
Proof. 1. Assume X ⊆ Y and LC (ϕ, s, X), hence up(ϕ, s, X), low (ϕ, s, X) and local (ϕ, s, X).

From up(ϕ, s, X), we have s ∈X ϕ u (s, s ) ≥ 1, so we get up(ϕ, s, Y ):

s ∈Y ϕ u (s, s ) = ( s ∈X ϕ u (s, s )+ s ∈Y \X ϕ u (s, s )) ≥ (1+ s ∈Y \X ϕ u (s, s )) ≥ 1
From local (ϕ, s, X), we have ∀s ∈ Y \ X : ϕ (s, s ) = 0, and from low (ϕ, s, X), we have s ∈X ϕ (s, s ) ≤ 1, so we get low (ϕ, s, Y ):

s ∈Y ϕ (s, s ) = ( s ∈X ϕ (s, s ) + s ∈Y \X ϕ (s, s )) = s ∈X ϕ (s, s ) + 0 ≤ 1 Finally, from local (ϕ, s, X), it holds that for s ∈ Y , if s ∈ X then ϕ (s, s ) ≤ ϕ u (s, s ), else ϕ (s, s ) = 0, which also implies ϕ (s, s ) ≤ ϕ u (s, s ). If s ∈ Y then s ∈ X, so ϕ (s, s ) = 0. So we get local (ϕ, s, Y
). This proves that LC (ϕ, s, Y ). 2. Assume LC (ϕ, s, X), hence up(ϕ, s, X), low (ϕ, s, X) and local (ϕ, s, X). Note that if s ∈ X \ sup(ϕ, s), by definition of sup, we obtain ϕ u (s, s ) = 0 and by local (ϕ, s, X), we obtain ϕ (s, s ) = 0.

s ∈X∩sup(ϕ,s) ϕ u (s, s ) = s ∈X ϕ u (s, s ) -t∈X\sup(ϕ,s) ϕ u (s, s ) = s ∈X ϕ u (s, s ) -0 ≥ 1 s ∈X∩sup(ϕ,s) ϕ (s, s ) = s ∈X ϕ (s, s ) -s ∈X\sup(ϕ,s) ϕ (s, s ) = s ∈X ϕ (s, s ) -0 ≤ 1 Finally, if s ∈ X ∩ sup(ϕ, s) then s ∈ X, so ϕ (s, s ) ≤ ϕ u (s, s ).
Otherwise, s ∈ X or s ∈ X \ sup(ϕ, s), but in both cases ϕ (s, s ) = 0.

Co-inductive Definition of Global Consistency

Global consistency of (P)IMCs can be defined in several ways, e.g. co-inductively and inductively. Here, we introduce a new co-inductive definition of global consistency, as a greatest fixed point (gfp). We first introduce an abbreviation for the set of locally consistent states w.r.t. a set X:

Notation 13. LC ϕ (X) := {s | LC (ϕ, s, X)}
Next, we define Cons as the greatest fixed point of LC ϕ . Intuitively, from consistent states one can keep taking locally consistent steps to other consistent states.

Definition 14 (Global consistency, co-inductive). Cons := gfp(LC ϕ ).

Lemma 15. From the definition of greatest fixed point, Cons is the largest set C s.t. C ⊆ LC ϕ (C): Proof. Since M I, there is a simulation relation R, with s M0 Rs I 0 , and for all s M ∈ S M , s I ∈ S I , if s M Rs I , there is a correspondence δ, satisfying properties (2a)-(2d) of Def. 7. We will prove that {s I | ∃s M : s M Rs I } ⊆ Cons. Since s M0 Rs I 0 , it will follow that s I 0 ∈ Cons. We proceed using the gfp-property (Lemma 15(2)), so it is sufficient to prove:

1. s ∈ Cons ≡ s ∈ LC ϕ (Cons) ≡ s ∈ LC ϕ (Cons ∩ sup(ϕ, s)) 2. If C ⊆ LC ϕ (C) then C ⊆ Cons.
{s I ∈ S I | ∃s M ∈ S M : s M Rs I } ⊆ LC ϕ ({s I ∈ S I | ∃s M ∈ S M : s M Rs I }). Let s I ∈ S I be given with s M ∈ S M s.t. s M Rs I . Define X := {s I ∈ S I | ∃s M ∈ S M : δ(s M , s I ) > 0}. Clearly, if s I ∈ X, then for some s M ∈ S M , δ(s M , s I ) > 0
and by the correspondence property of Def. 7(2c), s M Rs I . So X ⊆ {s I ∈ S I | ∃s M ∈ S M : s M Rs I }. Thus, by monotonicity, Lemma 12(1), it is sufficient to show that s I ∈ LC ϕ (X). To check that s I ∈ LC ϕ (X), we first check that the corresponding transitions yield a probability distribution:

s I ∈X s M ∈S M µ(s M , s M ) • δ(s M , s I ) = s I ∈S I s M ∈S M µ(s M , s M ) • δ(s M , s I ) (if s I ∈ X, δ(s M , s I ) = 0 by def. of X) = s M ∈S M µ(s M , s M ) • ( s I ∈S I δ(s M , s I )) (by -manipulation) = s M ∈S M µ(s M , s M ) • 1 (δ is a prob. distrib. by Def. 7(2b)) = 1 (µ is a prob. dist. by Def. 1 of MC) By Def. 7(2a), ∀s I ∈ X, ϕ (s I , s I ) ≤ s M ∈S M µ(s M , s M )•δ(s M , s I ) ≤ ϕ u (s I , s I ).
By the computation above, s I ∈X ϕ (s I , s I ) ≤ 1 and s I ∈X ϕ u (s I , s I ) ≥ 1, proving low (ϕ, s I , X) and up(ϕ, s I , X), respectively. For s I ∈ X we already established ϕ (s I , s I ) ≤ ϕ u (s I , s I ). For s I ∈ X, by definition of X: ∀s M : δ(s M , s I ) = 0. Thus, ϕ (s I , s I ) ≤ 0 by the computation above, proving local (ϕ, s I , X). This proves s I ∈ LC ϕ (X).

Conversely, we prove that a consistent IMC can be implemented by at least one MC. Note that the proof of Theorem 17 provides the construction of a concrete MC.

Theorem 17. For IMC I = (S, s 0 , ϕ), if s 0 ∈ Cons, then there exist a probability distribution µ and a MC M = (Cons, s 0 , µ) such that M I.

Proof. Assume I is consistent. Consider an arbitrary state s ∈ Cons. We will define µ(s, s ) in between ϕ (s, s ) and ϕ u (s, s ), scaling it by a factor p such that µ(s) sums up to 1. Define L := s ∈Cons ϕ (s, s ) and U := s ∈Cons ϕ u (s, s ). Set p := 1-L U -L (or 0 if L = U ). Finally, we define µ(s, s

) := (1 -p) • ϕ (s, s ) + p • ϕ u (s, s )).
By Lemma 15, s ∈ LC ϕ (Cons), thus L ≤ 1 ≤ U . Hence 0 ≤ p ≤ 1, and indeed ϕ (s, s ) ≤ µ(s, s ) ≤ ϕ u (s, s ). We check that µ(s) is a probability distribution:

s ∈Cons µ(s, s ) = s ∈Cons (1 -p) • ϕ (s, s ) + p • ϕ u (s, s ) = (1 -p)L + pU = L + p(U -L) = L + 1-L U -L (U -L) = 1
Finally, we show that M implements I. Define R := {(s, s) | s ∈ Cons}. Define δ(s , s ) := 1 and δ(s , s ) := 0 for s = s . Properties (2a)-(2c) of Def. 7 follow directly from the definition of δ, so by Lemma 9, M I.

Inductive n-consistency

Next, we define n-consistency for a state s ∈ S in an IMC, inductively. This rephrases the definition from [START_REF] Delahaye | Parameter Synthesis for Parametric Interval Markov Chains[END_REF]. Intuitively, n-consistent states can perform n consistent steps in a row. That is, they can evolve to (n -1)-consistent states.

Definition 18 (Consistency, inductive). Define sets Cons n ⊆ S by recursion on n: Next, we show that universal n-consistency coincides with global consistency. Note that this depends on the assumption that the system is finitely branching.

Cons 0 = S, Cons n+1 = LC ϕ (Cons n ).
Theorem 20. Let sup(ϕ, s) be finite for all s. Then s ∈ Cons ≡ ∀n : s ∈ Cons n .

Proof. ⇒: Induction on n.

. . . . . [ 0 , 1 ] [ 0 , 1 ] [0, 1] [0, 1] [0, 1]
Fig. 4: Infinitely-branching IMC

The following example shows that the condition on finite branching is essential. The situation is similar to the equivalence of the projective limit model with the bisimulation model in process algebras [START_REF] Bergstra | The algebra of recursively defined processes and the algebra of regular processes[END_REF].

Example 21. Let t [0,1] -→ t i , ∀i and t i+1 [0,1]
-→ t i , see Fig. 4. Then ∀i : t i is i-consistent, but not (i + 1)-consistent (since no transition exits t 0 ). So t is n-consistent for all n. However, no t i is globally consistent, and LC (t, ∅) = ⊥, so t is not globally consistent either.

Finally, we would like to limit the n that we need to check. It has been shown before [START_REF] Delahaye | Parameter Synthesis for Parametric Interval Markov Chains[END_REF] that when the number of states is finite, n = |S| is sufficient. We now show that we can further bound the computation to the length of the longest simple path.

Definition 22 (Paths properties). We define a (reverse) path of length n as a sequence s 0 , . . . , s n-1 , such that for all 0 ≤ i < n, ϕ u (s i+1 , s i ) > 0. The path is simple if for all i, j, with 0 ≤ i < j < n, we have s i = s j . This path is bounded by m if n ≤ m.

Note that, for instance, a path (s 0 , s 1 , s 2 ) has length 3 according to this definition. The essential argument is provided by the following lemma:

Lemma 23. If s ∈ Cons n+1 \ Cons n+2 , then there exists a s , with ϕ u (s, s ) > 0, such that s ∈ Cons n \ Cons n+1 . Proof. Assume s ∈ Cons n+1 and s ∈ Cons n+2 . By Lemma 12(2): s ∈ LC ϕ (Cons n ∩ sup(ϕ, s)). Now if Cons n ∩ sup(ϕ, s) ⊆ Cons n+1 , by monotonicity we would have s ∈ LC ϕ (Cons n ∩ sup(ϕ, s)) ⊆ LC ϕ (Cons n+1 ) = Cons n+2 , which contradicts the assumption. So there must be some s ∈ Cons n with ϕ u (s, s ) > 0 and s ∈ Cons n+1 .

Since Cons n+1 (s) depends on Cons n of its direct successors only, consistency information propagates along paths. In particular, it propagates no longer than the longest simple path. This can be made more formal as follows:

Theorem 24. If all simple paths from s are bounded by m, then:

Cons m (s) ≡ ∀n : Cons n (s)
Proof. We first prove the following statement by induction on n:

(*) If s ∈ Cons n \ Cons n+1 , then there exists a simple path from s of length n + 1, s 0 , . . . , s n = s, such that for all 0 ≤ i ≤ n, s i ∈ Cons i+1 .

Case n = 0: we take the path [s]. Case n + 1: Let s ∈ Cons n+1 but s ∈ Cons n+2 . By Lemma 23, we obtain some s with ϕ u (s, s ) > 0 and s ∈ Cons n \ Cons n+1 . By induction hypothesis, we get a simple path s 0 , . . . , s n = s , with for all 0 ≤ i ≤ n, s i ∈ Cons i+1 . Extend this path with s n+1 := s. We must show that the extended path is still simple, i.e. s i = s for i ≤ n. Since s ∈ Cons n+1 , by Lemma 19 [START_REF] Bart | Reachability in Parametric Interval Markov Chains Using Constraints[END_REF], s ∈ Cons i+1 but s i ∈ Cons i+1 , so s = s i . Finally, to prove the theorem, assume s ∈ Cons m , with all simple paths from s bounded by m. We prove s ∈ Cons n by induction on n. If n ≤ m, s ∈ Cons n by Lemma 19 [START_REF] Bart | Reachability in Parametric Interval Markov Chains Using Constraints[END_REF]. Otherwise, assume as induction hypothesis s ∈ Cons n . Note that there is no simple path from s of length n + 1 since n + 1 > m. By the statement (*), we obtain s ∈ Cons n+1 . So ∀n : s ∈ Cons n .

To summarize, if the longest simple path from s 0 in I = (S, s 0 , ϕ) is of length m, we can compute s 0 ∈ Cons m . From Theorem 24, it follows that ∀n : s 0 ∈ Cons n . By Theorem 20, we then obtain s 0 ∈ Cons. By Theorem 17 we then know that there exists a Markov Chain M = (S, s 0 , µ), s.t. M I. Conversely, if there exists any M = (S , s 0 , µ ) s.t. M I, we know by Theorem 16 that I is consistent.

Example 25. Let us consider again the IMC in Fig. 2b. The longest simple paths from state 0 are [0, 2, 1, 3] and [0, 2, 4, 3], of length 4. Hence to check consistency of the IMC, it suffices to check that state 0 is in Cons 4 .

Algorithms for Consistency Checking of IMCs

In this section, the developed theory is used to provide algorithms to check the consistency of a finite IMC (S, s 0 , ϕ) (i.e. without parameters). In the next section, we will synthesize parameters for PIMCs that guarantee their consistency. For IMCs, we present a forward algorithm and a backward algorithm, which are both polynomial. The justification of these algorithms is provided by the following Corollary to Lemma 12 and Def. 18 and 14.

Corollary 26. Let IMC (S, s 0 , ϕ) be given, let s ∈ S and n ∈ N.

1. s ∈ Cons n+1 ≡ s ∈ LC ϕ (Cons n ∩ sup(ϕ, s)). 2. s ∈ Cons ≡ s ∈ LC ϕ (Cons ∩ sup(ϕ, s)).
The backward variant (Alg. 1) follows our simple co-inductive definition, rephrased as Corollary 26 [START_REF] Bart | Reachability in Parametric Interval Markov Chains Using Constraints[END_REF]. Initially, it is assumed that all states are consistent (true), which will be actually checked by putting them in the work list Q. When some state s is not locally consistent (LC, according to Def. 11), it is marked false (l. 5) and all predecessors t of s that are still considered consistent, are put back in the work list Q (l. [START_REF] Daws | Symbolic and Parametric Model Checking of Discrete-Time Markov Chains[END_REF][START_REF] Dehnert | Prophesy: A probabilistic parameter synthesis tool[END_REF][START_REF] Delahaye | Consistency for Parametric Interval Markov Chains[END_REF].

The forward Alg. 2 is based on the inductive definition of consistency, rephrased in Corollary 26 [START_REF] Bagnara | The Parma Polyhedra Library: Toward a complete set of numerical abstractions for the analysis and verification of hardware and software systems[END_REF]. It is called with a consistency level m and a state s to check if Algorithm 1 Consistency (backward) consistent(s)

Require: t.cons = true (∀t ∈ S) 1: Q := S 2: while Q = ∅ do 3: pick r from Q; Q := Q \ {r} 4: X := {t ∈ sup(ϕ, r) | t.cons = true} 5:
if ¬LC(ϕ, r, X) then 6:

r.cons := false 7: for all t s.t. r ∈ sup(ϕ, t) do 8:

if t.cons = true then 9:

Q := Q ∪ {t} 10: return s.cons Co-inductive (backward) and inductive (forward) algorithms for checking consistency of IMCs.

Algorithm 2 Consistency (forward) consistent(m)(s)

Require: t.pc = 0, t.nc = ∞ (∀t ∈ S) 1: if m ≤ s.pc then 2: return true 3: else if m ≥ s.nc then 4:
return false 5: C := ∅ 6: for all t ∈ sup(ϕ, s) do 7:

if consistent(m -1)(t) then 8:

C := C ∪ {t} 9: if LC(ϕ, s, C) then 10:

s.pc := m 11:

return true 12: else 13:

s.nc := m 14:

return false s ∈ Cons m . It stores and reuses previously computed results, to avoid unnecessary computations. In particular, for each state, we store both the maximal level of consistency demonstrated so far (in field pc, positive consistency, initially 0), and the minimal level of inconsistency (in field nc, negative consistency, initially ∞). We exploit monotonicity to reuse these cached results: By Lemma 19 [START_REF] Bart | Reachability in Parametric Interval Markov Chains Using Constraints[END_REF], if a state is n-consistent for some n ≥ m, then it is m-consistent as well (l. 1-2 of Alg. 2). By contraposition, if a state is not n-consistent for n ≤ m, then it cannot be m-consistent (l. [START_REF] Bergstra | The algebra of recursively defined processes and the algebra of regular processes[END_REF][START_REF] Ceska | PRISM-PSY: precise GPU-accelerated parameter synthesis for stochastic systems[END_REF]. In all other cases, all successors t ∈ sup(ϕ, s) are recursively checked and the (m -1)-consistent ones are collected in C (l. 5-8). Finally, we check the local consistency (LC) of C (l. 9), and store and return the result of the computation in l. 9-14.

Lemma 27. Let |S| be the number of states of the IMC and let |ϕ| := |{(s, t) | ϕ u (s, t) > 0}| be the number of edges. Let d be the maximal degree d := max s |sup(ϕ, s)|. Alg. 2 could start at m equal to the length of the longest simple path, which cannot be efficiently computed in general. Alg. 1 does not require computing any bound.

Parameter Synthesis for Parametric IMCs

In this section, we reconsider intervals with parameters from P . In particular, we present algorithms to synthesize the exact constraints on the parameters for which a PIMC is consistent. Note that given a PIMC and concrete values for all its parameters, we actually obtain the corresponding IMC, by just replacing the parameters by their values. This allows us to reuse all theoretical results on consistency from Section 3 on IMCs.

In particular, we can view parameters as "logical variables", and view a PIMC as a collection of IMCs. For instance, consider a PIMC (P, S, s 0 , ϕ) with parameters P = {p, q}. Given a state s and a finite set of states X ⊆ S, the expression LC (ϕ, s, X) can be viewed as a predicate over the logical variables p and q (appearing as parameters in ϕ). Also Cons(s) and Cons n (s) can be viewed as predicates over p and q. In PVS, we can use universal quantification to lift results from IMCs to PIMCs. For instance, for PIMCs over P , Lemma 19.1 reads: ∀p, q : ∀s ∈ S : Cons n+1 (s) ⇒ Cons n (s).

Inspecting the expression LC (ϕ, s, X) in Def. 11, one realizes that it is actually a constraint over p and q in linear arithmetic. However, due to the recursive/inductive nature of Def. 14 and 18, Cons and Cons n are not immediately in the form of a Boolean combination over linear arithmetic constraints. We can rephrase the definition using an enumeration over all subsets of successors, similar to [START_REF] Delahaye | Parameter Synthesis for Parametric Interval Markov Chains[END_REF]. Since we consider finite PIMCs, the enumeration ∃X ⊆ S corresponds to a finite disjunction. Doing this we get the following variation of the inductive and co-inductive consistency definition:

Corollary 28. Let IMC (S, s 0 , ϕ) be given, and let s ∈ S, n ∈ N

1. s ∈ Cons n+1 ≡ ∃X ⊆ sup(ϕ, s) : s ∈ LC ϕ (X) ∧ X ⊆ Cons n 2. s ∈ Cons ≡ ∃X ⊆ sup(ϕ, s) : s ∈ LC ϕ (X) ∧ X ⊆ Cons
Proof. We only prove (1), since (2) is similar. ⇒: Choosing X := Cons n is sufficient by Lemma 19 [START_REF] Bagnara | The Parma Polyhedra Library: Toward a complete set of numerical abstractions for the analysis and verification of hardware and software systems[END_REF]. ⇐: If for some X, s ∈ LC ϕ (X ∩ sup(ϕ, s)) and X ⊆ Cons n , then by monotonicity, Lemma 12(1), s ∈ LC ϕ (Cons n ∩ sup(ϕ, s)), so s ∈ Cons n+1 by Lemma 19 [START_REF] Bagnara | The Parma Polyhedra Library: Toward a complete set of numerical abstractions for the analysis and verification of hardware and software systems[END_REF].

It becomes clear that the synthesised parameter constraints will be Boolean combinations over linear arithmetic constraints. In particular, expressions in DNF (disjunctive normal form) provide clear insight in all possible parameter combinations. The number of combinations can be quite large, but we noticed that in many examples, most of them are subsumed by only a few maximal solutions. In particular, we will use the following notations for operators on DNFs:

-, ⊥ denote true and false (universe and empty set) for their union (including subsumption simplification) for their intersection (including transformation to DNF and simplification) for their (semantic) subsumption relation

We have experimented with two prototype realizations of our algorithms. One approach is based on CLP (constraint logic programming) in SWI-Prolog [START_REF] Wielemakers | SWI-prolog version 7 extensions[END_REF] + CLP(Q). We wrote a small meta-program for the subsumption check. The other approach is based on Parma Polyhedra Library [START_REF] Bagnara | The Parma Polyhedra Library: Toward a complete set of numerical abstractions for the analysis and verification of hardware and software systems[END_REF]. In particular, its Pointset Powerset Closed Polyhedra provide efficient implementations of the operations on DNFs.

Inductive Approach

In the inductive approach, Corollary 28(1) gives rise to a set of equations on variables v n,s (state s is n-consistent):

let v 0,s = let v n+1,s = X⊆sup(ϕ,s) LC ϕ (X) t∈X v n,t
Starting from the initial state v |S|,s0 , we only need to generate the reachable equations that are not pruned away by inconsistent LC ϕ (X) constraints, and we need to compute each equation only once. Note that there will be at most |S| 2 reachable equations. The number of conjunctions per equation is bounded by 2 d , the number of X ⊆ sup(ϕ, s), and for each X we build a conjunction of length O(d). So, the size of the whole set of equations is bounded by O(|S| 2 .d.2 d ). In general, however, there is no polynomial upper bound on the size of the corresponding solution. Also, note that by Theorem 24, we could replace |S| by the length of the longest simple path.

The set of equations can be interpreted directly as a Constraint Logic Program in Prolog, with predicates cons(N,S). Prolog will compute the dependency tree for s ∈ Cons n , by backtracking over all choices for X. Along the way, all encountered LC ϕ predicates are asserted as constraints to the CLP solver. This has the advantage that locally inconsistent branches will be pruned directly, without ever generating their successors. By enumerating all feasible solutions, we obtain the complete parameter space as a disjunction of conjunctive constraints.

However, the computation tree has a lot of duplicates, and the number of returned results is very high, since we start out with a deeply nested and-or-expression. We provide a more efficient version in Alg. 3. Here recomputations are avoided by caching all intermediate results in a Table (see l. 3 and 12). For each enumerated subset of successors X (l. 6), the algorithm checks (n -1)-consistency. Note that we "shortcut" this computation as soon as we find that either X is not locally consistent, or some t ∈ X is not (n -1)-consistent (l. 8). The final optimization is to suppress all subsumed results in the resulting conjunctions and disjunctions. We show this by using and . This drastically reduces the number of returned disjunctions.

We have implemented Alg. 3 in Prolog+CLP, using meta-programming techniques to suppress subsumed results. Alternatively, one could implement the algorithm directly on top of the Parma Polyhedra Library.

Co-inductive approach

Next, we show how to encode co-inductive consistency in a Boolean Equation System (BES) (over sets of polyhedra). Here, the equations will be recursive. The largest solution for variable v i indicates that state s i is consistent. This solution provides then a description of the set of all parameters for which the PIMC is consistent.

Definition 29 (BES in DNF). Given a PIMC P = (P, S, s 0 , ϕ), we define the BES as the following set of equations, for each formal variable v s , s ∈ S:

v s = X⊆sup(ϕ,s) LC ϕ (X) t∈X v t s ∈ S
We can bound the size of this BES and the number of iterations for its solution. Again, the size of the final solution cannot be bounded polynomially.

Lemma 30. For each PIMC P = (P, S, s 0 , ϕ), with out-degree bounded by d, the corresponding BES has size O(|S|.d.2 d ). The BES can be solved in O( ) iterations, where is the length of the longest simple path in P.

Proof. We have |S| equations of size at most O(d.2 d ) each. The BES can be solved by value iteration. Let F s denote the right hand side of the equation for v s . We can compute the largest solution by iteration and substitution as follows:

σ 0 = λs. σ n+1 = λs.F s [v t → σ n (t) | t ∈ S]
By monotonicity, σ n ⊇ σ n+1 (pointwise). We can terminate whenever σ n ⊆ σ n+1 . Since it can be proved by induction that σ n ≡ Cons n , the process terminates within steps by Lemma 24.

Solving this BES can be done by straightforward value iteration, see Lemma 30. The intermediate expressions can be viewed as collections of polyhedra, represented e.g. by the Parma Polyhedra Library as Powersets of Convex Polyhedra [START_REF] Bagnara | The Parma Polyhedra Library: Toward a complete set of numerical abstractions for the analysis and verification of hardware and software systems[END_REF]. Alg. 4 provides a variant of the iteration in Lemma 30. Here we only update the polyhedra for nodes whose successors have been modified. To this end, we maintain a worklist Q of states that we must check initially (l. 1) or when their successors are updated (l. 9). This algorithm can be viewed as the parametric variant of the backward Alg. Q := Q ∪ {t} 10: return s0.sol Inductive and co-inductive algorithms for parameter synthesis in PIMCs. We solve the simplified BES by value iteration as follows. In Approximation 0, each vi=true. We show approximations 1-3, which is the stable solution. From the final result, we can conclude that the initial state in Fig. 2a is consistent, if and only if 0.3 ≤ q ≤ 0.7 ∨ q = 1. To get an indication of the effectiveness of our algorithms and optimizations, we performed some experiments in a Prolog prototype implementation on Lehmann and Rabin's randomized dining philosophers from Prism [START_REF] Kwiatkowska | PRISM 4.0: Verification of probabilistic real-time systems[END_REF]. First, we modified that DTMC to an IMC by replacing probabilities like 0.1666 by intervals [0.1, 0.2]. This made the consistency analysis numerically more stable. Subsequently, we replaced some probabilities by parameters to get a PIMC, and experimented with different intervals as featured in the first column of Table 1, for one parameter P or two parameters P and Q.

The number of edges with these parameters is given in the third column of the table. We compared the inductive algorithm for increasing n-consistency with the co-inductive algorithm. Column CLP shows our Prolog implementation of the inductive algorithm from [START_REF] Delahaye | Parameter Synthesis for Parametric Interval Markov Chains[END_REF]. CLP+opt corresponds to the inductive Alg. 3, including our optimizations, i.e. caching and subsumption. PPL shows our co-inductive Alg. 4. We carried out the experiments on the model for 3 philosophers (956 states, 3625 edges) and 4 philosophers (9440 states, 46843 edges). Table 1 shows the results; all times are measured with the SWI-Prolog library statistics. Increasing n-consistency highly impacts the performance. It is clear that caching and subsumption provide useful optimizations, since we can now compute consistency for much higher n. The co-inductive variant with PPL wins, since it is always faster than CLP+opt for n = 50. We also observe that the increase time from 3 to 4 philosophers is considerable. This is consistent with the complexity result (note that for phil4, d ≈ 5 so d • 2 d ≈ 150).

Note that PPL computes consistency constraints for all states and for all n, whereas CLP only computes this for small n and the initial state. As an example, the constraint computed by PPL for 3 philosophers, 2 parameters, intervals [0, P ] and [0.3, Q] is (3P ≥ 0.5 ∧ Q ≥ 0.34) ∨ (2P + Q ≥ 1 ∧ p ≥ 0.25 ∧ 3Q ≥ 1).

Fig. 1 :

 1 Fig. 1: Examples of a PMC (a), an IMC (b), and of their generalization PIMC (c). The MC (d) implements the PIMC (c), as shown by the dashed edges, and formalized in Def. 7. We drop self-loops with probability 1 (or [1, 1]) in all terminal nodes.

Lemma 9 .

 9 Def. 7 with clauses (2a)-(2c) is equivalent to Def. 7 with (2a)-(2d).

Fig. 2 :

 2 Fig. 2: Running Examples

Fig. 3 :

 3 Fig. 3: The Markov Chain (left) implements the Interval Markov Chain (right)

Proof. ( 1 )

 1 holds because Cons is a fixed point; the second equation uses Lemma 12(2); (2) holds because Cons is the greatest fixed point. (Tarski) We motivate the definition of consistency by the following two theorems: Theorem 16. Let M = (S M , s M0 , µ) be a MC, I = (S I , s I 0 , ϕ) an IMC, and assume M I. Then s I 0 ∈ Cons.

Lemma 19 . 1 . 1 .

 1911 We have the following basic facts on local consistency: Cons n+1 ⊆ Cons n 2. If m ≤ n then Cons n ⊆ Cons m . 3. If Cons n+1 = Cons n and s ∈ Cons n then ∀m : s ∈ Cons m . Proof. Induction on n. n = 0 is trivial. Let s ∈ Cons n+2 = LC ϕ (Cons n+1 ). By induction hypothesis, Cons n+1 ⊆ Cons n , so by the monotonicity lemma 12(1, s ∈ LC ϕ (Cons n ) = Cons n+1 , indeed. 2. Induction on n -m, using (1). 3. If m > n, we prove the result with induction on m-n. Otherwise the result follows from (2).

1 .

 1 Example 31. On the example in Fig 2a, Def. 29 gives rise to the following equation system (simplifying trivial arithmetic inequalities and global bounds 0 ≤ p, q ≤ 1).Algorithm 3 Inductive Parameter Synthesis Algorithm Cons(s, n)Require: Initialize: T able := ∅ 1: if n = 0 then 2: return 3: if ∃R : (s, n, R) ∈ Table then 4:return R 5: D := ⊥ 6: for all X ⊆ sup(ϕ, s) do 7:C := LCϕ(X) 8:while X = ∅ ∧ C = ⊥ do 9: pick t from X; X := X \ {t} 10:C := C Cons(t, n -1) 11:D := D C 12: add (s, n, D) to

  .3 & q=<0.7 | q>=0.3 & q=<0.7 | q=1 v1 = q=<0.7 & q>=0.3 v1 = q>=0.3 & q=<0.7 v1: idem v2 = p+q>=0.5 v2 = p+q>=1 & q>=0.3 & q=<0.7 v2: idem |

  The base case is trivial. Assume s ∈ Cons. Then s ∈ LC ϕ (Cons). By induction hypothesis, Cons ⊆ Cons n . So, by monotonicity, Lemma 12(1), s ∈ LC (Cons n ) = Cons n+1 . Assume that s ∈ n≥0 Cons n . Define Y n := Cons n ∩sup(ϕ, s). By Lemma 19(1), s ∈ Cons n+1 = LC (Cons n ) = LC ϕ (Y n ) and Y n is a decreasing sequence of finite sets (since ϕ has finite support). Hence it contains a smallest member, say Y m . For Y m , we have s ∈ LC ϕ (Y m ) and Y m ⊆ n≥0 Cons n . By monotonicity, Lemma 12(1), s ∈ LC ϕ ( n≥0 Cons n ). So we found another fixed point, and by Lemma 15(2), n≥0 Cons n ⊆ Cons, so indeed s ∈ Cons.

		t0
		t1
	t	t2
	.

⇐:

  Note that in Alg. 1 every state is set to ⊥ at most once. So every state s is added to Q at most |ϕ u (s)| + 1 = O(d) times. Handling a state requires checking its incoming and outgoing edges, leading to O(|ϕ| • d) time complexity. Only one bit per state is stored. Alg. 2 is called at most m ≤ |S| times per state. Every call inspects the outgoing edges a constant number of times, leading to time complexity O(|S| • |ϕ|). It stores two integers, which are at most |S|, which requires 2 log 2 |S| + 1 bits.

1. Algorithm 1 has worst-case time complexity O(|ϕ|•d) and space complexity O(|S|). 2. Algorithm 2 has worst-case time complexity O(|S| • |ϕ|) and space complexity O(|S| • log 2 |S|).

Proof.

Table 13 :

 13 return D Algorithm 4 Co-inductive Parameter Synthesis Algorithm

	3:	pick s from Q; Q := Q \ {s}
	4:	sol := X⊆sup(ϕ,s)
		(LCϕ(X)	t∈X t.sol)
	5:	if sol s.sol then
	6:	s.sol := sol
	7:	for all t s.t. s ∈ sup(ϕ, t) do
	8:	if t.sol = ⊥ then
	9:

Require: Initialize: s.sol := (∀s ∈ S)

1: Q := S 2: while Q = ∅ do

The complete text of the proofs, their PVS formalisation, Prolog programs, and experimental data can be found at http://fmt.cs.utwente.nl/ ˜vdpol/PIMC2018.zip.

In the following, for the sake of readability, we do not consider linear combinations of parameters as bounds of the intervals. However, allowing them would not change the results.

Acknowledgement. The authors would like to thank the reviewers for their extensive comments, which helped them to improve the paper. They acknowledge the support of University Paris 13 and of the Van Gogh project PAMPAS, that covered their mutual research visits.

This research was conducted with the support of PHC Van Gogh project PAMPAS.

Perspectives

Using inductive and co-inductive definitions of consistency, we provided forward and backward algorithms to synthesize an expression for all parameters for which a PIMC is consistent. The co-inductive variant, combined with a representation based on convex polyhedra, provides the most efficient algorithm. We believe that our work extends straightforwardly when the intervals are replaced by arbitrary linear constraints, since both CLP and PPL can handle linear constraints. The resulting formalism would generalize (linear) Constraint Markov Chains [START_REF] Delahaye | New results for Constraint Markov Chains[END_REF] by adding global parameters. Also, our approach should apply directly to parameter synthesis for consistent reachability [START_REF] Delahaye | Parameter Synthesis for Parametric Interval Markov Chains[END_REF]. We also plan to experiment with other case studies, e.g. the benchmarks of [START_REF] Bart | Reachability in Parametric Interval Markov Chains Using Constraints[END_REF], with an implementation that is more elaborate than our initial prototype. This would give insight on how the algorithms scale up w.r.t. the number of parameters and of parametric edges. Finally, [START_REF] Bart | Reachability in Parametric Interval Markov Chains Using Constraints[END_REF] gives a polynomial size CLP with extra variables, but doesn't address the parameter synthesis problem. Polynomial size CLP programs without extra variables can be obtained using if-then-else, e.g. (v 0 ?1 : 0) + (v 1 ?1 : 0) + (v 2 ?p : 0) ≤ 1. However, we don't know of a method to solve equation systems with conditionals without expanding them to large intermediate expressions.