MONFROY M Éric

Charlotte Mme

Truchet

Professeur M Salvador Abreu

Mme Béatrice

Professeur B Érard

Professeur M Nicolas Beldiceanu

Professeur M Philippe Codognet

Maître M Benoît Delahaye

Keywords: Constraint Modelling -Constraint Solving -Program Verification -Abstract Interpretation -Model Checking viii modélisation par contraintes -résolution par contraintes -vérification de programmes -interprétation abstraite -vérification de modèles Constraint Modelling, Constraint Solving, Program Verification, Abstract Interpretation, Model Checking

Constraint Modelling and Solving of some Verification Problems Short abstract: Constraint programming offers efficient languages and tools for solving combinatorial and computationally hard problems such as the ones proposed in program verification. In this thesis, we tackle two families of program verification problems using constraint programming. In both contexts, we first propose a formal evaluation of our contributions before realizing some experiments. The first contribution is about a synchronous reactive language, represented by a block-diagram algebra. Such programs operate on infinite streams and model real-time processes. We propose a constraint model together with a new global constraint. Our new filtering algorithm is inspired from Abstract Interpretation. It computes over-approximations of the infinite stream values computed by the block-diagrams. We evaluated our verification process on the FAUST language (a language for processing real-time audio streams) and we tested it on examples from the FAUST standard library. The second contribution considers probabilistic processes represented by Parametric Interval Markov Chains, a specification formalism that extends Markov Chains. We propose constraint models for checking qualitative and quantitative reachability properties. Our models for the qualitative case improve the state of the art models, while for the quantitative case our models are the first ones. We implemented and evaluated our verification constraint models as mixed integer linear programs and satisfiability modulo theory programs. Experiments have been realized on a PRISM based benchmark.

Introduction

Computer scientists started to write programs in order to produce softwares realizing dedicated tasks faster and more efficiently than a human could perform. However, in adhoc developments the more complex is the problem to solve the longer it takes to write its corresponding solving program. Moreover, few modifications in the description of the problem to solve may impact many changes in the program. The artificial intelligence research domain tries to develop more generic approaches such that a single artificially intelligent program may solve a wide variety of heterogenous problems. Constraint programming is a research axis in the artificial intelligence community where constraints are sets of rules to be satisfied and the intelligent program must find a solution according to these rules. Thus, the objective of the constraint programming community is to produce languages and tools for solving constraint based problems. Such problems are expressed in a declarative manner where programs consist in a set of rules (called constraints) to be satisfied. Thus, a constraint programming user enumerates his/her rules and uses a black-box tool (called solver) for solving his/her problem. These are two major research activities in constraint programming: modelling and solving. The modelling activity works on the expressiveness of the constraint language and manipulates constraint programs in order to improve the resolution process. The solving activity consists in developing algorithms, tools, and solvers for improving the efficiency of the resolution process.

For the last decades computers and information systems have been highly democratized for private and company usages. In both contexts, more and more complex systems are developed in order to realize a wide variety of applications (smart applications, embedded systems for air planes, medical robot assistants, etc.). As for many other production fields, writing systems must respect quality rules such as conformity, efficiency, and robustness. In this thesis, we are concerned by the verification problem consisting in verifying if an application, a program, a system matches its specifications (i.e., its expected behavior). This concern gained an important interest after social or business impacts are identified, or after past failures. One of the most remarkable examples is the crash of the Ariane 5 missile, 36 seconds after its launch on June 4, 1996. The accident was due to a conversion of a 64-bit floating point number into a 16-bit integer value. Another example is the bug in Intel's Pentium II floating-point division unit in the 90's, which forced to replace faulty processors, severely damaged Intel's reputation, and implied a loss of about 475 million US dollars. These events happened in the 90', and software are now more and more used to automatically control critical systems such as nuclear power plants, chemical plants, trafficc o n t r o ls y s t e m s ,a n ds t o r ms u r g eb a r r i e r s . F u r t h e r m o r e ,e v e np r o g r a m sw i t hl e s s critical impact require attention, since the competition between products gives benefits to the systems with less bugs, a better reactivity, etc. Thus, the verification objective is to attest the validity of a system according to an expected behavior.

While such problems may be solved using add-hoc techniques or proper tools, it appears that by nature or by reformulation of the problem, constraint programming offers effective solutions. For instance, the system/program can be formulated as a set of rules and the expected behavior as a set of constraints. Thus, verifying the validity of the system/program behavior consists in determining if satisfying the rules implies to satisfy the expected behavior. On the other hand, some verification considerations may produce combinatorial problems. In this context constraint programming clearly appears as a suitable solution. In this thesis we tackle program verification problems as applications to be treated using constraint programming.

Scientific Context

As said before this thesis concerns constraint programming modelling and solving for some program verification problems. In this section we briefly present all the scientific context of the thesis by identifying separately the various scientific thematics tackled in this manuscript. We start by presenting constraint modelling and solving. Then, we continue with the two program verification approaches used in this thesis, and we conclude by presenting the two programming paradigms to be verified in this thesis.

Constraint Modelling. A Constraint Satisfaction Program (CSP for short) is a set of constraints over variables each one associated with a domain. Thus, constraint modelling consists in formulating a given problem into a CSP. There exist various research communities each one dedicated to model families of CSPs. Recall first that the general problem of satisfying a CSP (i.e., finding a valuation of the variables satisfying all the constraints in the CSP) is a hard problem. There exists CSP families being tractable in exponential, polynomial, or ever linear time. In this thesis we consider constraint modelling ranging from mathematical programming such as continuous and mixed integer linear programing (respectively LP and MILP for short), finite and continuous domains programs without linearity restrictions on the constraints (respectively named FD and CD for short), and Satisfiability Modulo Theory (SMT for short) mixing Boolean and theories such as arithmetics. See Section 2.2 for more details.

Constraint Solving. Various tools, named solvers, have been developed for solving CSP instances. Each one is mainly specialized to solve specific CSP families (e.g.,u nbounded integer linear arithmetics, constraints over variables with finite domain, continuous constraints). The combinatorics implied by the relations between the variables in the constraints makes a CSP hard to solve. This requires to explore search spaces composed of all the valuations possibly candidate for solving the problem. However, the size of such search space is exponential in terms of the problem sizes (number of variables) in general. Huge research efforts has been put into solvers in order to propose tools for (intelligently) explore huge search spaces and solve CSP instances. See Section 2.3 for more details.

Program Verification A program describes the behavior of a possibly infinite process by defining possible transitions from states to states. Due either to the runtime environment or to the non determinism of the state successions, one program may have a finite or even an infinite number of possible runs. Also, according to the nature of a program its runs may encounter either a finite or an infinite number of states in theory. Thus, program verification consists in determining if the program traces (i.e., the state sequences realized by the runs) respect a given property. These properties may be time dependent (e.g., for each run the state A must be encountered after the state B, the state A must not be encountered before a given time t) or time independent (e.g., for each run all the variables are bounded by given constants). There are two main approaches for verifying properties on program: dynamic analysis vs. static analysis. Dynamic analysis requires to run the program to attest the validity of the property. On the contrary, static analysis performs verification at compilation time without running the program/system (roughly speaking dynamic analysis can be considered as an online process compared to static analysis which is an offline process). See Section 3.1 for more details. In this thesis we only consider complete static analyzes of programs with infinite runs (i.e.,w ed on o t consider dynamic and bounded analyzes).

Abstract Interpretation. Abstract Interpretation is a program verification technique for static program analysis. In this context, we consider programs with unbounded running times and infinite state systems. Recall that in such cases the general program verification problem is undecidable since this class of problems contains the halting problem. Thus, Abstract Interpretation provides a verification process, which terminates, using over-approximations of the semantics of the program to verify. Indeed, well chosen abstractions produce semi-decidable problems. Thus, verification tools based on abstract interpretation either prove the validity of the property or may not conclude. Hence, such method cannot find counter-examples and falsify properties. See Section 3.2 for more details.

Model Checking. Model Checking is a program verification technique for static program analysis. As for Abstract Interpretation, programs/models to be verified may have unbounded running times and infinite state space. Thus, model checking is a verification method that explores all possible system states. In this way, it can be shown that a given system model truly satisfies a certain property. Hence, such method proves the validity or the non validity of the property. More specifically, it can return a counter-example in non validity case. See Section 3.3 for more details.

Synchronous Reactive Language. Motivated by the nature of embedded controllers requiring to be reactive to the environment at real-time, synchronous languages have been designed for programming reactive control systems. These languages naturally deal with 1.2. Problems and Objectives the complexity of parallel systems. Indeed, parallel computations are realized in a lockstep such that all computations are synchronized reactions. Hence, this synchronization ensures by construction a guarantee of determinism and deadlock freedom. Finally, these languages abstract away all architectural and hardware issues of embedded, distributed systems such that the programmer can only concentrate on the functionalities. Instances of such languages are Faust, Lustre, and Esterel and have been successfully used in the context of critical systems requiring strong verification (e.g., space applications, railway, and avionics) using certified compiler (e.g., Scade [Sca] tool from Esterel Technologies providing a DO-178B level A certified compiler). Chapter 4 concerns the verification of synchronous reactive languages.

Probabilistic Programming Language. Various systems are subject to phenomena of a stochastic nature, such as randomness, message loss, probabilistic behavior. Probabilistic programming languages are used to describe such systems using probabilities to define the sequence of states in the program. One of the most popular probabilistic models for representing stochastic behaviors are the discrete-time Markov Chains (MCs for short). Instance of probabilistic programming languages for writing MCs are Problog and Prism. Chapter 5 concerns the verification of models extending the Markov chain model describing parametrized probabilistic systems.

Problems and Objectives

As presented in the previous sections, program verification is a computationally hard problem with major issues. Recall first that a program describes the behavior of a possibly infinite process by defining possible transitions from states to states. However, the verification is performed on an abstraction of the program named model 1 . In this thesis, we consider finite models with infinite state spaces and infinite runs.

Even if a program admits a priori an infinite state space its executions may encounter a( p o t e n t i a l l yi n fi n i t e )s u b s e to ft h ed e c l a r e ds t a t es p a c e . T h u s ,o n ew o u l dl i k et od e t e rmine this smaller state space in order to verify the non reachability of undesired states. This problem is reducible to the search of program over-approximations, i.e.,b o u n ding all the program variables. This is an objective of Abstract Interpretation where the program describing precisely the system evolution from a state to another, named the concrete program, is abstracted. This abstracted construction is related to the concrete program in such a manner that if an over-approximation holds for the abstraction then, this approximation also holds for the concrete program. Furthermore, constraint programs allow to describe over-approximations such as convex polyhedrons using linear constraints, ellipsoids using quadratic constraints, etc. Thus, since constraint programming is a generic declarative programing paradigm it may be seen as a verification process for over-approximating variable in declarative programs. In the first contribution, we consider a block-diagram language where executions are infinite streams and the objective is to bound the stream values using constraint programming.

However, bounding the state space is not enough for some verification requirements. In our second problem, the objective is to determine if a specific state is reachable at execution time. Indeed, abstractions can only determine if a specific state is unreachable. For this verification problem, we consider programs representable as finite graph structures where the nodes form the state space and the edges give state to state transitions. Thus, verifying the reachability of a state in such a structure is performed by activating or deactivating transitions in order to reach the target state. However, these activations can be restricted by guards, or other structural dependent rules. Clearly, this corresponds to acom binatoricproblemtosolv e. F orthisreason,sinceoneoftheobjectiv esofconstrain t programming is to solve highly combinatorial problems, the verification community is interested in the CP tools. Some links between constraint programming and program verification are presented in Section 3.4. To conclude, constraint programming proposes languages to model and solve problems by focusing on the problem formulation instead of the resolution process. Program verification leads to problems which by definition or by nature are close to constraint programs. Thus, the verification community uses constraint programming tools for developing analyzers instead of producing ad-hoc algorithms. In this thesis, we position ourself as constraint programmers and we consider verification problems as applications. Thus, our objective is to present how the constraint programming advances in modelling and solving helps to answer some verification problems.

Contributions

The contributions are split into two distinct chapters, and they are related to different verification research axes, but both using constraint programming. The first contribution applies constraint programming to verify some properties of a real-time language, while the second one is about verification of extensions of Markov chains. Here are the abstracts of these two contributions.

Verifying a Synchronous Reactive Language with constraints (Chapter 4). Formal verification of real time programs in which variables can change values at every time step, is difficult due to the analyses of loops with time lags. In our first contribution, we propose a constraint programming model together with a global constraint and a filtering algorithm for computing over-approximation of real-time streams. The global constraint handles the loop analysis by providing an interval over-approximation of the loop invariant. We apply our method to the FAUST language which is a language for processing real-time audio streams. We conclude with experiments that show that our approach provides accurate results in short computing times. This contribution has been published in a national conference [1], an international conference [2], and a journal [3].

Verifying a Parametric Probabilistic Language with constraints (Chapter 5). Parametric Interval Markov Chains (pIMCs) are a specification formalism that extends Markov Chains (MCs) and Interval Markov Chains (IMCs) by taking into account imprecision in the transition probability values: transitions in pIMCs are labeled with parametric intervals of probabilities. In this work, we study the difference between pIMCs and other Markov Chain abstractions models and investigate the three usual semantics for IMCs: once-and-for-all, interval-Markov-decision-process, and at-every-step. In particular, we prove that all these semantics agree on the maximal/minimal reachability probabilities of agivenIMC.W etheninvestigatesolutionstoseveralparametersynthesisproblemsinthe context of pIMCs -consistency, qualitative reachability, and quantitative reachabilitythat rely on constraint encodings. Finally, we conclude with experiments by implementing our constraint encodings with promising results. This contribution has been published in a national conference [4], an international workshop without proceedings [5], and an international conference [6] (to appear).

Outline

The thesis in organized in four main chapters. Chapter 2 presents the constraint programming paradigm. Chapter 3 introduces program verification/model checking problems. We conclude this chapter by briefly introducing the two verification methods named Abstract Interpretation and Model Checking in order to motivate the two following chapters which respectively use these verification methods. Chapter 4 contains our first contribution. This chapter proposes a constraint programming model together with a global constraint and a filtering algorithm inspired from abstract interpretation for computing over-approximation of real-time streams. This chapter is also illustrated and validated by some experiments. Chapter 5 contains our second contribution. This chapter proposes constraint programming models for verifying qualitative and quantitative properties of parametric interval Markov chains with a model checking objective. This chapter also concludes with experiments. Note that both contribution chapters are self-contained including introduction, motivation, background, state of the art, contributions, and bibliography. Finally, Chapter 6 concludes this thesis document.

Chapter 2 Constraint Programming

Introduction

Computer scientists started to write programs in order to produce softwares realizing dedicated tasks faster and more efficiently than a human could perform. However, in ad-hoc developments the more complex is the problem to solve the longer it is to write its corresponding solving program. Moreover, few changes in the description of the problem to solve may impact many changes in the program. Thus, the artificial intelligence research domain tries to develop more generic approaches such that a single artificially intelligent program may solve a wide variety of heterogeneous problems. Among all possible artificial intelligences, we focus in this thesis on those dealing with constraint based problems. In such problems, one can enumerate a set of objects with possibly many different states for each object and a set of accepted configurations over these objects w.r.t. the states (cf. Definition 2.1.1). Definition 2.1.1 (Constraint Based Problem). Let A be a set of objects, and S be a set of object states. A Constraint Based Problem P over objects A with states S represents a set of configurations (i.e., a set of associations between objects from A and states in S). Formally P ⌘ L s.t. L ✓ S A .

In this chapter, we first present constraint modelling (i.e., variables, domains, constraints, and constraint programs definitions) and various research axes dedicated to constraint modelling (SAT, CP, LP, etc.). Then, we present these research axes dealing with constraint programs by describing their common resolution processes and their specific strategies developed in each one.

Restrictions. In this thesis we consider modelling with real, integer, and Boolean variables with finite or infinite domains without restrictions on the constraints (e.g., enumerations, linear and non-linear inequations, Boolean compositions, global constraints) using the existential quantification of variables and being time-independent 1 . Finally, we consider complete methods for solving such models.

Constraint Modelling

Constraint modelling is the action of formulating a given constraint based problem into a constraint based program. Definition 2.1.1 recalled that a constraint based problem is described by a set of objects, a set of object states, and gathered into a set of configurations. Constraint programming uses a dedicated vocabulary. In the following we take care to well separate the constraint based problems from constraint based programs. Indeed constraint based problems are commonly expressed in a natural language while constraint programs are expressed in a mathematical (or mathematical-like) language or a programming language. A constraint program uses variables associated with domains linked by constraints. Roughly speaking, the variables with their domains will model the objects with their states in the constraint based program while the constraints will model the configurations in the constraint based program. We now present a wide landscape of variables, domains, and constraints encountered in constraint modelling while encoding a constraint based problem into a constrained program.

5 Z0Z0Z 4 0Z0Z0 3 Z0Z0Z 2 0Z0Z0 1 Z0Z0Z abcde Q Q Q Q Q (a)
Example 1 (n-Queens Problem). The n-Queens problem will be our backbone example for illustrating constraint modelling and solving in this section. Let n be a natural number. Thus we consider an n ⇥ n chessboard and n queens. The n-Queens Problem objective is to place the n queens on the chessboard such that no two queens threaten each other (i.e., no two queens share the same row, column, or diagonal). In this example, objects are the n queens and states are the n ⇥ n cells of the chessboard. Thus, a configuration is an arrangement of the n queens on the chessboard.

Variables and Domains

A constraint based problem is described by a set of variables, each variable being associated with a non-empty set called its domain. From now on in this section, X will refer to as e to fn variables x 1 ,...,x n , D x will be the domain associated to the variable x 2 X, and D will contain all the domains associated to the variables in X. We identify four variable types according to their domain. We say that a variable x with domain D x is:

• aB oo l e a nv a r i a b l ei ff its domain is a binary set (i.e., D x = {true, false})

• an integer variable iff its domain only contains integers (i.e., D x ✓ Z)

• ar a t i o n a lv a r i a b l ei ff its domain only contains rational numbers (i.e., D x ✓ Q)

• ar e a lv a r i a b l ei ff its domain only contains real numbers (i.e., D x ✓ R) A domain can be given in extension by enumerating all the elements composing it or in intension using an expression representing all its elements. One common compact representation is the interval representation together with the union of intervals. Formally, let E ✓ R be a non-empty totally ordered set and a, b 2 R2 be two interval endpoints. We write I E ([a, b]) for the set containing all the (closed, semi-opened, opened) intervals subsets of the interval [a, b] ✓ E. When modelling, we usually separate real variables with interval domains from others. The first ones are called continuous variables while the remaining are called discrete variables. Furthermore, we separate finite variables (i.e., variables whose domains have a finite number of elements) from infinite variables. For instance afi n i t ev a r i a b l ec a nb ei n t r o d u c e db yd o m a i ne n u m e r a t i o n( e.g.,d o m a i n{1, 2,...,50}) and infinite variables can be defined by interval domain (e.g., domain [-1, 1] subset of R). Note that there exists other domains such that the symbolic domains where each domain may contain an infinite number of possibly ordered symbols, or the set domains where each domain element is a set of values. In this thesis we perform constraint modelling with Boolean, integer, rational, and real-number domains. Finally, a valuation of the variables in X 0 ✓ X is a mapping v associating to each variable in X 0 av a l u ei ni t sd o m a i n( i.e., v :

X 0 ! D s.t. v(x) 2 D x for all x 2 X 0 ). Example 2.
Here are some domain instances:

• {0, 1,...,100} =[0, 100] ✓ N finite domain over integers • {0, 1, 2, 3, 5, 7, 11} finite discontinuous domain enumeration • [0, 100] ✓ R infinite continuous domain • {0} [ [1, 100] ✓ R infinite semi-continuous domain

Constraints

A constraint is defined over a set of variables and represents a set of accepted valuations. Formally a constraint c over the variables X with domains D is semantically equivalent to a set of valuations from X to D: c ⌘ V such that V ✓ D X . Constraints can be represented in extension by enumerating accepted valuations or in intension by a predicate over the variables in the constraint. With Boolean variables, the atomic constraints are the logical predicates such as the negation (¬), the conjunction (^), the disjunction (_), the implication ()), the equivalence (,). For other domains, we consider atomic constraints as equations or inequations where their left-hand side and right-hand side are arithmetic expressions (i.e., any mathematical expressions such that polynomials, trigonometric functions, logarithms, exponentials, etc.). In the context of finite variables, the Constraint Programming community proposes a catalogue of constraints with a high level semantics called global constraints (cf. Section 2.2.5). According to the domains considered in this thesis (i.e., B, Z, Q,a n dR)o n ei m po r t a n tc o n s t r a i n tc h a r a c t e r i z a t i o n is the linearity. We say that a constraint is linear iff its arithmetic expressions are linear arithmetic expressions (i.e., not containing products of variables). Less importantly one may also consider the convexity properties of the arithmetic expressions. Furthermore, recall that there exist two quantifiers: the existential and the universal quantifiers. Thus, in quantified constraints, variables are associated to quantifiers and the CSP is satisfiable iff the quantifiers hold for the given domains (e.g., 9x 2 [-1, 1], 8y 2 [0, 1] : x + y  1i s satisfiable). In this thesis we only consider constraints with the existential quantifier (i.e., the universal quantifier is not allowed). Finally, a constraint problem is the composition of atomic constraints with logical operators. Example 3. Figure 2.2 describes three constraints c 1 , c 2 ,andc 3 over two variables x and y. Geometrically speaking, constraint c 1 defines a disc, c 2 is an upper half-space, and c 3 is a rectangle. Thus, c 1 can be expressed by a quadratic inequality, c 2 by a non-linear inequality, and c 3 by a conjunction of four linear inequalities. The pink zone contains all the solutions of the CSP C 1 with constraints c 1 , c 2 , c 3 over variables x, y with respective domains [0, 8] ✓ R,a n d[ 0 , 6] ✓ R. One may also consider the CSPs C 2 and C 3 which respectively contain the constraints c 1 ^(c 2 _ c 3 )a n dc 1 , (¬c 2 ^c3 ) producing different solution areas (i.e., solution spaces/feasible regions).

Satisfaction and Optimization Problems

A constraint satisfaction problem consists in determining if a constraint satisfaction program (cf. Definition 2.2.1)i se i t h e rsatisfiable or unsatisfiable. Formally, a valuation v satisfies a CSP P =(X, D, C)i ff there exists a valuation v over variables X satisfying all the constraints in C (i.e., the set of constraints in C is interpreted as a conjunction of constraints). If such a valuation v exists we say that P is satisfiable (and v is named a solution of P), otherwise we say that P is unsatisfiable. In the following, we call CSP family a set of CSPs sharing properties (e.g.,o n l y using integer variables, only considering linear constraints). Thus, according to a CSP family its theoretical complexity for the satisfaction problem may be polynomial or not, and either be undecidable. Table 2.1 from [7] synthesizes theoretical complexities for solving the satisfaction problem according to variables and constraints types. For instance the satisfaction of: a conjunction of linear constraints over real variables can be solved in polynomial time [START_REF] Gács | Khachiyan's algorithm for linear programming[END_REF]; a conjunction of constraints over integer finite variables is an NP-complete problem [START_REF] Thomas | The Complexity of Satisfiability Problems[END_REF]; non-linear constraints over unbounded integer variables is an undecidable problem [7].

Constraint Modelling

Given a problem to answer, the objective of constraint modelling is to encode the problem to be solved into a constraint program such that a solution of the constraint program can be translated into a solution of the original problem. Definition 2.2.2 recalls the concept of CSP modelling. Constraint modelling is presented in Definition 2.2.3. In order to construct a constrain program P 0 modelling a constraint based problem P one must find a correspondence relation linking the valuations satisfying P 0 with the configurations belonging to P. Thus, if one is able to satisfy the CSP the correspondence relation ensures the existence of a configuration belonging to the constraint based problem. Furthermore, if the correspondence relation is decidable (ideally in polynomial time), one can construct at least one valid configuration from a solution given by the CSP. Definition 2.2.2 (Model). Let A be a set of objects, S be a set of object states, and P be a constraint based problem. We say that the CSP (X, D, C) models P iff there exists a correspondence relation R ✓ D X ⇥ S A s.t.

1. for each (v, v 0 ) 2 R, the valuation v satisfies C and the configuration v 0 belongs to P Modelling a constraint based problem as a constraint satisfaction program can be characterized in four steps. Definition 2.2.3 requires the existence of a correspondence relation. Thus, the programmer mainly builds the CSP while taking into account the correspondence between the original problem and the developed CSP. Firstly, the programmer identifies the decisions variables: i.e., the variables with a clear semantics in the problem to be solved. Secondly, she/he determines the auxiliary variables (i.e.,n o n decision variables used for intermediates constraints/computations). Thirdly, she/he sets the domain of each variable, also called the limits of each variable in the context of interval based domains. Fourthly, she/he adds the constraints that must be satisfied by the variables. These four steps are not necessarily straightforward and the programmer usually refines each step until a fix point is reached: the constructed CSP models the problem to solve. The following example proposes a modelling for the n-Queens problem. Note that this is a first modelling and that we are going to improve it in the following sections.

Example 4 (Example 1 continued). We propose a first CSP modelling M 0 for solving the n-Queens problem where the decision variables model the columns and the lines chosen for the queens. Formally, let L be the set of all the n-Queens problems with n 2 N. M 0 is the mapping associating to each n-Queens problem in L the CSP (X, D, C)s u c ht h a tX contains one variable c i and one variable `i per queen index i 2 {1,...,n}. These variables respectively indicate the column and the line position of the ith queen on the chessboard. Furthermore, the domain for all these variables is {1,...,n} and the constraints are the followings ones for each pair (i, j)oftwodifferent queen indexes: 1. queens i and j are not on the same line: `i 6 = `j; 2. queens i and j are not on the same column: c i 6 = c j ; 3. queens i and j are not on the same diagonal: |(`i -`j)/(c ic j )| 6 = 1. Note the abstraction difference between the modelling M 0 and the CSP produced by M 0 which models the n-Queens problem in L with n 2 N fixed. The CSPs produced by M 0 have a quadratic size in terms of n (cf. the 3 ⇥ n 2 constraints) and use non linear constraints over integer variables.

As in other programing paradigms (functional programming, object oriented programming, etc.) one problem can be written as many (syntactically) different constraint programs with equivalent semantics (i.e., they are all equivalently satisfiable or unsatisfiable or they all find the same optimal solution). We discuss this problematic in Section 2.3.2.

Modeller.

According to the type of variables (e.g., Boolean, integer, continuous variables) and the type of the constraints (e.g., linear, convex, non-linear, global constraints) one may look for the most appropriate research axes for modelling its problem. With an objective to share a common modelling language the mathematical programming community proposed A Mathematical Programming Language (AMPL for short) [START_REF] Fourer | Algorithms and Model Formulations in Mathematical Programming[END_REF] as an algebraic modelling language for describing CSPs. AMPL is supported by dozens of state-of-the-art tools for constraint program solving (e.g., CPLEX [11], Couenne [START_REF] Belotti | Mixed-integer nonlinear optimization[END_REF], Gecode [13], JaCoP [START_REF] Kuchcinski | JaCoP -Java Constraint Programming Solver[END_REF]). However, each research axe (each one specialized on dedicated families of CSPs) developed its proper modelling languages and tools. We present a landscape of CSPs families with their respective modelling languages and tools.

1. SAT (for Boolean Satisfiability Problem) contains CSPs with contraints over Boolean variables. The Conjunctive Normal Form (CNF for short) which consists of conjunctions of disjunctions of literals (e.g.,( x 1 _ ¬x 2 ) ^(x 2 _ x 3 )w h e r ex 1 , x 2 ,a n d x 3 are three Boolean variables) is the main practical modelling language used in this community. The DIMACS [15] format is the standard text format for CNF representation. See [START_REF] David | CNF Encodings[END_REF] for more details about CNF encodings.

2. LP, IP, MILP (respectively for Linear Programming, Integer Programming, and Mixed-Integer Linear Programming) contain constraint programs with respectively: linear constraints over continuous variables; linear constraints over integer variables; and linear constraints over continuous and integer variables. These three families are identified as mathematical programming languages. Formally the constraint programs of these families are presented in the following form: Ax  b where x is ac o l u m nv e c t o ro fv a r i a b l e sw i t hh e i g h tn,a n dA 2 R m,n and b 2 R m,1 are two matrices of coefficients. This encodes m inequalities over n variables. [START_REF] Aris | Mathematical modelling techniques[END_REF] recalls various modelling technics and use for these CSPs families.

3. FD (for Finite Domain Programming) contains constraint programs with constraints over variables with finite domains. There is no restriction on the constraints types. They can be linear, convex, non convex, non-linear such as trigonometric functions, exponential. There are also richer constraints expressed in the form of predicates, known as global (or meta) constraints which have been identified for their expressiveness (e.g., all-different, element, global-cardinality) and help the solution process (cf. Section 2.3.1). See the Global Constraint Catalogue for more details [START_REF] Beldiceanu | Global Constraint Catalog: Past, Present, and Future[END_REF]. Finally, there are two main formats for representing CSPs (XCSP3 [START_REF] Boussemart | XCSP3: An Integrated Format for Benchmarking Combinatorial Constrained Problems[END_REF]a n d FlatZinc [START_REF] Becket | Specification of FlatZinc[END_REF]) each one associated with a constraint modeller (resp. MCSP3 [START_REF] Lecoutre | MCSP3 : la modélisation pour tous[END_REF]and MiniZinc [START_REF] Nethercote | MiniZinc: Towards a Standard CP Modelling Language[END_REF]). While this CSP family allows any logical combination of constraints (negation, disjunction, implications, etc.) FD solvers are called propagation based solvers and are specialized for solving conjunction of constraints [START_REF] Rossi | Handbook of Constraint Programming[END_REF].

4. SMT (for Satisfiability Modulo Theory) allows any logical combinations of constraints over continuous and integer variables. The satisfiability stands for the logical combination of constraints while the theory stands for the semantics of the combined constraints. The logical combination of constraints can use any logical constraints (i.e., conjunction, disjunction, negation, implication, equivalence). Theories range from linear-constraints to non-linear constraints with integer, real-number, Boolean, or any combination of these types (even bit vectors and floating-point numbers).

The SMT-LIB format [START_REF] Barrett | The SMT-LIB Standard: Version 2.0[END_REF] is the standard format for representing CSP from this family. This norm also describes all the standard theories and their dependencies.

SMT is more general than SAT, IP, LP, MILP. See [START_REF] De | Satisfiability Modulo Theories: Introduction and Applications[END_REF] for an introduction to and applications of SMT.

Example 5 (n-Queens Problem Continued). We proposed in Example 4 the modelling M 0 for solving the n-Queens problem. This modelling can be transformed into a linear integer modelling M 1 producing CSPs from the IP family by replacing the non-linear constraints |(`i -`j)/(c ic j )| 6 = 1 by the constraints `i -`j 6 = c ic j and `i -`j 6 = c jc i . Furthermore, this modelling can be transformed into a FD modelling M 2 by replacing the 2 ⇥ n 2 constraints ensuring the "no threat" requirement by lines and columns with the only two following constraints: all-different(`1,...,`n)a n dall-different(c 1 ,...,c n ). Thus, M 2 models are smaller than those from M 0 and M 1 Consider the 5-Queens problem. M 0 , M 1 , and M 2 respectively produces 30, 40, and 22 constraints and have 10 variables. In addition to having less constraints, the models produced by M 2 use the all-different global constraint which ensures faster resolution than the use of a clique of binary inequality constraints.

Example 5 illustrates how our n-Queens problem can be supported by the IP and the FD families. Thus, a constraint based problem can be modelled as many constraint programs such that each one can be targeted to possibly different constraint satisfaction program families. In the next section we explain how the different CSPs families are solved.

Constraint Solving

In this section we give an overview of CSP solving. While we presented in the previous section various CSP families for modelling constraint based problem, we present in this section how these families are solved in practice.

Remark We present in this section some general methods for solving the CSPs families presented previously. However, before using the general solution one may also check if its problem does not belong to a subfamilies with practical/theoretical advantages.

For instance, SAT community uses the Post's lattice for differentiating clones of Boolean functions for whose the satisfaction problem is in P or in NP [START_REF] Harry | Satisfiability Problems for Propositional Calculi[END_REF]. In FD these complexity differentiation are dichotomy theorems, one famous is the Schaefer's dichotomy theorem [START_REF] Thomas | The Complexity of Satisfiability Problems[END_REF]. Finally, in the non-linear programming context, the quadratic convex programming is in lower complexity class than non-linear programming [START_REF] Kozlov | Polynomial Solvability of Convex Quadratic Programming[END_REF].

Satisfaction

In the general case, the combinatorics implied by the relations between the variables in the constraints makes a CSP hard to solve. In practice, complete solvers need to explore the search space (i.e., the set containing all the valuations). This is performed by branch and reduce algorithm where the search space is explored by developing a dynamic tree construction. Each node in the tree corresponds to a state in the exploration process (i.e., a succession of choices/decisions leading to a partial valuation of the variables and/or a reduction of the domains size and/or the adjunction of learned knowledges, etc.). Thus, ap a t hf r o mt h er o o tt oal e a fr e c u r s i v e l yc u tt h es e a r c hs p a c ei n t os m a l l e rs e a r c hs p a c e s until the satisfiability or the unsatisfiability is proven [START_REF] Land | An automatic method for solving discrete programming problems[END_REF][START_REF] Clausen | Branch and Bound Algorithms -Principles And Examples[END_REF]. The search starts from the root node which consists of the original CSP to solve (i.e.,a l lt h ev a l u a t i o n sa r e candidates possibly satisfying the CSP). Then, for each node in the tree exploration process the algorithm starts by reducing the current search space. This mainly consists in applying inferences rules such as resolution rules, computing consistency in order to reduce the search space while preserving all the valuations satisfying the CSP. Thanks to these reductions the next step checks if the reduced CSP is trivially satisfiable or unsatisfiable (e.g., the CSP has been syntactically reduced to a tautology, a contradiction, an empty set of constraints, etc.). If the CSP is trivially satisfiable, then a valid valuation can be found (mainly by reading the domains which has been reduced thanks to the successive cuts). containing the decisions history. If the CSP is trivially unsatisfiable, then this exploration path is closed and the exploration process carries on in an other opened exploration path. Otherwise, the current state space is split into possibly 2, 3, . . . , n smaller search spaces and the exploration process will be evaluated for each smaller CSP instances.

Algorithm 1 recalls this generic search strategy. The two main generic functions are reduce and splitSearchSpace which respectively reduces the search of the CSP while preserving all the valuations satisfying it (i.e., this function may only remove unsatisfying valuations), and split the current CSP in many k CSPs (with a possibly different k 2 N at every loop iteration) such that the union of their search spaces cover the whole search space of the split CSP (it is not required to perform a partitioning and sub-problems may share valuations). Also, we considered here a queue as a CSP buffer but a more sophisticated object may be used to select dynamically the next buffered CSP to the treated. The algorithm stops when it finds a valuation satisfying one sub-problem. We now discuss how this generic is implemented for treating CSPs from various famillies. queue.add(P)

6:

while not(queue.empty()) do # Reduces the CSP while preserving all solutions 9:

P 0 reduce(P 0 ) 10: 11:

# Case the CSP is trivially satisfiable after reduction: returns a sat valuation • In the SAT community the DPLL algorithm [START_REF] Davis | A Machine Program for Theorem-proving[END_REF] corresponds to the instantiation of splitSearchSpace by the selection of a non-instantiated variable x (i.e.,a variable x with domain {true, false})a n dt oth ec o n s tru c tio no ft w oC S P ss u c hth a t the first one contains the clause x and the second one contains the clause ¬x. Then, the reduce function performs unit propagation and pure literal elimination. The isTriviallySat function checks if constraints form a consistent set of literals and isTriviallyUnsat function checks the emptiness of the set of constraints.

• In the FD community, the constraint propagation with backtracking method consists in instantiating splitSearchSpace and reduce in the following way. In general, splitSearchSpace starts by selecting a non-instantiated variable x. Then, it constructs one CSP per value k in the domain of x such that each constructed CSP is derived from the current CSP by setting the domain of x to the singleton domain {k}. We call search strategy a heuristic returning for a given CSP the next variables and domain values to use in order to realize the split search. On the other hand, the reduce function performs propagations by calling filtering algorithms and computing consistencies (e.g., node consistency, arc consistency, path consistency). Informally, a filtering algorithm removes values that do not appear in any solution. Global constraints usually come with dedicated filtering algorithms empowering the propagation process. Finally, the isTriviallySat function checks if the instantiated variables satisfy all the constraints and the isTriviallyUnsat function checks if a constraint is violated or if a variable domain becomes empty. See [START_REF] Rossi | Handbook of Constraint Programming[END_REF] for more details.

• The branch-and-reduce framework used for solving non-linear programs with continuous variables, for instance HC4 [START_REF] Benhamou | Revising Hull and Box Consistency[END_REF], corresponds to instantiate in Algorithm 1 the function splitSearchSpace by the branching function (e.g., select a variable x with domains [a, b] ✓ R and a real number c 2 [a, b] in order to construct two CSPs which respectively contain the constraints x  c and x ≥ c), the reduce uses reducing consistencies in order to filter domain variables while preserving solutions. Finally, the isTriviallySat function guesses a valuation satisfying all the constraints for tight domains and the isTriviallyUnsat function checks if a constraint is violated or if a variable domain became empty.

• The SMT community gathers solving techniques from various CSP families. Indeed, a SMT instance is considered as the generalization of a Boolean SAT instance in which various sets of variables are replaced by predicates (e.g., linear or non-linear expressions for continuous variables, integer constraints). Thus, the splitSearchSpace enumerates solutions of the SAT instance abstracting the CSP to solve (i.e., each constraint which is not a Boolean function is replaced by a unique Boolean variable).

Then, each solution of the SAT instance is translated into a set of constraints which leads to a conjunction of constraints, each one being a sub-problem to be solved. According to the theory of this sub-problem (linear programming, integer programming, etc.) proper methods from the corresponding CSP family are used. This approach, which is referred to as the eager approach loses the high-level semantics encoded in the predicates. Actual SMT solvers now use a lazy approach solving partial SAT sub-problem and then answering their corresponding predicate parts while constructing a global solution [START_REF] Monniaux | A Survey of Satisfiability Modulo Theory[END_REF]. In SMT, we call strategy an implementation/construction of the splitSearchSpace and reduce functions.

Furthermore each community (i.e., SAT, FD, etc.) provides many tools which implement the generic Algorithm 1. The performance of these tools is mainly due to their implementation of the reduce and splitSearchSpace functions inherited from years of research next to the practical resolution of real world problems. This includes the study and the availability of wide variety of concrete heuristics [START_REF] David | Branch-and-bound algorithms: A survey of recent advances in searching, branching, and pruning[END_REF] and search strategies [START_REF] Peter Van Beek | Backtracking Search Algorithms[END_REF] eventually branched with an offline or online learning (e.g., no good, learned clauses). In this thesis we focus on constraint modelling of constraint based problems and on domain reducing functions called propagators implemented in the reduce function.

We presented independently how various CSPs families tackle the solving problem. However, some research has been realized in order to make them collaborate. For instance, the finite domains CSP family met continuous domains CSP family while preserving global constraints by linking CHOCO and IBEX solvers [START_REF] Fages | Combining finite and continuous solvers[END_REF]. Also, the integration of both IP and FD has been discussed helping to design a system such as SIMPL [START_REF] Tallys | An Integrated Solver for Optimization Problems[END_REF]. On the other hand, we already mentioned the fact that the SMT community uses solving techniques for clearly identified theories. In the same time, they started to include global constraints from FD and [START_REF] Bankovic | An Alldifferent Constraint Solver in SMT[END_REF] shows how the all-different constraint can be supported by SMT solvers which offers promising results. Finally, in [START_REF] Arbab | Coordination of Heterogeneous Distributed Cooperative Constraint Solving[END_REF] the authors develop cooperative constraint solver systems using a control-oriented coordination language. This work has been used for solving non-linear problems [START_REF] Monfroy | Implementing Non-linear Constraints with Cooperative Solvers[END_REF] and interval problems [START_REF] Granvilliers | Symbolic-interval Cooperation in Constraint Programming[END_REF] as well.

We presented here a generic complete algorithm answering the constraint satisfaction problem. Such complete method always returns a valuation satisfying the given CSP if it exists and returns none if such valuation does not exist. Thus, an incomplete algorithm may not be able to indicate if the CSP is unsatisfiable but may find a valuation satisfying the constraint program. We consider complete solvers in this thesis.

Improving Models

As said in the modelling section there is more than one CSP which encodes a given constraint based problem. Furthermore, the time required for solving these equivalent CSPs may differ from one to another with possibly an exponential gap. We present here various methods exploring how CSPs can be improved for reducing solving time: reformulation, symmetry-breaking, redundant constraints, relaxation, and over-constraint. In all cases these improvements can be performed by hand. However, solvers may implement them for automatic uses. There exists model transformations for transposing a CSP from a family to another one. Definition 2.3.1 recalls the concepts of reformulation, i.e., how to produce a new CSP from an existing CSP modelling the same contraint based problem. A low level constraint language such that the Conjunctive Normal Form (i.e., a Boolean functions expressed as conjunctions of disjunctions of literals) language used in the SAT community is now tractable with SAT state-of-the-art solvers for millions of variables and constraints [START_REF] Marijn | Solving and Verifying the Boolean Pythagorean Triples Problem via Cube-and-Conquer[END_REF]. In some cases reformulating a satisfaction problem into a lower constraint language may offer better resolution times. For instance in [START_REF] Lardeux | Expressively Modeling the Social Golfer Problem in SAT[END_REF], the authors reformulate their modelling from CP to SAT which highly increases the sizes of the CSP. But the first modelling is not solved by CP solvers while the second one is solved by SAT solvers.

Example 6 (n-Queens Refomulation). Consider the modelling M 2 presented in Example 5. Recall that the "no threat" rule for diagonals is managed by the constraints `i-`j 6 = c i -c j and `i -`j 6 = c jc i considered for each pair of two different queen indexes i and j. These constraints are equivalent to `ic i 6 = `jc j and `i + c i 6 = `j + c j . Since they must hold for each pair of two different queen indexes, all these constraints can be replaced by the two all-different global constraints. Since the all-different constraint support variables as inputs we create the auxiliary variables x i and y i for all i 2 {1,...,n} such that x i = `ic i and y i = `i + c i . Thus, the constraints expressing the "no threat" rule for diagonals can be replaced by the two constraints all-different(x 1 ,...,x n )a n d all-different(y 1 ,...,y n ). We call M 3 this modelling derived from M 2 . M 3 is called a reformulation of M 2 . M 3 models contain n +3 c o n s t r a i n t s w h e r e a s M 2 models contain a quadratic number of constraints in term of the number of queens n. Note that a reformulation may also change the variables and their domains and is not restricted to constraint modifications. Definition 2.3.2 (Symmetry). Le P be a constraint based problems over a set of objects A with states S. We say that P contains symmetries iff there exists a permutation σ of the set of configurations s.t. P is stable by σ.( i.e., σ(c) 2 L, for all c 2 L ✓ S A s.t.

L ⌘ P.)

A symmetry in a constraint based problem is a permutation of the configurations in the problem (cf. Definition 2.3.2). Thus, symmetry breaking consists in taking advantages of symmetry detection in constraint based problem to only model a subset of all the configurations in the problem, i.e., to only model the configurations which can not be obtained by symmetries. Symmetry breaking reduces the size of the search space and therefore, the time wasted in visiting valuations which are symmetric to the already visited valuations. The solution time of a combinatorial problem can be reduced by adding new constraints, referred as symmetry breaking constraints. We invite the reader to consider [START_REF] Cohen | Symmetry Definitions for Constraint Satisfaction Problems[END_REF] for more details.

Example 7 (n-Queens Symmetry Breaking). Consider the modelling M 3 presented in Example 6. Let n be a fixed number of queens and C be the CSP produced by M 3 for the n queens problem. Note that in C the n queens are unordered: i.e., all the queens are totally identical. Thus, for any valuation solution of C one may interchange the values (`i,c i )r e p r e s e n t i n gt h ep o s i t i o no ft h eith queen with the values (`j,c j )r e p r e s e n t i n g the position of the jth queen to obtain another valuation solution of C. We construct a new modelling, named M 4 , ordering the queens and realizing some symmetry breaking.

M 4 is such that for each n 2 N its corresponding CSP model (X, D, C) for solving the n-Queens problem contains the c i variables with domain {1,...,n} and no variable `i. Similarly to the previous modellings the c i variables represent the column position of the queens. However, in this modelling each c i with i 2 {1,...,n} is fixed with a line, the ith line. Thus, c i contains the column position of the queen on the ith line and there are no more `i variables in M 4 . The constraints x i = `ic i and y i = `i + c i from M 3 are respectively replaced by x i = ic i and y i = i + c i in M 4 for all i 2 {1,...,n}. To sum up, the constraints in C are the following ones: all-different(c 1 ,...,c n ), all-different(x 1 ,...,x n ), all-different(y 1 ,...,y n ), x i = ic i and y i = i + c i for all i 2 {1,...,n}. Note that this modelling still contains symmetries (e.g., chessboard rotations, chessboard plane symmetries). For instance setting the domain of the variable c 1 to {1,...,dn/2e} removes some chessboard plane symmetries.

Definition 2.3.3 (Redundancy). Let C be a CSP and c be a constraint over a set of variables X. We say that c is a redundant constraint for C iff adding the constraint c to the CSP C does not change the solution space of C.

In a general context minimizing the number of constraints (and/or the number of variables) in a CSP does not necessary implies lower solving time in practice. We call redundant constraint a constraint which does not change the set of valuations satisfying a given CSP when adding this constraint to the CSP (cf. Definition 2.3.3). In practice adding well chosen redundant constraints may speed up the solving process, or obtain as c a l eu p( s e e [START_REF] Asarin | Using Redundant Constraints for Refinement[END_REF] for instance). However, in the linear programming case detecting redundant constraints in order to remove them may accelerate the resolution process (see [START_REF] Paulraj | A comparative study of redundant constraints identification methods in linear programming problems[END_REF] for more details). Definition 2.3.4 (Relax & Over-constrain). Let P be constraint based problem over a set of objects A and a set of states S. Let C be a CSP. We say that C is:

• a relaxed modelling of problem P iff there exists a constraint based problem P 0 s.t. CSP C models problem P 0 and all the configurations in P belongs to P 0 ;

• an over-constrained modelling of problem P iff there exists a constraint problem P 0 s.t. CSP C models problem P 0 and all the configurations in P 0 belongs to P.

As last modelling strategies we present the relaxation and the over-constrain cases (cf. Definition 2.3.4). A relaxation is an over-approximation of a difficult problem by a nearby problem that is easier to solve. For instance a relaxation may transform integer variables into real variables (indeed this produces a greater solution space), or may only consider a convex hull of the problem by using only linear inequalities (e.g., [START_REF] Telgen | On relaxation methods for systems of linear inequalities[END_REF]). An over-constrain model is an under-approximation. This consists in modelling a constraint based problem contained by the original problem to solve. Thus, by reducing the size of the search space, one may hope a gain in term of resolution time (see [START_REF] Lardeux | Set constraint model and automated encoding into SAT: application to the social golfer problem[END_REF] for instance).

Real numbers vs. Floating-point numbers

As presented previously, one common variable domain for modelling is the real-numbers domain, written R. When using this domain one expects that the solver takes into account the classical arithmetic properties verified by R (e.g., associativity, commutativity, infinite limits, etc.). In practice, computer scientists use floating-point numbers for simulating real numbers. Floating-point numbers represent a finite numbers of real numbers with finite (binary) representation. The IEEE 754 norm [START_REF]IEEE Standard for Binary Floating-Point Arithmetic[END_REF] is now considered as the norm for representing floating-point numbers in programs. This norm encodes 2 32 finite real numbers where the smallest non-zero positive number that can be represented is 1⇥10 -101 and the largest is 9.999999 ⇥ 10 96 , the full range of numbers is -9.999999 ⇥ 10 96 through 9.999999 ⇥ 10 96 ; it contains two signed zeros +0 and -0, two infinities +1 and -1,a n d two kinds of N aN s. In the following we write F for the set of real-numbers representable in the IEEE 754 norm. 3 The first notable fact is that floating-point arithmetic (i.e., arithmetic over F)i sn o te q u i v a l e n tt or e a ln u m b e ra r i t h m e t i c( i.e., arithmetic over R). Precision limitation with floating point numbers implies rounding: a real-number x 2 R which is not in F is rounded to one of the neartest floating-point number. The IEEE 754 norm describes five rounding rules (two rules round to a nearest value while the others are called directed roundings and round to a nearest value in a direction such as 0, +1, -1). For instance: 0.1 10 (number 0.1r e p r e s e n t e di nb a s e1 0 )d o e sn o th a v eafi n i t e representation in base 2 and thus, it does not belong to F; there exists floating-point numbers x 2 F s.t. x +1=x in the floating-point arithmetic.

Implementing real number arithmetic in CSP solvers is challenging. Recall that we presented CSP valuation solutions as a mapping from the variables to their respective domains. Since some valuations to R may not be representable with floating-point numbers, solvers like RealPaver [START_REF] Granvilliers | Algorithm 852: RealPaver: an interval solver using constraint satisfaction techniques[END_REF] find reliable characterizations with boxes (Cartesian product of intervals) of sets implicitly defined by constraints such that intervals with floating point bounds contain real-number solutions. Thus, the real number valuation solutions are bounded by the interval valuation solutions. Since softwares take more and more control over complex systems with possibly critical impact on the society (e.g., car driving software, automatic action placements, ...) the verification community develops methods for ensuring the validity of such programs. After introducing in a first section the main objectives of program verification, we go deeper into the two verification fields concerned by our contributions. Our first contribution relates to Abstract Interpretation and the second one considers Model Checking for Markov chains. Finally, we present a brief overview concerning how constraint programming meets verification problems.

Warning. We choose the word "program" for system change descriptions while the verification community also uses the word "model" with the same signification. Recall that we already introduced the word "model" in the constraint programming background (cf. Section 2.2). Thus we reserve it for the constraint context. We focus in this thesis on program verification problems, i.e., we do not consider hardware verification problems. In this context, the word "program" refers to a computer science program written in a dedicated programming language [START_REF] Knuth | The Art of Computer Programming[END_REF]. There is a wide variety of programming languages which can be grouped by programming paradigms: functional programming (e.g., Javascript, Python), object oriented programming (e.g., C++, Java), reactive programming (e.g., FAUST, LUSTRE), probabilistic programming (e.g., ProbLog, RML), etc. Even if these languages may have different programming approaches they all share the same verification expectations. Indeed, whatever the language, a program is designed to be executed (in our concern we consider that programs are executed on a machine with memory). We briefly recall some vocabulary proper to program verification. We call run an execution of a program. During a run the machine memory varies over the time. We call state as n a p s h o to ft h em e m o r ya tag i v e nt i m e . Finally, a trace is the succession of states corresponding to a run of the program. Thus, program verification consists in analyzing traces in order to determine if a given property is satisfied. We name concrete semantics the set of all the traces of a given program. The variations for a single program between its traces may come from user inputs given at running time, non determinism of the program, probabilistic transitions in the program, etc.

Introduction

Example 8. Figure 3.1 describes a simple program using one variable x as memory.

Here, the concrete semantics of this program contains exactly four traces. Each trace is represented as a curve on the graphics such that each time step t corresponds to the value of x at this time.

Verification consists in verifying properties on the concrete semantics of programs. Recall first that these semantics are an "infinite" mathematical object (i.e.,a ni n fi n i t e set of potentially infinite sequences of states) which is not computable: it is not possible to write a program able to represent and to compute all the possible traces of any program. Otherwise, one may also solve the halting problem [START_REF] Turing | On Computable Numbers, with an Application to the Entscheidungsproblem[END_REF]. Thus, in the general case, questions about the concrete semantics of a program are undecidable. In practice the program traces may be finite. However note that in this thesis both contributions only consider infinite traces. Properties on such traces may be expressed using different formalisms. First, they can be time independent. In such case the property must hold during each execution time (e.g.,t h ev a r i a b l ex must never be equal to zero, the variable x must always take its values between -1a n d1 ) : s u c hp r o p e r t i e sa r ec a l l e di n v a r i a n t s . S e c o n d l y ,t i m e dependent properties express how the memory must vary over time for each trace (e.g., the variable x must not be equal to zero before a given line of the program, the variable x must be bounded by -1 and 1 at the end of the execution, using temporal modalities such as the linear temporal logic [START_REF] Pnueli | The Temporal Logic of Programs[END_REF]). Finally, a verification process has the objective to determine according to a given program and a property if this program satisfies this property. Recall that the program verification problem is undecidable in the general case (the halting problem can be turned into a verification problem). Thus, such verification process may validate, invalidate, or be non conclusive concerning the satisfaction of the property by the program.

We now present two main approaches, named static analysis and dynamic analysis, for tackling verification problems. Roughly speaking, the first one may be seen as offline verification and the second one as online verification. We call static analysis av erification process working without explicitly running the programs. On the other hand, a dynamic analysis verification process requires to run the program in order to validate or invalidate a property. Furthermore, both approaches also consider bounded verification vs. unbounded verification. Bounded verification only checks the validity of the properties for sub traces (i.e., for a bounded time range of execution of the program) while unbounded verification checks the validity of the properties for all traces regardless of their length. Recall that the total set of traces of a given program is called the concrete semantics of this program. Given a concrete semantics an abstraction is a mathematical model (possibly a program) representing at least all the traces in the concrete semantics. Thus, the verification process may be performed with an abstraction of the program instead of the original program itself. We say that a verification process is sound w.r.t. to a program abstraction iff it agrees with the verification of the concrete domain. Otherwise this process is called unsound. Example 10. Figure 3.3a contains a program described in pseudo code using two variables x and y.V a r i a b l e y is initialized to 1 and variable x is initialized to an integer randomly selected between 1 and 5. Then, the loop body is evaluated while the condition y<3 ^x<5i st r u e ,a n dfi n a l l y ,t h ev a r i a b l ex is incremented by 1. Clearly, this simple program admits 5 traces presented in Figure 3.3b. These different traces come from the random function on line 3 allowing 5 possible outputs. Note that traces may share states/state sequences (e.g., state (4, 2) is in traces trace 1 and trace 3 ), traces may have different lengths (e.g.,

|trace 1 | = |trace 2 | = |trace 3 | =6w h i l e|trace 4 | = 4
). Also the number of traces may be exponential or even infinite. Recall that computing this number is an undecidable problem in the general case.

As said previously, a verification process is performed on an abstraction of the concrete semantic. In order to bound all the variables at every program step, AI uses a connexion between the concrete semantics and the so called abstract semantics. Regarding a program concrete semantic and a variable in this program, we call concrete domain the values taken by the variables at each program step. On the other hand, for the same program and variable an abstract domain contains a super set of the the variable concrete domain at each program step (i.e., an abstract domain is an over-approximation of a concrete domain). While the concrete domain is unique there exist many possible abstract domains. Thus, AI proposes a variety of (mathematical) abstractions such that each one has advantage and disadvantage in term of precision, representativity, computability, etc. The problem of determining tight abstract domains becomes harder when the program contains loops. Indeed, this problem can be reduced to the search of inductive invariant (ideally the smallest). AI uses widening and narrowing operators in order to approach such solution. This is performed by considering an abstraction of the loop transfer function. Then, using this transfer function for testing over-approximation candidates and following successive widening and narrowing iterations terminates and converges to an inductive invariant. We invite the reader to consider [START_REF] Cousot | Static determination of dynamic prop erties of programs[END_REF][START_REF] Cousot | Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints[END_REF] for a formal and exhaustive presentation of AI since no more background is required for our contributions. describes the link between concrete and abstract semantics and presents the interest of tight abstract domains to possible false positive. This example presents the interval and the polyhedron abstractions. There exists other abstract domains such as the sign and the octogone abstract domains. Furthermore, a precision gain with an abstract domain increases the theoretical complexity for maintaining it while progressing in the verification process. However the use of abstractions may offer a guarantee of termination of the verification process. Indeed, well chosen abstractions produce semi-decidable problems. Thus verification tools based on abstract interpretation either proves the satisfaction of the bounding property or cannot conclude.

Example 11. Assume that a program using two variables x and y admits at a program step the concrete semantics presented in Figure 3.4a. Thus, each dot in the figure corresponds to a state encountered by one or more program traces at the given program step.

One possible abstraction for this concrete domain is the use of intervals to create a box (i.e., a cartesian product of intervals). Figure 3.4b presents the smallest interval domain containing the concrete semantics. On the other hand, Figure 3.4c presents the smallest polyhedron domain containing the concrete domain. According to this concrete domain and these abstract domains consider the unsafe region as the red region presented in Figure 3.4d. Since none of the states in the concrete domain overlap the unsafe region, the program satisfies the property. However, note that the interval domain intersects with the unsafe region in Figure 3.4e. Thus, this abstract domain is not able to prove the validity of the property on the concrete semantics. Conversely, the polyhedron abstract domain presented in Figure 3.4f successfully proves the validity of the property on the concrete semantics.

Model Checking

Model Also, in our setting Markov chains do not have final states. Thus, we consider that the accepted runs are all the infinite sequences of states with non zero transition probabilities. Indeed, each run is associated with a probability corresponding to the product of all the probabilities encountered on the transitions. Figure 3.5b present the prefixes with size 4 of five infinite runs with their corresponding probability. The probability for the runs not starting from the initial state or including a missing transition is set to zero.

As presented in section 3.1 we consider system/program verification based on trace properties. Model checking (also named property checking) consists in exhaustively and automatically checking whether the model of a system meets a given specification/property. In the context of finite-state machines, such properties are expressed in order to discriminate infinite runs (e.g., all the runs meeting state B before state C, all the runs reaching D before 5 transitions). Since the number of states is finite, and runs are infinite, the number of different runs is infinite but countable. The Linear Temporal Logic [START_REF] Pnueli | The Temporal Logic of Programs[END_REF] (LTL for short) uses temporal operators (e.g., next, until)a l l o w i n gt od e fi n es u c h sets of traces. Finally, qualitative verification and quantitative verification take into account a measure over the traces and consist in checking that the set of runs accepted by Example 13 (Example 12 continued). Consider the property asserting that the runs must encounter state D. This property does not hold for the Markov chain presented in Figure 3.5a. Indeed, there exist runs infinitely looping in state B or C which never encounter state D (more precisely there exists an infinite number of such runs). On the other hand, consider the property asserting that the probability of encountering state D equals 1: this property holds. Indeed, the probability of looping infinitely in state B or C equals to zero. Thus, all the runs with a non zero probability reach D and the probability of reaching D equals to 1.

Recall, that runs are infinite and the set of state is finite. Thus, model checking explores all possible system states in a brute-force manner. This way, it can be shown that a given system model formally satisfies or falsifies a certain property. Hence, such method proves the validity of the property or returns a counter-example otherwise.

Constraints meet Verification

Considerable improvements in the efficiency and expressive power of constraint program solvers allowed to tackle problems more and more difficult to answer. In this section, after motivating the use of constraint programming for answering the two mains program verification problems considered in this thesis we present various verification processes using constraint programming.

Even if a program admits a priori an infinite state space its executions may encounter a (potentially infinite) subset of the declared state space. Thus, one would like to determine this smaller state space in order to verify the non reachability of undesired states. This problem is reducible to the search of program over-approximations, i.e.,b o u n ding all the program variables. This is an objective of Abstract Interpretation where the program describing precisely the system evolution from a state to another, named the concrete program, is abstracted. This abstracted construction is related to the concrete program in such a manner that if an over-approximation holds for the abstraction then, this approximation also holds for the concrete program. Furthermore, constraint programs allow to describe over-approximations such as convex polyhedrons using linear constraints, ellipsoids using quadratic constraints, etc. Thus, since constraint programming is a generic declarative programing paradigm it may be seen as a verification process for over-approximating variable in declarative programs. In the first contribution, we consider a block-diagram language where executions are infinite streams and the objective is to bound the stream values using constraint programming.

However, bounding the state space is not enough for some verification requirements. In our second problem, the objective is to determine if a specific state is reachable at execution time. Indeed, abstractions can only determine if a specific state is unreachable. For this verification problem, we consider programs representable as finite graph structures where the nodes form the state space and the edges give state to state transitions. Thus, verifying the reachability of a state in such a structure is performed by activating or deactivating transitions in order to reach the target state. However, these activations can be restricted by guards, or other structural dependent rules. Clearly, this corresponds to a combinatoric problem to solve. For this reason, since one of the objectives of constraint programming is to solve highly combinatorial problems, the verification community is interested in the CP tools.

Dynamic Analysis. Software testing consists in checking the validity of a property on ag i v e np r o g r a mb yr u n n i n gs i m u l a t i o n s . T h ec l a s s i c a lboo kThe Art of Software Testing [START_REF] Glenford | The Art of Software Testing[END_REF] defines software testing as "the process of executing a program with the intent of finding errors" (i.e., finding runs which do not satisfy the specification). Thus, Constraint-Based Testing is the process of generating program test cases by using the constraint programming technology [START_REF] Demillo | Constraint-Based Automatic Test Data Generation[END_REF]. The test cases are not written by hand but constraint programming solvers are used to produce them. A recent survey for this research field can be found in [START_REF] Gotlieb | Constraint-Based Testing: An Emerging Trend in Software Testing[END_REF].

Static Analysis. Static program analysis is the automatic determination of runtime properties of programs. This consists in finding run-time errors at compilation time without code instrumentation or user interaction. K. R. Apt formalized the link between chaotic iterations such as used in abstract interpretation for moving between fixed points or inductive invariants and the resolution process used in contraint programming [START_REF] Krzysztof | From Chaotic Iteration to Constraint Propagation[END_REF][START_REF] Krzysztof | The Essence of Constraint Propagation[END_REF]. More recently, in [START_REF] Pelleau | A Constraint Solver Based on Abstract Domains[END_REF], the authors integrate abstract domains into a constraint programming solver by developing a tool named Absolute.

Bounded Model Checking. Binary Decision Diagrams (BDDs) have been used for formal verification of finite state systems with success since their introduction in the beginning of the 90's. However, in [START_REF] Biere | [END_REF] the authors proposed CNF modellings instead of BDD modellings for realizing Bounded Model Checking (BMC for short). This CNF based verification process takes advantages of the efficiency of the SAT solvers which are now considered as the state-of-the-art techniques for bounded model checking. This formulation in the BMC context led to a scale up in the size of the verified programs and also replaced the dedicated methods developed with BDDs.

CP solvers for testing applications More generally, constraint programming solvers have been used to test applications thanks to the expressiveness and the efficiency of constraint programming languages. For instance, [START_REF] Gerault | Constraint Programming Models for Chosen Key Differential Cryptanalysis[END_REF] uses constraint propagation to check a cryptanalysis problem: by providing a better solution, they proved that a solution claimed to be optimal in two cryptanalysis papers was not optimal.

Constraints in formal verification More and more the verification community uses

SMTst o o l si n s t e a do fd e d i c a t e da l g o r i t h m sf o rp e r f o r m i n gv e r i fi c a t i o np r o c e s s . I n d e e d , the actual best state-of-the-art SMT solvers are able to handle linear, non-linear, and even quantified constrained programs which may appear in program verification problems. For instance, see [START_REF] Bjørner | Program Verification as Satisfiability Modulo Theories[END_REF] for symbolic software model checking or the Extended Static Checker (ESC) tool using the Simplify SMT solver [START_REF] Detlefs | Simplify: A Theorem Prover for Program Checking[END_REF]. This concludes our overview of constraint programming and program verification. After having put in perspective both research fields we now propose two chapters, each one self contained, about solving some program verification problems using constraint modelling and solving.

Chapter 4

Verifying a Real-Time Language with Constraints

Contents

This chapter treats the verification of synchronous languages modelled as blockdiagrams. The verification problem consists in bounding all the variables in the program. This problem is called the stream over-approximation problem. We present a global constraint in the spirit of Constraint Programming designed to deal with this problem. We propose filtering algorithms inspired from abstract interpretation and prove their validity. These algorithms are inspired from both continuous constraint programming and abstract interpretation. Finally, we propose an implementation of our modellings and discuss the results. This chapter is self-contained including introduction, motivation, background, state of the art, and contributions.

Introduction

Constraint programing (CP) [START_REF] Montanari | Networks of Constraints: Fundamental Properties and Applications to Picture Processing[END_REF]o ffers a set of efficient methods for modelling and solving combinatorial problems. One of its key ingredients is the propagation mechanism, which reduces the search space by over-approximating the solution set. For continuous constraints [START_REF] Benhamou | Applying interval arithmetic to real, integer and Boolean constraints[END_REF][START_REF] Chabert | Contractor programming[END_REF], propagation is defined in a generic way on a given constraint language, usually containing equalities, inequalities, and many operators (arithmetic operations, mathematical functions, etc). In this chapter, we present a method using this generic propagation scheme, combined with a new solving algorithm, for the resolution of av e r i fi c a t i o np r o b l e m .

Our problem consists in checking the range of the outputs of programs written as block-diagrams, a common model for many real-time languages. More precisely, we are interested in DSP (Digital Signal Process) programs, based on a block-diagram algebra, which contains both typical real-time operations (split, merge, delay, ...) and mathematical functions [START_REF] Orlarey | An Algebra for Block Diagram Languages[END_REF]. All the variables are infinite streams over the reals. A stream represents the values taken by a variable at each time step. All the variables/streams are synchronized and they all receive a value at each tick of the clock. All the loops are thus, in theory, infinite by construction: the programs do never stop by themselves. Of course, they may stop computing in practice when all the signals are constant, or alternatively they can be killed by the user. The problem we tackle is the following: considering a block-diagram, which comes from a real-time program on streams, can we compute or approximate at a good precision the range of the stream output by this program? This problem is, in a more general form, at the core of another research area, Abstract Interpretation, as introduced in [START_REF] Cousot | Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints[END_REF][START_REF] Cousot | Static determination of dynamic prop erties of programs[END_REF]. Abstract Interpretation offers a great variety of tools to over-approximate traces of programs to prove the absence of some runtime errors, such as overflows. It relies on abstractions of the program traces, i.e. the possible values the variables may take during an execution. The set of all the possible program traces cannot be computed in the general case. In Abstract Interpretation, they are represented by an abstract element, easier to compute, which must both include all the program traces and be reasonably easy to compute. One of the first examples of such abstraction is the interval abstract domain [START_REF] Cousot | Static determination of dynamic prop erties of programs[END_REF], which is used in this work. An abstraction comes with several operators to mimic the program execution. Abstract Interpretation has been successfully applied to a wide range of applications the most famous one being the analysis of the flight-control commands of the Airbus A380 aircraft.

In this work, we use tools from constraint programming to compute precise abstractions of all the stream variables of a real-time program. Our method is generic and can be applied to any language based on a block-diagram algebra for bounding the values taken by the input, output, or inner streams of the program. We present three applications of our method: compiler assistance, refactoring, and verification. We chose the verification application for the experiment section that we applied on the FAUST (Functional Audio Stream)1 language. This language has been designed for sound design and analysis [START_REF] Orlarey | Syntactical and semantical aspects of Faust[END_REF] of audio streams. FAUST is a functional language with a proper semantic based on block-diagrams, which makes it a language quite similar to LUSTRE [START_REF] Halbwachs | The synchronous dataflow programming language Lustre[END_REF]o ri t s commercial version SCADE. In practice, the compiler automatically generates a blockdiagram for each program. The outputs of these block-diagrams are real-valued streams which represent audio signals. These signals can for instance be sent to loudspeakers or other applications.

By convention, digital audio signals must stay in the range [-1, 1]. In case the signal takes values out of this range, it can either damage the loudspeakers, or, more currently, be arbitrarily cut by the sound driver. In this case, the shape of the sound is modified and this produces a very audible sound effect called saturation. For this purpose, we compute bounds for the values taken by all the signals in the program and then we verify that the output streams stay in [-1 ; 1]. Verifying FAUST programs is essential since this language is intended for non computer scientists. An overflowing program not only produces a corrupted sound, but in practice, it often has conception mistakes. Moreover, FAUST programs are now used in concerts or commercial applications [START_REF][END_REF].

FAUST already embarks a static analyzer based on Abstract Interpretation, using the interval abstract domain. The analyzer computes the outputs of each operator from its inputs, with the bottom-up top-down (or HC4) algorithm. When the programs do not have loops or delays, this works very well. However, as soon as the programs have loops, the interval analysis cannot provide precise over-approximation (returning [-1, +1]) and the analysis fails.

In this chapter, we first propose a model of the verification of a block-diagram as a constraint problem. Propagation based on the constraints allows us to compute an over-approximation of the range of the computed streams. But as soon as the program has loops, the approximations are too large. We present a specific solving method which identifies the loops in the constraint graph, and propagates these constraints in a specific way to find over-approximation with a better precision. We implemented this method on FAUST block-diagrams, using IBEX [START_REF] Araya | Upper Bounding in Inner Regions for Global Optimization under Inequality Constraints[END_REF][START_REF] Chabert | Contractor programming[END_REF] a constraint programming solver over continuous domains. We tested it on several programs from the FAUST library. Most of the times, the over-approximation returned by our method is optimal, in the sense that it is the best interval approximation. We have tested our method on the programs given as examples in the standard FAUST library, with good results: we were able to detect errors in two of these programs, and in general to fastly compute precise intervals over-approximating the program outputs. This chapter is organized as follows: Section 4.2 introduces the notion of blockdiagrams. Section 4.3 presents the conversion of block-diagrams into a first constraint model. Section 4.4 defines the global constraint used for a more efficient model. Different applications of our optimized model are presented in Section 4.5 and we consider one of them in Section 4.6 with our application language and present the results of the experimentation followed by related works. Finally, Section 4.7 discusses the contribution and future works.

Related Works

The research on Constraint Programming and Verification has always been rich, and gained a great interest in the past decade. Constraint Programming has been applied to verification for test generation (see [START_REF] Gotlieb | Constraint-Based Testing: An Emerging Trend in Software Testing[END_REF] for an overview), constraintbased model-checking [START_REF] Podelski | Static Analysis: 7th International Symposium, SAS 2000[END_REF], control-flow graph analysis [START_REF] Lee | Compiler Construction: 16th International Conference[END_REF] or even worst-execution time estimations [START_REF] Bygde | An Efficient Algorithm for Parametric WCET Calculation[END_REF]. More recently, detailed approaches have been presented by [START_REF] Collavizza | Generating Test Cases Inside Suspicious Intervals for Floating-point Number Programs[END_REF]o r [START_REF] Ponsini | Verifying floating-point programs with constraint programming and abstract interpretation techniques[END_REF] to carefully analyze floating-points conditions with continuous constraint methods.

Other approaches mix CP and Abstract Interpretation. It has been known for a long time that both domains shared a lot of ideas, since for instance [START_REF] Krzysztof | The Essence of Constraint Propagation[END_REF] which expresses the constraint consistency as chaotic iterations. A key remark is the following: Abstract Interpretation is about over-approximating the traces of a program, and Constraint Programming uses propagation to over-approximate a solution set. It is worth mentioning that one of the over-approximation algorithms used in Abstract Interpretation, the bottom-up top-down algorithm for the interval abstraction [START_REF] Cousot | Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints[END_REF][START_REF] Cousot | Abstract Interpretation Frameworks[END_REF], is the same as the HC4 constraint propagator [START_REF] Benhamou | Applying interval arithmetic to real, integer and Boolean constraints[END_REF] (in the following, we will refer to this algorithm as HC4), which shows how close CP and Abstract Interpretation can sometimes be. More recent works explored these links in both ways, either to refine CP techniques [START_REF] Denmat | An abstract interpretation based combinator for modeling while loops in constraint programming[END_REF][START_REF] Pelleau | A Constraint Solver Based on Abstract Domains[END_REF] or to improve the Abstract Interpretation analysis [START_REF] Ponsini | Refining Abstract Interpretation-based Approximations with Constraint Solvers[END_REF][START_REF] Di | Worst-Case Scheduling of Software Tasks -A Constraint Optimization Model to Support Performance Testing[END_REF]. Finally GATeL [START_REF] Blanc | Handling State-Machines Specifications with GATeL[END_REF] uses Constraint Logic Programming for verifying real-time programs by test cases generation.

In some sense, our work can be seen as solving a constraint problem on streams. There have been other works on stream constraints in the literature (e.g., [START_REF] Jasperc | Towards Practical Infinite Stream Constraint Programming: Applications and Implementation[END_REF][START_REF] Lallouet | Constraint programming on infinite data streams[END_REF]). However, this approach radically differs from ours because their stream constraints are meant to build an automaton whose paths are solutions of the constraints. In particular, we would not be able to analyze infinite streams in a non-regular language with these b 1

op := x 2 b 2 op := - b 3 op := ⇥ Figure 4.1: A block-diagram in BD(R)
stream constraints. On the contrary, our constraints are expressed on infinite streams, and generated in order to compute hulls of the streams.

Background

This section introduces the block-diagram algebra for representing real-time programs.

Syntax

A block is a function that applies an operator on some ordered inputs, and generates one or more ordered outputs. For any block, we say that input i (respectively output j)e x i s t si ff i (resp. j)i sa n integer between 1 and the number of inputs (resp. outputs) of the block. Throughout this chapter, given a nonempty set E, Block(E)d e n o t e st h es e to fa l lt h eb l oc k so v e rE.

(b 1 [1], [1]b 2 )fromblockb 1 to block b 2 ;(b 1 [1], [1]b 3 )fromb 1 to b 3 and (b 2 [1], [2]b 3 ) from b 2 to b 3 . This block-diagram has two inputs (i.e.,[ 1 ] b 1 and [2]b 2 )a n do n eo u t p u t (i.e., b 3 [1]).

Semantics

After the syntax, it is natural to define the block-diagram semantics: block-diagram interpretation, and block-diagram model. An interpretation is any valuation of all the inputs and all the outputs. We introduce the notion of model to highlight the interpretations considering the operators (i.e., such that the outputs correspond to the image of the inputs by the operators) and the connectors.

Stream

Up to here, we built block-diagrams over arbitrary sets. Now, we consider the set of streams. A stream is an infinite discrete sequence of values possibly different at each time step. We abbreviate streams using bracket notation. For instance the stream s starting with the values 2, 4.5, and -3( i.e., s(0

) = 2, s(1) = 4.5, s(2) = -3) is abbreviated in [2, 4.5, -3,...].
In the following, it is important to remind that all the streams are infinite.

Considering block-diagrams over streams reveals two categories of blocks: functional blocks,a n dtemporal blocks. Functional blocks can be computed independently at each time step, whereas temporal blocks have time dependencies. Functional blocks are introduced in Definition 4.2.7. Temporal blocks are blocks which are not functional blocks (i.e., ab l o c ki se i t h e rf u n c t i o n a lo rt e m p o r a l ) . W ee x h i b i to n eb l o c ka m o n ga l lt h et e m p o r a l blocks: the fby block (cf. Definition 4.2.8). This block has two inputs and one output. The output at time zero is the value given by its first input at time zero. For the following times, the fby operator outputs its second input delayed by one time step.

BD(S(R)

). d has no input and no output. d contains 5 functional blocks: 0, 0.1, 0.9, +, and ⇥. Blocks 0, 0.1a n d0 .9u s ec o n s t a n to p e r a t o r s( i.e., 8t 2 N :0 .9(t)=0 .9). Blocks + (resp. ⇥)w i t hr e a l -n u m b e ri n p u ts t r e a m sa, b and real-number output stream c is such that c(t)=a(t)+b(t)( r e s p . c(t)=a(t) ⇥ b(t)). d contains one temporal block: the fby block (note that temporal blocks are hatched).

Block-diagrams over streams are used for programming real-time applications. In this context we name execution trace or simply trace amodelofabloc k-diagram. Acycleina 0.1 + 0.9 ⇥ fby 0 [0.9; 0.9; 0.9; 0.9] [0; 0; 0; 0] [0. block-diagram is equivalent to a loop in a classic programming language. In practice, in order to be runnable (i.e., to compute a trace in real-time) a block-diagram over streams needs to satisfy two properties [START_REF] Oppenheim | Signals & Systems[END_REF]: no value must be depending on future values (called the causality property); infinite computation in cycle must be avoided (any cycle must contain temporal blocks to avoid infinite computation at each time step).

In our contribution we only allow to use the fby block as temporal block. Under this condition, this implies that for any runnable block-diagram over streams each cycle contains at least one fby block. From now on, we only consider block-diagram verifying this statement. We will see in Section 4.6 that this restriction is not poor and that the fby block allows to represent many other temporal blocks.

Stream Over-Approximation Problem

Block-diagrams over streams can express the semantics of real-time programs. In such cases, the programmer could be interested in the verification of some properties of his/her program. These properties can concern outputs or internal streams (i.e.,o u t p u t so r local variables). We propose here a logical constraint model for the following problem: determine bounds of the streams of a block-diagram.

Temporal and Interval Abstractions

We illustrate the problematic on our running example. Figure 4.4 presents the first 21 values for the output streams of blocks ⇥, +, and fby model of our running example from Figure 4.3. For the first 21 time steps, one can see that the values are strictly increasing (i.e., streams are strictly increasing) between 0 and 1. Furthermore the same observation is still correct for the first 100, 1, 000, 1, 000, 000, and more, time steps (in our example, model streams are "infinitely" strictly increasing). Clearly, the greedy algorithm running the block-diagram time by time and gathering the accessible states (a state is a tuple composed of the values of all the streams at one time step) until convergence (i.e.,n o new state is reached) may not halt. Furthermore, a block-diagram can admit an infinite uncountable set of models/traces. Thus, there is no hope to run all these traces for gathering all the reachable states. In this context, Abstract Interpretation [START_REF] Cousot | Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints[END_REF][START_REF] Cousot | Static determination of dynamic prop erties of programs[END_REF]o ffers a great variety of tools for over-approximating traces of programs. It relies on abstractions of the program traces. The set of all the possible program traces is undecidable in the general case. In Abstract Interpretation, they are represented by an abstract element, easier to compute, which must both include all the program traces and be reasonably easy to compute. One of the first examples of such abstraction is the interval abstract domain [START_REF] Cousot | Static determination of dynamic prop erties of programs[END_REF]. While finding one over-approximation of the traces is easy (i.e., returning [-1, +1]) the objective is to find over-approximations with good quality (i.e., as small as possible intervals). Following paragraphs formally introduce the over-approximation problem with the over-approximation quality comparator. set may be infinite, discontinuous and even uncountable (i.e., a representation in extension is thus not possible). Thereby, given a stream we consider an interval superset of the temporal abstraction for representing this stream (i.e., this corresponds to the use of the interval abstract domain in Abstract Interpretation [START_REF] Cousot | Static determination of dynamic prop erties of programs[END_REF]). The best over-approximation (in the intervals) of a stream, is the smallest interval containing its temporal abstraction.

Definition 4.3.1 (Temporal Abstraction). The temporal abstraction of a stream s, written ṡ, is the set of all its values. Any superset of ṡ is called an over-approximation of s and ṡ is the smallest over-approximation of s.

ṡ = [ t2N s(t)
For each interval I, we write dIe its upper bound and bIc its lower bound. In the following, we assume that D is a totally ordered set and we write I(D)t h es e to fa l lt h e intervals over D. Furthermore, D is called the extended set of D and it is equal to the union of D and its limits (e.g., R = R [ {-1, +1} and I(R)ist h es e tc o n ta in in gallth e intervals with finite and infinite bounds). Finally, given A ✓ D we write [A] the smallest interval in I(D)c o n t a i n i n gA.

Model in Constraint Programming

Constraint programming (CP for short) is a declarative programming paradigm, in which a program consists of a list of variables (each one declared with a domain) together with a list of constraints over these variables. Firstly, we do constraint programming modelling with variables domains over streams. Secondly, we focus on interval constraint programming [START_REF] Benhamou | Continuous and Interval Constraints[END_REF], i.e., constraint programming with variable domains over set of intervals. is the set of all the domains associated to the variables in X; C is a set of constraints over variables from X. A constraint is defined over a set of variables x 1 ,...,x k from X with k 2 N and is a subset of

D x 1 ⇥ ...⇥ D x k . A valuation v of P is a map from X 0 ✓ X to D s.t. v(x) 2 D x for all x 2 X 0 . A valuation v satisfies a constraint c ✓ D x 1 ⇥ ...⇥ D x k iff (v(x 1 ),...,v(x k )) 2 c
. Finally, a valuation satisfies P iff it satisfies all the constraints in P. We recall that the over-approximation problem presented in the previous section asks for over-approximations of all the traces of the block-diagram. Since one solution of the naive model corresponds to one trace of the block-diagram, one must find all the solutions of the naive model to solve the over-approximation problem. In the previous section we motivated the use of over-approximations in the intervals for representing set of traces. We now present a second model with variables over intervals for solving the over-approximation problem.

This model, called medium model, is derived from the naive model. It consists in: 1) the same variables where domains are over intervals instead of streams (i.e., over I(D) instead of S(D)); 2) the same signatures of constraints where the operators over streams are replaced by their corresponding constraint for interval propagation. Interval propagation combines various technics from interval arithmetic, interval constraint propagation, domain filtering with partial consistency algorithms. Note that these extensions are not trivial and continue to motivate researchers (see [START_REF] Benhamou | Continuous and Interval Constraints[END_REF][START_REF] Lhomme | Consistency techniques for numeric csps[END_REF][START_REF] Collavizza | A Note on Partial Consistencies over Continuous Domains[END_REF]). In the following, we will particularly use interval arithmetic and interval (constraint) propagation.

Example 20 (Interval Arithmetic). Instances of interval computation

: [2, 6] + [-1, 3] = [1, 9] [2, 6] -[-1, 3] = [-1, 7] [2, 6] -[2, 6] = [-4, 4] [2, 6] ⇥ [-1, 3] = [-6, 18] [-1, 3] ⇥ [-1, 3] = [-3, 9]
[-1, 3] 2 =[ 0 , 9] Note that some properties in real-number arithmetic are not true in interval arithmetic. Examples above illustrate that in general A -A 6 =[0, 0] and A 2 6 = A ⇥ A.

[f ] from (I(D)) n to (I(D)) m such that [f ](X 1 ,...,X n )=Y 1 ,...,Y m where Y i = [{ ẏi | 9x j 2 X j ,y 1 ,...,y m = f (x 1 ,...,x n )}].
Interval arithmetic received big interest since Moore [START_REF] Edgar | Interval Analysis[END_REF] and the developments of interval analysis. We focus on interval arithmetic with interval extension of real-valued functions. Interval arithmetic concerns how classical functions from real-number arithmetic operates on intervals (see Example 20). We propose Definition 4.3.3 for transposing function over streams to interval functions which extends the definition from [START_REF] Edgar | Interval Analysis[END_REF] for extending real-number functions to interval functions. Table 4.1 presents standard arithmetic functions over real-numbers next to their corresponding stream functions and interval extension functions. When it is not ambiguous (i.e., in the context of intervals) we omit the brackets over the function names in order to keep the expressions simpler.

Real Function

Stream Function Interval Extension Function

a, b 7 ! a + b a, b 7 ! c, s.t. c(t)=a(t)+b(t), 8n 2 N [a 1 ,a 2 ], [b 1 ,b 2 ] 7 ! [a 1 + b 1 ,a 2 + b 2 ] a, b 7 ! a -b a, b 7 ! c, s.t. c(t)=a(t) -b(t), 8n 2 N [a 1 ,a 2 ], [b 1 ,b 2 ] 7 ! [a 1 -b 2 ,a 2 -b 1 ] a, b 7 ! a ⇥ b a, b 7 ! c, s.t. c(t)=a(t) ⇥ b(t), 8n 2 N [a 1 ,a 2 ], [b 1 ,b 2 ] 7 ! [c 1 ,c 2 ] s.t. c 1 = min(a 1 ⇥b 1 ,a 1 ⇥b 2 ,a 2 ⇥b 1 ,a 2 ⇥b 2 ) c 2 = max(a 1 ⇥b 1 ,a 1 ⇥b 2 ,a 2 ⇥b 1 ,a 2 ⇥b 2 ) a 7 ! a 2 a 7 ! c, s.t. c(t)=a(t) 2 , 8n 2 N [a, b] 7 ! [c, max(a 2 ,b 2 )] s.t. c =0,ifa  0  b c = min(a 2 ,b 2 ), otherwise
Table 4.1: Real-number functions, stream functions, and interval extension functions for the addition, the subtraction, the multiplication and the square functions

The interval extension function of an operator is not unique but the functions with smallest images will by preferred (i.e., the function always returning D is a universal interval extension function).

Constraint propagation is one of the key ingredient for CSP resolution [START_REF] Benhamou | Continuous and Interval Constraints[END_REF]. This consists in explicitly removing values in some variables domains which cannot satisfy the CSP, while preserving all the solutions. A function performing such operation over one constraint is called a propagator (cf. Definition 4. • for all x 2 X \ X 0 : In such cases interval propagation will contract the domains blocks after blocks (i.e., constraint after constraint). However, the convergence may appear after a huge number of interval propagations. In order to reach the gap to better over-approximation in less time we introduce a new constraint: the real-time-loop constraint.

D 00 x = D 0 x • for all x 2 X 0 : D 00 x ✓ D 0 x • for all valuations v of x 1 ,...,x n in D 0 x 1 ,...,D 0 xn : if v satisfies c, then v(x i ) 2 D 00 x i for all x i 2 X 0 .

Definition

The real-time-loop constraint will model cycles2 in block-diagrams. A cycle in a blockdiagram corresponds to a directed cycle in the directed graph representing it. A cycle is a sub block-diagram in a block-diagram. The real-time-loop constraint takes three arguments: the cycle itself as a block-diagram/list of constraints, the cycle inputs as a vector of variables and the cycle outputs as a vector of variables. Let d be a blockdiagram cycle, inputs be its inputs, and outputs be its outputs, we instantiate the real-time-loop constraint as: real-time-loop(d,inputs,outputs) . An interpretation satisfies a real-time-loop constraint if and only if it satisfies the list of constraints (i.e., all the constraints). According to this new constraint, we propose two propagators in the following sections. The first one propagates from input domains to output domains and the second one do the opposite way.

Optimized Model

This section describes how we exploit the structure of block-diagrams to improve the precision of the over-approximations using our real-time-loop constraint in an optimized model. Even if there is a thin syntactical difference between the medium model and this optimized model, there is a big gap in terms of deduction power. From a constraint programming point of view, these graphs are the constraints dependency graphs (where nodes are the CSP constraints), except that the arcs are directed by the dependencies implied by the blocks. Figure 4.8 draws the dependency graph of the block-diagram in Figure 4.5. Again, temporal block nodes are hatched. The optimized model is derived from the first one presented in section 4.3.2. Note that each strongly connected component (i.e., set of nodes such that it exists a path between any two nodes from this set) in the dependency graphs is related to a loop in the block-diagram. Thereby, regarding the dependency graph of the block-diagram, we compute its strongly connected components and we replace for each one all its corresponding constraints in the medium model by one real-time-loop constraint taking the strongly connected component as argument. Figure 4.9 models the block-diagram in Figure 4.5 using the real-time-loop constraint. Note that in this model the real-time-loop constraint has three variables as inputs and none as outputs.

Inputs to outputs propagator

We now present how to propagate the real-time-loop constraints from inputs to outputs: according to over-approximations of the inputs of the loop, we want to determine overapproximations for the outputs of the loop. Remember that the block-diagram is evaluated over infinite discrete time. Given a cycle/loop, we extract a transfer function for this loop and then, we consider the interval extension function of this transfer function in order to find over-approximations.

F (I(x 1 )(t),...,I(x k )(t)) = I(x 1 )(t +1),...,I(x k )(t +1)
Given a set of block inputs or outputs, a loop transfer function computes values at the next time according to values at a given time. Real-time languages must ensure the causality property [START_REF] Oppenheim | Signals & Systems[END_REF]( i.e., it must not exist a stream computing its values according to future values). Due to this property, it is clear that each cycle block-diagram admits at least one loop transfer function and even admits at least one loop transfer function with an argument of minimal size. This problem can be reduced to a "covering graph problem". Let d be a cycle block-diagram, G =(V, A)bethedependencygraphofd,and S ✓ V be a set of vertices. The set S 0 such that S 0 ◆ S, for all s 2 S 0 all its predecessors are in S 0 ,a n dS 0 is minimal, is named the cover of G by S. Furthermore, we say that S is a causal set of G if the cover of G by S equals to V . Thus, finding a loop transfer function with an argument of minimal size can be reduced to finding a minimal causal set and then performing a breadth-first search from this set for constructing the transfer function. We propose a greedy algorithm, Algorithm 2, for computing a minimal causal set of a dependency graph. It enumerates the subsets of V by starting from the subsets with minimal size and stops when it has found a causal set. In our benchmark presented in Table 4. 4, we can see that this greedy algorithm does not run out-of-time (i.e.,i n practice in our benchmark it does not enumerate all the subsets of V but only a small amount). Finally, we use the Definition 4.3.3 to get a loop transfer function extended to the intervals (in the following, we simply call it a loop transfer function too). Once we get this function, we want to over-approximate associated streams. Proposition 1 allows to do so by finding stable intervals such as defined in Definition 4.4.3. An example is given below.

Definition 4.4.3 (Interval Stability). Let D be a non-empty set, F be an interval function with arity n 2 N, and S 1 ,...,S n be n intervals from I(D). We say that S 1 ,...,S n is stable by # Look for the first subset of V which is a causal set 7:

F iff F (S 1 ,...,S n ) = S 0 1 ,...,S 0 n s.t. S 0 i ✓ S i for all 1  i  n.
for each A ✓ V enumerated by increasing size do . Let f and g be two functions from R to R such that f (y)=fby(0,y ⇥ 0.9+0.1) and g(y)=0 .9 ⇥ fby(0,y)+0.1f o ra l ly 2 R. Remind from Figure 4.5 that the symbol a stands for the fby block output and the ⇥ block first input. We have that f with argument {a} and g with argument {c} are two loop transfer functions for the cycle in our block-diagram running example. and that the symbol c stands for the + block output and the fby block second input. Thus, for any model I of the block-diagram and for all time step t in N, the value associated to a (resp. c)b yI at time t + 1 corresponds to the image by f (resp. g)o ft h ev a l u ea s s o c i a t e dt oa (resp. c) by I at time t (i.e.,i th o l d st h a tI(a)(t +1)=f (I(a)(t)) and

I(c)(t +1)=g(I(c)(t))).
Let F and G be two functions from

I(R)t oI(R)s u c ht h a tF (Y )=fby([0],Y ⇥ [0.9] + [0.1]) and G(Y )=[ 0 .9] ⇥ fby([0],Y)+[0.1] (
here in the context of intervals the function "⇥", "+", and "fby" are not the real valued functions but their respective interval extension functions). Function F extends f to the intervals and function G extends g to the intervals. We have that F with argument {a} and G with argument {c} are two loop transfer functions (extended to the intervals) for the cycle in our block-diagram running example.

Considering the loop transfer function F . Intervals [0; 1], [-1; 1] and [-4; 3] are stable by F . (the images are respectively [0; 1], [-0.8; 1] and [-3.5; 2.8]). Thus, by Proposition 1 all these intervals are valid over-approximations for stream c (i.e., the argument of F ). On the contrary intervals ; and [0, 0] are not stable (their images are respectively [0; 0] and [0; 0.1]). We conclude that ; and [0, 0] are not valid over-approximations for stream c.

One of our main contributions is Algorithm 3. We propose a method inspired by abstract interpretation techniques viewed as a constraint program to determine stable sets of intervals. Proposition 2 states the correctness of the algorithm. Note that this algorithm may not systematically return the minimal over-approximation, but in practice it gives acceptable ones (see experiments in Section 4.6). This algorithm starts by associating each argument element of the function to a search space bounded by the intervals min[i] and max[i] which are respectively initialized with the empty set and the extended set of the considered domain. Then, at each iteration current[i] is selected such that it contains min[i] and it is contained in max[i]( i.e., min[i] ✓ current[i] ✓ max[i]i sa n invariant of the loop). Also, the variable state takes its values between "Increasing" and "Decreasing" and is initialized to "Increasing". It switches from increasing to decreasing when the interval current[i] is stable by the transfer function and switches from decreasing to increasing when the contrary occurs. Finally, functions selectIntervalBetween and continueLooping are heuristics (resp. selection heuristic and looping heuristic). If S in I(D) k is stable by F then, S is an over-approximation of the elements in X.

Proposition 2. [Algorithm 3 Correctness] Let (u n ) n2N , (v n ) n2N
, and (w n ) n2N be the sequences of values taken respectively by the variables "min", "current", and "max" at each evaluation of the loop condition (line 8) during an execution of Algorithm 3 over a function F . The following statements hold: for each i from 1 to k do return max 38: end function Algorithm 3: Over-approximation random search function Proof for Statements 2 and 3 are obtained by induction on the number of evaluations of the loop condition. We first check the validity of both statements at the first evaluation of the loop condition (line 8). We have that u 0

1. (u n ) is increasing and (w n ) is decreasing 2. for all n 2 N: u n ✓ v n ✓ w n 3. for all n 2 N: w n is stable by F . Proof. Let (u n ) n2N ,(v n ) n2N ,
[i]=v 0 [i]=;,a n dw 0 [i]=D for all i 2 {1,...,k}. Clearly, u 0 [i] ✓ v 0 [i] ✓ w 0 [i] for all i 2 {1,...,k}. This implies that u 0 ✓ v 0 ✓ w 0 (Statement 2). Furthermore w 0 equals to D k makes F (w 0 ) [ w 0 = D k =
[i]=u n [i] ✓ v n+1 [i] ✓ v n [i]=w n+1 [i] (Statement 2). Moreover, the value v n set to w n+1 (cf. max[i] current[i],
for all i 2 {1,...,k}) verify F (v n ) [ v n = v n in the considered case. Thus w n+1 is stable by F (statement 3). Proofs for cases 2, 3, and 4a r es i m i l a r .

Proof for Statement 1. Let i be in {1,...,k}. Note that min[i]( i.e., u n [i]) is only updated at line 20 and that max[i](i.e., w n [i]) is only updated at line 22. Both are updated with the value of current[i]( i.e., v n [i]). Thus, we get that for all n 2 N:

u n+1 [i]=v n [i] or u n+1 [i]=u n [i]; and w n+1 [i]=v n [i]o rw n+1 [i]=w n [i]. We get by statement 2 that u n [i] ✓ u n+1 [i]a n dw n+1 [i] ✓ w n [i]
and this is correct for all i in {1,...,n}. We conclude that u n ✓ u n+1 and that w n+1 ✓ w n , i.e., u n is increasing and w n is decreasing.

Example 23 (Example 22 continued). Table 4.2 details a trace of Algorithm 3 for the transfer function F in Example 22. Each column corresponds to one iteration of the "while" loop. Each line gives the values of the variables at the end of each iteration, except for current which contains the value when starting the iteration.

Outputs to inputs propagator

For this section, outputs are given and we want to over-approximate with an interval (as small as possible) the set containing all the inputs that could generate those outputs. This is done by propagating all the constraints in the real-time-loop constraint until a fixpoint is reached. Indeed, since the outputs are fixed, propagating the constraints either reduce the input domains or do not change any domain. Since an input domain of a block can be an output domain of another block, we continue propagating the domains until no domain is modified. This procedure corresponds to the standard HC4 algorithm [START_REF] Benhamou | Applying interval arithmetic to real, integer and Boolean constraints[END_REF] from interval constraint programming.

Applications

We present three generic applications using our model for real-time programs that can be represented as Block-Diagrams.

Verification Program verification consists in checking properties of a given program written in a specific language. Block-Diagram programs are designed to run on a definite (possibly infinite) duration. Users may be interested in ensuring that no problem will occur during execution (especially if the software failure can impact damages). From a programmer point of view, one of the classic properties that can be checked is to ensure that some strategic or critical variables will stay into a specific interval. This problem is usually known as overflow checking. In our CP approach, fixing the input and then solving our model makes it possible to compute over-approximation for each stream/variable.

Refactoring Usually, a single semantics meaning can be implemented by many different syntactical writings. It is well known that the same result (even for a given algorithm) can be obtained by different implementations. Refactoring consists in restructuring an existing implementation without changing its external behavior. On Block-Diagrams, refactoring consists in removing or adding blocks or connections without changing the output values. For instance, an if-then-else condition which is always evaluated to "true" can be replaced by its "then" statement. This is a particular case of refactoring: removing dead code. In our CP approach, fixing inputs and outputs before solving enables removing blocks leading to empty over-approximations.

Compilation Assistant Block-Diagram is a high-level programming language designed to create Real-Time programs in an elegant and human readable way. As seen in the previous sections, such languages can manipulate delays. Note that these delays can be the result of a complex computation. This implies that the maximum delay may be unknown at compilation time. Thus it must be given at run time and at each-time step (i.e., the delay can change during execution). Hence, if the compiler is able to estimate the maximal delay, no value will be missing at execution time. With our CP model we can bound maximum delay for temporal blocks: such information can be given to the compiler in order to allocate appropriate arrays for saving delays.

Application to FAUST and Experiments

For the application section, we chose the Real-Time language FAUST and we focused on a verification problem. FAUST allows us to manipulate audio streams. To illustrate this section, we selected the volume-controller program (a real-world program) from the official set of examples as the running example. We first introduce the FAUST language, then the constraint programming model for verification problem, and finally we conclude with experiments over a set of real-world FAUST programs.

Model FAUST Programs

FAUST (Functional Audio Stream) has been designed for real-time signal processing and synthesis. Figure 4.10 presents the compilation scheme for creating FAUST applications. First, it needs a program, called the source program, written in the dedicated FAUST language (this language is not significant for our contribution and is similar to other languages designed for digital signal processing). See [START_REF] Orlarey | An Algebra for Block Diagram Languages[END_REF] for more details. Then, this source program must be compiled by the FAUST compiler. This produces a C++ program that can finally be compiled with a usual C++ compiler by targeting the desired device. This hatched process, allows a single FAUST program to run on phones, web browsers, concert devices, etc.

The goal of the FAUST compiler is to produce a C++ optimized code (i.e., a code with good performances and well managed memory in order to run efficiently in real-time, even on small devices). The actual FAUST compiler already contains various technics from the compilation research field for tackling this objective. As shown on Figure 4.10, it operates in four steps:

Block Semantics Constraint Model b = mem(a) ( b(0) = 0 b(t)= a(t -1), if t>0 b =[a S 0] c = delay(a, b) ( c(t)= 0 , i f t<b(t) c(t)= a(t -b(t)), otherwise c =[a S 0] c = prefix(a, b) ( c(0) = a(0) c(t)= b(t -1), if t>0 c =[a S b]
Table 4.3: FAUST temporal blocks

• it loads the source program in an internal representation, easy to manipulate (i.e., block-diagram)

• it rewrites this block-diagram to a normal form by syntactic analyzis (e.g., simplifying redundant forms such as xx by 0)

• it performs a static analysis in order to compute approximations of the semantics of the program (e.g., estimate the maximal size for a delay)

• and finally it produces the C++ program thanks to all the gathered information In our experiments, we use the model proposed in the previous sections to improve the static analysis inside the FAUST compiler. To do so, we will consider the blockdiagram just before the C++ code generation. Note that the normalization and the static analyzis made by the actual FAUST compiler helps working on expressions with few occurrences of the same variable: this is important for the constraint programming model since propagation over continuous variables performs poorly on variables occurring in many constraints [START_REF] Edgar | Interval Analysis[END_REF]( e.g., the stream "s 0 = ss"e q u a l st oz e r of o ra l lt i m ew h i l ei t s constraint model over intervals "S 0 = S -S"i sn o te q u i v a l e n tt o[ 0 ;0 ] ) .

The FAUST language for writing source code has a formally well defined semantics in the Block-Diagram language [START_REF] Orlarey | An Algebra for Block Diagram Languages[END_REF] and is expressive thanks to: three temporal blocks (prefix, mem,a n ddelay); common arithmetic functions (e.g., addition, subtraction, ...); many C++ imported functions (e.g., sin, cos, exp, ...); relational and conditional operators. 3 All these block operators admit an interval extension (as defined in Definition 4.3.3)w i t han a t u r a lt r a n s l a t i o nt oi n t e r v a lc o n s t r a i n t s . I np a r t i c u l a r ,T a b l e4.3 presents the semantics and the models of the temporal blocks.

Example 24. Figure 4.11 is our running example in FAUST (the FAUST Volume Controller Program) while Figure 4.5 is its equivalent representation in block-diagram (note that this block-diagram is not in normal form since the constant expression 1 -0.999 has not been reduced to 0.001). When running this program with FAUST, the graphical interface presents a slider (vslider in the FAUST source code stands for "vertical slider") allowing to control the output volume (left sliding reduces the volume and right sliding increases the volume).

CP problems are formatted in three parts. The first one contains the variable declaration: it introduces the variables with their corresponding type (e.g., integer, real-number). The second one precises a domain as an interval for each declared variable. The third one contains the constraints. Figure 4.13 depicts these parts for our running example using the Medium model presented in Section 4.3 and the optimized model presented in Section 4.4. We can read that: only Variables 10, 14, and 18 are over integers; Variables 8, 10, 12, 14, 16, 18 correspond to constants from the block-diagram; Variable 17 models the vslider with range/domain [-70; 4]; and Variable 2 stands for the input audio stream 4 . Note that the normalization performed by FAUST and used for our CP modelling replaced the constant expression "1 -0.999" by the constant 0.001 (cf. Variable 12 in Figure 4.13b); replaced the expression "vslider / 20" by the expression "vslider ⇥ 0.05" (cf. in Figure 4.13b the constraint [15] =mul [START_REF] David | CNF Encodings[END_REF][START_REF] Aris | Mathematical modelling techniques[END_REF]); and introduced identity operators (cf. identity constraints over the Variables 4 and 5 in Figure 4.13b). Even if the identity operators increase the size of the CP model, they will not affect the quality of the over-approximations (i.e., identity propagation can be done without loss of precision). We discuss about this point and possible improvements in Section 4.7. The block-diagram contains one loop, and thus, it is not surprising to find out the corresponding real-time-loop constraint in the CP model (see Figure 4.13d).

Verifying FAUST Programs

We described how to model FAUST programs in CP. We now discuss about the CP solver. The solver has been implemented using IBEX. It is able to deal with two types of variables: real-numbers (i.e., in practice approximated by floating-point numbers intervals) and integers (i.e., C++ int). Table 4.4 presents the results for our benchmark programs. It is composed of some pathological DSP programs, and of real world programs from the FAUST standard library. They have been selected for their interest since they are basics for many bigger FAUST compositions. From left to right, columns of the table represent: the name of the FAUST program; the number of constraints followed by the number of variables in the medium model; the number of constraints followed by the number of variables in the optimized model; the number of real-time-loop constraints with the maximum number of constraints and the maximum number of arguments for the transfer function; the average time for compiling a FAUST program into the medium model; the average time for compiling the medium model into the optimized model; the average time for solving the optimized model; the over-approximation returned by the solver for the output stream associated with an indicator of reachability of the smallest p "s t a n d sf o rverified over-approximation by human while "?" stands for unverified over-approximation mainly due to the program complexity in term of number of blocks/streams. In order to get readable outputs, intervals are given in decimal format with a fixed precision of 10 -2 .

Among those programs, counter is an incremental infinite loop starting at 0; noise generates a random noise (i.e., sequence of random numbers) ; oscillator generates an oscillating sound wave, freeverb generates a reverb on the input stream, firstorder-filter is well named and corresponds to a first-order filter. Note that benchmarks from counter to freeverb presented in Table 4.4 are fundamental block-diagrams for building more complex programs by composition. As instances of aggregation, we propose af a m i l yo f6be n c h m a r k sf o ra d d i t i v es y n t h e s i s [START_REF] Smith | Spectral Audio Signal Processing[END_REF] concataning from 5 to 1, 000 of these fundamental block-diagrams (cf. add-synth-X-oscs benchmarks in Table 4.4). The whole benchmark description, with the detailed information (DSP, block-diagram, and models) for each program, can be found at http://anicet.bart.free.fr/benchmarks/ FAUST.

Each call to the real-time-loop constraint propagator runs five times Algorithm 3 and returns the intersection of the computed over-approximations. Each call to Algorithm 3 is limited to 500 loop iterations/transfer function evaluations. The selection heuristic in Algorithm 3 does intelligent search by selecting a new bound for the moving/changing bound (e.g., if the application of the transfer function does not change the lower bound of an interval, it will only select a new upper bound for the next evaluation). The selected precision for interval is 10 -5 . The solver has been launched 10 times for each benchmark and the averages of computation times and solutions on the 10 runs are presented in Table 4. 4. Experimentation has been done on a 2.4 GHz Intel Core i5 processor with a memory limit set to 16 Go.

Results and Discussion

Results in Table 4.4 can be partitioned into three sets.

• counter, paper-example, sinus, noise, allpass-filter, volume, combfilter, echo, stereo-echo, oscillator add-synth-X-oscs are benchmark programs for which the returned solution is the smallest overapproximation of the output stream, i.e., the smallest interval containing all the possible values at any runtime execution. It is well known in abstract interpretation that first order filters, cannot generally be over-approximated efficiently using intervals. However, the first-order-filter benchmark is a special case (nevertheless a standard in FAUST) for which the floating-point interval abstraction is contracting.

• pink-noise, capture, karplus-strong, band-filter are benchmark programs for which the returned solution is the smallest over-approximation of the output stream using interval analyses. Indeed, the analysis/propagation is made block by block/constraint by constraint and some patterns cannot give small overapproximation without knowing local semantics such as e.g., xfloor(x)c o r r esponds to the decimal part of x.

• for the other programs (see lines in Table 4.4 containing the "?" symbol), the returned solution may not be the smallest over-approximation of the output stream but we were not able to prove it by hand.

In order to be included into the FAUST compiler, the verification must be executed in averyshorttime(moreorlessasecond). F orourexperiments,thesolverperformswellon that matter: even in rather complex programs (such as freeverb or harpe)itisableto answer quickly. For most of the programs, the longest task is to compile the medium model into the optimized model. This is due to the use of an external library to represent graph data structures and compute strongly connected components. However it seems to have good scalability: Table 4.4 shows that even when the size of the benchmark program is multiplied by more than 20, the execution time is only multiplied by 2. Finally, according to the over-approximations computed with our method, a FAUST user expert confirmed the existence of saturation in 3 programs: volume, pitch-shifter, and mixer. The saturation came from the fundamental volume FAUST program, which contained an incorrectly set constant (i.e., a vslider ranging from [-70; 4] instead of [-70 ; 2]). Due to the execution time of our method and the quality of the returned solutions, the FAUST developers shown a big interest for integrating our contribution in a future version of the official FAUST compiler. Nevertheless, note that our add-synth-X-oscs benchmarks ranging from 5 to 1,000 oscillators illustrates an exponentiel tendance in compiling and solving time, compared to the block-diagram size.

Related works

The research on Constraint Programming and Verification has always been rich, and gained a great interest in the past decade. Constraint Programming has been applied to verification for test generation (see [START_REF] Gotlieb | Constraint-Based Testing: An Emerging Trend in Software Testing[END_REF] for an overview), constraint-based model-checking ( [START_REF] Podelski | Static Analysis: 7th International Symposium, SAS 2000[END_REF]), control-flow graph analysis [START_REF] Lee | Compiler Construction: 16th International Conference[END_REF], or even worst-execution time estimations ( [START_REF] Bygde | An Efficient Algorithm for Parametric WCET Calculation[END_REF]). More recently, detailed approaches have been presented by [START_REF] Collavizza | Generating Test Cases Inside Suspicious Intervals for Floating-point Number Programs[END_REF]or [START_REF] Ponsini | Verifying floating-point programs with constraint programming and abstract interpretation techniques[END_REF] to carefully analyze floating-points conditions with continuous constraint methods.

Our contribution mixes CP and Abstract Interpretation. It has been known for a long time that both domains shared a lot of ideas, since for instance [START_REF] Krzysztof | The Essence of Constraint Propagation[END_REF] which expresses the constraint consistency as chaotic iterations. A key remark is the following: Abstract Interpretation is about over-approximating the traces of a program, and Constraint Programming uses propagation to over-approximate a solution set. It is worth mentioning that one of the over-approximation algorithms used in Abstract Interpretation, the bottom-up top-down algorithm for the interval abstraction [START_REF] Cousot | Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints[END_REF][START_REF] Cousot | Abstract Interpretation Frameworks[END_REF], is the same as the HC4 constraint propagator [START_REF] Benhamou | Applying interval arithmetic to real, integer and Boolean constraints[END_REF]. Recent works explored this links in both ways, either to refine CP techniques [START_REF] Pelleau | A Constraint Solver Based on Abstract Domains[END_REF], or to improve the Abstract Interpretation analysis [START_REF] Di | Worst-Case Scheduling of Software Tasks -A Constraint Optimization Model to Support Performance Testing[END_REF].

As a close work in the Constraint Programming community, GATeL [START_REF] Blanc | Handling State-Machines Specifications with GATeL[END_REF] is a software based on logical constraint programming verifying real-time programs. This tool first translates a Lustre program (representable as a block-diagram) and the specification of its environment in an equivalent Prolog representation, i.e., in a Constraint Logic Program (CLP). Then, it adds the user defined test objective in the CLP and solves it, computing at e s ti n p u ts a t i s f y i n gt h eo b j e c t i v ef o rt h eg i v e nL u s t r ep r o g r a m . T h i sw o r ka l r e a d y gathers the CP and the verification of real-time programs communities. However, while Gatel performs test cases generation for real-time programs we are interesting in finding precise over-approximations.

As a close work in the Abstract Interpretation community, ReaVer5 is a state-of-theart software for safety verification of data-flow languages, like Lustre, Lucid Synchrone or Zelus (all are close to FAUST), providing time-unbounded analysis based on abstract interpretation techniques. It features partitioning techniques and several analysis methods [START_REF] Schrammel | Logico-Numerical Verification Methods for Discrete and Hybrid Systems[END_REF] (e.g., Kleene iteration based methods with increasing and descending iterations, abstract acceleration, max-strategy iteration, and relational abstractions; logico-numerical product and power domains with convex polyhedra, octagons, intervals, and template polyhedra). Considering our problem of over-approximating stream in block-diagrams, while a solver like ReaVer embarks many technics from Abstract Interpretation to answer this problem, in our approach we focus on how a slightly modified Constraint Programming solver can be turned into a verification tool with good performances (i.e., in computation time and in over-approximations qualities). Experiments in the previous section show that our realtime-loop constraint together with the proposed propagators achieve these objectives. However, it is clear that this approach is not competitive when the interval abstract domain cannot tightly fit the concrete domain (i.e., in these cases, polyhedra, octagons, or an other domains may provide better over-approximations). In some cases the interval [-1, +1] is returned as over-approximation of the output streams, which is indeed the smallest over-approximation of the output streams in the interval abstract domain while [-1, 1] is a valid over-approximation of the concrete output stream.

Conclusion and Perspectives Conclusion

We proposed a constraint model using a global constraint for overapproximation of real-time streams represented with block-diagrams. The experiments show that our approach can reach very good, nearly always optimal, over-approximations in a short running time. Our method has been taken in consideration for a future implementation into the FAUST compiler.

In addition, we showed that constraint programming can handle block-diagram analyses in an elegant and natural way. The concept of digital signal processing is not proper to FAUST nor to audio processing. Indeed, it also appears in a lot of applications receiving and processing digital signals: modems, multimedia devices, GPS, video processing; which empower this model. Thus, this gives good perspectives for this work.

Perspectives The results of our experiments are fast and of good quality. However, we would like to point out some possible improvements. A common way to improve performances is to consider pre-processing. This consists in taking advantage of some knowledge about the semantics of the problem in order to find faster a solution. According to the application (e.g., verification, refactoring) it could be interesting to propagate variables with respect to a global order. For instance for verification, it will be faster to propagate from inputs to outputs instead of a totally arbitrary order. Algorithm 3 for stable interval search applies many times the transfer function of the loop. Thus, reducing the number of blocks per transfer function would have two impacts: decreasing the time needed by the solver, and decreasing the number of variable multiple occurrences. Factoring sets of blocks with specific semantics would lead to better models from which faster and better over-approximation would be computed. For example, removing identity constraints, factoring sub block-diagram with specific meaning such as filter would lead to better models. This chapter treats model checking of qualitative and quantitative properties over abstractions of Markov chains. In particular, we show in the qualitative context how constraint modellings produce better models in terms of size and resolution time. We also present a formal theorem allowing to produce a first practical approach for verifying some quantitative properties on the considered Markov chain abstractions. Finally, we propose an implementation of our modellings and discuss the results. This chapter is self-contained including introduction, motivation, background, state of the art, and contributions.

Introduction

Discrete time Markov chains (MCs for short) are a standard probabilistic modelling1 formalism that has been extensively used in the litterature to reason about software [START_REF] James | A Markov chain model for statistical software testing[END_REF] and real-life systems [START_REF] Husmeier | Probabilistic Modeling in Bioinformatics and Medical Informatics[END_REF]. However, when modelling real-life systems, the exact value of transition probabilities may not be known precisely. Several formalisms abstracting MCs have therefore been developed. Parametric Markov chains [START_REF] Alur | Parametric Real-time Reasoning[END_REF] (pMCs for short) extend MCs by allowing parameters to appear in transition probabilities. In this formalism, parameters are variables and transition probabilities may be expressed as polynomials over these variables. A given pMC therefore represents a potentially infinite set of MCs, obtained by replacing each parameter by a given value. pMCs are particularly useful to represent systems where dependencies between transition probabilities are required. Indeed, a given parameter may appear in several distinct transition probabilities, therefore requiring that the same value is given to all its occurences. Interval Markov chains [START_REF] Jonsson | Specification and Refinement of Probabilistic Processes[END_REF] (IMCs for short) extend MCs by allowing precise transition probabilities to be replaced by intervals, but cannot represent dependencies between distinct transitions. IMCs have mainly been studied with three distinct semantics interpretations. Under the once-andfor-all semantics, a given IMC represents a potentially infinite number of MCs where transition probabilities are chosen inside the specified intervals while keeping the same underlying graph structure. The interval-Markov-decision-process semantics (IMDP for short), such as presented in [START_REF] Chatterjee | Model-Checking omega-Regular Properties of Interval Markov Chains[END_REF][START_REF] Sen | Model-Checking Markov Chains in the Presence of Uncertainties[END_REF], does not require MCs to preserve the underlying graph structure of the original IMC but instead allows an "unfolding" of the original graph structure: new probability values inside the intervals can be chosen each time a state is visited. Finally, the at-every-step semantics, which was the original semantics given to IMCs in [START_REF] Jonsson | Specification and Refinement of Probabilistic Processes[END_REF], does not preserve the underlying graph structure too while allowing to "aggregate" and "split" states of the original IMC in the manner of probabilistic simulation.

Model-checking algorithms and tools have been developed in the context of pMCs [START_REF] Dehnert | PROPhESY: A PRObabilistic ParamEter SYnthesis To ol[END_REF][START_REF] Moritz Hahn | PARAM: A Model Checker for Parametric Markov Models[END_REF][START_REF] Kwiatkowska | PRISM 4.0: Verification of Probabilistic Real-Time Systems[END_REF] and IMCs with the once-and-for-all and the IMDP semantics [START_REF]Model Checking of Open Interval Markov Chains[END_REF][START_REF] Benedikt | LTL model checking of interval Markov chains[END_REF]. State of the art tools [START_REF] Dehnert | PROPhESY: A PRObabilistic ParamEter SYnthesis To ol[END_REF] for pMC verification compute a rational function on the parameters that characterizes the probability of satisfying a given property, and then use external tools such as SMT solving [START_REF] Dehnert | PROPhESY: A PRObabilistic ParamEter SYnthesis To ol[END_REF] for computing the satisfying parameter values. For these methods to be viable in practice, the allowed number of parameters is quite limited. On the other hand, the model-checking procedure for IMCs presented in [START_REF] Benedikt | LTL model checking of interval Markov chains[END_REF] is adapted from machine learning and builds successive refinements of the original IMCs that optimize the probability of satisfying the given property. This algorithm converges, but not necessarilly to a global optimum. It is worth noticing that existing model checking procedures for pMCs and IMCs strongly rely on their underlying graph structure (i.e., respect the onceand-for-all semantics). However, in [START_REF] Chatterjee | Model-Checking omega-Regular Properties of Interval Markov Chains[END_REF] the authors perform model checking of !-PCTL formulas on IMCs w.r.t. the IMDP semantics and they show that model checking of LTL formulas can b e solved for the IMDP semantics by reduction to the mo del checking problem of !-PCTL on IMCs with the IMDP semantics. For all that, to the best of our knowledge, no solutions for model-checking IMCs with the at-every-step semantics have been proposed yet.

In this thesis chapter, we focus on Parametric interval Markov chains [START_REF] Delahaye | Parameter Synthesis for Parametric Interval Markov Chains[END_REF] (pIMCs for short), that generalize both IMCs and pMCs by allowing parameters to appear in the endpoints of the intervals specifying transition probabilities, and we provide four main contributions.

First, we formally compare abstraction formalisms for MCs in terms of succinctness: we show in particular that pIMCs are strictly more succinct than both pMCs and IMCs when equipped with the right semantics. In other words, everything that can be expressed using pMCs or IMCs can also be expressed using pIMCs while the reverse does not hold.

Second, we prove that the once-and-for-all, the IMDP, and the at-every-step semantics are equivalent w.r.t. reachability properties, both in the IMC and in the pIMC settings. Notably, this result gives theoretical backing to the generalization of existing works on the verification of IMCs to the at-every-step semantics.

Third, we study the parametric verification of fundamental properties at the pIMC level: consistency, qualitative reachability, and quantitative reachability. Given the expressivity of the pIMC formalism, the risk of producing a pIMC specification that is incoherent and therefore does not model any concrete MC is high. We therefore propose constraint encodings for deciding whether a given pIMC is consistent and, if so, synthesizing parameter values ensuring consistency. We then extend these encodings to qualitative reachability, i.e., ensuring that given state labels are reachable in all (resp. none)o f the MCs modelled by a given pIMC. Finally, we focus on the quantitative reachability problem, i.e., synthesizing parameter values such that the probability of reaching given state labels satisfies fixed bounds in at least one (resp. all) MCs modelled by a given pIMC. While consistency and qualitative reachability for pIMCs have already been studied in [START_REF] Delahaye | Parameter Synthesis for Parametric Interval Markov Chains[END_REF], the constraint encodings we propose are significantly smaller (linear instead of exponential). To the best of our knowledge, our results provide the first solution to the quantitative reachability problem for pIMCs. Our last contribution is the implementation of all our verification algorithms in a prototype tool that generates the required constraint encodings and can be plugged to any SMT solver for their resolution.

Background

In this section we introduce notions and notations that will be used throughout this chapter. Given a finite set of variables X = {x 1 ,...,x k }, we write D x for the domain of the variable x 2 X and D X for the set of domains associated to the variables in

X.A valuation v over X is a set v = {(x, d)|x 2 X, d 2 D x } of elementary valuations (x, d)
where for each x 2 X there exists a unique pair of the form (x, d)i nv. When clear from the context, we write v(x)=d for the value given to variable x according to valuation v. A rational function f over X is a division of two (multivariate) polynomials g 1 and g 2 over X with rational coefficients, i.e., f = g 1 /g 2 .W ew r i t eQ for the set of rational numbers and Q X for the set of rational functions over X. The evaluation v(g)o fap o l y n o m i a lg under the valuation v replaces each variable x 2 X by its value v(x).

An atomic constraint over X is a Boolean expression of the form f (X) ./ g(X), with ./ 2 {, ≥,<,>,=} and f and g two functions over variables in X. An atomic constraint is linear if the functions f and g are linear. A constraint over X is a Boolean combination of atomic constraints over X.

Given a finite set of states S, we write Dist(S)f o rt h es e to fp r o b a b i l i t yd i s t r i b u t i o n s over S, i.e., the set of functions µ : S ! [0, 1] such that P s2S µ(s)=1. W ewriteI for the set containing all the interval subsets of [0, 1]. In the following, we consider a universal set of symbols A that we use for labelling the states of our structures. We call these symbols atomic propositions. We will use Latin alphabet in state context and Greek alphabet in atomic proposition context.

Constraints. Constraints are first order logic predicates used for modelling and solving combinatorial problems [START_REF] Rossi | Handbook of Constraint Programming (Foundations of Artificial Intelligence)[END_REF]. A problem is described with a list of variables, each in a given domain of possible values, together with a list of constraints over these variables. Such problems are then sent to solvers which decide whether the problem is satisfiable, i.e., if there exists a valuation of the variables satisfying all the constraints, and in this case compute a solution. Recall that checking satisfiability of constraint problems is difficult in general (cf. Chapter 2).

Formally, a Constraint Satisfaction Problem (CSP) is a tuple Ω =(X, D, C)w h e r eX is a finite set of variables, D = D X is the set of all the domains associated to the variables from X,a n dC is a set of constraints over X. We say that a valuation over X satisfies Ω if and only if it satisfies all the constraints in C. We write v(C)f orthes atisfac tionre sult of the valuation of the constraints C according to v (i.e., true or false). In the following we call CSP encoding as c h e m ef o rf o r m u l a t i n gag i v e np r o b l e mi n t oaC S P .T h es i z eo f a CSP corresponds to the number of variables and atomic constraints appearing in the problem. Note that, in constraint programming, having less variables or less constraints during the encoding does not necessarily imply faster solving time of the problems.

Discrete Time Markov Chains. A Discrete Time Markov Chain (DTMC or MC for short) is a tuple M =( S, s 0 , p, V ), where S is a finite set of states containing the initial state s 0 , V : S ! 2 A is a labelling function, and p : S ! Dist(S)i sap r o b a b i l i s t i c transition function. We write MC for the set containing all the discrete time Markov chains.

A Markov Chain can be represented as a directed graph where the nodes correspond to the states of the MC and the edges are labelled with the probabilities given by the transition function of the MC. In this representation, a missing transition between two states represents a transition probability of zero. As usual, given an MC M, we call a path of M asequenceofstatesobtainedfromexecutingM, i.e., a sequence ! = s 1 ,s 2 ,... such that the probability of taking the transition from s i to s i+1 is strictly positive, p(s i )(s i +1)> 0, for all i.Ap a t h! is finite iff it belongs to S ⇤ , i.e., it represents a finite sequence of transitions from M. Example 25. Figure 5.1 illustrates the Markov chain M 1 =( S, s 0 , p, V ) 2 MC where the set of states S is given by {s 0 ,s 1 ,s 2 ,s 3 ,s 4 }, the atomic proposition are restricted to {↵, β}, the initial state is s 0 , and the labelling function V corresponds to {(s 0 , ;), (s 1 , {↵}), (s 2 , {β}), (s 3 , {↵, β}), (s 4 , ↵)}. The sequences of states (s 0 ,s 1 ,s 2 ), (s 0 ,s 2 ), and (s 0 ,s 2 ,s 2 ,s 2 ), are three (finite) paths from the initial state s 0 to the state s 2 .

Reachability. A Markov chain M defines a unique probability measure P M over the paths from M. According to this measure, the probability of a finite path ! = s 0 ,s 1 ,...,s n in M is the product of the probabilities of the transitions executed along this path, i.e., P M (!)=p(s 0 )(s 1 ) • p(s 1 )(s 2 ) • ... • p(s n-1 )(s n ). This measure naturally extends to infinite paths (see [START_REF] Baier | Principles of Model Checking (Representation and Mind Series[END_REF]) and to sequences of states over S that are not paths of M by giving them a zero probability.

Given an MC M, the overall probability of reaching a given state s from the initial state s 0 is called the reachability probability and written P M s 0 (3s)o rP M (3s)w h e nc l e a r from the context. This probability is computed as the sum of the probabilities of all finite paths starting in the initial state and reaching this state for the first time. Formally, let reach s 0 (s)={! 2 S ⇤ | ! = s 0 ,...s n with s n = s and s i 6 = s 80  i<n } be the set of such paths. We then define P M (3s)= P ω2reachs 0 (s) P M (!)i fs 6 = s 0 and 1 otherwise. This notation naturally extends to the reachability probability of a state s from a state t that is not s 0 , written P M t (3s)a n dt ot h ep r o b a b i l i t yo fr e a c h i n gal a b e l↵ ✓ A written P M s 0 (3↵). In the following, we say that a state s (resp. a label ↵ ✓ A)i sr e a c h a b l ei nM iff the reachability probability of this state (resp. label) from the initial state is strictly positive. Example 26 (Example 25 continued). In Figure 5.1 the probability of the path (s 0 ,s 2 , s 1 ,s 1 ,s 3 )is0.3•0.5•0.5•0.5=0.0375 and the probability of reaching the state s 1 from s 0 is

P M 1 s 0 (3s 1 )=p(s 0 )(s 1 )+Σ +1 i=0 p(s 0 )(s 2 )•p(s 2 )(s 2 ) i •p(s 2 )(s 1 )=p(s 0 )(s 1 )+p(s 0 )(s 2 )•p(s 2 )(s 1 )• (1/(1 -p(s 2 )(s 2 ))) = 1.
Furthermore, the probability of reaching β corresponds to the probability of reaching the state s 2 , which is 0.3h e r e .

Markov Chain Abstractions

Modelling an application as a Markov Chain requires knowing the exact probability for each possible transition of the system. However, this can be difficult to compute or to measure in the case of a real-life application (e.g., because of precision errors or limited knowledge). In this section, we start with a generic definition of Markov chain abstraction models. Then we recall three abstraction models from the literature, respectively pMC, IMC, and pIMC, and finally we present a comparison of these existing models in terms of succinctness. A Markov chain Abstraction Model is a specification theory for MCs. It consists in as e to fa b s t r a c to b j e c t s ,c a l l e dspecifications, each of which representing a (potentially infinite) set of MCs -implementations -togetherwithasatisfactionrelationdefiningthe link between implementations and specifications. As an example, consider the powerset of MC (i.e., the set containing all the possible sets of Markov chains). Clearly, (2 MC , 2) is a Markov chain abstraction model, which we call the canonical abstraction model. This abstraction model has the advantage of representing all the possible sets of Markov chains but it also has the disadvantage that some Markov chain abstractions are only representable by an infinite extension representation. Indeed, recall that there exists subsets of [0, 1] ✓ R which cannot be represented in a finite space (e.g., the Cantor set [START_REF] Cantor | Uber unendliche, lineare Punktmannigfaltigkeiten V (On infinite, linear point-manifolds)[END_REF]). We now present existing MC abstraction models from the literature.

Existing MC Abstraction Models

Parametric Markov Chain is an MC abstraction model from [START_REF] Alur | Parametric Real-time Reasoning[END_REF] where a transition can be annotated by a rational function over parameters. We write pMC for the set containing all the parametric Markov chains. Definition 5.3.2 (Parametric Markov Chain). A Parametric Markov Chain ( pMC for short) is a tuple I =(S, s 0 ,P,V,Y) where S, s 0 , and V are defined as for MCs, Y is a set of variables (parameters), and P : S ⇥ S ! Q Y associates with each potential transition a parameterized probability.

Let M =(S, s 0 , p, V )beanMCandI =(S 0 ,s 0 0 ,P,V 0 ,Y)beapMC. Thesatisfaction relation |= p between MC and pMC is defined by M| = p I iff S = S 0 , s 0 = s 0 0 , V = V 0 ,a n d there exists a valuation v of Y such that p(s)(s 0 )e q u a l sv(P (s, s 0 )) for all s, s 0 in S.

Example 27. Figure 5.2 shows a pMC I 0 =( S, s 0 ,P,V,Y)w h e r eS, s 0 ,a n dV are identical to those of the MC M from Figure 5.1, the set Y contains only one variable p, and the parametric transitions in P are given by the edge labelling (e.g., P (s 0 ,s 1 )=0.7, P (s 1 ,s 3 )=p,a n dP (s 2 ,s 2 )=1-p). Note that the pMC I 0 is a specification containing the MC M from Figure 5.1.

Interval Markov Chains extend MCs by allowing to label transitions with intervals of possible probabilities instead of precise probabilities. We write IMC for the set containing all the interval Markov chains. Definition 5.3.3 (Interval Markov Chain [START_REF] Jonsson | Specification and Refinement of Probabilistic Processes[END_REF]). An Interval Markov Chain ( IMC for short) is a tuple I =( S, s 0 ,P,V), where S, s 0 , and V are defined as for MCs, and P : S ⇥ S ! I associates with each potential transition an interval of probabilities. Example 28. Figure 5.3 illustrates IMC I =(S, s 0 ,P,V)whereS, s 0 ,a n dV are similar to the MC given in Figure 5.1. By observing the edge labelling we see that P (s 0 ,s 1 )= [0, 1], P (s 1 ,s 1 )=[ 0 .5, 1], and P (s 3 ,s 3 )= [ 1 , 1]. On the other hand, the intervals of probability for missing transitions are reduced to [0, 0], e.g., P (s 0 ,s 0 )=[0, 0], P (s 0 ,s 3 )= [0, 0], P (s 1 ,s 4 )=[0, 0].

In the litterature, IMCs have been mainly used with three distinct semantics: atevery-step, interval-Markov-decision-process and once-and-for-all. All these semantics are associated with distinct satisfaction relations which we now introduce.

The once-and-for-all IMC semantics [START_REF] Dehnert | PROPhESY: A PRObabilistic ParamEter SYnthesis To ol[END_REF][START_REF] Wongpiromsarn | TuLiP: A Software Toolbox for Receding Horizon Temp oral Logic Planning[END_REF][START_REF] Puggelli | Polynomial-Time Verification of PCTL Properties of MDPs with Convex Uncertainties[END_REF] is alike to the semantics for pMC, as introduced above. The associated satisfaction relation |= o I is defined as follows: An MC M =(T,t 0 , p, V M )s a t i s fi e sa nI M CI =(S, s 0 ,P,V I )i ff (T,t 0 ,V M )=(S, s 0 ,V I )a n df o r all reachable state s and all state s 0 2 S, p(s)(s 0 ) 2 P (s, s 0 ). In this sense, we say that MC implementations using the once-and-for-all semantics need to have the same structure as the IMC specification.

Next, the interval-Markov-decision-process IMC semantics (IMDP for short) [START_REF] Chatterjee | Model-Checking omega-Regular Properties of Interval Markov Chains[END_REF][START_REF] Sen | Model-Checking Markov Chains in the Presence of Uncertainties[END_REF] operates as an "unfolding" of the original IMC by picking each time a state is visited a possibly new probability distribution which respects the intervals of probabilities. Thus, this semantics allows to produce MCs satisfying IMCs with a different structure. Formally, the associated satisfaction relation |= d I is defined as follows: An MC M =( T,t 0 , p, V M ) satisfies an IMC I =(S, s 0 ,P,V I )iff there exists a mapping ⇡ from T to S s.t. ⇡(t 0 )=s 0 , V I (⇡(t)) = V M (t)f o ra l ls t a t et 2 T , p(t)(t 0 ) 2 P (⇡(t), ⇡(t 0 )) for all pair of states t, t 0 in T , and for all state t 2 T and all state s 2 S there exists at most one state t 0 2 Succ(t) such that ⇡(t 0 )=s. Thus, we have that |= d I is more general than |= o I (i.e., whenever M| = o I I we also have M| = d I I). Note that in [START_REF] Chatterjee | Model-Checking omega-Regular Properties of Interval Markov Chains[END_REF][START_REF] Sen | Model-Checking Markov Chains in the Presence of Uncertainties[END_REF] the authors allows the Markov chains satisfying the IMCs w.r.t. |= d I to have an infinite state space. In this work we consider Markov chains with a finite state space.

Finally, the at-every-step IMC semantics, first introduced in [START_REF] Jonsson | Specification and Refinement of Probabilistic Processes[END_REF], operates as a simulation relation based on the transition probabilities and state labels, and therefore allows MC implementations to have a different structure than the IMC specification. Compared to the previous semantics, in addition to the unfoldings this one allows to "aggregate" and "split" states from the original IMC. Formally, the associated satisfaction relation |= a I is defined as follows: An MC M =( T,t 0 , p, V M )s a t i s fi e sa nI M CI =(S, s 0 ,P,V I ) iff there exists a relation R ✓ T ⇥ S such that (t 0 ,s) 2 R and whenever (t, s) 2 R,w e have 1. the labels of s and t correspond: V M (t)=V I (s), 2. there exists a correspondence function δ :

T ! (S ! [0, 1]) s.t. a) 8t 0 2 T if p(t)(t 0 ) > 0t h e nδ(t 0 )i sad i s t r i b u t i o no n S b) 8s 0 2 S :(Σ t 0 2T p(t)(t 0 ) • δ(t 0 )(s 0 )) 2 P (s, s 0 ), and c) 8(t 0 ,s 0 ) 2 T ⇥ S,i fδ(t 0 )(s 0 ) > 0, then (t 0 ,s 0 ) 2 R.
Example 29 illustrates the three IMC semantics and Proposition 3 compares them. We say that an IMC semantics |= 1 is more general than another IMC semantics |= 2 iff for all IMC I and for all MC M if M| = 2 I then M| = 1 I. Also, |= 1 is strictly more general than |= 2 iff |= 1 is more general than |= 2 and |= 2 is not more general than |= 1 . Note that two probability distributions have been chosen for the state s 1 from I. This produces two states t 1 and t 0 1 in M 2 and changes the structure of the graph. Thus, M 2 6 |= o I I and M 2 |= a I I. Finally, in the MC M 3 with state space T the state s 3 from I has been "split" into two states t 3 and t 3 0 and the state t 1 "aggregates" the states s 1 and s 4 from I. The relation R ✓ T ⇥ S containing the pairs (t 0 ,s 0 ), (t 1 ,s 1 ), (t 1 ,s 4 ), (t 2 ,s 2 ), (t 3 ,s 3 ), and (t 3 0 ,s 3 )i sas a t i s f a c t i o nr e l a t i o nbe t w e e nM 2 and I such as defined by |= a I . Thus, M 3 |= a I I. On the other hand, M 3 6 |= d I I since there exist probabilities on transitions that cannot belong to their respective interval of probabilities on the IMC (e.g., p(t 2 ,t 1 )=0.8 6 2 [0, 0.6] = P (s 2 ,s 1 )).

Proposition 3. The at-every-step satisfaction relation is (strictly) more general than the interval-markov-decision-process satisfaction relation which is (strictly) more general than the once-and-for-all satisfaction relation. I : ⇡(t 0 )=t 0 = s 0 , V 0 (s)=V (s)=V (⇡(s)) for all state s 2 S,a n dp(s)(s 0 ) 2 P (⇡(s), ⇡(s 0 )) since P (⇡(s), ⇡(s 0 )) = P (s, s 0 )a n dp(s)(s 0 ) 2 P (s, s 0 )f o ra l ls, s 0 2 S. Thus, M| = d I I. (2) If M| = d I I then there exists a mapping ⇡ from T to S s.t. ⇡(t 0 )=s 0 , V 0 (t)= V (⇡(t)) for all state t 2 T ,a n dp(t)(t 0 ) 2 P (⇡(t), ⇡(t 0 )) for all pair of states t, t 0 in T . The relation 3 . Consider the correspondence function δ from T to (S ! [0, 1]) such that δ(t 1 )(s 1 )=4 /5, δ(t 1 )(s 2 )=1 /5, δ(t 2 )(s 2 )=1,δ(t 0 )(s 0 )=1,andδ(t)(s)=0otherwise. Ontheotherhand,sincethe outgoing probabilities from state t 0 in M 0 3 do not belong to their respective interval on probabilities in I,w eh a v et h a tM 0 3 6 |= d I I.

s 0 ; s 1 α s 2 α [0, 0.4] [0.6, 1] [0, 1] [0, 1] [0, 1] [0, 1] IMC I t 0 ; t 1 α t 2 α 0.4 0.6 0.5 0.5 0.5 0.5 MC M 0 1 t 0 ; t 1 α t 2 α t 2 0 α 0.4 0.6 1 1 MC M 0 2 t 0 ;
R = {(t, ⇡(t)) | t 2 T } is such
Parametric Interval Markov Chains, as introduced in [START_REF] Delahaye | Parameter Synthesis for Parametric Interval Markov Chains[END_REF], abstract IMCs by allowing (combinations of) parameters to be used as interval endpoints in IMCs. Under a given parameter valuation the pIMC yields an IMC as introduced above. pIMCs therefore allow the representation, in a compact way and with a finite structure, of a potentially infinite number of IMCs. Note that one parameter can appear in several transitions at once, requiring the associated transition probabilities to depend on one another. Let Y be a finite set of parameters and v be a valuation over Y . By combining notations used for IMCs and pMCs the set I(Q Y )c o n t a i n sa l lp a r a m e t r i z e di n t e r v a l so v e r[ 0 , 1], and for all

s 0 s 1 α s 2 β s 3 α, β s 4 α [0, 1] [0, 1] [q, 1] [0.3,q] [0,p] [0.2,p] [0, 0.5] 1 [0, 0.5] [0.5, 1]
I =[ f 1 ,f 2 ] 2 I(Q Y ), v(I)d e n o t e st h ei n t e r v a l[ v(f 1 ),v(f 2 )] if 0  v(f 1 )  v(f 2 )  1
and the empty set otherwise2 . We write pIMC for the set containing all the parametric interval Markov chains. Definition 5.3.4 (Parametric Interval Markov Chain [START_REF] Delahaye | Parameter Synthesis for Parametric Interval Markov Chains[END_REF]). A Parametric Interval Markov Chain ( pIMC for short) is a tuple P =(S, s 0 ,P,V,Y), where S, s 0 , V and Y are defined as for pMCs, and P : S ⇥ S ! I(Q Y ) associates with each potential transition a (parametric) interval.

In [START_REF] Delahaye | Parameter Synthesis for Parametric Interval Markov Chains[END_REF] the authors introduced pIMCs where parametric interval endpoints are limited to linear combination of parameters. In our contribution we extend the pIMC model by allowing rational functions over parameters as endpoints of parametric intervals. Given ap I M CP =( S, s 0 ,P,V,Y)a n dav a l u a t i o nv, we write v(P)f o rt h eI M C( S, s 0 ,P v ,V) obtained by replacing the transition function P from P with the function P v : S ⇥ S ! I defined by P v (s, s 0 )=v(P (s, s 0 )) for all s, s 0 2 S. The IMC v(P)i sc a l l e da ninstance of pIMC P. Finally, depending on the semantics chosen for IMCs, three satisfaction relations can be defined between MCs and pIMCs. Finally, the parametric intervals from the transition function P are given by the edge labelling (e.g., P (s 1 ,s 3 )=[ 0 .3,q], P (s 2 ,s 4 )=[ 0 , 0.5], and P (s 3 ,s 3 )= [ 1 , 1]). Note that the IMC I from Figure 5 In the following, we consider that the size of a pMC, IMC, or pIMC corresponds to its number of states plus its number of transitions not reduced to 0, [0, 0] or ;. We will also often need to consider the predecessors (Pred), and the successors (Succ)o fs o m eg i v e n states. Given a pIMC with a set of states S, a state s in S, and a subset S 0 of S, we write:

• Pred(s)={s 0 2 S | P (s 0 ,s) / 2 {;, [0, 0]}} • Succ(s)={s 0 2 S | P (s, s 0 ) / 2 {;, [0, 0]}} • Pred(S 0 )= S s 0 2S 0 Pred(s 0 ) • Succ(S 0 )= S s 0 2S 0 Succ(s 0 )

Abstraction Model Comparisons

IMC, pMC, and pIMC are three Markov chain Abstraction Models. In order to compare their expressiveness and compactness, we introduce the comparison operators v and ⌘. Let (L 1 , |= 1 )and(L 2 , |= 2 ) be two Markov chain abstraction models containing respectively L 1 and L 2 . We say that L 1 is entailed by L 2 , written L 1 v L 2 ,i ff all the MCs satisfying L 1 satisfy L 2 modulo bisimilarity. (i.e., 8M|

= 1 L 1 , 9M 0 |= 2 L 2 s.t.
M is bisimilar to M 0 ). Definition 5.3.5 recalls the bisimilarity property from [START_REF] Baier | Principles of Model Checking (Representation and Mind Series[END_REF]. We say that L 1 is (semantically) equivalent to L 2 , written L 1 ⌘ L 2 ,i ff L 1 v L 2 and L 2 v L 1 . Definition 5.3.6 introduces succinctness based on the sizes of the abstractions.

Definition 5.3.5 (Bisimulation [START_REF] Baier | Principles of Model Checking (Representation and Mind Series[END_REF]). Let M =( S, S 0 , p, V ) be an MC possibly containing more than one initial state (i.e., S 0 ✓ S). A probabilistic bisimulation on M is an equivalence relation R on S such that for all states (s 1 ,s 2 ) 2 R: V (s 1 )=V (s 2 ) and σ t2T p(s 1 ,t)=σ t2T p(s 2 ,t) for all T 2 S/R. We say that two MCs M 1 and M 2 are bisimilar iff there exists a probabilistic bisimulation over their union containing the pair (s 0 ,s 0 0 ) where s 0 and s 0 0 ) are respectively the initial state of M 1 and M 2 .

Definition 5.3.6 (Succinctness). Let (L 1 , |= 1 ) and (L 2 , |= 2 ) be two Markov chain abstraction models. L 1 is at least as succinct as L 2 , written L 1  L 2 ,i ff there exists a polynomial p such that for every L 2 2 L 2 , there exists

L 1 2 L 1 s.t. L 1 ⌘ L 2 and |L 1 |  p(|L 2 |). 3 Thus, L 1 is strictly more succinct than L 2 , written L 1 < L 2 ,i ff L 1  L 2 and L 2 6  L 1 .
We start with a comparison of the succinctness of the pMC and IMC abstractions. Since pMCs allow the expression of dependencies between the probabilities assigned to distinct transitions while IMCs allow all transitions to be independant, it is clear that On the other hand, IMCs imply that transition probabilities need to satisfy linear inequalities in order to fit given intervals. However, these types of constraints are not allowed in pMCs. It is therefore easy to exhibit IMCs that, regardless of the semantics considered, do not have any equivalent pMC specification. As a consequence, pMC 6  (IMC, |= o I ), pMC 6  (IMC, |= d I ), and pMC 6  (IMC, |= a I ). We now compare pMCs and IMCs to pIMCs. Recall that the pIMC model is a Markov chain abstraction model allowing to declare parametric interval transitions, while the pMC model allows only parametric transitions (without intervals), and the IMC model allows interval transitions without parameters. Clearly, any pMC and any IMC can be translated into a pIMC with the right semantics (once-and-for-all for pMCs and the chosen IMC semantics for IMCs). This means that (pIMC, |= o pI )i sm o r es u c c i n c tt h a npMC and pIMC is more succinct than IMC for the three semantics. Furthermore, since pMC and IMC are not comparable due to the above results, we have that the pIMC abstraction model is strictly more succinct than the pMC abstraction model and than the IMC abstraction model with the right semantics. Clearly, any pMC and any IMC can be translated into a pIMC with the right semantics (once-and-for-all for pMCs and the chosen IMC semantics for IMCs). This means that (pIMC, |= o pI ) is more succinct than pMC and that pIMC is more succinct than IMC for the three semantics. Furthermore since pMC and IMC are not comparable (cf Lemma 1), we have that the pIMC abstraction model is strictly more succinct than the pMC abstraction model and than the IMC abstraction model with the right semantics.

s 1 α s 0 β [0, 1] [0, 1] 1 IMC I s 1 α s 0 β p 1-p 1 pMC P 1 s 1 α s 2 α s 0 β p 1 q 1 1-p 1 -q 1 p 2 1-p 2 1 pMC P 2 s 1 α s 2 α ... ... sn α s 0 β p 1 q 1 1-p 1 -q 1 p 2 q 2 1-p 2 -q 2 pn 1-pn 1 pMC P n
1 α 0 β 1-p p p 1-p pMC P 1 α 0 β [0, 1] [0, 1] [0, 1] [0, 1] IMC I 1 α 0 β 1/4 3/4 3/4 1/4 MC M 1 1 α 0 β 1/4 3/
Note that (pMC, |= p )  (IMC, |= o I )c o u l db ea c h i e v e db yc o n s i d e r i n gad o m a i nf o re a c h parameter of a pMC, which is not allowed here. However, this would not have any impact on our other results.

Qualitative Properties

As seen above, pIMCs are a succinct abstraction formalism for MCs. The aim of this section is to investigate qualitative properties for pIMCs, i.e., properties that can be evaluated at the specification (pIMC) level, but that entail properties on its MC implementations. pIMC specifications are very expressive as they allow the abstraction of transition probabilities using both intervals and parameters. Unfortunately, as it is the case for IMCs, this allows the expression of incorrect specifications. In the IMC setting, this is the case either when some intervals are ill-formed or when there is no probability distribution matching the interval constraints of the outgoing transitions of some reachable state. In this case, no MC implementation exists that satisfies the IMC specification. Deciding whether an implementation that satisfies a given specification exists is called the consistency problem. In the pIMC setting, the consistency problem is made more complex because of the parameters which can also induce inconsistencies in some cases. One could also be interested in verifying whether there exists an implementation that reaches some target states/labels, and if so, propose a parameter valuation ensuring this property. This problem is called the consistent reachability problem. Both the consistency and the consistent reachability problems have already been investigated in the IMC and pIMC setting [START_REF] Delahaye | Consistency for Parametric Interval Markov Chains[END_REF][START_REF] Delahaye | Parameter Synthesis for Parametric Interval Markov Chains[END_REF]. In this section, we briefly recall these problems and propose new solutions based on CSP encodings. Our encodings are linear in the size of the original pIMCs whereas the algorithms from [START_REF] Delahaye | Consistency for Parametric Interval Markov Chains[END_REF][START_REF] Delahaye | Parameter Synthesis for Parametric Interval Markov Chains[END_REF] are exponential.

Existential Consistency

A pIMC P is existential consistent iff there exists an MC M satisfying P (i.e., there exists an MC M satisfying an IMC I instance of P). As seen in Section 5. In [START_REF] Delahaye | Consistency for Parametric Interval Markov Chains[END_REF], the author firstly proved that |= a pI and |= o pI semantics are equivalent w.r.t. existential consistency, and proposed a CSP encoding for verifying this property which is exponential in the size of the pIMC. Now, by Proposition 3 we also get that the three s with domain [0, 1] per transition (s, s 0 )i n{{s} ⇥ Succ(s) | s 2 S}; and one Boolean variable ⇢ s per state s in S. These Boolean variables will indicate for each state whether it appears in the MC solution of the CSP (i.e., in the MC satisfying the pIMC P). For each state s 2 S, Constraints are as follows:

ρ 0 ρ 1 ρ 2 ρ 3 ρ 4 πp 2 [0, 1] πq 2 [0, 1] θ 1 0 θ 2 0 θ 1 1 θ 3 1 θ 1 2 θ 2
(

1) ⇢ s ,i f s = s 0 (2) ¬⇢ s , Σ s 0 2Pred(s)\{s} ✓ s s 0 =0, ifs 6 = s 0 (3) ¬⇢ s , Σ s 0 2Succ(s) ✓ s 0 s =0 (4) ⇢ s , Σ s 0 2Succ(s) ✓ s 0 s =1
(5) ⇢ s ) ✓ s 0 s 2 P (s, s 0 ), for all s 0 2 Succ(s)

Recall that given a pIMC P the objective of the CSP C 9c (P)istoconstructanMCM satisfying P. Constraint (1) states that the initial state s 0 appears in M. Constraint (2) ensures that for each non-initial state s,v a r i a b l e⇢ s is set to false iff s is not reachable from its predecessors. Constraint (4) ensures that if a state s appears in M, then its outgoing transitions form a probability distribution. On the contrary, Constraint (3) propagates non-appearing states (i.e., if a state s does not appear in M then all its outgoing transitions are set to zero). Finally, Constraint (5) states that, for all appearing states, the outgoing transition probabilities must be selected inside the specified intervals.

Example 31. Consider the pIMC P given in Figure 5.7. Figure 5.10 describes the variables in C 9c (P): one variable per transition (e.g., ✓ 1 0 , ✓ 2 0 , ✓ 1 1 ), one Boolean variable per state (e.g., ⇢ 0 , ⇢ 1 ), and one variable per parameter (⇡ p and ⇡ q ). The following constraints correspond to the Constraints (2), ( 3), (4),a n d(5) generated by our encoding C 9c for the state 2 of P:

¬⇢ 2 , ✓ 2 0 =0 ¬⇢ 2 , ✓ 1 2 + ✓ 2 2 + ✓ 4 2 =0 ⇢ 2 , ✓ 1 2 + ✓ 2 2 + ✓ 4 2 =1 ⇢ 2 ) 0  ✓ 1 2  ⇡ p ⇢ 2 ) 0.2  ✓ 2 2  ⇡ p ⇢ 2 ) 0  ✓ 4
2  0.5 Finally, Figure 5.11 describes a solution for the CSP C 9c (P). Note that given a solution of a pIMC encoded by C 9c , one can construct an MC satisfying the given pIMC w.r.t. |= o I by keeping all the states s such that ⇢ s is equal to true and considering the transition function given by the probabilities in the ✓ s 0 s variables. We now show that our encoding works as expected. Proposition 5. A pIMC P is existential consistent iff C 9c (P) is satisfiable.

Proof. Let P =(S, s 0 ,P,V,Y)beap I M C .

[)] The CSP C 9c (P)=(X, D, C)i ss a t i s fi a b l ei m p l i e st h a tt h e r ee x i s t sav a l u a t i o nv of the variables in X satisfying all the constraints in C. Consider the MC M =(S, s 0 , p, V ) such that p(s, s 0 )=v(✓ s 0 s ), for all ✓ s 0 s 2 Θ and p(s, s 0 )=0otherwise. Firstly, we show by induction that for any state s in S:" i fs is reachable in M then v(⇢ s ) equals to true". This is correct for the initial state s 0 thanks to the Constraint (1). Let s be a state in S and assume that the property is correct for all its predecessors. By the Constraints (2), v(⇢ s )e q u a l strue if there exists at least one predecessor s 00 6 = s reaching s with a non-zero probability (i.e., v(✓ s s 00 ) 6 =0 ) . T h i si so n l yp o s s i b l eb yt h e Constraint (4) if v(⇢ s 00 )e q u a l strue. Thus v(⇢ s )e q u a l strue if there exists one reachable state s 00 s.t. v(✓ s s 00 ) 6 =0. Secondly, we show that M satisfies the pIMC P w.r.t. |= o I . We use Theorem 4 from [START_REF] Delahaye | Parameter Synthesis for Parametric Interval Markov Chains[END_REF] stating that |= a pI and |= o pI are equivalent w.r.t. qualitative reachability. We proved above that for all reachable states s in M,w eh a v ev(⇢ s )e q u a l st otrue. By the Constraints (5) it implies that for all reachable states s in M: p(s)(s 0 ) 2 P (s, s 0 )f o ra l l s and s 0 .4

[(] The pIMC P is consistent implies by the Theorem 4 from [START_REF] Delahaye | Parameter Synthesis for Parametric Interval Markov Chains[END_REF] stating that |= a pI and |= o pI are equivalent w.r.t. qualitative reachability, that there exists an implementation of the form M =(S, s 0 , p, V )where,forallreachablestatess in M,itholdsthatp(s)(s 0 ) 2 P (s, s 0 )foralls 0 in S. Consider M 0 =(S, s 0 ,p 0 ,V)s.t. foreachnonreachablestates in S:

p 0 (s)(s 0 )=0,foralls 0 2 S. The valuation v is s.t. v(⇢ s )equalstrue iff s is reachable in M, v(✓ s 0 s )=p 0 (s)(s 0
), and for each parameter y 2 Y av alidv aluecanbeselectedaccordingto p and P when considering reachable states. Finally, by construction, v satisfies the CSP C 9c (P).

Our existential consistency encoding is linear in the size of the pIMC instead of exponential for the encoding from [START_REF] Delahaye | Parameter Synthesis for Parametric Interval Markov Chains[END_REF] which enumerates the powerset of the states in the pIMC resulting in deep nesting of conjunctions and disjunctions.

Qualitative Reachability

Let P =( S, s 0 ,P,V,Y)b eap I M Ca n d↵ ✓ A be a state label. We say that ↵ is existential reachable in P iff there exists an implementation M of P where ↵ is reachable (i.e., P M (3↵) > 0). In a dual way, we say that ↵ is universal reachable in P iff ↵ is reachable in any implementation M of P. As for existential consistency, we use a result from [START_REF] Delahaye | Consistency for Parametric Interval Markov Chains[END_REF] that states that the |= a I and the |= o I pIMC semantics are equivalent w.r.t. existential (and universal) reachability. As for the consistency problem, we get by Proposition 3 that the three IMC semantics are equivalent w.r.t. existential (and universal) reachability. Note first that in our C 9r encoding each ⇢ s variable indicates if the state s appears in the constructed Markov chain. However, the ⇢ s variable does not indicate if the state s is reachable from the initial state, but only if it is reachable from at least one other state (i.e., possibly different from s 0 ). Indeed, if the graph representation of the constructed Markov chain has strongly connected components (SCCs for short), then all the ⇢ s variables in one SCC may be set to true while this SCC may be unreachable from the initial state. This is not an issue in the case of the consistency problem. Indeed, if a Markov chain containing an unreachable SCC is proved consistent, then it is also consistent without this unreachable SCC. However, in the case of the reachability problem, these SCCs are an issue. The following encoding therefore takes into account these isolated SCCs such that ⇢ s variables are set to true if and only if they are all reachable from the initial state. This encoding will solve the qualitative reachability problems (i.e., checking qualitative reachability from the initial state). We propose a new CSP encoding, written C 9r , that extends C 9c , for verifying these properties. Formally, CSP C 9r (P)= (X [ X 0 ,D[ D 0 ,C[ C 0 )issuchthat(X, D, C)=C 9c (P), X 0 contains one integer variable ! s with domain [0, |S|] per state s in S, D 0 contains the domains of these variables, and C 0 is composed of the following constraints for each state s 2 S:

(6) ! s =1, ifs = s 0 (7) ! s 6 =1, ifs 6 = s 0 (8) ⇢ s , (! s 6 =0) (9) ! s > 1 ) W s 0 2Pred(s)\{s} (! s = ! s 0 +1)^(✓ s 0 s > 0), if s 6 = s 0 (10) ! s =0, V s 0 2Pred(s)\{s} (! s 0 =0)_ (✓ s 0 s =0), ifs 6 = s 0
Recall first that CSP C 9c (P )c o n s t r u c t saM a r k o vc h a i nM satisfying P w.r.t. |= o I . Informally, for each state s in M the Constraints (6), ( 7), ( 9) and (10) in C 9r ensure that ! s = k iff there exists in M ap a t hf r o mt h ei n i t i a ls t a t et os of length k -1w i t h non zero probability; and state s is not reachable in M from the initial state s 0 iff ! s equals to 0. Finally, Constraint (8) enforces the Boolean reachability indicator variable ⇢ s to bet set to true iff there exists a path with non zero probability in M from the initial state s 0 to s (i.e., ! s 6 =0).

Let S α be the set of states from P labeled with ↵. C 9r (P)thereforeproducesaMarkov chain satisfying P where reachable states s are such that ⇢ s = true. As a consequence, ↵ is existential reachable in P iff C 9r (P)a d m i t sas o l u t i o ns u c ht h a t W s2Sα ⇢ s ;a n d↵ is universal reachable in P iff C 9r (P)a d m i t sn os o l u t i o ns u c ht h a t V s2Sα ¬⇢ s . This is formalised in the following proposition. Proposition 6. Let P =( S, s 0 ,P,V,Y) be a pIMC, ↵ ✓ A be a state label, S α = {s | V (s)=↵}, and (X, D, C) be the CSP C 9r (P).

• CSP (X, D, C [ W s2Sα ⇢ s ) is satisfiable iff ↵ is existential reachable in P • CSP (X, D, C [ V s2Sα ¬⇢ s ) is unsatisfiable iff ↵ is universal reachable in P Proof. Let P =(S, s 0 ,P,V,Y)b eap I M C ,↵ ✓ A be a state label, S α = {s | V (s)=↵},
and (X, D, C)bet h eC S PC 9r (P). Recall first, that by Proposition 5 the constraints (1) to (5) in C 9r (P)a r es a t i s fi e di ff there exists an MC M satisfying P w.r.t.

|= a I . • [)] If CSP (X, D, C [ W s2Sα ⇢ s )
i ss a t i s fi a b l et h e nt h e r ee x i s t sav a l u a t i o nv solution of this CSP and a corresponding MC M satisfying P w.r.t. |= a I such as presented in the proof of Proposition 5. Furthermore, the constraints ( 6) to [START_REF] Fourer | Algorithms and Model Formulations in Mathematical Programming[END_REF] ensure by induction that for all state s 2 S: v(! s )=k with k ≥ 1i f there exists a path from the initial state s 0 to the state s of size k -1w i t h non zero probability in M,a n dv(! s )=0o t h e r w i s e . B yc o n s t r a i n t(8) we have that v(⇢ s )=true iff state s is reachable in M from the initial state s 0 . Finally, constraint W s2Sα ⇢ s ensures that at least one state labeled with ↵ must be reachable in M. Thus, ↵ is existential reachable in P.

[(] If ↵ is existential reachable in P, then by [START_REF] Delahaye | Parameter Synthesis for Parametric Interval Markov Chains[END_REF] there exists an MC M satisfying P w.r.t. |= o I s.t. ↵ is reachable in M. By construction of our encoding, one can easily construct from M av a l u a t i o nv satisfying all the constraints in C [ W s2Sα ⇢ s s.t. v(! s ) contains the size (plus one) of an existing path in M from the initial state to the state s with a non zero probability, and v(! s )=0 if s is not reachable in M.

• Note that ↵ is universal reachable in P iff there is no MC M satisfying P w.r.t. |= a I s.t. none of the states labelled with ↵ is reachable in M. "CSP (X, D, C[ V s2Sα ¬⇢ s ) is unsatisfiable" encodes this statement.
As for the existential consistency problem, we have an exponential gain in terms of size of the encoding compared to [START_REF] Delahaye | Parameter Synthesis for Parametric Interval Markov Chains[END_REF]: the number of constraints and variables in C 9r is linear in terms of the size of the encoded pIMC.

Remark. In C 9r Constraints (2) inherited from C 9c are entailed by Constraints ( 8) and [START_REF] Fourer | Algorithms and Model Formulations in Mathematical Programming[END_REF] added to C 9r . Thus, in a practical approach one may ignore Constraints (2) from C 9c if they do not improve the solver performances.

Quantitative Properties

We now move to the verification of quantitative reachability properties in pIMCs. Quantitative reachability has already been investigated in the context of pMCs and IMCs with the once-and-for-all semantics. In this section, we propose our main theoretical contribution: a theorem showing that the three IMC semantics are equivalent with respect to quantitative reachability, which allows the extension of all results from [START_REF] Wongpiromsarn | TuLiP: A Software Toolbox for Receding Horizon Temp oral Logic Planning[END_REF][START_REF] Benedikt | LTL model checking of interval Markov chains[END_REF]t o the at-every-step semantics. Based on this result, we also extend the CSP encodings introduced in Section 5.4 in order to solve quantitative reachability properties on pIMCs regardless of their semantics.

t quantitative reachability

Given an IMC I =( S, s 0 ,P,V)a n das t a t el a b e l↵ ✓ A, a quantitative reachability property on I is a property of the type P I (3↵)⇠p, where 0 <p<1a n d⇠2{,<,> , ≥}. Such a property is verified iff there exists an MC M satisfying I (with the chosen semantics) such that P M (3↵)⇠p.

As explained above, existing techniques and tools for verifying quantitative reachability properties on IMCs only focus on the once-and-for-all and the IMDP semantics. However, to the best of our knowledge, there are no works addressing the same problem with the at-every-step semantics or showing that addressing the problem in the onceand-for-all and IMDP setting is sufficiently general. The following theorem fills this theoretical gap by proving that the three IMC semantics are equivalent w.r.t quantitative reachability. In other words, for all MC M such that M| = a I I or M| = d I I and for all state label ↵, there exist MCs M  and M ≥ such that M  |= o I I, M ≥ |= o I I and P M  (3↵)  P M (3↵)  P M ≥ (3↵). This is formalised in the following theorem.

Theorem 1. Let I =( S, s 0 ,P,V) be an IMC, ↵ ✓ A be a state label, ⇠2{,<,> , ≥} and 0 <p<1. I satisfies P I (3↵)⇠p with the once-and-for-all semantics iff I satisfies P I (3↵)⇠p with the IMDP semantics iff I satisfies P I (3↵)⇠p with the at-everystep semantics.

The proof presented in the following is constructive: we use the structure of the relation R from the definition of |= a I in order to build the MCs M  and M ≥ . In the following, when it is not specified the IMC satisfaction relation considered is the at-every-step semantics (i.e.,t h e|= a I satisfaction relation). As said previously, we use the structure of the relation R from the definition of |= a I in order to build the MCs M  and M ≥ presented in Theorem 1. Thus, we introduce some notations relative to R. Let I =(S, s 0 ,P,V I )b ea nI M Ca n dM =(T,t 0 , p, V M )b ea nM Cs u c ht h a tM| = a I I. Let R ✓ T ⇥ S be a satisfaction relation between M and I. For all t 2 T we write R(t)f o r the set {s 2 S | t R s}, and for all s 2 S we write R -1 (t)f o rt h es e t{t 2 T | s R t}. Furthermore we say that M satisfies I with degree n (written M n |= a I I)i fM satisfies I with a satisfaction relation R such that each state t 2 T is associated by R to at most n states from S (i.e., |R(t)|  n); M satisfies I with the same structure than I if M satisfies I with a satisfaction relation R such that each state t 2 T is associated to at most one state from S and each state s 2 S is associated to at most one state from T (i.e., |R(t)|  1f o ra l lt 2 T and |R -1 (s)|  1f o ra l ls 2 S). Proposition 7. Let I be an IMC. If an MC M satisfies I with degree n 2 N then there exists an MC M 0 satisfying I with degree 1 such that M and M 0 are bisimilar.

The main idea for proving Proposition 7 is that if an MC M with states space T satisfies an IMC I with a states space S according to a satisfaction relation R then, each state t related by R to many states s 1 ,...,s n (with n>1) can be split in n states t 1 ,...,t n . The derived MC will satisfy I with a satisfaction relation R 0 where each t i is only associated by R 0 to the state s i (i  n). This M 0 will be bisimilar to M and it will satisfy I with degree 1. Note that by construction the size of the resulting MC is in

O(|M| ⇥ |I|).
Furthermore, we will use the until temporal modality (abbreviated U ) as presented in [START_REF] Baier | Principles of Model Checking (Representation and Mind Series[END_REF]. Let M be an MC and ↵, β be two state labelings. The probability of the property ↵ U β is given by the sum of the probabilities of all the finite paths starting in the initial state containing only states labeled with ↵ excepted for the last state which is labeled with β. Formally, let until s 0 (s)={! 2 S ⇤ | ! = s 0 ,...s n with V (s n )=β and V (s i )= ↵ 80  i<n} be the set of such paths. Thus, P M (↵ U β)= P ω2reachs 0 (s) P M (!). As for the reachability property, this notation naturally extends to states instead of labels, as well as conjunctions and disjunctions of states/labels.

Proof for Proposition 7. Let I =( S, s 0 ,P,V I )b ea nI M Ca n dM =( T,t 0 , p, V )b ea n MC. If M satisfies I (with degree n)t h e nt h e r ee x i s t sas a t i s f a c t i o nr e l a t i o nR verifying the |= a I satisfaction relation. For each association (t, s) 2 R, we write δ s t the correspondence function chosen for this pair of states. M satisfies I with degree n means that each state in M is associated by R to at most n states in I. To construct an MC M 0 satisfying I with degree 1 we create one state in M 0 per association (t, s)inR. Formally, let M 0 be equal to (U, u 0 ,p 0 ,V

0 )suchthatU = {u s t | (t, s) 2 R}, u 0 = u s 0 t 0 , V 0 = {(u s t ,v) | v = V (t)}, and p 0 (u s t )(u s 0 t 0 )=p(t)(t 0 ) ⇥ δ s t (t 0 )(s 0 ).
The following computation shows that the outgoing probabilities given by p 0 form a probability distribution for each state in M 0 and thus that M 0 is an MC.

X t 0 Rs 0 p 0 (u s t )(u s 0 t 0 )= X t 0 Rs 0 p(t)(t 0 ) ⇥ δ s t (t 0 )(s 0 ) = X t 0 2T p(t)(t 0 ) ⇥ X s 0 2S δ s t (t 0 )(s 0 )= X t 0 2T p(t)(t 0 ) ⇥ 1=1
Finally, by construction of M 0 based on M which satisfies I, we get that R 0 = {(u s t ,s) | t 2 T,s 2 S} is a satisfaction relation between M 0 and I. Furthermore |{s | (u, s) 2 R 0 }| equals at most one. Thus, we get that M 0 satisfies I with degree 1.

Consider the relation B 0 = {(u s t ,t) ✓ U ⇥ T | (t, s) 2 R}.W en o t eB the closure of B 0 by transitivity, reflexivity, and symmetry (i.e., B is the minimal equivalence relation based on B 0 ). We prove that B is a bisimulation relation between M and M 0 . By construction each equivalence class from B contains exactly one state t from T and all the states u s t such that (t, s) 2 R. Let (u s t ,t)b ei nB, t 0 be a state in T ,a n dB be the equivalence class from B containing t 0 (i.e., B is the set {t 0 } [ {u s 0 t 0 2 U | s 0 2 S and (t 0 ,s 0 ) 2 R}). Firstly note that by construction the labels agree on u s t and t: V 0 (u s t )=V (t). Secondly the following computation shows that p 0 (u s t )(B \ U )e q u a l st op(t)(B \ T ) and thus that u s t and t are bisimilar:

p 0 (u s t )(B \ U )= X u s 0 t 0 2B\U p 0 (u s t )(u s 0 t 0 )= X u s 0 t 0 2B\U p(t)(t 0 ) ⇥ δ s t (t 0 )(s 0 ) = X {s 0 2S|s 0 Rt 0 } p(t)(t 0 ) ⇥ δ s t (t 0 )(s 0 )=p(t)(t 0 ) ⇥ X {s 0 2S|s 0 Rt 0 } δ s t (t 0 )(s 0 ) = p(t)(t 0 ) ⇥ 1=p(t)({t 0 })=p(t)(B \ T )
Corollary 1. Let I be an IMC, M be an MC satisfying I, and γ be a PCTL ⇤ formulae.

There exists an MC M 0 satisfying I with degree 1 such that the probability P M 0 (γ) equals the probability P M (γ).

Corollary 1 is derived from Proposition 7 joined with the probability preservation of the PCTL* formulae on bisimilar Markov chains (see [START_REF] Baier | Principles of Model Checking (Representation and Mind Series[END_REF], Theorem 10.67, p.813). Corollary 1 allows to reduce to one the number of states in the pIMC I satisfied by each state in the MC M while preserving probabilities. Thus, one can construct from an MC M satisfying an IMC I another MC M 0 satisfying the same IMC I where the states in M 0 are related to at most one state in I. However, some states in I may still be related to many states in M 0 . The objective of Lemma 2 is to reduce these relations to an "at most one" in both directions (I to M 0 and M 0 to I). Lemma 2. Let I =( S, s 0 ,P,V) be an IMC, M =( T,t 0 , p, V ) be an MC satisfying I with degree 1, and α ✓ A be a proposition. If M does not have the same structure than I then there exists an MC M 1 (resp. M 2 ) satisfying I with a set of states S 1 (resp. S 2 ) s.t. S 1 ⇢ S and P M 1 (3↵)  P M (3↵) (resp. S 2 ⇢ S and P M 2 (3↵) ≥ P M (3↵)).

s 0 s 1 s 2 s 3 α 0.5 0.5 [0, 1] [0, 1] [0, 1] [0, 1] 1 IMC I t 0 t 1 t 0 1 t 2 t 3 α t 0 2 0.4 0.5 0.1 0.5 0.5 1 1 1 1 MC M 1 t 0 t 1 t 0 1 t 3 α t 0 2
Lemma 2 reduces the number of states in M while preserving the maximal or minimal reachability probability. This lemma has a constructive proof. The main idea of the proof is that we select one state s from the IMC I which is satisfied by many states t 1 ,...,t n in M. Thus, the MC M 0 keeping the state t k maximizing the probability of reaching ↵ in M and removing all the other states t i (i.e., remove the states t i such that i 6 = k and move the transitions to a state t i such that i 6 = k to arrive to the state t k )w i l lh a v el e s s states than M and will verify P M 1 (3↵) ≥ P M (3↵). Figure 5.12 contains an IMC I and three MCs M 1 , M 2 ,a n dM 3 . This illustrates how Lemma 2 operates for reducing the state space. We describe how to obtain M 2 from M 1 . Consider the state s 2 from I. This state is related to the states t 2 and t 0 2 in M 1 . Since

P M 1 t 2 (3↵)=0andP M 1 t 0 2
(3↵)=1 we remove t 2 and we keep t 0 2 which has an higher probability to reach ↵. Then, all the transitions going to t 2 are changed in order to go to t 0 2 . This creates M 2 . Next, the same mechanism can be iterated to produce M 3 : consider s 1 from I and remove t 0 1 and keep t 1 from M 2 to produce M 3 . This allows to reduce the number of states in the constructed Markov chain while preserving the maximal/minimal reachability probability. Before proving Lemma 2, we introduce Lemma 3 which will be used for proving Lemma 2. Lemma 3. Let M =( S, s 0 , p, V ) be an MC, ↵ ✓ A be a proposition, and s be a state from S. Then

P M s (3↵)= P M s (¬s U ↵) 1 -P M s (¬↵ U s)
Proof. Let S 0 be the subset of S containing all the states labeled with ↵ in M. We write Ω n with n 2 N ⇤ the set containing all the paths ! starting from s s.t. state s appears exactly n times in ! and no state in ! is labeled with ↵.F o r m a l l yΩ n contains all the

! = s 1 ,...,s k 2 S k s.t. k 2 N, s 1 is equal to s, |{i 2 [1,k] | s i = s}| = n,a n d↵ 6 ✓ V (s i ) for all i 2 [1,k].
Given two sets of paths Ω and Ω 0 , we write Ω⇥Ω 0 their Cartesian product which is the set of paths {!! 0 | ! 2 Ω and ! 0 2 Ω 0 }. We get by (a) that (P M s (Ω n ⇥ S 0 )) n≥1 is a geometric series. For (⇤)recallthatgiv enanMCM and two non-empty paths ! and ! 0 on M s.t. s and s 0 are respectively the first state in ! and ! 0 we have by definition that P M s (!! 0 )=P M s (!s 0 ) • P M s 0 (! 0 ). In (b) we partition the paths reaching ↵ according to the Ω n sets and we use the geometric series of the probabilities to retrieve the required result.

(a)

P M s (Ω n ⇥ S 0 )=P M s (Ω 1 ⇥ Ω n-1 ⇥ S 0 ) (⇤) = P M s (Ω 1 ⇥ {s}) • P M s (Ω n-1 ⇥ S 0 ) = P M s (¬↵ U s) • P M s (Ω n-1 ⇥ S 0 ) (b) P M s (3↵)=Σ +1 n=1 P M s (Ω n ⇥ S 0 ) = P M s (Ω 1 ⇥ S 0 ) 1 -P M s (¬↵ U s) = P M s (¬s U ↵) 1 -P M s (¬↵ U s)
Proof for Lemma 2. Let I =( S, s 0 ,P,V I )b ea nI M Ca n dM =( T,t 0 , p, V )b ea nM C satisfying I with degree 1. We write R the satisfaction relation between M and I with degree 1. The following proves in 3 steps the P M 1 (3↵)  P M (3↵)c a s e .

1. We would like to construct an MC M 0 satisfying I with less states than M 0 such that P M 0 (3↵)  P M (3↵). Since the degree of R equals to 1 each state t in T is associated to at most one state s in S. Furthermore, since M does not have the same structure than I then there exists at most one state from S which is associated by R to many states from T . Let s be a state from S such that |R -1 (s)| ≥ 2, T = {t 1 ,...,t n } be the set R -1 (s)w h e r et h et i are ordered by decreasing probability of reaching ↵ (i.e., P M t i (3↵) ≥ P M t i+1 (3↵)f o ra l l1 i<n). In the following we refer t as t n .W e produce M 0 from M by replacing all the transitions going to a state t 1 ,...,t n-1 by a transition going to t n , and by removing the corresponding states. Formally M 0 =(T 0 ,t 0 ,p 0 ,V 0 )s . t . T 0 =(T \ T ) [ { t}, V 0 is the restriction of V on T 0 , and for all t, t 0 2 T 0 : p 0 (t)(t 0 )=p(t)(t 0 )i ft 0 6 = t and p 0 (t)(t 0 )= P t 0 2 T p(t)(t 0 )o t h e r w i s e .

X t 0 2T 0 p 0 (t)(t 0 )= X t 0 2T 0 \{ t} p 0 (t)(t 0 )+p 0 (t)( t) (1) = X t 0 2T 0 \{ t} p(t)(t 0 )+ X t 0 2 T p(t)(t 0 ) = X t 0 2T 0 \{ t}[ T p(t)(t 0 ) (2) = X t 0 2T p(t)(t 0 )=1
The previous computation holds for each state t in M 0 . It shows that the outgoing probabilities given by p 0 form a probability distribution for each state in M 0 and thus that M 0 is an MC. Note that step (1) comes from the definition of p 0 with respect to p and that step (2) comes from the definition of T 0 according to T and t.

2. We now prove that M 0 satisfies I. M satisfies I implies that there a exists a satisfaction relation R between M and I. Let R 0 ✓ T ⇥ S be s.t. t R 0 s if t R s and t R 0 s if there exists a state t 0 2 T s.t. t 0 R s.W e p r o v e t h a t R 0 is a satisfaction relation between M 0 and I. For each pair (t, s) 2 R we note δ (s,t) the correspondence function given by the satisfaction relation R. Let (t, s) be in R 0 and δ 0 :

T 0 ! (S ! [0, 1]) be s.t. δ 0 (t 0 )(s 0 )=δ (t,s) (t 0 )(s 0 )i ft 0 6 = t and δ 0 (t 0 )(s 0 )=max t 0 2 T (δ (t,s) (t 0 )(s 0 )) otherwise.
δ 0 is a correspondence function for the pair (t, s)i nR 0 such as required by the |= a I satisfaction relation: a) Let t 0 be in T . If t 0 6 = t then δ 0 (t 0 )i se q u i v a l e n tt oδ (t,s) (t 0 )(s 0 ) which is by definition a distribution on S. Otherwise t 0 = t and the following computation proves that δ 0 ( t)i sad i s t r i b u t i o no nS. For the step (1) remind that R is a satisfaction relation with degree 1 and that t R s. This implies that δ (t,s) ( t)(s 0 ) equals to zero for all s 0 6 =s. For the step (2), R is a satisfaction relation with degree 1 implies that δ (t,s) (t 0 )(s 0 )e q u a l st o0o r1f o ra l lt 0 2 T and s 0 2 S. Finally the recursive definition of the satisfaction relation R implies that there exists at least one state t 00 2 T s.t. δ (t,s) (t 00 )(s)d o e sn o te q u a lt oz e r o( i.e., equals to one).

X s 0 2S δ 0 ( t)(s 0 )= X s 0 2S\{s} δ 0 ( t)(s 0 )+δ 0 ( t)(s) = X s 0 2S\{s} δ (t,s) ( t)(s 0 )+max t 00 2 T (δ (t,s) (t 00 )(s)) (1)
= max t 00 2 T (δ (t,s) (t 00 )(s 0 ))

=1 b) Let s 0 be in S.

Step (1) uses the definition of p 0 according to p.

Step (2) uses the definition of δ 0 according to δ (t,s) . Step (3) comes from the fact that for all t, t 0 2 T ⇥ T , we have by the definition of the satisfaction relation R with degree 1 and by construction of T that if p(t, t 0 ) 6 =0t h e nδ (t)(s) (t 0 , s)=1a n d δ (t,s) (t 0 )(s 0 )=0foralls 0 6 =s. Finally, step (4) comes from the definition of the correspondence function δ (t,s) for the pair (t, s)i nR.

X t 0 2T 0 p 0 (t)(t 0 ) ⇥ δ 0 (t 0 )(s 0 ) = X t 0 2T 0 \{ t} p 0 (t)(t 0 ) ⇥ δ 0 (t 0 )(s 0 )+p 0 (t, t) ⇥ δ 0 ( t)(s 0 ) (1) = X t 0 2T 0 \{ t} p(t)(t 0 ) ⇥ δ 0 (t 0 )(s 0 )+ X t 0 2 T p(t)(t 0 ) ⇥ δ 0 ( t)(s 0 ) (2) = X t 0 2T 0 \{ t} p(t)(t 0 ) ⇥ δ (t,s) (t 0 )(s 0 )+ X t 0 2 T p(t)(t 0 ) ⇥ max t 00 2 T (δ (t,s) (t 00 )(s 0 )) (3) = X t 0 2T 0 \{ t} p(t)(t 0 ) ⇥ δ (t,s) (t 0 )(s 0 )+ X t 0 2 T p(t)(t 0 ) ⇥ δ (t,s) (t 0 )(s 0 ) = X t 0 2T 0 \{ t}[ T p(t)(t 0 ) ⇥ δ (t,s) (t 0 )(s 0 )= X t 0 2T p(t)(t 0 ) ⇥ δ (t,s) (t 0 )(s 0 ) (4)
2 P (s, s 0 ) c) Let t 0 be in T 0 and s 0 be in S. We have by construction of R 0 from R that if δ 0 (t 0 )(s 0 ) > 0t h e n( t 0 ,s 0 ) 2 R.

3. Ne now prove that the probability of reaching ↵ from t is lower in M 0 than in M. We consider the MC M 00 from M where the states containing the label ↵ are replaced by absorbing states. Formally M 00 =( T,t 0 ,p 00 ,V)s u c ht h a tf o ra l l t, t 0 2 T : p 00 (t, t 0 )=p(t, t 0 )i f↵ 6 ✓ V (t)e l s ep 00 (t, t 0 )=1i ft = t 0 and p 00 (t, t 0 )=0 otherwise. By definition of the reachability property we get that P M 00 t (3↵)e q u a l s to P M t (3↵)f o ra l ls t a t et in T 0 . Following computation concludes the proof.

Step (1) comes from Lemma 3. Step (2) comes by construction of M 0 from M. Step (3) comes by construction of M 00 from M where states labeled with ↵ are absorbing states. Step (4) comes from the fact that P M 00 tn (3↵)i se q u a lt oP

M 00 tn (¬(t 1 _ ... _ t n )U↵)+Σ 1in P M 00 tn (¬(t 1 _ ..._ t n )Ut i ) ⇥ P M 00 t i (3↵).
Step (5) uses the fact that P M t i (3↵) ≥ P M tn (3↵)f o ra l l1 i  n and by construction this is also correct in M 00 . Last steps are straightforward.

P M 0 t (3↵) (1)
= P M 0 t (¬ t U ↵) 1 -P M 0 t (¬↵ U t) (2)
= P M tn (¬(t 1 _ ..._ t n )U↵) 1 -P M tn (¬↵ U( t 1 _ ..._ t n )) (3)
= P M 00 tn (¬(t 1 _ ..._ t n )U↵) 1 -P M 00 tn (3(t 1 _ ..._ t n )) (4)
= P M 00 tn (3↵) -

P 1in P M 00 tn (¬(t 1 _ ..._ t n )Ut i ) ⇥ P M 00 t i (3↵) 1 -P M 00 tn (3(t 1 _ ..._ t n )) (5)
 P M 00 tn (3↵) -

P 1in P M 00 tn (¬(t 1 _ ..._ t n )Ut i ) ⇥ P M 00 tn (3↵) 1 -P M 00 tn (3(t 1 _ ..._ t n )) (6)
= P M 00 tn (3↵) ⇥ (1 -

P 1in P M 00 tn (¬(t 1 _ ..._ t n )Ut i )) 1 -P M 00 tn (3(t 1 _ ..._ t n )) (7)
= P M 00 tn (3↵) ⇥ (1 -P M 00 tn (3(t 1 _ ..._ t n ))) 1 -P M 00 tn (3(t 1 _ ..._ t n )) = P M 00 tn (3↵) = P M t (3↵)
The same method can be used for proving that P M 2 (3↵) ≥ P M (3↵)b yd e fi n i n g T = {t 1 ,...,t n } to be the set R -1 (s)s.t. thestatest i are ordered by increasing probability of reaching ↵. Thereby the symbol  at step (5) for the computation of P M 0 t (3↵)i s replaced by the symbol ≥.

Next, Lemma 4 is a consequence of Corollary 1 and Lemma 2 and states that the maximal and the minimal probability of reaching a given proposition is realized by Markov chains with the same structure than the IMC. Proof. Let I be an IMC and M be an MC satisfying I w.r.t. |= a I . Consider the sequence of MCs (M n ) n2N s.t. M 0 is the MC satisfying I with degree 1 obtained by Corollary 1 and for all n 2 N, M n+1 is the MC satisfying I with strictly less states than M n and verifying P M n+1 (3↵)  P Mn (3↵)g i v e nb yL e m m a2 if M n does not have the same structure than I and equal to M n otherwise. By construction (M n ) n2N is finite and its last element is aM a r k o vc h a i nM 0 with the same structure than I s.t. P M 0 (3↵)  P M (3↵). Thus, M 0 satisfies I w.r.t. |= o I s.t. P M 0 (3↵)  P M (3↵). The same method can be used for proving the other side of the inequality (i.e., there exists an MC M 0 s.t. M 0 |= o I I and P M (3↵)  P M 0 (3↵)).

Finally, the following proves our Theorem 1 using Lemma 4 and Proposition 3.

Proof for Theorem 1. Let I =(S, s 0 ,P,V)beanIMC,↵ ✓ A be a state label, ⇠2{,< ,>,≥} and 0 <p<1. Recall that according to an IMC satisfaction relation the property P I (3↵)⇠p holds iff there exists an MC M satisfying I (with the chosen semantics) such that P M (3↵)⇠p.

Constraint Encodings

Note that the result from Theorem 1 naturally extends to pIMCs. We therefore exploit this result to construct a CSP encoding for verifying quantitative reachability properties in pIMCs. As in Section 5.4, we extend the CSP C 9c , that produces a correct MC implementation for the given pIMC, by imposing that this MC implementation satisfies the given quantitative reachability property. In order to compute the probability of reaching state label ↵ at the MC level, we use standard techniques from [START_REF] Baier | Principles of Model Checking (Representation and Mind Series[END_REF] that require the partitioning of the state space into three sets S > , S ? ,a n dS ? that correspond to states reaching ↵ with probability 1, states from which ↵ cannot be reached, and the remaining states, respectively. Once this partition is chosen, the reachability probabilities of all states in S ? are computed as the unique solution of a linear equation system (see [START_REF] Baier | Principles of Model Checking (Representation and Mind Series[END_REF], Theorem 10.19, p.766). We now explain how we identify states from S ? ,S > and S ? and how we encode the linear equation system, which leads to the resolution of quantitative reachability.

Let P =( S, s 0 ,P,V,Y)b eap I M Ca n d↵ ✓ A be a state label. We start by setting S > = {s | V (s)=↵}. We then extend C 9r (P)i no r d e rt oi d e n t i f yt h es e tS ? . Let

↵ s =1, if↵ = V (s) (12) ↵ s 6 =1, if↵ 6 = V (s) (13) λ s , (⇢ s ^(↵ s 6 =0)) (14) ↵ s > 1 ) W s 0 2Succ(s)\{s} (↵ s = ↵ s 0 +1)^(✓ s 0 s > 0), if ↵ 6 = V (s) (15) ↵ s =0, V s 0 2Succ(s)\{s} (↵ s 0 =0)_ (✓ s 0 s =0), if↵ 6 = V (s)
Note that variables ↵ s play a symmetric role to variables ! s from C 9r : instead of indicating the existence of a path from s 0 to s, they characterize the existence of a path from s to a state labeled with ↵. In addition, due to Constraint (13), variables λ s are set to true iff there exists a path with non zero probability from the initial state s 0 to a state labeled with ↵ passing by s. Thus, ↵ cannot be reached from states such that λ s = false. Therefore, S ? = {s | λ s = false}, which is formalised in Proposition 8. First, note that s 3 is the only state labelled by {↵, β} in P. By considering the MC M built from the valuation of the transition variables in Figure 5.13 we have that: ↵ 0 =3 ,w h i c hi m p l i e st h a tt h e r ee x i s t sap a t hi nM with size 2 reaching ↵ from s 1 ; ↵ 1 = 2, which implies that there exists a path in M with size 1 reaching ↵ from s 1 ;a n d↵ 2 =0 ,w h i c hi m p l i e st h a tt h e r ei sn op a t hi nM reaching ↵ from s 1 , etc. Finally, by Constraint (13) we have that: λ 0 , λ 1 ,a n dλ 3 are true which implies that the states s 0 , s 1 ,a n ds 3 are reachable in M and they can reach ↵; λ 2 and λ 4 are false which implies that the states s 2 and s 4 cannot reach ↵ in M.

Finally, we encode the equation system from [START_REF] Baier | Principles of Model Checking (Representation and Mind Series[END_REF] in a last CSP encoding that extends

C 0 9r .L e t C 9r (P, ↵)=( X [ X 0 ,D [ D 0 ,C [ C 0
)b es u c ht h a t( X, D, C)=C 0 9r (P, ↵), X 0 contains one variable ⇡ s per state s in S with domain [0, 1], D 0 contains the domains of these variables, and C 0 is composed of the following constraints for each state s 2 S:

(16) ¬λ s ) ⇡ s =0 (17) λ s ) ⇡ s =1, if↵ = V (s) (18) λ s ) ⇡ s = Σ s 0 2Succ(s) ⇡ s 0 ✓ s s 0 ,i f ↵ 6 = V (s)
As a consequence, variables ⇡ s encode the probability with which state s eventually reaches ↵ when s is reachable from the initial state and 0 otherwise. Proposition 9. Let P =( S, s 0 ,P,V,Y) be a pIMC and ↵ ✓ A be a proposition. There exists an MC M| = a pI P iff there exists a valuation v solution of the CSP C 9r (P, ↵) s.t. v(⇡ s ) is equal to P M s (3↵) if s is reachable from the initial state s 0 in M and is equal to 0 otherwise. Proof. Let P =( S, s 0 ,P,V,Y)b eap I M Ca n d↵ ✓ A be a state label. C 9r extends the CSP C 0 9r that produces a MC M satisfying P (cf. Proposition 8)b yc o m p u t i n gt h e probability of reaching ↵ in M. In order to compute this probability, we use standard techniques from [START_REF] Baier | Principles of Model Checking (Representation and Mind Series[END_REF] that require the partitioning of the state space into three sets S > , S ? ,a n dS ? that correspond to states reaching ↵ with probability 1, states from which ↵ cannot be reached, and the remaining states, respectively. Once this partition is chosen, the reachability probabilities of all states in S ? are computed as the unique solution of an equation system (see [START_REF] Baier | Principles of Model Checking (Representation and Mind Series[END_REF], Theorem 10.19, p.766). Recall that for each state s 2 S variable ↵ s is equal to true iff s is reachable in M and s can reach ↵ with a non zero probability. Thus we consider S ? = {s | ↵ s = false}, S > = {s | V (s)=↵},a n d S ? = S \ (S ? [ S > ). Finally constraints in C 9r encodes the equation system from [START_REF] Baier | Principles of Model Checking (Representation and Mind Series[END_REF] according to chosen S ? , S > ,a n dS ? . Thus, ⇡ s 0 equals the probability in M to reach ↵.

Example 33 (Example 32 continued). Consider the valuation given in Figure 5.13 as a partial solution to the CSP C 9r (P, {↵, β}). Let M be the MC built from this partial valuation. Since s 2 and s 4 cannot reach {↵, β} in M we have that S ? contains s 2 and s 4 . Furthermore, s 3 is the only state labelled by {↵, β} in M. Thus, S > contains s 3 and the remaining states s 0 and s 1 are in S ? . Finally, Constraints ( 16), [START_REF] Aris | Mathematical modelling techniques[END_REF],a n d( 18) encode the following system to compute for each state the quantitative reachability of {↵, β} in M:

8 > > > > > > < > > > > > > : ⇡ 0 =0 .7⇡ 1 +0.3⇡ 2 ⇡ 1 =0 .5⇡ 1 +0.5⇡ 3 ⇡ 2 =0 ⇡ 3 =1 ⇡ 4 =0 , 8 > > > > > > < > > > > > > : ⇡ 0 =0 .7⇡ 1 +0 ⇡ 1 =0 .5⇡ 1 +0.5 ⇡ 2 =0 ⇡ 3 =1 ⇡ 4 =0 , 8 > > > > > > < > > > > > > : ⇡ 0 =0 .7 ⇡ 1 =1 ⇡ 2 =0 ⇡ 3 =1 ⇡ 4 =0 Let p 2 [0, 1] ✓ R

Prototype Implementation and Experiments

Our results have been implemented in a prototype tool5 which generates the above CSP encodings, and CSP encodings from [START_REF] Delahaye | Parameter Synthesis for Parametric Interval Markov Chains[END_REF] as well. In this section, we first present our benchmark, then we evaluate our tool for the qualitative properties, and we conclude with the quantitative properties.

Benchmark

MCs have been used for many decades to model real-life applications. PRISM [START_REF] Kwiatkowska | PRISM 4.0: Verification of Probabilistic Real-time Systems[END_REF]i sa reference for the verification of probabilistic systems. In particular, it is able to verify properties for MCs. As said in Section 5.2, pIMCs correspond to abstractions of MCs. PRISM references several benchmarks based on MCs 6 . Note first that we only consider pIMCs with linear parametric expressions. In this context all the CSPs encodings for verifying the qualitative properties only use linear constraints while the CSPs encodings for verifying the quantitative properties produce quadratic constraints (i.e., non-linear constraints). This produces an order of magnitude between the time complexity for solving the qualitative properties vs the quantitative properties w.r.t. our encodings. Thus, we consider two different benchmarks presented in Table 5.1 and 5.2. In both cases, pIMCs are automatically generated from the PRISM model in a text format inspired from [START_REF] Wongpiromsarn | TuLiP: A Software Toolbox for Receding Horizon Temp oral Logic Planning[END_REF].

For the first benchmark used for verifying qualitative properties, we constructed the pIMCs from existing MCs by randomly replacing some exact probabilities on transitions by (parametric) intervals of probabilities. Our pIMC generator takes 4 arguments: the MC transition function; the number of parameters for the generated pIMC; the ratio of the number of intervals over the number of transitions in the generated pIMC; the ratio of the number of parameters over the number of interval endpoints for the generated pIMC. The benchmarks used are presented in Table 5.1. We selected 5 applications from PRISM [START_REF] Kwiatkowska | PRISM 4.0: Verification of Probabilistic Real-time Systems[END_REF]: herman -the self-stabilisation protocol of Herman from [START_REF] Kwiatkowska | Probabilistic Verification of Herman's Self-Stabilisation Algorithm[END_REF]; egl -t h e contract signing protocol of Even, Goldreich & Lempel from [START_REF] Norman | Analysis of Probabilistic Contract Signing[END_REF]; brp -t h eb o u n d e d retransmission protocol from [START_REF]Reachability analysis of probabilistic systems by successive refinements[END_REF]; crowds -t h ec r o w d sp r o t oc o lf r o m [START_REF] Shmatikov | Probabilistic Model Checking of an Anonymity System[END_REF]; and nand -the nand multiplexing from [START_REF] Norman | Evaluating the Reliability of NAND Multiplexing with PRISM[END_REF]. Each one is instantiated by setting global constants (e.g., N for the application herman, L and N for the application egl)l e a d i n gt om o r e or less complex MCs. We used our pIMC generator to generate an heterogeneous set of benchmarks: 459 pIMCs with 8 to 15, 102 states and 28 to 21, 567 transitions not reduced to [0, 0]. The pIMCs contain from 2 to 250 parameters over 0 to 7772 intervals.

For the second benchmark used for verifying quantitative properties we extended the nand model from [START_REF] Norman | Evaluating the Reliability of NAND Multiplexing with PRISM[END_REF]. The original MC nand model has already been extended as a pMC in [START_REF] Dehnert | PROPhESY: A PRObabilistic ParamEter SYnthesis To ol[END_REF], where the authors consider a single parameter p for the probability that each of the N nand gates fails during the multiplexing. We extend this model to pIMC by considering one parameter for the probability that the initial inputs are stimulated and we have one parameter per nand gate to represent the probability that it fails. We consider 4 pIMCs with 104 to 7, 392 states and 147 to 11, 207 transitions not reduced to [0, 0]. The pIMCs contain from 4 to 12 parameters appearing over 82 to 5, 698 transitions.

Constraint Modelling

Given a pIMC in a text format our tool produces the desired CSP according to the selected encoding (i.e., one from [START_REF] Delahaye | Parameter Synthesis for Parametric Interval Markov Chains[END_REF], C 9c , C 9r ,orC 9r ). Recall that our benchmark only consider linear parametric expressions on transitions. The choice of the contraint programming language for implementing a CSP encoding depends on its nature (e.g.,t h et y p eo ft h e variables: integer vs. continuous, the kind of the contraints: linear vs. non-linear). Table 5.3 summarizes the natures the encodings where SotA stands the encoding from [START_REF] Delahaye | Parameter Synthesis for Parametric Interval Markov Chains[END_REF] answering the existential consistency problem. Thus, SotA, C 9c ,a n dC 9r can be implemented as Mixed Integer Linear Programs (MILP) [START_REF] Pablo | Mixed Integer Linear Programming Formulation Techniques[END_REF] and as Satisfiability Modulo Theory (SMT)p r o g r a m s [START_REF] Clark | Satisfiability Modulo Theories[END_REF] with QF LRA logic (Quantifier Free linear Real-number Arithmetic). This logic deals with Boolean combinations of inequations between linear polynomials over real variables. Note that, QF NRA does not deal with integer variables. Indeed logics mixing integers and reals are harder than those over reals only. However, all the integer variables in our encodings can be replaced by real-number variables. 7 Each integer variable x can be declared as a real variable whose real domain bounds are its original integer domain bounds; we also add the constraint x<1 ) x =0 . S i n c ew e only perform incrementation of x this preserves the same set of solutions (i.e., ensures integer integrity constraints). Finally, due to the non-linear constraints in C 9r ,t h e s e encodings are implemented as SMT programs [START_REF] Clark | Satisfiability Modulo Theories[END_REF] with the QF NRA logic (Quantifier Free Non linear Real-number Arithmetic). We use the same technique than for C 9c and C 9r for replacing integer variables by real-number variables. We chose the programming language Python for implementing our CSP modeller. We do not evaluate any arithmetic expression while generating CSPs, and numbers in the interval endpoints of the pIMCs are read as strings and no trivial simplification is performed while modelling. We do so to avoid any rounding of the interval endpoints when using floating point numbers.

Experiments have been realized on a 2.4 GHz Intel Core i5 processor. Time out has been set to 10 minutes. Memory out has been set to 2Gb. Table 5.4 presents the size of the instances (i.e., the number of variables and the number of constraints) for solving the existential consistency problem on our benchmark using (1) SMT SotA encoding, (2) SMT C 9c encoding, and (3) MILP C 9c encoding. First, note that all the pIMCs are successfully compiled when using our C 9c encoding while the SotA encoding produces out of memory errors for 4 sets of benchmarks: more than 20% of the instances (see OM cells in Table 5.4). We recall that the SotA encoding is defined inductively and that it iterates over the power set of the states. In practice, this implies deep recursions joined with enumeration over the power set of the states. The exponential gain exposed in Section 5.4 is visible in terms of number of variables and constraints in Table 5.4, and in terms of encoding time in Figure 5.15. Each dot in Figure 5.15 corresponds to one instance of our benchmark. While the encoding time ranges between 0 and 1s when using the C 9c encoding, it varies between 0 and 500s when using the SotA encoding (if it does not run out of memory).

MILP formulation of logical constraints (e.g., conjunction, disjunction, implication, equivalence) implies the introduction of binary variables called indicator variables [START_REF] Belotti | On handling indicator constraints in mixed integer programming[END_REF]. Each indicator variable is associated to one or more constraints. The valuation of the indicator variable activates or deactivates its associated constraints. We tried to formulate the SotA encoding into MILP. Unfortunately, the nested conjunctions and disjunctions imply the introduction of a huge number of indicator variables, leading to giant instances giving bad encoding and solving time. However, since the Boolean variables in C 9c exactly correspond to indicator variables, the MILP formulation of the C 9c encoding does not

Solving

We chose Z3 [START_REF] De | Z3: An Efficient SMT Solver[END_REF] in its last version (v. 4.4.2) as SMT solver. We chose CPLEX [11]i n its last version (v. 12.6.3.0) as MILP solver. Both solvers have not been tuned and we use their default strategies. Experiments have been realized on a 2.4 GHz Intel Core i5 processor. Time out has been set to 10 minutes. Table 5.4 presents the resolution time for the existential consistency problem on our first benchmark using (1) SMT SotA encoding, (2) SMT C 9c encoding, and (3) MILP C 9c encoding. While the SotA CSPs are larger than the C 9c CSPs, the solving time for the SotA CSPs appears to be competitive compared to the solving time for the C 9c CSPs. The scatter plot in Figure 5.16 (logarithmic scale) compares solving times for the SMT SotA encoding and SMT C 9c encoding. However when considering the resolution time of the problem (i.e., the encoding time plus the solving time) the C 9c encoding clearly answers faster than the SotA encoding. Finally, the comparison between the solving time using SMT C 9c encoding and MILP C 9c encoding is illustrated in Figure 5.17. It shows that the loss of safety by passing from real numbers with Z3 SMT resolution to floating point numbers with CPLEX MILP resolution leads to a non negligible gain in terms of resolution time (near to an exponential gain in our benchmark). Indeed the SMT C 9c encoding requires 50 seconds to complete the solving process while the MILP C 9c encoding needs less than 5 seconds for the same instances. Table 5.5 summarizes the results w.r.t. our second benchmark: the pIMC sizes (in terms of states, transitions, and parameters), the CSP sizes (in terms of number of variables and constraints), and the resolution time using the Z3 solver. Note first that we perform pre-processing when verifying reachability properties: i.e., we eliminate all the states that cannot reach the goal states. This explains why C 9r has less variables and constraints than C 9c . Finally, note the order of magnitude between the resolution time required for solving the qualitative properties vs the quantitative properties w.r.t. our encodings. Indeed, we did not succeed in solving pIMCs with more than 300 states and 400 transitions for quantitative properties while we verified pIMCs with more than 10,000 states and 20,000 transitions in the qualitative context.

Conclusion and Perspectives

In this chapter, we have compared several Markov Chain abstractions in terms of succinctness and we have shown that Parametric Interval Markov Chain is a strictly more succinct abstraction formalism than other existing formalisms such as Parametric Markov Chains and Interval Markov Chains. In addition, we have proposed constraint encodings for checking several properties over pIMC. In the context of qualitative properties such as existential consistency or consistent reachability, the size of our encodings is significantly smaller than other existing solutions. In the quantitative setting, we have compared the three semantics for IMCs and pIMCs and showed that the semantics are equivalent with respect to quantitative reachability properties. As a side effect, this result ensures that all existing tools and algorithms solving reachability problems in IMCs under the once-and-for-all semantics can safely be extended to the at-every-step semantics with no Based on this result, we have then proposed CSP encodings addressing quantitative reachability in the context of pIMCs regardless of the chosen semantics. Finally, we have developed a prototype tool that automatically generates our CSP encodings and that can be plugged to any constraint solver accepting the SMT-LIB format as input.

Our tool for pIMC verification could be extended in order to manage other, more complex, properties (e.g., supporting the LTL-language in the spirit of what Tulip [START_REF] Wongpiromsarn | TuLiP: A Software Toolbox for Receding Horizon Temp oral Logic Planning[END_REF] does). Also one could investigate a practical way of computing and representing the set of all solutions to the parameter synthesis problem.

Chapter 6 Conclusion and Perspectives

In this thesis we tackled two families of program verification problems. In both cases we first investigated the nature of the verification problem in order to propose an accurate constraint resolution. Since we had no a priori restrictions on the constraint language, we proposed constraint models using non-linear constraints with unbounded continuous variables, mixed integer/continuous domain variables over linear constraints, and also quadratic constraints over mixed variables. We first present in this chapter the conclusions and perspectives of both contributions. We close this thesis with a general conclusion on the benefits of considering constraint programming for program verification.

Block-Diagram Verification Block-diagrams are used to model real-time systems such as digital signal processes. Such systems appear in many applications receiving and processing digital signals: modems, multimedia devices, GPS, audio and video processing. We proposed a constraint model using our global constraint called real-time-loop for computing over-approximations of real-time streams, based on their block-diagrams representations. We introduced a global constraint and presented a dedicated filtering algorithm inspired by Abstract Interpretation. The experiments show that our approach can reach very good over-approximations in a short running time. Thus, our proposal has been taken in consideration for a future implementation into the FAUST compiler. More generally, our method shows that constraint programming can handle block-diagram analyses in an elegant and natural way.

However we point out some perspectives. Firstly, the propagation loop may be improved according to the tackled verification problem (for instance, when verifying output streams one should favor input to output propagations instead of an arbitrary scheme). Secondly, some constraint patterns offer poor over-approximations when considering interval extensions (e.g., the interval extension of the pattern |xint(x)| which should compute the decimal part of x returns the interval abstraction [0; 20] with [-10; 10] as input domain whereas the concrete output domain of this pattern is [0; 1]). Thus, managing such patterns would improve the quality of the computed over-approximations. Thirdly, Chapter 6. Conclusion and Perspectives one should test our approach on a language which is not dedicated to audio processing in order to test the practical robustness of our approach with respect to the nature of the programs. Finally, over-approximations intervals ensure that there are no stream values outside the intervals but cannot conclude if they contain at least one stream value. Thus, one may investigate inner-approximations in order to certify the presence of stream values. This could be used to partition the space in three: the intervals that contain only stream values, the intervals that may contain stream values, and the intervals that do not contain any stream value.

Markov Chain Abstraction Verification Markov chains model softwares and reallife systems for which probabilities play a fundamental role. We considered the Parametric Interval Markov Chain (pIMC for short) specification formalism for abstracting Markov chains. We first presented a formal theorem proving the equivalence of the three main pIMC semantics with respect to the reachability property. Then, we exploited this result for proposing constraint modellings answering consistency, qualitative, and quantitative reachability properties. For consistency and qualitative reachability, the state-of-the-art constraint models had an exponential size in terms of the verified pIMCs. We proposed constraints models with a linear size in terms of the pIMC size for solving the same problems using the same type of constraints and variables. For quantitative reachability, there was no existing verification process. We thus proposed the first verification process as constraint models in order to answer this problem. Furthermore, we took benefits of the constraint programming paradigm to propose modular constraints models: i.e., the quantitative models extend the qualitative models which extend the consistency models. We implemented our constraint models and we evaluated our prototype over a pIMC benchmark generated from PRISM programs. Constraint models have been generated as mixed linear integer programs and satisfiability modulo theory programs and we obtained promising results. In practice, these results lead to pIMCs closer to the effective resolution of real-word problems.

We now present some perspectives. Firstly, parameters in pIMCs may correspond to possibly controllable inputs in the probabilistic systems or may model a cost to minimize or maximize. Thus, by adding an optimization function to our constraint encodings one may investigate such problems. Secondly, parameters may correspond to decisions to be taken for implementing the pIMC as an IMC in the real-world. The visualization of the parameters state space according to the satisfiability with respect to the property to verify helps to select accurate parameter valuations. However, while some research has been realized with 2 or 3 parameters, one should also investigate cases with more parameters. Finally, the pIMC specification formalism allows to abstract sets of Markov chains. It appears that our constraint encoding may offer another specification formalism. Indeed, one should take benefit of our constraint modellings for expressing guards, relations between parameters, constraints over some probabilities on transitions, etc. Thus, all the expresivness of the constraint tools could be used for modelling and solving the verification of "constrained Markov chains".

To conclude, program verification is such a rich domain that it can potentially use many constraint tools. The theoretical complexity of program verification such as constraint satisfaction may belong to high complexity levels. Nevertheless, constraint programming solvers may offer a practical resolution to some hard problems However, several constraint programming communities chose different directions and they develop solvers dedicated to separate constraint languages. In this thesis, we considered verification problems through the prism of constraint programming. We proposed constraint programming approaches using various constraint languages for solving the considered verification problems. Our contributions help both fields of constraint programming and program verification to move closer together.

Introduction

La programmation par contraintes est un champ de recherche rattaché à l'intelligence artificielle. Un des objectifs de l'intelligence artificielle est de proposer des méthodes et des outils permettant de réaliser des tâches considérées comme complexes tant à un niveau logique, qu'à un niveau algorithmique. Ainsi le Graal de l'intelligence artificielle est de trouver une solution, un outil capable de résoudre une variété la plus grande possible de problèmes hétérogènes. C'est avec cet objectif que la programmation par contraintes se propose de résoudre tout un ensemble de problèmes qui peuvent être formulés à partir de contraintes. Une contrainte est une relation posée sur un ensemble de variables restreignant les affectations possibles entre les variables et leurs valeurs. En effet, une variable est un objet mathématique associé à un ensemble de valeurs pouvant lui être affectées. Ainsi, nous appelons valuation le choix de valeurs pour les variables, et satisfaire une contrainte revient à trouver une valuation qui satisfasse toutes les relations variables/valeurs établies par les contraintes. La modélisation en contraintes regroupe les différentes techniques utilisées pour passer d'un problème présenté en langage naturel vers un problème formellement décrit mathématiquement ou sous la forme d'un programme en contraintes (LP format, DIMACS format, XCSP format) appelé modèle. Une fois l'étape de modélisation terminée, le modèle est envoyé dans le système intelligent, appelé solver, pour être résolu. La première étape est appelée modélisation (en : modelling)e tl as e conde résolution (en : solving). Dans cette thèse, nous nous intéressons à la modélisation et à la résolution d'applications ciblées : la vérification de programmes.

Lors de ces dernières décennies, l'informatique s'est démocratisée tant dans les usages privés que professionnels. Ainsi, ordinateurs et systèmes d'informations réalisent des applications les plus variées : application intelligentes, systèmes embarqués d'avions, robots médicaux, etc. Comme c'est le cas dans le cadre des chaînes de production, l'écriture de ces systèmes/applications doit respecter un certain nombre de règles de qualité telles que la conformité, l'efficacité, la robustesse. La vérification de programmes a pour objectif de s'assurer qu'une application, un programme, un système réponde aux spécifications données, c'est-à-dire que son comportement soit correct, qu'il ne contienne pas de "bug". En effet, l'histoire a démontré la nécessité de la mise en oeuvre de telles vérifications. Qu'il s'agisse de la fusée Ariane 5 qui a explosé 36 secondes après son décalage ou du défaut de l'unité de calcul du Pentium II d'Intel qui a causé une perte de 475 millions de dollars et qui a nui gravement à l'image de la marque, ces deux évènements auraient pu être évités s'ils avaient été certifiés, vérifiés formellement d'un point de vue logiciel/programme informatique. Pour autant, la vérification de programme est une tâche difficile car c'est un problème indécidable : en général, il n'est pas possible de construire un système capable de déterminer en temps fini si un programme est correct ou non. Pour autant, indécidable ne veut pas dire infaisable en pratique. Dans cette thèse, nous modélisons et résolvons via la programmation par contraintes des problèmes de vérification de programmes. Nous présentons dans les deux sections suivantes un résumé des deux chapitres contributions de la thèse. Chacun porte sur un problème de vérification de programmes et propose une résolution en contraintes.

Vérification en contraintes d'un langage temps réel

La programmation par contraintes s'attaque en général à des problèmes statiques, sans notion de temps. Cependant, les méthodes de réduction de domaines pourraient par exemple être utiles dans des problèmes portant sur des flux. C'est le cas de la vérification de programmes temps réel où les variables peuvent changer de valeur à chaque pas de temps. Pour cette contribution, nous nous intéressons à la vérification de domaines de variables (flux) dans le cadre d'un langage de diagrammes de blocs. La première contribution de cette thèse (Chapitre 4) propose une méthode de réduction de domaines de ces flux, pour encadrer finement les valeurs prises au cours du temps. En particulier, nous proposons une nouvelle contrainte globale real-time-loop, nous présentons une application au langage FAUST (un langage fonctionnel temps réel pour le traitement audio) et nous testons notre approche sur différents programmes FAUST.

Contexte et problématique

Comme précisé en introduction de cette section, nous souhaitons vérifier un langage temps réel. Plus précisément, ce langage se positionne dans la famille des diagrammes de blocs que nous présentons ci-dessous. Nous terminons cette section par présenter la problématique de vérification traitée dans cette contribution.

Un bloc est une fonction appliquant un opérateur à un ensemble d'entrées ordonnées et produisant une ou plusieurs sorties ordonnées. A partir de là, un connecteur relie une sortie d'un bloc à une entrée d'un bloc. Nous appelons un diagramme de blocs un ensemble de blocs reliés par des connecteurs. Formellement, notons E un ensemble non vide. Un 0.1 + 0.9 ⇥ fby 0 [0.9; 0.9; 0.9; 0.9] [0; 0; 0; 0] [0. pour tout t 2 N. d contient également un bloc temporel : le bloc followed by abrégé par fby Par convention, nous hachurons les blocs temporels. La présence du bloc temporel permet de casser la dépendance cyclique. Ainsi, ce diagramme de blocs admet une seule exécution. Les valeurs pour les quatre premiers temps sont inscrites entre crochets à côté des connecteurs (remarquez le délai dû au bloc fby).

Après avoir décrit les diagrammes de blocs et leurs exécutions, nous présentons la problématique de vérification sous-jacente. La présence de circuits dans la représentation graphique des diagrammes de blocs ainsi que les branchements de flux d'entrées faiblement bornés peuvent générer des exécutions plus ou moins variées. Un des souhaits récurrents de la vérification est de borner les valeurs prises par les variables d'un programme. Traduit dans le contexte des diagrammes de blocs, cela revient à chercher quelles valeurs peuvent passer par les entrées et les sorties des blocs qui composent un diagramme de blocs. Ainsi, le problème de vérification que nous considérons est celui de trouver pour chaque entrée et sortie de bloc un intervalle, appelé sur-approximation, qui contienne l'ensemble des valeurs prises sur cette entrée ou sortie pour toutes les exécutions possibles du diagramme de blocs. Nous appelons ce problème, le problème de sur-approximation de flux.

Modélisation et résolution en contraintes

Nous proposons une modélisation et une résolution en contraintes du problème de surapproximation de flux dans les diagrammes de blocs. La première remarque est que nous restreignons l'usage des blocs temporels au bloc fby uniquement. Ainsi, sous cette condition, tout cycle dans un diagramme de blocs admet au moins un bloc fby. 1Nous rappelons que modéliser en contraintes revient à transformer un problème à résoudre en un problème de satisfaction/d'optimisation de contraintes. Pour le problème qui nous intéresse, nous souhaitons trouver pour chaque entrée et sortie de bloc un intervalle qui sur-approxime l'ensemble des valeurs des flux pouvant passer par cette entrée/sortie. L'approche que nous avons choisie est de trouver une sur-approximation la plus petite possible sans imposer le critère de minimalité. Nous verrons par la suite que les résultats que nous obtenons sont très satisfaisants, proches du minimum. Pour rappel, un CSP est défini comme un ensemble de variables X chacune associée à un domaine D x (x 2 X)e tu ne n s e m b l ed ec o n t r a i n t e sC. Les contraintes définissent les valuations des variables acceptées par le CSP (ex : la contrainte x =2+y porte sur deux variables x et y et impose l'égalité entre la valeur de x et la valeur de y plus 2).

Dans cette thèse, nous procédons en trois étapes de raffinement de nos modèles en contraintes pour atteindre notre modélisation finale. Le premier modèle, appelé modèle naïf, transforme le diagramme de blocs en un réseau de contraintes où les variables du CSP correspondent aux entrées et aux sorties des blocs du diagramme de blocs, et les contraintes sont exactement les opérateurs des blocs. Ainsi, toute solution de ce CSP correspond à une exécution du diagramme de blocs (c'est-à-dire les domaines des variables sont l'ensemble des flux à valeurs dans D). Les flux solutions pouvant être infinis et le nombre de solutions pouvant également être infini, il y a peu d'espoir de parvenir à synthétiser par ce modèle en contraintes l'ensemble des flux solutions pour chaque variable via une sur-approximation dans les intervalles. De fait, en s'inspirant de l'interprétation abstraite, nous considérons une abstraction du problème (qui peut être vue comme une relaxation pour la communauté contrainte) pour construire un deuxième modèle en contraintes. Ce second modèle, appelé modèle intermédiaire, considère comme domaine des variables l'ensemble des intervalles fermés à bornes dans D. 2 Les opérateurs des blocs sur les flux sont remplacés par une de leurs extensions aux intervalles. Ce modèle est tel que toute solution répond au problème de la sur-approximation de flux. Cependant, ce modèle intermédiaire retourne des solutions de faible qualité et il reste facilement bloqué aux infinis lors de la propagation de contraintes. Dès lors, nous proposons un dernier modèle, appelé modèle final, prenant en compte ce défaut de filtrage. Pour ce faire, nous introduisons une nouvelle contrainte globale : la contrainte real-time-loop . Nos recherches ont montré que la difficulté se posait au niveau des circuits. Chaque contrainte real-time-loop contient l'ensemble de la sémantique d'un circuit. C'est grâce à la connaissance de la sémantique haut niveau de cette contrainte que nous avons proposé un algorithme de filtrage dédié offrant des sur-approximations de meilleure qualité.

L'algorithme de filtrage proposé est inspiré de l'interprétation abstraite et plus particulièrement de la technique de recherche d'invariant inductif par la méthode des montées et descentes dans le treillis des sur-approximations (widening and narrowing technique). L'algorithme proposé n'assure pas de retourner une sur-approximation minimale. Cependant il possède des heuristiques permettant d'augmenter les possibilités de recherche et donc d'augmenter les chances de s'approcher de la solution minimale. L'exemple 2 illustre les différences entre le modèle naïf, intermédiaire et final. Pour évaluer notre modélisation en contraintes, nous avons choisi le langage FAUST permettant de faire la synthèse et le traitement temps réel de flux audio. Ce langage possède une sémantique bien définie de telle sorte que le compilateur FAUST peut générer pour chaque programme le diagramme de blocs qui en est la sémantique. Ainsi, nous avons considéré un ensemble de programmes de la bibliothèque FAUST et nous les avons modélisés en contraintes en utilisant notre encodage final. Nous avons ensuite utilisé le solveur de contraintes continues IBEX pour y implanter notre contrainte globale real-time-loop . L'objectif était de vérifier que les flux de sorties des programmes ne provoquaient pas de saturation (c'est-à-dire qu'ils étaient sur-approximés par l'intervalle [-1; 1]). Nos résultats montrent que nous parvenons dans la majeure partie des cas à trouver la plus petite sur-approximation dans les intervalles et dans des temps très courts (de l'ordre de la seconde). Ainsi notre approche a été prise en considération par les développeurs de FAUST pour une éventuelle intégration dans une version future du logiciel. Pour autant, il est important de noter que la plus petite sur-approximation dans les intervalles par le calcul intervalle est parfois très éloignée du plus petit intervalle contenant les valeurs prises par les flux. En effet, les calculs à partir de sur-approximations produisent des marges de sur-approximations qui se répètent et s'amplifient. Il existe également des opérateurs de blocs produisant de grandes imprécisions lorsqu'ils sont étendus aux intervalles (ex : X[-]X 6 = {0}).

Pour conclure, nous avons proposé plusieurs modélisations en contraintes pour le problème de la sur-approximation de flux dans les diagrammes de blocs. Nous avons proposé la contrainte globale real-time-loop pour répondre au problème donné. Puis nous avons évalué avec succès notre approche en considérant le problème de recherche de saturation dans des programmes FAUST. Ces travaux ont montré l'intérêt de l'utilisation de techniques de programmation par contraintes dans des cadres exotiques (la vérification de programmes utilisant des variables de flux). Ces travaux ont fait l'objet de trois communications/publications [1,2,3].

Vérification en contraintes de systèmes probabilistes

Les chaînes de Markov (MCs) sont largement utilisées pour modéliser une très grande variété de systèmes basés sur des transitions probabilistes (ex : protocoles aléatoires, systèmes biologiques, environnements financiers). D'un autre côté, les chaînes de Markov à i n t e r v a l l e s p a r a m é t r é s ( p I M C s ) s o n t u n f o r m a l i s m e d e s p é c i fi c a t i o n p e r m e t t a n t d e représenter de façon compacte des ensembles infinis de chaînes de Markov. En effet, les PIMCs prennent en compte l'imprécision ou le manque de connaissances quant à la probabilité exacte de chaque évènement/transition du système en considérant des intervalles paramétrés de probabilités. Dans la seconde contribution de cette thèse (Chapitre 5), nous proposons d'abord une comparaison formelle de trois sémantiques existantes pour les PIMCs. Ensuite, nous proposons des encodages en contraintes pour vérifier des propriétés d'accessibilité qualitative et quantitative sur les pIMCs. En particulier, l'étude formelle des diffé r e n t e s s é m a n t i q u e s d e s p I M C s a p e r m i s d e p r o p o s e r d e s e n c o d a g e s e n contraintes succincts et performants. Enfin, nous concluons avec des expériences montrant l'amélioration de nos encodages en contraintes par rapport à ceux de l'état de l'art résolvant les mêmes problèmes sur les pIMCs.

Contexte et problématique

Un processus aléatoire est un système dans lequel le passage d'un état à un autre état est probabiliste : chaque état successeur a une certaine probabilité d'être choisi. Une chaîne de Markov à temps discret est un processus aléatoire dont le passage d'un état à un autre Modéliser une application comme une chaîne de Markov suppose de connaître exactement les probabilités pour chaque transition du système. Cependant, ces quantités peuvent être difficiles à calculer ou à mesurer pour des applications réelles (ex : erreurs de mesure, connaissance partielle). Les chaînes de Markov à intervalles (IMCs) étendent les chaînes de Markov en autorisant les probabilités de transition à varier dans des intervalles donnés. Ainsi, à chaque transition d'état à état est associé un intervalle au lieu d'une probabilité exacte.

Enfin, les chaînes de Markov à intervalles paramétrés (pIMCs) autorisent l'utilisation d'intervalles dont les bornes sont variables. Ces bornes variables sont alors représentées par des paramètres (ou des combinaisons de paramètres), ce qui permet notamment l'expression de dépendances entre plusieurs transitions du système. Ainsi, les pIMCs représentent, d'une manière compacte et avec une structure finie, un ensemble potentiellement infini d'IMCs. Par transitivité, les pIMCs permettent de représenter potentiellement une infinité d'ensembles de chaînes de Markov.

La propriété que nous allons vérifier est celle de l'accessibilité (en : reachability)d a n s les MCs. Formellement, la probabilité d'atteindre un état dans une MCs est donnée par la somme de la probabilité de tous les chemins atteignant l'état désiré (c'est-à-dire tous les chemins finis partant de l'état initial, terminant par l'état désiré et ne rencontrant pas cet état avant). De plus, la probabilité d'un chemin correspond aux produits des probabilités rencontrées sur les transitions état à état. Nous notons P M (3s)laprobabilit éd'atteindre un état s dans une MC M. Exemple 3. La figure 5 représente une MC M avec 5 états s 0 , s 1 , s 2 , s 3 et s 4 où s 0 est l'état initial et où nous pouvons lire par exemple que la probabilité de passer de l'état s 0 à l ' é t a t s 1 vaut 0.7e tq u ec e l l ed ep a s s e rd el ' é t a ts 0 à s 2 vaut 0.3. Ainsi les séquences d'états (s 0 ,s 1 ,s 3 ), (s 0 ,s 3 )e t( s 0 ,s 2 ,s 1 ,s 3 )s o n tt r o i sc h e m i n s( fi n i s )p a r t a n td el ' é t a t initial s 0 et terminant dans l'état s 3 ayant pour probabilités respectives 0.7 • 0.5=0 .35, 0.7•0=0et0.3•0.5•0.5=0.075 . Enfin, la probabilité d'atteindre l'état s 1 vaut p(s 0 )(s 1 )+ Σ +1 i=0 p(s 0 )(s 2 )•p(s 2 )(s 2 ) i •p(s 2 )(s 1 )=p(s 0 )(s 1 )+p(s 0 )(s Les pIMCs et les IMCs sont appelées des modèles d'abstractions de chaînes de Markov. En effet, comme dit précédemment, tout pIMC ou IMC représente/abstrait un ensemble de chaînes de Markov. Ainsi, nous disons qu'une chaîne de Markov satisfait une abstraction de chaînes de Markov ssi la chaîne de Markov appartient à l'ensemble des MCs représentées par l'abstraction. De plus, les IMCs sont formellement définies avec trois sémantiques d'abstractions : 1) once-and-for-all,2)IMDP et 3) at-every-step. La première sémantique définit que l'ensemble des MCs qui satisfont une IMC sont celles qui ont la même structure que l'IMC et dont la probabilité p de passer d'un état s accessible à un état s 0 appartient à l ' i n t e r v a l l e d e p r o b a b i l i t é s s u r l a t r a n s i t i o n d e s vers s 0 dans l'IMC. Nous disons que pour chaque intervalle de l'IMC une et une seule probabilité est sélectionnée. La seconde sémantique définit que l'ensemble des MCs qui satisfont une IMC sont celles qui autorisent de choisir plusieurs probabilités pour un même intervalle d'une IMC. Nous disons que l'IMC originale est "dépliée". Ainsi, un état d'une IMC peut se retrouver "copié" plusieurs fois dans la MC qui satisfait l'IMC. Enfin, la troisième sémantique autorise sous certaines conditions que certains états de l'IMC peuvent être fusionnés ou scindés en plusieurs états tout en autorisant le dépliage de l'IMC. Cette sémantique correspond à la sémantique originelle donnée aux IMCs. Nous montrons dans cette thèse que la sémantique at-everystep est plus générale que la IMDP, qui est plus générale que la once-and-for-all. Toutes ces sémantiques s'étendent aux pIMCs.

Ainsi, la partie contribution aborde trois problèmes majeurs de vérification sur les pIMCs : la consistance (existentielle),l ' accessibilité qualitative (existentielle) et l'accessibilité quantitative (existentielle). Le problème de la consistance d'une pIMC détermine si une pIMC admet au moins une MC qui la satisfait. Le problème de l'accessibilité qualitative détermine si pour un ensemble d'états à atteindre il existe une MC qui satisfait la pIMC où un des états but peut être atteint (c'est-à-dire qu'il existe un chemin avec une probabilité non nulle qui part de l'état initial de cette MC et atteint l'état but). Le problème de l'accessibilité quantitative détermine si, pour un ensemble d'états à atteindre et un seuil d'accessibilité, il existe une MC qui satisfait la pIMC où la probabilité d'atteindre les états buts est supérieure ou inférieure au seuil.

Modélisation et résolution en contraintes

Dans un premier temps, nous avons prouvé que les valeurs de probabilités maximales et minimales d'accessibilité d'états sont atteintes par les MCs de même structure que les IMCs/pIMCs. C'est grâce à ce théorème fort que nous avons pu proposer des modèles en contraintes succincts pour vérifier les problèmes présentés dans la précédente section. En effet, il n'est plus nécessaire de considérer toutes les MCs avec "dépliages" pour vérifier la consistance et les propriétés d'accessibilité qualitatives et quantitatives, mais uniquement les MCs de même structure que la pIMC. Nous présentons maintenant les modèles en contraintes proposés. Nos modélisations en contraintes sont modulaires. C'est-à-dire qu'un premier lot de contraintes résout le problème de la consistance, puis l'ajout d'un second lot de contraintes vient répondre au problème de l'accessibilité qualitative et l'ajout d'un dernier lot permet de répondre au problème de l'accessibilité quantitative. L'objectif de nos modèles en contraintes est de construire une chaîne de Markov qui satisfasse l'IMC vérifiant la propriété désirée (consistance, accessibilité qualitative ou accessibilité quantitative). Ainsi, nos modèles en contraintes encodent de telles MCs. Formellement, étant donnée une pIMC à vérifier et T un ensemble d'états à atteindre, nos modèles en contraintes définissent les variables ⇢ s , ! s , ↵ s , λ s , ⇡ s pour chaque état s de la pIMC, une variable φ p par paramètre p de la pIMC et une variable θ s 0 s par intervalle paramétré dans la pIMC. Rappelons que ces variables ont pour objectif de construire une MC. Chaque variable θ s 0 s détermine la probabilité de la transition allant de l'état s vers l'état s 0 dans la MC. Pour tout état s,l av a r i a b l eρ s est une variable booléenne indiquant si l'état s est accessible depuis l'état initial ; la variable ω s est une variable entière qui vaut k s'il existe un chemin de taille k -1d e p u i sl ' é t a ti n i t i a lv e r ss, et qui vaut 0 sinon ; la variable α s est une variable entière qui vaut k s'il existe un chemin de taille k -1d e p u i ss vers un état but s 0 dans T , et qui vaut 0 sinon ; la variable λ s est une variable booléenne qui vaut true ssi il existe un chemin depuis l'état initial vers un état but de T passant par s ; et la variable π s vaut la probabilité d'atteindre l'état s depuis l'état initial si s est accessible et qui vaut 0 sinon. Voici les contraintes à considérer pour chaque état s de la pIMC :

(1) ρ s , si s = s 0

(2) ¬ρ s , Σ s 0 2Pred(s)\{s} θ s s 0 =0, sis 6 = s 0

(3) ¬ρ s , Σ s 0 2Succ(s) θ s 0 s =0 (4) ρ s , Σ s 0 2Succ(s) θ s 0 s =1 (5) ρ s ) θ s 0 s 2 P (s, s 0 ), pour tout s 0 2 Succ(s) Nous montrons dans cette thèse que ces lots de contraintes permettent de répondre aux problèmes de la consistance existentielle (contraintes (1) à ( 5)), l'accessibilité qualitative existentielle (contraintes (1) à ( 10))e tl ' a c c e s s i b i l i t éq u a n t i t a t i v ee x i s t e n t i e l l e (contraintes (1) à ( 18)). De plus, nos modèles sont linéaires en taille par rapport à la taille de la pIMC là où les modèles de l'état de l'art sont exponentiels en taille. Nous terminons la contribution par une évaluation pratique de nos modèles en contraintes. Les contraintes sont linéaires (sauf la contrainte (18) qui est quadratique) et utilisent des expressions logiques comme l'équivalence et l'implication. Quant aux variables, nous sommes dans le cas mixte avec la présence de variables booléennes, entières et réelles. Ainsi, la communauté Satisfiability Modulo Theory se propose de résoudre ce genre de problèmes. Dans le cas linéaire il y a également la communauté Mixed Integer Linear Programming qui accepte nos CSPs. Nous sommes allés chercher un jeu de tests dans la communauté des MCs. Nous avons étendu ces MCs à des pIMCs et avons vérifié dessus les propriété de consistance, d'accessibilités qualitative et quantitative. Notre outil est disponible en ligne. 3 Nos résultats montrent que nos modèles en contraintes sont plus performants que ceux de l'état de l'art. En effet, nos modèles en contraintes gagnent un ordre de complexité en terme de taille ce qui permet de s'attaquer à des pIMCs beaucoup plus grandes (c'est-à-dire avec des dizaines de milliers d'états). Enfin, nous proposons un premier outil pour réaliser la vérification d'accessibilité quantitative sur des pIMCs. Pour cette propriété, nous parvenons à traiter des pIMCs ayant une centaine d'états.

(
Pour conclure, dans cette partie de la thèse, nous avons réalisé une analyse formelle de propriétés sur les abstractions de chaînes de Markov. Dans cette analyse, nous avons montré que les différentes sémantiques données aux IMCs sont équivalentes par rapport à l'accessibilité quantitative de probabilité maximale et minimale (ce qui s'étend aux pIMCs). Grâce à ce résultat, nous avons présenté des modèles en contraintes qui forment la première solution pratique au problème de l'accessibilité quantitative dans les pIMCs. Dans le même temps, nous avons amélioré les encodages en contraintes existants pour résoudre la consistance existentielle et l'accessibilité qualitative. Enfin, nous avons proposé un outil implémentant nos divers encodages en contraintes. Ces travaux ont fait l'objet de trois communications/publications [4,5,6].

Contents 1 . 1 5 1. 2 7 1. 3 8 1. 4

 11527384 Scientific Context ............................. Problems and Objectives ......................... Contributions ............................... Outline ................................... 9

  Empty 5⇥5 chessboard with 5 Queens.

  Queens positioning respecting "no threat" rules.

  Queens positioning violating twice the diagonal "no threat" rule.

Figure 2 . 1 : 5 -

 215 Figure 2.1: 5-Queens problem illustrated with: (a) its 5⇥5 empty chessboard and its 5 queens; (b) a queen configuration satisfying the 5-Queens problem; and (c) a queen configuration violating the 5-Queens problem.

Figure 2 . 2 :

 22 Figure 2.2: Three constraints c 1 , c 2 and c 3 over two variables x and y.

1 :

 1 function satisfaction(P =(X, D, C):CSP) return Map<X,D>

Definition 2 . 3 . 1 (

 231 Reformulation). Le C be a CSP. A reformulation ⇢ transforms a CSP C into a CSP C 0 s.t. all the solutions of C can be mapped to a solution in C 0 and all the solutions of C 0 are translatable as a solution C. Thus, C 0 models the same problem than C.

Figure 2 . 3 :

 23 Figure 2.3: Box Paving for a Constraint Satisfaction Problem. Gray boxes only contain solutions. Pink boxes contains at least one solution. The union of the gray and the pink boxes covers all the solutions.

  ................................ 3.2 Abstract Interpretation .......................... 3.3 Model Checking .............................. 3.4 Constraints meet Verification .......................

Figure 3 . 1 :

 31 Figure 3.1: Instance of four possible traces of a variable x while executing the same program.

Figure 3 . 2 :

 32 Figure 3.2: Instance of four possible traces of a variable x while executing the same program.

Figure 3 . 3 :

 33 Figure 3.3: Running program example with its five traces.

  Polyhedron AbstractProving the no forbidden zone overlapping.

Figure 3 . 4 :

 34 Figure 3.4: A concrete domain (a) over variables x and y abstracted by an interval abstract domain (b) and a polyhedron abstract domain (c) respectively without (a,b,c) and with (d,e,f) a forbidden zone s.t. interval abstraction produces a false alarm (e) while polyhedron abstraction proves safety (f).

  pref ix 1 : ABBD 0.168 pref ix 2 : ACBD 0.09 pref ix 3 : ACCB 0.075 pref ix 4 : ACEE 0 pref ix 5 : EEEE 0 (b) 5 trace prefixes with their respective probability to occur.

Figure 3 . 5 :

 35 Figure 3.5: A Markov chain next to 5 trace prefixes with size 4, associated with their respective probability to occur.

Definition 4 . 2 . 1 (

 421 Block). Let E be a nonempty set. A block over E is a triple b = (op, n, m) such that: n 2 N is the number of inputs of the block, m 2 N is the number of outputs, and op : E n ! E m is the operator of the block. The n inputs and the m outputs are ordered: [i]b refers to the ith input (1  i  n) and b[j] to the jth output (1  j  m).

Definition 4 . 2 . 2 (

 422 Connector). Let B be a set of blocks. A connector over B is a pair (b[i], [j]b 0 ) such that: b and b 0 are blocks from B; output i exists for block b and input j exists for block b 0 . Definition 4.2.3 (Block-Diagram). Let E be a nonempty set. A block-diagram over E is a pair d =( B, C) such that: B is a set of blocks over E and C is a set of connectors over B. An input (respectively output) of a block in B that does not appear in a connector of C is an input (respectively an output) of the block-diagram d. Similarly to the blocks, if a block-diagram d has n inputs and m outputs, we can order them and: [i]d refers to the ith input (1  i  n), and d[j]tothejth output (1  j  m). Finally, we denote BD(E)t h es e to fa l lt h eb l oc k -d i a g r a m so v e rE. Example 14.

Figure 4 .

 4 1 depicts a block-diagram over real numbers in Block(R)c o ntaining three blocks: block b 1 has the square function as operator; block b 2 has the subtraction, and block b 3 has the multiplication. Connectors are represented by arrows: connector

Definition 4 . 2 . 4 (

 424 Interpretation). Let E be a nonempty set, b =( op, n, m) a block in Block(E), and d =(B, C) a block-diagram in BD(E).A ninterpretation I of block b is a mapping from each input i to an element in E (noted I([i]b)), and a mapping from each output j to an element in E (noted I(b[j])). An interpretation I of the block-diagram d is an interpretation of each block in B.

Definition 4 . 2 . 5 (

 425 Model). Let E be a nonempty set, b =(op, n, m) a block in Block(E), and d =(B, C) a block-diagram in BD(E). • An interpretation I of block b is a model of b iff op(I([1]b),...,I([n]b)) = (I(b[1]),...I(b[m])) • An interpretation I of block-diagram d is a model of d iff 8b 2 B : I is a model of b and 8(b[i], [j]b 0 ) 2 C : I(b[i]) = I([j]b 0 ) Example 15 (Example 14 continued). A block-diagram interpretation is presented in Figure 4.2. The interpretation is given by labeling all the inputs and all the outputs. For instance, I([1]b 2 )equals4andI(b 3 [1]) equals 12. Moreover, this interpretation is a model of the block-diagram expressing that the input 2, 1 produces the output 12. Note that a block-diagram can have one or many models. The model presented in Example 15 is one among an infinity of possible ones.

Figure 4 . 2 :

 42 Figure 4.2: A block-diagram in BD(R) labeled with an interpretation

Definition 4 . 2 . 7 (

 427 Functional Block). Let D be a nonempty set, and b =( op, n, m) in Block(S(D)). b is a functional block iff 9f : D n ! D m such that 8s 1 ,...,s n ,s 0 1 ,...,s 0 m 2 S(D): op(s 1 ,...,s n )=(s 0 1 ,...,s 0 m ) implies the following: 8t 2 N,f(s 1 (t),...,s n (t)) = (s 0 1 (t),...,s 0 m (t)) Definition 4.2.8 (Followed-by Block). Let D be a nonempty set. The followed-by block over D (written fby) is the block (op, 2, 1) in Block(S(D)) such that op is the function from S(D) ⇥ S(D) to S(D) where op(a, b)=c, c(0) = a(0), and c(t)=b(t -1), for all t>0.Example 16.

Figure 4 .

 4 3 shows a block-diagram d over real-number streams: d 2

Figure 4 . 3 :

 43 Figure 4.3: A block-diagram over streams from BD(S(R)). In brackets, the first values of the model for t =0, 1, 2, 3.

Example 17 (

 17 Example 18 continued). Block-diagram d over real-number streams in Figure 4.3 contains one cycle which contains one fby block. This block-diagram admits only one model/trace. Indeed, using the three constant blocks 0, 0.1a n d0 .9fi x e sa l lt h e values in the cycle. Values for the 4 first time steps of the model are attached to each connector (note the delay due to the fby block). Values for the 21 first time steps are presented in Figure 4.4. Note the delay between the output of the block + and the output of the fby block: the height of the circle corresponds to the height of the square at the previous time step.

  Problem Definition. Let D be a nonempty set and d be a block-diagram in BD(S(D)). Associate to each block input/output s in d as u b s e tS of D s.t. for each model/trace I of d and for each time step t in N the value s(t)isinS. S is called an over-approximation of s in d. Over-Approximation Quality. Let D be a nonempty set, d be a block-diagram in BD(S(D)), s be a block input/output in d,a n dS, S 0 subsets of D be two overapproximations of s in d. If S ✓ S 0 then the over-approximation S is preferred to the over-approximation S 0 . Example 18 (Example 17 continued). Interval [0, 1] contains all the values taken by the streams model of the outputs for the blocks +, ⇥ and fby for the first 21 time steps in the block-diagram in Figure 4.3. Interval [0.1, 0.9] is a better over-approximation than [0, 1] for the output of the block + for the 21 first time steps.We introduce the temporal abstraction of streams in Definition 4.3.1. The temporal abstraction of a stream returns the set of all values taken by this stream. This set (and any superset) is called an over-approximation of the stream. As said previously, the size of this

Figure 4 . 4 :

 44 Figure 4.4: Values of the streams model of the block-diagram in Figure 4.3 for the outputs of blocks ⇥,+ ,a n dfby for the 21 first time steps.

Figure 4 . 5 :

 45 Figure 4.5: A block-diagram over streams from BD(S(R)) with connectors labelled by variables

Figure 4 . 6 :

 46 Figure 4.6: Naive constraint model for the block-diagram in Fig 4.5

Figure 4 . 7 :

 47 Figure 4.7: Medium constraint model for the block-diagram in Fig 4.5

Definition 4 .

 4 3.2 introduces Constraint Satisfaction Problems. We propose to model as aC S Pt h es t r e a mo v e r -a p p r o x i m a t i o np r o b l e m . B l o c k -d i a g r a m sc o m p u t eo u t p u t sf r o m inputs. To determine over-approximations of the streams in a block-diagram (B, C)i nBD(S(D)), we associate to each input and to each output from the blocks in B a variable with domain S(D). Then, for each block in B we consider its operator as a constraint linking the block outputs to the block inputs. Furthermore, for each connector in C, we add a constraint to ensure the equality of its streams. We name naive model this model using variables over streams. Example 19 presents the naive model on our running example.Example 19 (Example 18 continued).

  Figure 4.5 contains the same block-diagram as in Example 18 with constraint variables associated to the inputs and the outputs. Note that in our example, variables have been unified per connectors (e.g.,[ 1 ] +=⇤[1] = b). About the constraint programming model, the block with the operator + computes c as af u n c t i o no fb and d, yielding the constraint: c = b + d.

Figure 4 .

 4 6 shows the constraint model over streams for our example.

  Definition 4.3.3 (Interval Extension Function). Let D be a nonempty set and f be a function from S(D) n to S(D) m with n, m 2 N. An interval extension function of f , is a function

  3.4). For instance consider the constraint a = b+c over intervals. The function f (A, B, C)=(A\(B+C),B\(A-C),C\(A-B)) is apropagatorforthisconstraint. Ifthedomainsforthevariablesa, b,andc are respectively [-1, 4], [-1, 3], and [0, +1] then the propagator f reduces the domains for the variable a, b,a n dc to respectively [-1, 4], [-1, 3] and [0, 5]. Definition 4.3.4 (Constraint Propagator). Let (X, D, C) be a CSP with X = {x 1 ,...,x n }, and let c be a constraint in C defined over the set of variables X 0 ✓ X. A propagator f for the constraint c is a function from P(D) to P(D) such that f (D 0 x 1 ,...,D 0 xn )=D 00 x 1 ,...,D 00 xn with

Figure 4 .

 4 Figure 4.7 shows the medium constraint model for the block-diagram in Figure 4.5 constructed from its naive constraint model over streams in Figure 4.6.S o l v i n g t h i s constraint model computes an interval over-approximation of each stream, provided that the interval extensions of the functions are correct. Therefore, this translation of blockdiagrams into a constraint problem allows to compute hulls (over-approximations) of the streams.

Figure 4 . 8 :

 48 Figure 4.8: Dependency graph of the block-diagram in Figure 4.5 where strongly connected components are surrounded with dashed lines

Figure 4 . 9 :

 49 Figure 4.9: Optimized model of the block-diagram in Figure 4.5

Definition 4 . 4 . 1 (

 441 Dependency Graph). Let E be a nonempty set, and d =( B, C) be a block-diagram in BD(E). The dependency graph of d is the directed graph G =( V, A) in which each node of V corresponds to a different block from B such that |V | = |B| and each arc of A corresponds to a different connector from C such that |A| = |C|.

Definition 4 . 4 . 2 (

 442 Loop Transfer Function). Let d be a cycle block-diagram in BD(S(D)) and X = {x 1 ,...,x k } be a set of blocks inputs or outputs from d called argument. F : D k 7 ! D k is a loop transfer function of d for argument X,i ff for all I model of d and for all t in N:

1 :

 1 function minimalCausalSet(G : Graph) return Set<Vertex> 2:

Proposition 1 .

 1 Let D be a nonempty set, d =( B, C) be a block-diagram in BD(S(D)) and F be a loop transfer function (extended to intervals) of d with argument X of size k.

  and(w n ) n2N be the sequences of values taken respectively by the variables "min", "current", and "max"ateac hev aluationoftheloopcondition(line 8) during an execution of Algorithm 3 with a function F from I(D) k to I(D) k (k 2 N). Note that values for u n , v n ,a n dw n are in I(D) k . Let n 2 N and i 2 {1,...,k} we write u n [i], v n [i], and w n [i]t h eith interval in u n , v n , and w n respectively. Then we have u n [i], v n [i], and w n [i] belonging to I(D).

1 :

 1 function overApproximation(f : I(D) k ! I(D) k ) return List<I(D)> , max, image : List<I(D)> 4:

Figure 4 . 10 :

 410 Figure 4.10: FAUST Compilation Scheme

  ----------------------------------------------// Title : Volume control in dB // Remark : extracted from Faust examples //----------------------------------------------import (" music . lib" ); smooth ( c ) = * (1-c) : +˜ * (c) ; // vslider :default value : 0 // range between : -70 and +4 // range with a step of : 0.1 gain = vslider (" [1]" ,0 ,-70, +4, 0.1) :d b 2 l i n e a r:s m o o t h ( 0 . 9 9 9 ) ; process = * (gain);

Figure 4 Figure 4 . 12 :0=R

 4412 Figure 4.11: FAUST Volume Controller Source Program

Figure 5 . 1 :

 51 Figure 5.1: MC M 1

Definition 5 . 3 . 1 (

 531 Markov chain Abstraction Model). A Markov chain abstraction model (an abstraction model for short) is a pair (L, |=) where L is a nonempty set and |= is a relation between MC and L. Let P be in L and M be in MC we say that M implements P iff (M, P) belongs to |= (i.e., M| = P). When the context is clear, we do not mention the satisfaction relation |= and only use L to refer to the abstraction model (L, |=).

  Figure 5.2: pMC I 0

Figure 5 .

 5 Figure 5.3: IMC I

Figure 5 . 4 :Figure 5 . 5 :

 5455 Figure 5.4: MC M 2 satisfying the IMC I from Figure 5.3 w.r.t. |= d I

( 1 )

 1 Proof. Let I =( S, s 0 ,P,V)b ea nI M Ca n dM =( T,t 0 , p, V 0 )b ea nM C .W es h o wt h a t (1) M| = o I I ) M| = d I I;( 2 )M| = d I I ) M| = a I I; (3) in general M| = d I I 6 ) M| = o I I; (4) in general M| = a I I 6 ) M| = d I I. This will prove that |= a I is strictly more general than |= d I and that |= d I is strictly more general than |= o I . At the same time, note that the following examples also illustrates that even if a Markov chain satisfies an IMC with the same graph representation w.r.t. the |= a I relation it may not verify the |= o I relation. If M| = o I I then by definition of |= o I we have that T = S, t 0 = s 0 , V (s)=V 0 (s)f o r all s 2 S,a n dp(s)(s 0 ) 2 P (s, s 0 )f o ra l ls, s 0 2 S. The mapping ⇡ from T = S to S being the identity function is such as required by definition of |=

  d

3 Figure 5 . 6 :

 356 Figure 5.6: IMC I, MCs M 0 1 , M 0 2 ,a n dM 0 3 s.t. M 0 1 |= a I I, M 0 1 |= d I I and M 0 1 |= o I I; M 0 2 |= d I I and M 0 2 6 |= o I I; M 0 3 |= a I I and M 0 3 6 |= d I I; the graph representation of I, M 0 1 , and M 0 3 are isomorphic;

  as required by definition of |= a I (consider for each state in T the correspondence function δ : T ! (S ! [0, 1]) s.t. δ(t)(s)=1if⇡(t)=s and δ(t)(s)=0otherwise). Th usM| = a I I. (3) Consider IMC I and MC M 0 2 from Figure 5.6. By definition of |=

Figure 5 .

 5 Figure 5.7: pIMC P

Example 30 .

 30 They are written |= a pI , |= d pI ,a n d|= o pI and defined as follows: M| = a pI P (resp. |= d pI , |= o pI )i ff there exists an IMC I instance of P such that M| = a I I (resp. |= d I , |= o I ). Consider the pIMC P =( S, s 0 ,P,V,Y) given in Figure 5.7. The set of states S and the labelling function are the same as in the MC and the IMC presented in Figures 5.1 and 5.3 respectively. The set of parameters Y has two elements p and q.

Figure 5 . 8 :

 58 Figure 5.8: IMC I with three pMCs P 1 , P 2 ,a n dP n entailed by I w.r.t. |= a I .

Figure 5 . 10 :Figure 5 .

 5105 Figure 5.10: Variables in the CSP produced by C 9c for the pIMC P from Fig. 5.7

5. 5 . 1

 51 Equivalence of |= o I , |= d I and |= a I w.r.

3 Figure 5 . 12 :

 3512 Figure 5.12: An IMC I and three MCs M 1 , M 2 ,a n dM 3 satisfying I w.r.t. |= a I s.t. P M 1 (3↵)  P M 2 (3↵)  P M 3 (3↵)a n dM 3 has the same structure as I.

Lemma 4 .

 4 Let I =( S, s 0 ,P,V) be an IMC, M be an MC satisfying I w.r.t. |= a I , and ↵ ✓ A be a proposition. There exist MCs M 1 and M 2 satisfying I w.r.t. |= o I such that P M 1 (3↵)  P M (3↵)  P M 2 (3↵).

  C 0 9r (P, ↵)=( X [ X 0 ,D [ D 0 ,C [ C 0 )b es u c ht h a t( X, D, C)=C 9r(P), X 0 contains one Boolean variable λ s and one integer variable ↵ s with domain [0, |S|] per state s in S, D 0 contains the domains of these variables, and C 0 is composed of the following constraints for each state s 2 S:

state ρ s ω s α s λ s s 0 true 13true s 1 true 22true s 2 true 20false s 3 true 31true s 4 true 30false Figure 5 . 7 ( 11 )

 30false5711 Figure 5.13: A solution to the CSP C 0 9r (P, {↵, β})f o rt h ep I M CP from Fig. 5.7

Proposition 8 .

 8 Let P =( S, s 0 ,P,V,Y) be a pIMC and ↵ ✓ A be a state label. There exists an MC M| = a pI P iff there exists a valuation v solution of the CSP C 0 9r (P, ↵) s.t. for each state s 2 S: v(λ s ) is equal to true iff P M s (3↵) 6 =0. Example 32. Figure 5.13 presents a solution to the CSP C 0 9r (P, {↵, β})f o rt h ep I M C P from Figure 5.7.

  Figure 5.14: nand K=1; N=3 benchmark formulated in the PRISM adapted from[START_REF] Kwiatkowska | PRISM 4.0: Verification of Probabilistic Real-time Systems[END_REF].

Figure 5 . 15 :

 515 Figure 5.15: Comparing encoding time for the existential consistency problem

Figure 5 . 16 :

 516 Figure 5.16: Comparing solving time for the existential consistency problem Figure 5.17: Comparing solving time between SMT and MILP formulations

Figure 1 :Exemple 1 .

 11 Figure 1: A block-diagram over streams from BD(S(R)). In brackets, the first values of the model for t =0, 1, 2, 3.

Figure 2 :

 2 Figure 2: CSP C 1 produit par notre modèle en contraintes naïf pour le diagramme de blocs de la figure 1

Figure 3 :

 3 Figure 3: CSP C 2 produit par notre modèle en contraintes intermédiaire pour le diagramme de la figure 1

Figure 4 :

 4 Figure 4: CSP C 3 produit par notre modèle en contraintes final pour le diagramme de blocs de la figure 1

Exemple 2 .

 2 La figure 2 contient le CSP C 1 résultant de notre modélisation en contrainte naïve pour le diagramme de blocs d présenté dans la figure 1. Notez en premier, que chaque connecteur a été associé à une variable. Par exemple, les sorties des blocs constants 0.1, 0 et 0.9 correspondent aux variables d, e et f dans le CSP. De plus, chaque bloc produit une contrainte dans le CSP (nous utilisons une notation préfixée pour l'écriture des opérateurs en contraintes). Par exemple le bloc fby du diagramme de blocs d produit la contrainte a =fby(e, c)dansC 1 . Ainsi, nous avons que toute solution de C 1 correspond à une exécution de d. Ensuite, la figure 3 contient le CSP C 2 produit par notre modélisation en contrainte intermédiaire pour le diagramme de blocs d. Étant donné un opérateur sur des flux, la notation [f ] correspond à l'extension aux intervalles en tant que contrainte de la fonction f . Par exemple, a =[ 0 , 1], b =[ 2 , 3] et c =[ 2 , 4] satisfait la contrainte a[+]b = c.D e fait, le passage de C 1 à C 2 ar e m p l a c él e sd o m a i n e sd efl u xàd e sd o m a i n e sài n t e r v a l l e s , et les opérateurs dans les contraintes sont remplacés par leurs extensions aux intervalles. Ainsi, pour toute variable x de C 1 , pour toute solution de C 2 l'intervalle choisi pour x contient toutes les valeurs des flux solutions de C 1 pour la variable x (c'est-à-dire pour toute valuation v 2 solution de C 2 et pour toute valuation v 1 solution de C 1 nous avons v 1 (x)(t) 2 v 2 (x)p o u rt o u tt 2 N). Enfin, la figure 4 contient le CSP C 3 utilisant notre contrainte globale real-time-loop . Cette contrainte prend trois arguments qui sont, dans l'ordre : les contraintes formant le circuit, les variables d'entrées du circuit, les variables de sorties du circuit. Ainsi dans C 1 la contrainte real-time-loop contient les blocs fby, ⇥ et +, les entrées d, e et f et n'a pas de sorties.

  Figure 5: Exemple de MC

Figure 6 :

 6 Figure 6: Exemple d'IMC s 0

Figure 7 :

 7 Figure 7: Exemple d'IMC

  2 )•p(s 2 )(s 1 )• (1/(1-p(s 2 )(s 2 ))) = 1. A côté, la figure 6 représente une IMC I. Puisque M al am ê m es t r u c t u r eq u eI et que les probabilités des transitions de M appartiennent aux intervalles correspondants dans I nous disons que M satisfait I. Pour terminer, la figure 7 représente une pIMC utilisant deux paramètres p et q. Notons que choisir les valeurs 0.6p o u rp et 0.5p o u rq produit l'IMC I. Nous disons que I implémente P. De fait, puisque M satisfait I et que I implémente P nous disons que M satisfait P.

  components are surrounded with dashed lines ............................................ 4.9 Optimized model of the block-diagram in Figure 4.5 ............... 4.10 FAUST Compilation Scheme ............................ 4.11 FAUST Volume Controller Source Program ................... 4.12 FAUST volume controller block-diagram before normalization. Edges are labeled with their corresponding variables in the CSP in Fig. 4.13b . . . . . . . 63 4.13 CSP for the volume benchmark ......................... 5.1 MC M 1 ....................................... 5.2 pMC I 0 ....................................... 5.3 IMC I ........................................ 5.4 MC M 2 satisfying the IMC I from Figure 5.3 w.r.t. |= d I ............ 5.5 MC M 3 satisfying the IMC I from Figure 5.3 w.r.t. |= a I ............ 5.6 IMC I, MCs M 0 1 , M 0 2 ,a n dM 0 3 s.t. M 0 1 |= a I I, M 0 1 |= d I I and M 0 1 |= o I I; M 0 2 |= d I I and M 0 2 6 |= o I I; M 0 3 |= a I I and M 0 3 6 |= d I I; the graph representation of I, M 0 1 ,a n dM 0 3 are isomorphic; ........................ 5.7 pIMC P ....................................... 5.8 IMC I with three pMCs P 1 , P 2 ,a n dP n entailed by I w.r.t. |= a I . ....... 5.9 pMC P, IMC I, MC M 1 , and MC M 2 s.t. M 1 |= p P and M 1 |= a I I but M 2 6 |= p P and M 2 |= a I I while P is entailed by I w.r.t. |= a I . .............................. 5.10 Variables in the CSP produced by C 9c for the pIMC P from Fig. 5.7 .....

Table 2 .

 2 1: Complexity for the Constraint Satisfaction Problem Classes containing Linear and Non-Linear Constraints Problems over Real, Integer, Mixed, and Finite variables. CSP for short) is a triplet P =(X, D, C) where X is a set of variables, D contains the domains associated to the variables in X, and C is a finite set of contraints over variables from X.

		Real var. Integer var.	Mixed var.	Finite var.
	Linear	P	NP-complete NP-complete NP-complete
	Non-linear decidable undecidable	undecidable NP-complete
	Definition 2.2.1 (Constraint Satisfaction Program). A Constraint Satisfaction Program
	(

Table 4 .

 4 2: A trace table of Algorithm 3 for the transfer function F . still correct for the n +1th iteration. There are 4 cases depending on the variable states and current (i.e., v

n ):

1. state =" I n c r e a s i n g "a n dF (v n ) ✓ v n 2. state =" I n c r e a s i n g "a n dF (v n ) 6 ✓ v n 3. state =" D e c r e a s i n g "a n dF (v n ) ✓ v n 4. state =" D e c r e a s i n g "a n dF (v n ) 6 ✓ v n Consider the first case. Condition in line 12 is true. This sets the variable state to "Decreasing" and the variable switch to "true". Next, in the for statement only the condition in line 21 is true. Thus, for all i 2 {1,...,k}:

max[i] is updated to current[i] (i.e., w n+1 [i]=v(n)[i]); current[i]

is updated to an interval between min[i] and its current value (i.e., u n

[i] ✓ v n+1 [i] ✓ v n [i]

) and such interval exists by the inductive hypothesis v n ✓ u n ✓ w n ;a n dmin[i] is unchanged (i.e., u n+1 [i]=u n [i]). Finally we obtain by aggregation that u n+1

Table 4 . 4

 44

			#cstrs	real-time-loop	Time (in ms)		Verification
			medium	optim.		max.	max.	comp.	comp.		solver
	Program name counter paper-example sinus first-order-filter noise allpass-filter volume comb-filter echo stereo-echo pink-noise capture karplus-strong oscillator band-filter	#var 8 11 9 15 16 16 19 20 29 37 40 45 49 49 55	model 63 model # 141 cstrs args 73 151 74 141 10 6 151 10 6 151 11 6 161 11 7 151 15 5 1 11 1 19 15 151 26 18 251 28 15 2 10 1 34 21 361 35 18 381 35 23 361 42 34 191	medium 16 17 15 35 16 18 25 18 27 28 27 27 30 30 38	optim. solve 460 7 458 7 462 7 473 9 454 8 470 9 473 7 462 7 482 8 495 12 493 7 488 14 484 9 497 11 546 11	output [0; MAX] [0; 1] [-1; 1] [-1; 1] [-1; 1] [-3; 3] [-1.58; 1.58] [-oo; +oo] [-oo; +oo] [-oo; +oo] [-oo; +oo] [-oo; +oo] [-oo; +oo] [-1; 1] [-oo; +oo]	p p p p p p p p p p p p p p p
	lowboost	59	46	38	191	33	508 10	[-oo; +oo] ?
	pitch-shifter	60	50	46	151	32	510	8 [-59902;59902] ?
	smooth-delay	100	85	25	3	43	4	40	789 17	[-oo; +oo] ?
	mixer	356	310	234 19	5	1	65	824 49 [-20.01;20.01] ?
	freeverb	371	335	103 24	13	1	69	994 41	[-oo; +oo] ?
	harpe add-synth-5-oscs add-synth-10-oscs add-synth-50-oscs add-synth-100-oscs 1,530 1,320 814 102 407 348 197 24 106 85 54 761 8 1 181 150 94 12 6 1 780 670 414 52 6 1 6 1 add-synth-250-oscs 3,780 3,270 2,014 252 6 1 add-synth-500-oscs 7,530 6,520 4,014 502 6 1 add-synth-750-oscs 11,280 9,770 6,014 752 6 1 add-synth-1000-oscs 15,030 13,020 8,014 1,002 6 1	76 84 110 244 1,108 86 935 52 605 15 689 17 609 1.6s 314 2.5s 4.5s 1.6s 12.5s 17.3s 10.1s 39.8s 1'18s 48.8s 1'25s 2'43s 2'34s	[-oo; +oo] ? [-1; 1] p [-1; 1] p [-1; 1] p [-1; 1] p [-1; 1] p [-1; 1] p [-1; 1] p [-1; 1] p

: Experimental results on a benchmark of FAUST programs

  )=s 2 , and ⇡(t 2 0 )=s 2 . Let p be the transition function of M 0 2 and P be the interval probability transition function of I. Clearly, we have that p(t)(t 0 ) 2 P (⇡(t), ⇡(t 0 )). Indeed, the relation R containing (t 0 ,s 0 ), (t 1 ,s 1 ), (t 1 ,s 2 ), (t 2 ,s 1 )a n d (t 2 ,s 2 )i sas a t i s f a c t i o nr e l a t i o nb e t w e e nI and M 0

	d I we have that
	M 0 2 |= d
	On the other hand, it is clear that M 0 2 6 |= o I I since M 0 2 and I do not share the same state space.
	(4) Consider IMC I and MC M 0 3 from Figure 5.6. By definition of |= a I we have that M 0 3 |= a I I.

I I. Indeed, consider the mapping ⇡ s.t. ⇡(t 0 )=s 0 , ⇡(t 1 )=s 1 , ⇡(t 2

  .3 is an instance of P (by assigning the value 0.6totheparameter p and 0.5t oq). Furthermore, as said in Example 29, the Markov Chains M 1 and M 2 (from Figures 5.1 and 5.5 respectively) satisfy I w.r.t. |= a I , therefore M 1 and M 2 satisfy P w.r.t. |= a pI .

  Our comparison results are presented in Proposition 4. Firstly, Lemma 1 states that IMC and pMC are not comparable w.r.t. satisfaction relations Proof. We give a sketch of proof for each statement. Let (L 1 , |= 1 )a n d( L 2 , |= 2 )b et w o Markov chain abstraction models. Recall that according to the succinctness definition (cf. Definition 5.3.6) L 1 6  L 2 if there exists L 2 2 L 2 s.t. L 1 6 ⌘ L 2 for all L 1 2 L 1 .

	|= o I , |= d I ,a n d|= a I .
	Lemma 1. pMC and IMC abstraction models are not comparable in terms of succinctness:
	(1) pMC 6  (IMC, |= a I ), (2) pMC 6  (IMC, |= d I ), (3) pMC 6  (IMC, |= o I ), (4) (IMC, |= a I ) 6  pMC, (5) (IMC, |= d I ) 6  pMC, and (6) (IMC, |= o I ) 6  pMC.

(1) Consider IMC I and pMCs P 1 , P 2 ,a n dP n (with n 2 N) from Figure 5.8. IMC I verifies the case (1). Indeed, the pMCs P 1 , P 2 ,an dP n (with n 2 N)areallen tailed by I w.r.t. |= a I but none of them is equivalent to I. Indeed one needs an infinite

  Figure 5.9: pMC P, IMC I, MC M 1 , and MC M 2 s.t. M 1 |= p P and M 1 |= a I I but M 2 6 |= p P and M 2 |= a I I while P is entailed by I w.r.t. Same example than from case (1) using Figure 5.8 can be used since all the pMCs P 1 , P 2 ,a n dP n (with n 2 N)a r ee n t a i l e db yt h eI M CI w.r.t. |= d Recall that the pIMC model is a Markov chain abstraction model allowing to declare parametric interval transitions, while the pMC model allows only parametric transitions (without intervals), and the IMC model allows interval transitions without parameters.

	4	1/3
	2/3
	MC M 2
	|= a I .
	I . However countable number of states for creating a pMC equivalent to I w.r.t. |= a state spaces must be finite.
	(2)

I

(3) Consider IMC I 0 similar to I from Figure

5

.8 excepted that the transition from s 1 to s 0 is replaced by the interval [0.5, 1]. Since the pMC definition does not allow to bound values for parameters there is no equivalent I 0 w.r.t. |= a I . (4) Note that parameters in pMCs enforce transitions in the concrete MCs to receive the same value. Since parameters may range over continuous intervals there is no hope of modelling such set of Markov chains using a single IMC. Figure 5.9 illustrates this statement. (5) Same remark than item (4) (6) Same remark than item (4) Proposition 4. The Markov chain abstraction models can be ordered as follows w.r.t. succinctness: (pIMC, |= o pI ) < (pMC, |= p ), (pIMC, |= o pI ) < (IMC, |= o I ), (pIMC, |= d pI ) < (IMC, |= d I ), and (pIMC, |= a pI ) < (IMC, |= a I ).

Proof.

  1. We first prove the equivalence w.r.t. |= o I and |= a I . Recall also that |= a I is more general than |= o I : for all MC M if M| = o I I then M| = o I I (Proposition 3). P I (3↵)⇠p with the at-every-step semantics implies that there exists an MC M s.t. M| = a I I and M⇠p. Thus by Lemma 4 we get that there exists an MC M 0 s.t. M 0 |= o I I and M 0 ⇠p. P I (3↵)⇠p with the IMDP semantics implies that there exists an MC M s.t. M| = d I I and M⇠p. Since |= a I is more general than |= d I we have that M| = a I I. Thus by Lemma 4 we get that there exists an MC M 0 s.t. M 0 |= o I I and M 0 ⇠p.

	[)] Direct from the fact that |= a I is more general than |= o I (Proposition 3)
	[(] 2. We now prove the equivalence w.r.t. |= o I and |= d I
	[)] Direct from the fact that |= a I is more general than |= o I . (Proposition 3)
	[(]

  be a probability bound. Adding the constraint ⇡ s 0  p (resp. ⇡ s 0 ≥ p)t ot h ep r e v i o u sC 9r encoding allows to determine if there exists a MC M| = a pI P

			#intervals	#paramInBounds
	Set of benchmarks	#pIMCs #nodes #edges min avg max min avg max #parameters
	herman N=3 herman N=5 herman N=7 egl L=2; N=2 egl L=2; N=4 egl L=4; N=2 egl L=4; N=4 brp M=3; N=16 brp M=3; N=32 brp M=4; N=16 brp M=4; N=32 crowds CS=10; TR=3 crowds CS=5; TR=3 nand K=1; N=10 nand K=1; N=5 nand K=2; N=10 nand K=2; N=5	27 27 27 27 27 27 27 27 27 27 27 27 27 27 27 27 27	8 32 128 238 6,910 7,165 696 1,897 3,619 55 444 1,405 28 0 7 18 0 3 11 244 19 50 87 0 12 38 2,188 37 131 236 3 31 74 253 16 67 134 0 15 57 494 509 47 136 276 3 32 115 15,102 15,357 1448 4,068 7,772 156 951 3,048 886 1,155 16 64 135 1 15 45 1,766 2,307 40 128 275 3 32 129 1,095 1,443 22 80 171 0 20 62 2,183 2,883 49 164 323 3 39 139 6,563 15,143 1,466 3,036 4,598 57 235 535 1,198 2,038 190 410 652 8 31 76 7,392 11,207 497 980 1,416 109 466 1,126 {50, 100, 250} {2, 5, 10} {2, 5, 10} {5, 15, 30} {2, 5, 10} {2, 5, 10} {2, 5, 10} {2, 5, 10} {2, 5, 10} {2, 5, 10} {2, 5, 10} {2, 5, 10} {5, 15, 30} {5, 15, 30} 930 1371 60 121 183 9 58 159 {50, 100, 250} 14,322 21,567 992 1,863 2,652 197 866 2,061 {50, 100, 250} 1,728 2,505 114 217 329 23 101 263 {50, 100, 250}

Table 5 .

 5 1: Benchmarks comp osed of 459 pIMCs over 5 families used for verifying qualitative properties such that P M (3↵)  p (resp ≥ p). Formally, let ⇠2{,<,≥,>} be a comparison operator, we write 6 ⇠ for its negation (e.g., 6  is >). This leads to the following theorem.Theorem 2. Let P =(S, s 0 ,P,V,Y) be a pIMC, ↵ ✓ A be a label, p 2 [0, 1], ⇠2{,< , ≥,>} be a comparison operator, and (X, D, C) be C 9r (P, ↵):Proof. Let P =( S, s 0 ,P,V,Y)b eap I M C ,↵ ✓ A be a state label, p 2 [0, 1], and ⇠2{,<,≥,>} be a comparison operator. Recall that C 9r (P, ↵)i saC S Ps . t . e a c h solution corresponds to an MC M satisfying P where ⇡ s 0 is equal to P M (3↵). Thus adding the constraint ⇡ s 0 ⇠ p allows to find an MC M satisfying P such that P M (3↵) ⇠ p. This concludes the first item presented in the theorem. For the second item, we use Theorem 1 with Proposition 9 which ensure that if the CSP C 9r (P, ↵)t ow h i c hi sa d d e d the constraint ⇡ s 0 6 ⇠ p is not satisfiable then there is no MC satisfying P w.r.t. |= a pI such that P M (3↵) 6 ⇠ p;t h u sP M (3↵) ⇠ p for all MC satisfying P w.r.t. |= a pI .

	• CSP (X, D, C [ (⇡ s 0 ⇠ p)) is satisfiable iff 9M| = a pI P s.t. P M (3↵) ⇠ p
	• CSP (X, D, C [ (⇡ s 0 6 ⇠ p)) is unsatisfiable iff 8M| = a pI P: P M (3↵) ⇠ p

Table 5 .

 5 2: Benchmarks comp osed of 4 pIMCs used for verifying quantitative prop erties

		Size of the Boolean Integer Real-number Boolean Linear Quadratic
	Encoding produced CSPs var.	var.	var.	constr. constr. constr.
	SotA	exponential	no	no	yes	yes	yes	no
	C ∃c	linear	yes	no	yes	yes	yes	no
	C ∃r	linear	yes	yes	yes	yes	yes	no
	C ∃r	linear	yes	yes	yes	yes	yes	yes

Table 5 .

 5 3: Characteristics of the four CSP enco dings SotA, C 9c , C 9r ,a n dC 9r .

Table 5 .

 5 4: Comparison of sizes, modelling, and solving times for three approaches: (1) SotA encoding implemented in SMT, (2) C 9c encoding implemented in SMT, and (3) C 9c encoding implemented in MILP (times are given in seconds).

  N=10 7,392 11,207 12 18,611 111,366 9.46s 9,978 89,705 13.44s 17,454 147,015 T.O.

			pIMC		C ∃c	C ∃r	C ∃r
	Benchmark	#states #trans. #par. #var. #cstr. time #var. #cstr. time #var. #cstr. time
	nand K=1; N=2	104	147	4	255 1,526 0.17s 170 1,497 0.19s 296 2,457 69.57s
	nand K=1; N=3	252	364	5	621 3,727 0.24s 406 3,557 0.30s 703 5,828 31.69s
	nand K=1; N=5	930	1,371	7 2,308 13,859 0.57s 1,378 12,305 0.51s 2,404 20,165 T.O.
	nand K=1;

Table 5 .

 5 5: Comparison of solving times b etween qualitative and quantitative enco dings.

  6) ω s =1, sis = s 0 123 (7) ! s 6 =1, sis 6 = s 0 (8) ⇢ s , (! s 6 =0) (9) ! s > 1 ) W s 0 2Pred(s)\{s} (! s = ! s 0 +1)^(✓ s 0 s > 0), si s 6 = s 0 (13) λ s , (⇢ s ^(↵ s 6 =0)) (14) ↵ s > 1 ) W s 0 2Succ(s)\{s} (↵ s = ↵ s 0 +1)^(✓ s 0 s > 0), si s 6 2 T (15) ↵ s =0, V s 0 2Succ(s)\{s} (↵ s 0 =0)_ (✓ s 0

	(10) ! s =0,	V	s 0 2Pred(s)\{s} (! s 0 =0)_ (✓ s 0 s =0),	sis 6 = s 0
	(11) ↵ s =1,			sis 2 T
	(12) ↵ s 6 =1,			sis 6 2 T

s =0), sis 6 2 T (16) ¬λ s ) ⇡ s =0 (17) λ s ) ⇡ s =1, sis

2

T (18) λ s ) ⇡ s = Σ s 0 2Succ(s) ⇡ s 0 ✓ s s 0 , si s 6 2 T

We already introduced the word model in the constraint programming context. The reader must be careful that this word has an important role in both contexts.

Note that Chapter 4 models a problem with time-dependency (verification of a reactive synchronous programming language). However the constraint modelling is time-independent.

R is the extended set of R and equals the union of R and its limits (i.e., R = R [ {-1, +1}).

We chose the IEEE 754 norm but any set of floating-point numbers can be considered.

Be careful that in this thesis we use AI for Abstract Interpretation and not Artificial Intelligence.

In the case of the presence of state labelling, the trace is the succession of labels associated to the states encountered at running time (cf. Chapter 5).

FAUST is open source and available at http://faust.grame.fr

For reading facilities, we simply write cycle instead of directed cycle while working with directed structures such as block-diagrams.

See http://faust.grame.fr/index.php/documentation/references for listing and description.

In music, a numeric audio stream is a sequence of values between -1 and 1

https://www.cs.ox.ac.uk/people/peter.schrammel/reaver/

In this chapter we use modelling with the verification meaning and we call encoding a CSP modelling.

Indeed, when 0  v(f 1 )  v(f 2 )  1 is not respected, the interval is inconsistent and therefore empty.

|L 1 | and |L 2 | are the sizes of L 1 and L 2 ,r e s p e c t i v e l y .

As illustrated in Example 31, M is not a well formed MC since some unreachable states do not respect the probability distribution property. However, one can correct it by simply setting one of its outgoing transition to 1 for each unreachable state.

All resources, benchmarks, and source code are available online as a Python library at https: //github.com/anicet-bart/pimc_pylib

see the category discrete-time Markov chains on the PRISM website

Note that this is not always free to obtain integer integrity constraints over real-numbers.

Nous expliquons dans la thèse que cette restriction n'est pas trop forte et que les blocs temporels usuels (delay, memory, n-delay) peuvent être réécrits avec le bloc fby.

D appelé ensemble étendu de D correspond à l'union de D et de ses limites (e.g., R = R[{-1, +1})

https://github.com/anicet-bart/pimc_pylib

Dans cette thèse, nous avons abordé deux familles de problèmes traitant de la vérification de programmes. Pour chaque cas, nous avons d'abord étudié formellement la nature des problèmes de vérification concernés avant de proposer une résolution par les contraintes. Puisque nous ne nous imposions aucune restriction concernant le langage de contraintes, nous avons proposé des modélisations par contraintes utilisant des contraintes non-linéaires sur des variables non bornées, des variables mixtes entières/linéaires sur des contraintes linéaires, mais aussi des contraintes quadratiques sur des variables mixtes. Ainsi, la vérification de programmes est un champ de recherche riche pouvant faire appel à divers outils de la programmation par contraintes. La complexité théorique du problème de la vérification de programmes, comme celle du problème de la satisfaction de contraintes, peut s'avérer élevée. Cependant, les solveurs de la programmation par contraintes peuvent résoudre en partie ces problèmes difficiles. Pour autant, les communautés de la programmation par contraintes avancent sur des axes de recherches séparés en développant des solveurs dédiés à des langages de contraintes spécifiques. Finalement, dans cette thèse nous avons abordé la vérification de programmes sous l'angle de la programmation par contraintes. Cela nous a permis d'apporter de nouvelles idées dans les processus de vérification de programmes et de rapprocher ces deux domaines de recherche.

Thèse de Doctorat Anicet BART Modélisation et résolution par contraintes de problèmes de vérification

Constraint Modelling and Solving of some Verification Problems Résumé La programmation par contraintes offre des langages et des outils permettant de résoudre des problèmes à forte combinatoire et à la complexité élevée tels que ceux qui existent en vérification de programmes. Dans cette thèse nous résolvons deux familles de problèmes de la vérification de programmes. Dans chaque cas de figure nous commençons par une étude formelle du problème avant de proposer des modèles en contraintes puis de réaliser des expérimentations. La première contribution concerne un langage réactif synchrone représentable par une algèbre de diagramme de blocs. Les programmes utilisent des flux infinis et modélisent des systèmes temps réel. Nous proposons un modèle en contraintes muni d'une nouvelle contrainte globale ainsi que ses algorithmes de filtrage inspirés de l'interprétation abstraite. Cette contrainte permet de calculer des sur-approximations des valeurs des flux des diagrammes de blocs. Nous évaluons notre processus de vérification sur le langage FAUST, qui est un langage dédié à la génération de flux audio. La seconde contribution concerne les systèmes probabilistes représentés par des chaînes de Markov à intervalles paramétrés, un formalisme de spécification qui étend les chaînes de Markov. Nous proposons des modèles en contraintes pour vérifier des propriétés qualitatives et quantitatives. Nos modèles dans le cas qualitatif améliorent l'état de l'art tandis que ceux dans le cas quantitatif sont les premiers proposés à ce jour. Nous avons implémenté nos modèles en contraintes en problèmes de programmation linéaire en nombres entiers et en problèmes de satisfaction modulo des théories. Les expériences sont réalisées à partir d'un jeu d'essais de la bibliothèque PRISM.

Abstract

Constraint programming offers efficient languages and tools for solving combinatorial and computationally hard problems such as the ones proposed in program verification. In this thesis, we tackle two families of program verification problems using constraint programming. In both contexts, we first propose a formal evaluation of our contributions before realizing some experiments. The first contribution is about a synchronous reactive language, represented by a block-diagram algebra. Such programs operate on infinite streams and model real-time processes. We propose a constraint model together with a new global constraint. Our new filtering algorithm is inspired from Abstract Interpretation. It computes over-approximations of the infinite stream values computed by the block-diagrams. We evaluated our verification process on the FAUST language (a language for processing real-time audio streams) and we tested it on examples from the FAUST standard library. The second contribution considers probabilistic processes represented by Parametric Interval Markov Chains, a specification formalism that extends Markov Chains. We propose constraint models for checking qualitative and quantitative reachability properties. Our models for the qualitative case improve the state of the art models, while for the quantitative case our models are the first ones. We implemented and evaluated our verification constraint models as mixed integer linear programs and satisfiability modulo theory programs. Experiments have been realized on a PRISM based benchmark.

Mots clés

modélisation par contraintes, résolution par contraintes, vérification de programmes, interprétation abstraite, vérification de modèles.