Pawel Skruch
email: pawel.skruch@agh.edu.pl

Mathematical and Implementation Challenges Associated with Testing of the Dynamical Systems

Keywords: software system, model-based testing, dynamical system

The paper presents mathematical and implementation challenges associated with testing of embedded software systems with dynamic behavior. These challenges are related to notation of tests, calculation of test coverage, implementation of a test comparator, and automatic generation of test cases. Some author's ideas and solutions are presented with the help of abstract models that describe behavior of the software systems. The models are represented using the state space (or input/state/output) notation. An application example is given to illustrate theoretical analysis and mathematical formulation.

Introduction

Designing an embedded control system is a complex and error prone task. Within the last decades embedded systems have become increasingly sophisticated and their software content has grown rapidly. The increasing miniaturization of embedded control systems on the one hand and rising functional demands on the other hand require advanced and automated development and testing methodologies. In this context, model-based development (MBD) and model-based testing (MBT) approaches have the potential to facilitate the development of such systems under pressure of time-to-market constraints, quality assurance, and safety standards.

MBD is a process that provides the ability to graphically represent requirements, specification, and designs using domain-specific notations and simulate the resultant behavior for validation purposes. The code can be then generated from models, ranging from system skeletons to complete, deployable products. MBT is a related part that supports test generation from various kinds of models by application of a number of sophisticated methods.

Testing is the process of trying to discover every conceivable fault or weakness in a work product. The primary goal of the testing process is to found defects; the secondary goal is to show the system's compliance to its requirements. Testing can show that defects are present, but cannot prove that there are no defects [START_REF] Myers | The Art of Software Testing[END_REF]. Testing reduces the probability of undiscovered defects remaining in the software but, even if no defects are found, it is not a proof of correctness. Poorly tested systems may cost producers billions of dollars annually especially when defects are found by end users in production environments [START_REF] Leveson | An Investigation of the Therac-25 Accidents[END_REF], [START_REF] Lions | ARIANE 5. Flight 501 Failure. Ariane 501[END_REF], [START_REF] Skeel | Roundoff Error and the Patriot Missile[END_REF]. Barry Boehm's research analysis [START_REF] Boehm | Software Engineering Economics[END_REF] indicates that the cost of removing a software defect grows exponentially for each stage of the development life cycle in which it remains undiscovered. Boris Beizer [START_REF] Beizer | Software Testing Techniques[END_REF] estimates that 30 up to 90 percentage of the effort in put into testing. Another research project conducted by the United States Department of Commerce, National Institute of Standards and Technology [START_REF]The Physiology of the Grid: The Economic Impacts of Inadequate Infrastructure for Software Testing[END_REF] estimated that software defects cost the U.S. economy $60 billion per year.

Exhaustive testing is impossible what means that testing everything (all combinations of inputs and preconditions) is not feasible expect for trivial cases. This is valid in particular for software systems with dynamic behavior. The dynamic systems are modeled by difference or differential equations and have usually infinitely many states. Testing dynamic aspects of such systems requires tests that utilize time continuous input signals and time continuous output signals (even when the system is digitally processed). The process of selecting just a few of the many possible scenarios to be tested is a difficult and challenging task and currently is most often based on qualitative best engineering judgment.

In this paper, testing problem as well as test artifacts for software systems with dynamic behavior are formulated using the mathematical formalism. The main results concern the concept of testing with a model as an oracle (section 2), a proposal for test notation (section 4), an implementation of a test comparator (section 5), a calculation of test coverage (section 6), and a selection of tests (sections 7). An example (section 8) is given to present a perspective on the applicability of the approach for industrial projects.

Concept of Testing with a Model as an Oracle

The model of a software system shall specify the system's behavior in a clear and unambiguous form. It can be used in computer simulations in an early phase of the development to validate the system concept, calibrate parameters, and optimize the system performance. In the next phase, the physical system is designed (i.e., hardware and software) that shall meet the requirements specified by the model. Testing process shall be considered as the last phase in the development process that allows verifying that the physical system behavior is identical to that observed during computer simulations. When the tests failed then the system needs to be redesigned. The physical system that is being tested for the correct operation is often referred to as the system under test (SUT).

The model fully represents the requirements therefore it can be used an oracle to assess if the algorithm implemented in the electronic control unit (ECU) being tested correctly implements the requirements. The term test oracle describes a source to determine expected results to compare with the actual result of the SUT [START_REF] Adrion | Validation, Verification and Testing of Computer Software[END_REF]. The approach of a validated model being used as an oracle (the block Mathematical Model of the SUT on figure 1) is very popular in industry and often applied. The execution of a test case consists of exciting the system using actuators to simulate its working conditions and measuring the system's response in terms of electrical signals, motion, force, strain, etc. The signals are physical in case of the SUT and virtual in case of the model. The approach stipulates that the same inputs u(•) are applied to both the SUT and to the model. Next, the responses from the SUT y s (•) and from the model y(•) are compared by a test comparator to determine whether a test case has passed or failed. The state space (or input/state/output) representation provides a convenient way to model and analyze dynamical systems. The state space model consists of a set of input, output, and internal state variables that are expressed as vectors. The relationship between inputs, outputs, and internal states in a finitedimensional, time-invariant, nonlinear system with continuous-time parameter can be specified by the following equations:

Mathematical

ẋ(t) = f (x, u, t), x(0) = x 0 , (1)
y(t) = g(x, u, t) , (2)
where x(t) ∈ X ⊂ R n refers to the internal state, u(t) ∈ U ⊂ R r refers to the input state, y(t) ∈ Y ⊂ R m refers to the output state, the independent variable t > 0 is time, x 0 ∈ R n is the given initial condition, f : R n ×R r ×R → R n denotes a mathematical relationship describing the system behavior, g : R n × R r × R → R m determines the output, X is the internal state space, Y is the output state space, U is called the input state space, R n , R m , R r are real vector spaces of column vectors, n, m, r are positive integers that determine numbers of internal state, output, and input variables, respectively.

The physical and implementation constraints imposed by computer system resources lead to the assumption that the spaces U , X, and Y shall be bounded.

The assumption means that each space is contained in a ball of finite radius.

Test Notation

A test case can be considered as a set of inputs, execution preconditions, and expected outcomes developed for a particular objective, such as to exercise a particular program path or to verify compliance with a specific requirement [START_REF]IEEE Standard Glossary of Software Engineering Terminology[END_REF]. Adapting this definition to the state space modeling concept of the SUT (1), ( 2), a single test case T (j) case can be defined as

T (j) case = T (j) , x (j) 0 , u (j) (•), y (j) (•) , (3)
in case of black-box testing [START_REF] Beizer | Black-Box Testing. Techniques for Functional Testing of Software and Systems[END_REF], or

T (j) case = T (j) , x (j) 0 , u (j) (•), x (j) (•), y (j) (•) , (4)
in case of gray-box testing [START_REF] Patton | Software Testing[END_REF]. Here, u (j) : [0, T (j) ] → R r is an input function applied to the SUT, x (j) : [0, T (j) ] → R n is an expected state function, and y (j) : [0, T (j) ] → R m is an expected output function within the execution time window [0, T (j) ] when the system starts from an initial condition x

Test Comparator Implementation

The test comparator can be considered as a tool that implements a mechanism for determining whether a test has passed or failed [START_REF]International Software Testing Qualifications Board (ISTQB): Standard Glossary of Terms Used in Software Testing[END_REF]. In the concept, illustrated on figure 1, this tool compares the actual output y s (•) produced by the SUT with the expected output y(•) produced by the model. If the actual output is within a predefined tolerance range ǫ relative to the expected output, then the test is qualified as pass (z = 0, system ok ), otherwise the test is qualified as fail (z = 1, system error ). A possible practical realization of the comparison function z for a given test case T (j) case is presented below:

z(T (j) case ) = 0 if ∀ t∈[0,T (j) ] y (j) (t) -y s (j) (t) < ǫ y (j) (t) , 1 otherwise . (5)
In the formula (5) the standard Euclidean norm • has been used to measure the distance between two points in the space R m .

Test Coverage Calculation

The degree to which a given test suite T suite addresses all specified requirements for a given system is determined by a test coverage measure [START_REF]IEEE Standard Glossary of Software Engineering Terminology[END_REF]. The most obvious quantification of the system's behavior exercised by the test suite is computed by dividing the number of the system states explored by the test suite by the cardinality of the entire state space. However, the formula has limited usefulness for dynamical systems because the state space for such systems contains usually infinite number of states. In such situation, one of the possible ways out is to transform the internal state space X into another one X h that contains countable number of elements.

The test coverage C h of the test suite T suite = {T

(1) case , T (2)
case , . . . , T

(N ) case } can be defined as follows [START_REF] Skruch | A Coverage Metric to Evaluate Tests for Continuous-Time Dynamic Systems[END_REF]

C h (T suite ) = N j=1 V h (T (j) case ) |X h | , (6)
where

X h = {i ∈ Z n : ∃ x∈X : x ∈ G h (i)} (7)
is the transformed internal state space,

h = [h 1 h 1 . . . h n ] T , h k > 0 for k = 1, 2, . . . , n, Z stands for the set of integers, G h (i) = x ∈ R n : x = [x 1 x 2 . . . x n ] T , x k h k = i k , k = 1, 2, . . . , n (8)
denotes a partition with the size h in the space R n , x k h k is the largest integer not greater than

x k h k , V h (T (j) case ) = i ∈ X h : ∃ t∈[0,T (j) ] : x (j) (t) ∈ G h (i) (9)
is a set of states of the transformed internal state space covered by the test case T (j)

case . It should be noticed that the sum

V h (T suite ) = N j=1 V h (T (j) case ) ( 10
)
will contain the information about the internal states covered by the test suite T suite . The proposed test coverage measure is defined using a partition (or discretization) of the system internal state space. The partition forms a rectangular grid and, roughly speaking, the test coverage is defined by the number of the grid boxes visited by the system state during a test.

Conformance Test Selection Method

The section presents a proposal of the algorithm for generating test cases. The general principle of the algorithm is to create input functions u(•) for which the system trajectories x(•) cross every element G h (i) of the space X h . The selection and completeness of test cases is quantified by the coverage metric [START_REF] Kaner | Testing Computer Software[END_REF]. Test cases are selected to check that the functional specification (here in the form of the mathematical model) is correctly implemented, which is variously referred to in the literature as conformance testing [START_REF]International Software Testing Qualifications Board (ISTQB): Standard Glossary of Terms Used in Software Testing[END_REF], correctness testing [START_REF] Kaner | Testing Computer Software[END_REF], or functional testing [START_REF]IEEE Standard Glossary of Software Engineering Terminology[END_REF].

Algorithm 1 Conformance test selection method

1: h = [h1 h2 . . . hn] T , h1, h2, . . . , hn > 0, δ ∈ (0, 1], T > 0 2: Tsuite := ∅, V h (Tsuite) := ∅, C h (Tsuite) = 0, j := 0 3: while C h (Tsuite) ≤ δ do 4: Find xa ∈ G h (ia), x b ∈ G h (i b ) where i b ∈ X h \V h (Tsuite) 5:
Calculate the control function u * (•) that steers the system from the initial state x(0) = xa to the final state x(T ) = x b at finite time T 6:

Calculate the trajectory x * (•) and output function y * (•) 7:

j := j + 1 8: T (j) case := {T (j) , x (j) 0 , u (j)
(•), x (j) (•), y (j) (•)}, where T (j) := T , x (j) 0 :
= xa, u (j) (•) := u * (•), x (j) (•) := x * (•), y (j) (•) := y * (•) 9:
Tsuite := Tsuite ∪ T (j) case

10:

Calculate V h (Tsuite) and C h (Tsuite) 11: end while

Embedded PID Controller Example

An embedded PID controller is a system that can be considered as a combination of computer hardware and software designed to perform a dedicated control function. The PID controller works in a closed-loop system (figure 2) and attempts to minimize the error e(t) by adjusting the control input s(t). The error is calculated as the difference between a measured process output v(t) and a desired set point v sp (t). The control signal is a result of the following calculation

s(t) = K e(t) + 1 T i t 0 e(τ ) dτ + T d de(t) dt , (11)
where

K = 3.6 is proportional gain, T i = 1.81 [s] is integral time, T d = 0.45 [s]
is derivative time. The control signal is thus a sum of three terms: the P-term (which is proportional to the error), the I-term (which is proportional to the integral of the error), and D-term (which is proportional to the derivative of the error). The parameters K, T i , and T d can be obtained using the Ziegler algorithm [START_REF] Ziegler | Optimum Settings for Automatic Controllers[END_REF]. The model of the process to be controlled has been omitted in the example for the purpose of clarity and easy readability.

The algorithm 1 can be used to generate a set of conformance test cases. Before its execution, the equation ( 11) needs to be rewritten to the form

ẋ(t) = Ax(t) + Bu(t), x(0) = 0 , (12)
y(t) = Cx(t) , (13)
where

x(t) = [x 1 (t) x 2 (t)] T , x 1 (t) = t 0 e(τ ) dτ , x 2 (t) = ẋ1 (t), A = 0 1 -(T i T d ) -1 -T -1 d , B = 0 (KT d ) -1 , C = 1 0 0 1 . (14)
Then, the algorithm has been implemented and executed with the following parameters: h = [0.3, 0.2] T (size of the partition), δ = 0.7 (acceptable coverage level), T = 20 [s] (test execution time), -1.5 ≤ x 1 (t) < 1.5, -1 ≤ x 2 (t) < 1 (system implementation constraints). The test suite that guarantees the coverage level higher than δ consists of 10 test cases. The elements of these test cases are detailed in table 1, figures 3 and 4.

Conclusions

In spite of continuing research on test approaches for continuous and mixed discrete-continuous systems, there is still a lack for patterns, processes, methodologies, and tools that effectively support automatic generation and selection of the correct test cases for such systems. The model-based approach presented in the paper looks promising. The functional model of the system under test can be used as an oracle providing the capabilities to assess the results of test cases in an automatic way and also in test generation algorithms. Additional aspects, such as test notation, implementation of a test comparator, and coverage analysis have been discussed in the paper in order to have complete set of tools and mathematical methods for testing software systems with dynamic behavior. The example has been used to validate the concept and to have a perspective on its applicability for industrial projects.

case, . . . , T (j) case}.

j T (j) [s] x

Fig. 1 .

 1 Fig. 1. Testing approach of a validated model being used as an oracle

  j = 1, 2, . . . , N is a label to indicate different test cases. A collection of one or more test cases forms a test suite T suite = T

(j)T 0 u

 0 (j) (•) x (j) (•) y (j) (•) C h (T

Table 1 .

 1 An example test report for the test suite Tsuite = {T that guarantees the coverage level C h > δ, where h = [0.3, 0.2] T , δ = 0.7 (70%). The notation used in the last column means T

		(1) case, T	(2) case, . . . , T	(10) case}
	(j) suite = {T	(1) case, T

Acknowledgments. This work was supported by the National Science Centre (Poland) -project No N N514 644440.

T case

T case

T case

T case

T case

T case

T case [START_REF]The Physiology of the Grid: The Economic Impacts of Inadequate Infrastructure for Software Testing[END_REF] Fig. 3. Trajectories x (j) , j = 1, 2, . . . , 10 and elements (gray rectangles) of the transformed state space covered by the test cases T u (9) u (10) Fig. 4. Illustration of the input functions u (j) (•), j = 1, 2, . . . , 10 belonging to the test cases T (j) case


Nihel Kooli
email: nihel.kooli@loria.fr

Abdel Belaïd
email: abdel.belaid@loria.fr

Aurélie Joseph
email: aurelie.joseph@yooz.fr

Vincent Poulain
email: vincent.poulaindandecy@yooz.fr

D ' Andecy

Entity Local Structure Graph Matching for Mislabeling Correction

Keywords: entity local structure, subgraph matching, mislabeling correction, structure model, graph clustering

This paper proposes an entity local structure comparison approach based on inexact subgraph matching. The comparison results are used for mislabeling correction in the local structure. The latter represents a set of entity attribute labels which are physically close in a document image. It is modeled by an attributed graph describing the content and presentation features of the labels by the nodes and the geometrical features by the arcs. A local structure graph is matched with a structure model which represents a set of local structure model graphs. The structure model is initially built using a set of well chosen local structures based on a graph clustering algorithm and is then incrementally updated. The subgraph matching adopts a specific cost function that integrates the feature dissimilarities. The matched model graph is used to extract the missed labels, prune the extraneous ones and correct the erroneous label fields in the local structure. The evaluation of the structure comparison approach on 525 local structures extracted from 200 business documents achieves about 90% for recall and 95% for precision. The mislabeling correction rates in these local structures vary between 73% and 100%.

I. INTRODUCTION

An entity is defined as an existing or real thing, such as a person, a location, an organization, etc. It is contrasted with its attributes. For example, a person has the attributes: name, date of birth, social security number, etc. Extracting entities in documents is equivalent to identifying their attributes. This work lies in the context of entity extraction in document images guided by a predefined database, as reported in [START_REF] Kooli | Entity Matching in OCRed Documents with Structured Databases[END_REF]. This database describes the entity attributes by its records and informs about their semantics by its fields (columns). The entity attributes are labeled in the document, as proposed in our earlier work [START_REF] Kooli | Semantic Label and Structure Model based Approach for Entity Recognition in Database Context[END_REF], using dictionaries extracted from noun fields in the database and regular expression built from fields having a standard from. However, mislabeling may frequently occur as missed labels, extraneous labels or erroneous label fields. The impact is a final wrong detection of an entity. For example, if the social security number is wrongly detected, the person may be not detected or worst confused in the database with an other person having the same name. Missed labels are caused by OCR errors or non-standardized representations between the document and the database (for example, term permutation, abbreviations, typing errors, etc.). Erroneous labels are caused by a confusing syntax of some attributes, for example an amount number labeled by mistake as a zip-code. Finally, the extraneous labels represent noise.

In this paper, we propose to correct the mislabeling by employing the entity label arrangement in the document. We assume that attributes (labels within the page) which are physically close in the document page are more probably related to the same entity than the same ones faraway. These labels build a local structure which is modeled by a labeled graph, called entity local structure graph. In this graph, the nodes represent the content features (syntactic and semantic) and the presentation features of the labels and the arcs represent the geometric relationships between them. This graph is matched with a structure model, which is composed of a set of entity local structure graphs.

Labeled graphs are data structures that offer a significant modeling of complex entities. The labeled nodes describe the entity elements and the labeled arcs represent the relationships between them. Some previous works propose to employ graph modeling for semantic labeling in document images. For example, authors in [START_REF] Liang | Logical labeling of document images using layout graph matching with adaptive learning[END_REF] and [START_REF] Liang | Page Classification through Logical Labelling[END_REF] propose to model the document layout by graphs for logical labeling and document classification in journals and conference proceedings. This work is based on a model which is learned for each document class. The model represents spatial relationships between the blocks segmented by the OCR. However, this approach is dependent on the document class. The same authors propose in [START_REF] Liang | Content features for logical document labeling[END_REF] to add the document content study to its layout modeling in order to enhance the labeling in English business letters. However, this approach does not deal with the noisy content given by the OCR. Labeled graph matching is usually an NP-complete problem and whose objective is to find a way to correspond a graph to another, such that the topology and the node and arc labels are matched. In the domain of pattern recognition, graph matching techniques are generally used to correspond between an observed graph, called candidate graph and a known entity graph, called model graph. There exist two types of graph matching techniques [6] [7] in the literature: exact graph matching and inexact graph matching. Exact graph matching is to find an isomorphism between graphs. Inexact graph matching is the most commonly used and consists on searching for the best match by tolerating the noisy representation and the errors. For this purpose, the most used approach is the Graph Edit Distance (GED) [START_REF] Sanfeliu | A distance measure between attributed relational graphs for pattern recognition[END_REF]. GED is inspired from the string edit distance and is defined as the weighted sum of the edit operation costs which are needed to transform one graph to the other. However, in the case of labeled graph where the labels are not of nominal type but represent a set of numeral attributes resulting from a feature extraction step, it is generally not possible to find an exact mapping between these labels. To deal with such a problem, a label discretization based solution can be proposed to transform the numerical attributes into nominal labels, but it is clear that the mapping is sensitive to discretization errors. Another solution consists of defining the mapping cost as the sum of distances between the label values and using a cost threshold for the label mapping decision, but it is not easy to find the proper one. This problem was treated in [START_REF] Bodic | An Integer Linear Program for Substitution Tolerant Subgraph Isomorphism and its Use for Symbol Spotting in Technical Drawings[END_REF] by reformulating the problem in the Integer Linear Program (ILP) formalism and integrating the label mapping cost in the subgraph matching cost. However, this approach tolerates only the label substitution operation and does not deal with the deletion of nodes or arcs.

Our graph matching strategy lies with inexact subgraph matching which consists on searching an inexact matching between a candidate graph and a subgraph of a model graph. This paper treats also labeled graphs where the labels represent a set of numerical attributes (scalar or vectorial). The graph matching problem is solved by the integration of the feature dissimilarities in the cost function. This work is a thorough extension of the work reported in [START_REF] Kooli | Semantic Label and Structure Model based Approach for Entity Recognition in Database Context[END_REF] which performs substitution tolerant subgraph matching for the entity structure correction and involves human for the structure model learning. This paper deals with the node and arc deletion in the subgraph matching in order to tolerate the noisy representation of real graphs and extends the label representation features in the local structures. Furthermore, it proposes an unsupervised learning of the structure model based on a graph clustering algorithm.

The remainder of this paper is organized as follows. The entity structure matching approach is detailed in Section II. The experiments on real world data are presented and analyzed in Section III. The paper is concluded in Section IV.

II. ENTITY STRUCTURE MATCHING APPROACH

Fig. 1 presents the global schema of the proposed approach. Firstly, a candidate graph is built for each local structure extracted from an input document. Secondly, the candidate graph is compared to the structure model using a subgraph matching method. This model is initially learned from a chosen dataset using a graph clustering algorithm and is then incrementally updated for a document stream. Finally, the geometrical relations in the matched model graph are used to correct the eventual mislabeling in the local structure.

A. Local structure representation

A label in the local structure is defined as:

l i = (c i , v i , conf i ) (1)
where v i is the value of the label, c i is the corresponding field (column) in the database and conf i is the confidence of labeling l i given by the n-gram distances [START_REF] Kondrak | N-Gram Similarity and Distance[END_REF] which is used to compare between string values in the dictionary and in the document. v i is represented by a bag of words v i = {t j }. Each input document is defined by d = {l i }. An entity local structure in the document is modeled by a directed complete graph G = (N, A, μ, ξ) where N is a finite set of nodes that correspond to semantic labels, A ⊆ N ×N is a finite set of arcs that represent geometrical relations between the nodes, μ : N → L N and ξ : A → L A are two functions assigning a label to a node and an arc respectively. L N and L A are discrete sets of labels for the nodes and the arcs respectively. Each arc a ij ∈ A relating the nodes n i and n j is represented by n i n j . A node n i that corresponds to a label l i is defined by:

n i = (c i , conf i , nt i , nl i , p i ) (2)
where nt i is the number of label terms, nl i is the number of label lines and p i is the normalized font size according to the average font of the document (small: 0, medium: 1 2 , large: 1). For an arc a ij relating the nodes n i and n j , we define a feature vector describing the spatial relation between these nodes as:

a ij = (vs ij , hs ij , al ij ) (3)
where vs (vertical separation) is the number of lines that separate the labels corresponding to n i and n j . hs (horizontal separation) is the distance, in number of characters, that separates the bounding boxes of the labels corresponding to n i and n j . vs ij and hs ij are signed to inform about the relative vertical position (above, below) or the relative direction (on the right, on the left).

al ij = (rJust ij , lJust ij , cent ij ) is a

B. Structure comparison

This can be formulated as a problem of inexact subgraph matching between a candidate graph and a model graph in and extraneous arcs or nodes in the candidate graph. It is not necessary to deal with missing arcs or nodes since we search for a subgraph matching between a candidate graph and a model graph. In order to solve this problem which is generally NP-hard, we use the Branch and bound algorithm [START_REF] Wong | An algorithm for graph optimal monomorphism[END_REF] which proposes a tree search of the node mapping with backtracking using heuristics. This algorithm is easily adapted to our context since it takes into account the node and arc attributes to provide the matching heuristics. In fact, we employ semantic heuristics (for example, a node labeled by a zip code can not be mapped to a node labeled by a name in an address structure) and physical heuristics (for example, a node labeled by an author can not be placed above a node labeled by a title in a bibliography reference header structure).

Let t : G → M ∪ { } be a graph mapping function from a candidate graph G = (N G , A G , μ G , ξ G ) to a subgraph of a model graph M = (N M , A M , μ M , ξ M ).
To allow the node deletion, it is possible to map a node in G to . The graph matching cost for the mapping t from G to M is defined as:

C(G, M, t) = α |N G | n∈NG C N (n, t(n)) + 1 -α |A G | n∈G n ∈G C A (nn , t(n)t(n )) (4)
where α ∈ [0, 1] and

C N : N G × N M → R + and C A : A G × A M → R +
are the mapping cost functions for the nodes and the arcs respectively. Let Δ be the set of the possible mapping functions from G to a subgraph of M . The matching cost is then defined as:

C(G, M ) = min t∈Δ C(G, M, t) (5)
Let F N = {nt, nl , p} and F A = {vs, hs, al } be the sets of node and arc features respectively. The node mapping cost function from n = (c, conf , nt, nl , p) to n = (c , conf , nt , nl , p ) is then defined as:

C N (n, n ) = λ n (1 -conf .conf ) if c = c ; λ n f ∈FN λ f d f (n, n ) else. (6)
The arc mapping cost function from a = (vs, hs, al ) to a = (vs , hs , al ) is defined as:

C A (a, a ) = λ a f ∈FA λ f d f (a, a ) (7)
where λ n , λ a ∈ [0, 1] are the weight factors for nodes and arcs in the model graph and λ f ∈ [0, 1] depends on the feature relevance. Dissimilarities of scalar features are defined as:

d f (a, a ) = |f N -f N | ∀f ∈ F N ∪ F A \ {al} ( 8
)
f N is the normalized value of f defined by:

f N = f -max(f ) max(f ) -min(f ) (9)
where max(f ) and min(f ) represent the maximum and the minimum values respectively and are dataset dependent.

The alignment dissimilarity is defined as:

d al (a, a ) = 0 if al × al = 0; 1 else. ( 10
)
Comparing a candidate graph to all model graphs in the structure model is time consuming. We propose then to filter these graphs using semantic heuristics (for example, the number of nodes having a common label field) and structural heuristics (for example, the number of lines in the local structure or the logical order of the labels in a page line or column). Given a model graph dataset S M = {M 1 , ..., M n } and one candidate graph G, the structure comparison is equivalent to the selection of the model graph M match , where:

M match = arg min Mi∈SM C(G, M i ) (11)
The model M match is retained if the matching cost does not exceed an empirically fixed threshold.

C. Mislabeling correction

A matched model graph with a candidate is used to correct the three types of mislabeling (missed labels, erroneous label fields and extraneous labels in the local structure modeled by this candidate graph). The extraneous nodes in the model graph may correspond to missed labels in the local structure. The geometrical relations provided by the arcs related to these extraneous nodes are used to localize the missed labels in the document. To validate these label correspondence to the candidate entity in the database, their values are compared to the entity attributes by being less strict in the string distances. Furthermore, the substituted node labels in the model graph are used to correct the label fields in the local structure. Finally, the labels corresponding to deleted nodes in the candidate graph are pruned in the local structure. Fig. 3 shows an example of mislabeling correction in a structure model. In Fig. 3 (a), the value "3091Z" was labeled as a zip code due to a confusion made by the OCR of the character "Z" with the character "7". Furthermore, the mail was not labeled due to OCR errors and the fax was labeled as a phone since they have the same syntax. The candidate graph built from this local structure is shown in Fig. 3 (b). The matched model graph with this candidate graph using inexact subgraph matching is shown in Fig. 3 (c). This model graph is used to extract the missed mail, to correct the erroneous phone and to prune the extraneous zip code in the local structure represented in Fig. 3 (a).

D. Structure model learning

The structure model is initially learned via the incremental graph clustering algorithm detailed in Algorithm 1. The latter is executed on a dataset chosen to be representative of the corpus. It is an improvement of the Leaders algorithm [START_REF] Vijaya | Leaders-Subleaders: An efficient hierarchical clustering algorithm for large data sets[END_REF] by adding the incremental update of the centroid to be more representative of the cluster members. This algorithm is adapted to our case since it is a simple incremental clustering algorithm that requires one dataset scan. Besides, experiments on our corpus show that the performances are not affected by the data stream order. During the document stream processing, the structure model is incrementally updated. In fact, each model graph matched with a treated candidate graph is recomputed by considering this new candidate graph.

Let us define now the distance and the centroid mentioned in the algorithm: the distance is the graph matching cost function and the centroid is the group representative graph. The representative graph structure is built using the concept if distance with the nearest centroid < threshold then end if 10: end for of "Weighted Minimum Common Supergraph (WMCS)" proposed in [START_REF] Bunke | Graph clustering using the weighted minimum common supergraph[END_REF]. The representative graph attributes are learned by fusing the attributes of the member graphs in the cluster. For distances, the sample average is computed. For alignment, the dominant value is used. The representative graph weight factors are set up inversely proportional to the deviation of the attributes in the samples. That is to say, the larger the sample variation of an attribute is, the less discriminant it is and so the lower its weight factor is.

III. EXPERIMENTS

We work on a real-world industrial project in direct collaboration with the ITESOFT1 company. For tests, we use a dataset of 525 local structures extracted from 200 printed documents. These documents represent industrial invoices or purchase orders. The local structures are categorized into 4 types: postal address structures, contact information structures, fiscal information structures and mixed structures which are a combination of two or more types of structures. For the entity attribute labeling in the documents, a company intern tool called FullText is used. The dictionaries and the regular expressions are built from a database which is composed of a table containing about 230000 records, where each one denotes an entity. This database registers information about enterprises (industrial suppliers and clients) such as their names, addresses, contact numbers, etc. First, we evaluate the local structure graph matching approach on our corpus. Then, we highlight its benefits for the mislabeling correction. Finally, we evaluate the model learning module based on the graph clustering algorithm.

A. Graph matching results

For the graph matching experiments, we use a structure model composed of 41 model graphs (the experiments on the model learning will be presented in section III-C) and a dataset of 525 graph candidates built from the local structure samples. For evaluation, we use a ground truth table that links each candidate graph with its model graph. This ground truth was manually prepared by an expert.

A relevant model graph for a candidate graph is defined as a graph that contains a subgraph corresponding to this candidate graph. The precision and recall are then defined as: where RG, MG and RMG represent the relevant graphs, the matched graphs and the relevant matched graphs respectively.

recall = # RMG # RG precision = # RMG # MG (12)
Two strategies are used for the evaluation: always match a candidate graph with the best model graph (top 1) or match it with the best model graph only if their matching cost is below a threshold. The results are illustrated in Table I. It shows that the graph matching algorithm performs well for all structure types. Besides, it shows that the acceptance threshold strategy gives better precision (95.78% compared to 92.57%) and f-measure (93.26% compared to 92.57%) than the best match strategy even if the recall (90.86% compared to 92.57%) is worse. This is explicated by the considerable reduction of the false positives due to the rejection by the threshold. In order to limit the wrong corrections of the local structures, the acceptance threshold strategy is adopted for the remaining experiments.

The graph matching method is compared with existent methods in Table II. Results show that our method outperforms the GED + label discretization and the GED + decision threshold ones using either the substitution tolerant subgraph matching or the substitution and deletion tolerant subgraph matching due to the integration of the feature dissimilarities in the matching cost function. Furthermore, it gives better precision but worse recall than the optimization based method in the case of substitution tolerant subgraph matching. This is explained by the employed heuristics, in the branch and bound algorithm, which discard some "wrong" matching solutions.

B. Mislabeling correction results

The three types of mislabeling correction, using the structure matching, are evaluated separately on a set of labels of variant fields. Missed labels detection in the local structures is evaluated on a set of missed labels using a manually prepared ground truth. TABLE III presents the obtained results. It shows that the identification of all column labels gets high recall (varied between 73.75% and 96%) and precision (varied between 84.28% and 100%) rates. The erroneous label fields correction and the extraneous labels pruning are similarly evaluated and results are presented in TABLE IV and TABLE V respectively. Results are promising for both recall and precision rates. In fact, the recall (precision) rates are varied between 75% and 96% (90.91% and 100%) for erroneous label fields correction and between 77.14% and 97.5% (91.53% and 100%) for extraneous labels pruning. Errors cases are essentially caused by a wrong graph matching solution or a deficiency in verifying the similarity between the detected missed label value and the entity attribute value in the database.

C. Model learning results

For the clustering, a dataset of 290 local structure graphs extracted from 87 documents is used. The number of obtained clusters (model graphs) is 41. To evaluate the clustering algorithm, the Dunn index D is used. It is defined as:

D = min 1≤i<j≤n d(i, j) max 1≤k≤n d (k) (13)
where d(i, j) is the inter-cluster distance between the clusters i and j (the distance between the centroids) and d(k) is the intra-cluster distance of the cluster k (the maximal distance between any element pair in the cluster k).

The Dunn index is evaluated for three variant stream orders of processed graphs in the clustering algorithm. The obtained values are around 0.74 for the three stream orders with the same number of obtained clusters (41 clusters). These results prove that our corpus is independent of the data stream order.

Table VI presents a comparison of the clustering results

between the proposed algorithm and the Leaders one. Its shows that the proposed algorithm outperforms the Leaders one with a Dunn index of 0.74 compared to 0.71. This justifies our choice consisting of the incremental update of each cluster centroid.

IV. CONCLUSION AND FUTURE WORK

This paper proposes a structure comparison approach for mislabeling correction in documents using a structure model. The comparison is based on a subgraph matching method between a candidate graph (built for each local structure) and a model graph (in the structure model). The evaluation on a dataset of 525 local structures extracted from 200 documents is promising and achieves about 90% for recall and 95% for precision. Furthermore, the method has proven to be effective in correcting the mislabeling (missed labels, erroneous label fields and extraneous labels) in the local structures.

Our future work is to evaluate our approach on other datasets in order to investigate more local structure types such as table lines and bibliographic references. Another interesting work is to enhance the verification of the identified missed labels by combining different similarity measures and using an OCR correction model based on character shape classification Furthermore, we plan to propose a probabilistic score of entity matching in document images based on an estimation of the belonging of their labeled attributes to the local structures.

Fig. 1 .

 1 Fig. 1. Global schema of the proposed system

  vector of three binary values which inform about line alignment (right aligned, left aligned, centered text). Slight variation (lower than 20 pixels) between the line boundaries is tolerated for the alignment.

Fig. 2

 2 Fig. 2 shows examples of local structures extracted from real world document images with their representations by attributed graphs (for simplicity, we do not represent all the arcs in the graphs). Fig. 2 (a) and Fig. 2 (b) are extracted from administrative documents. They model an address and a fiscal information structures respectively. Fig. 2 (c) represents a bibliography header structure extracted from a scientific paper.

  Fig. 2. Examples of local structures

Algorithm 1

 1 Graph clustering1: select a graph g from the dataset, declare it as an initial centroid and assign it to a new cluster c 2: for each g ∈ dataset do

  g as a centroid and assign it to a new cluster 9:

Fig. 3 .

 3 Fig. 3. Mislabeling correction in a local structure using subgraph matching

TABLE I .

 I

			STRUCTURE GRAPH MATCHING RESULTS
	Structure		Best Match			Acceptance threshold
		Recall (%)	Precision (%)	F-measure (%)	Recall (%)	Precision (%)	F-measure (%)
	Postal addresses (135 graphs)	94.07	94.07	94.07	92.59	96.15	94.34
	Contact information (100 graphs)	88.00	88.00	88.00	86.00	90.53	88.21
	Fiscal information (175 graphs)	95.43	95.43	95.43	94.86	98.81	96.79
	Mixed (115 graphs)	90.43	90.43	90.43	86.96	95.24	90.91
	Total (525 graphs)	92.57	92.57	92.57	90.86	95.78	93.26

TABLE V

 V

		.	EXTRANEOUS LABELS PRUNING RATES
	Label field		Number of labels		Recall (%)	Precision (%)
		Extraneous Pruned	Correct
	Zip code	80	78	78	97.5	100
	Name	100	82	78	78	95.12
	City	100	87	85	85	97.70
	Phone	70	59	54	77.14	91.53
	Siret number	50	46	45	90	97.83

http://www.itesoft.com


Béatrice Bérard

Olga Kouchnarenko

John Mullins

Mathieu Sassolas

Probabilistic Opacity in Refinement-Based Modeling

Given a probabilistic transition system (PTS) A partially observed by an attacker, and an ω-regular predicate ϕ over the traces of A, measuring the disclosure of the secret ϕ in A means computing the probability that an attacker who observes a run of A can ascertain that its trace belongs to ϕ. In the context of refinement, we consider specifications given as Interval-valued Discrete Time Markov Chains (IDTMCs), which are underspecified Markov chains where probabilities on edges are only required to belong to intervals. Scheduling an IDTMC S produces a concrete implementation as a PTS and we define the worst case disclosure of secret ϕ in S as the maximal disclosure of ϕ over all PTSs thus produced. We compute this value for a subclass of IDTMCs and we prove that refinement can only improve the opacity of implementations.

Introduction

Context and motivation. When modeling complex systems, a top-down approach based on the refinement of models allows to gradually specify various system requirements. These refinements are designed to preserve some behavioral properties, like safety, reachability, and liveness under some conditions.

Security requirements, which are not behavioral ones [START_REF] Clarkson | Hyperproperties[END_REF], may not fare well under refinement, unless tailored specially to do so, as in [START_REF] Alur | Preserving secrecy under refinement[END_REF].

Several known security properties such as noninference or anonymity can be encoded in the framework of opacity [START_REF] Mazaré | Decidability of opacity with non-atomic keys[END_REF][START_REF] Bryans | Opacity generalised to transition systems[END_REF][START_REF] Alur | Preserving secrecy under refinement[END_REF]. In this context, an external observer tries to discover whether a predicate (given as an ω-regular set) holds by partially observing the system through a projection of its actions. A system is opaque if the attacker fails to discover this information. In the possibilistic setting, a violation of opacity captures the existence of at least one perfect leak.

In probabilistic models like Discrete Time Markov Chains (DTMCs), naturally random events such as faults, message transmission failure, actions of an external environment, etc. can be taken into account. Opacity was extended in the probabilistic setting [START_REF] Bérard | Quantifying opacity[END_REF][START_REF] Bérard | Probabilistic opacity for Markov decision processes[END_REF] to provide a measure of the set of runs disclosing information on the truth value of the predicate. As a result, opacity increases when the disclosure -which is the focus of this paper -decreases. Consider for instance the two systems in Fig. 1(a)-(b), which are DTMCs with the addition of labels on states (indicated inside). We assume that the occurrence of b must be kept secret and that all labels except b are observable. In this case, the only runs disclosing the secret are those observed by ad ω , since every such run betrays the occurrence of b. The probability of disclosure is 1/4 in A 1 while it is 3/4 in A 2 , hence A 1 is more secure than A 2 . Our aim is to establish sufficient conditions on systems like A 1 and A 2 , that can be compared, for one of them to be more secure than the other.

In the process of system modeling, it is common practice to use underspecified models as first steps of specification. A first approach is to consider sub-stochastic models where transition probabilities need not sum up to 1. In this framework, the notions of satisfaction and simulation were extensively studied in [START_REF] Baier | Comparative branching-time semantics for Markov chains[END_REF]. The second approach is to introduce non-determinism in the model which makes possible the description of some choices of the environment [START_REF] Jonsson | Specification and refinement of probabilistic processes[END_REF][START_REF] Segala | Modeling and Verification of Randomized Distributed Real-Time Systems[END_REF][START_REF] Chatterjee | Model-checking omega-regular properties of interval markov chains[END_REF][START_REF] Benedikt | LTL model checking of interval markov chains[END_REF][START_REF] Bérard | Probabilistic opacity for Markov decision processes[END_REF]. These models have also been studied in relation to the refinement process [START_REF] Jonsson | Specification and refinement of probabilistic processes[END_REF]. For example, both systems of Fig. 1(a)-(b) could have been derived from a single underspecified system S with the same structure but imprecise probabilities, like the one in Fig. 1(c). A particular case of such models is the Interval-valued DTMCs (IDTMCs) where the transition probabilities are underspecified by giving only bounds in the form of intervals, as done in Fig. 1(c). The refinement consists for example in restricting these intervals. Implementation, on the other hand, reduces the bounds to a single point, thus providing a Discrete Time Markov Chain.

Scheduling is an effective way to obtain an implementation: at each step, the scheduler provides a distribution satisfying the bounds, producing a (possibly infinite) DTMC on-the-fly. As such, a scheduler can represent a strategy of an agent inside the system. In the case of opacity, this scheduler is adversarial in the sense that it tries to disclose as much information as possible to the passive observer.

Contribution. In this work, we investigate the effect of refinement of probabilistic systems on opacity. Disclosure, as any security measure, is defined on IDTMCs as the worst case scenario for all its implementations, although not every implementation is obtained through scheduling.

In order to evaluate the disclosure of an IDTMC under realistic assumptions, we study the supremum of the disclosure of all scheduled implementations: this measures the information obtained by the passive observer when the system is controlled by the smartest scheduler in coalition with the observer. We show how to compute this value for a subclass of IDTMCs, namely IDTMCs where no transition can be completely blocked by the scheduler. The computation is based on techniques proposed in [START_REF] Chatterjee | Model-checking omega-regular properties of interval markov chains[END_REF]. Note that the previous approach in [START_REF] Bérard | Probabilistic opacity for Markov decision processes[END_REF] has already used schedulers to evaluate disclosure, although in the context of (fully specified) Markov Decision Processes.

We then show that a refinement of an IDTMC can only improve the opacity of all implementations obtained by scheduling. This can be viewed as an extension of the work in [START_REF] Alur | Preserving secrecy under refinement[END_REF] to the probabilistic setting. The main difficulty of this result comes from the restriction of the implementations to those obtained by scheduling.

Organization of the paper. In Section 2 we present the underlying models for specification and implementation, with the satisfaction relation and the simulation relation. We define probabilistic disclosure in this context and show how to compute it (for a restricted case) in Section 3. Finally, we prove monotonicity of opacity under simulation in Section 4. Due to lack of space, several proofs are provided in a separate appendix.

Finite automata and probabilistic models for refinement

In this section, we present the models used in this work: finite automata and the probabilistic models for specifications and implementations, as well as the satisfaction and simulation relations.

The set of natural numbers is denoted by N. The composition of relations R 2 and R 1 is defined by

R 2 • R 1 = {(x, z) | ∃y, (x, y) ∈ R 1 ∧ (y, z) ∈ R 2 }.
Given a finite alphabet Σ, we denote by Σ * (resp. Σ ω ) the set of finite (resp. infinite) words over Σ, with Σ ∞ = Σ * ∪ Σ ω and ε the empty word.

Given a countable set Z, a discrete distribution is a mapping µ :

Z → [0, 1] such that z∈Z µ(z) = 1. The support of µ is supp(µ) = {z ∈ Z | µ(z) > 0}.
The set of all discrete distributions on Z is denoted by Dist(Z). When dealing with a distribution on domain

Z 1 ×Z 2 (a joint distribution), it is convenient to write µ(Y 1 , Y 2 ) = y 1 ∈Y 1 ,y 2 ∈Y 2 µ(y 1 , y 2 ) for Y 1 ⊆ Z 1 and Y 2 ⊆ Z 2 . Moreover, we abusively write µ(y 1 , Y 2 ) = µ({y 1 }, Y 2 ) and µ(Y 1 , y 2 ) = µ(Y 1 , {y 2 }).

Models Definition (Deterministic Parity Automaton). A deterministic parity automaton (DPA) is a tuple

A = (Q, Σ, δ, q 0 , F ), where Q is a finite set of states, Σ is an input alphabet, δ : Q × Σ → Q is a transition function, q 0 ∈ Q is an initial state,
and F is a mapping from Q to a finite set of colors {1, . . . , k}.

A run of A on a word w = a 1 a 2 • • • ∈ Σ ω is an infinite sequence ρ = q 0 q 1 • • • ∈ Q ω such
that for all i ≥ 0, q i+1 = δ(q i , a i+1 ). For such a run ρ, we define Inf (ρ) as the set of states appearing infinitely often in the sequence. The run is accepting if min{F (q) | q ∈ Inf (ρ)} is even.

In this case, the corresponding word is accepted by A and L(A) is the subset of Σ ω of words accepted by A. A subset K of Σ ω is ω-regular if there is an automaton A such that K = L(A).

For the probabilistic context, we consider two models: Probabilistic Transition Systems (PTSs) for implementations, and Interval-valued Discrete Time Markov chains (IDTMCs) for specifications.

Probabilistic transition systems are a particular case of the probabilistic processes of [START_REF] Jonsson | Specification and refinement of probabilistic processes[END_REF], with the restriction of a countable set of states. They are classical Discrete Time Markov Chains (DTMCs), with the addition of state labeling. Definition 2.2 (Probabilistic Transition System). Let Σ be an alphabet. A probabilistic transition system (PTS) over Σ is a 4-tuple A = Q, q init , ∆, L where -Q is a countable set of states, with q init ∈ Q the initial state, -∆ : Q → Dist(Q) is a mapping associating with any state q ∈ Q a distribution ∆(q) over Q, with finite support, -L : Q → Σ is the labeling function on states.

A (finite or infinite) run of A starting from state q ∈ Q is a sequence of states ρ = q 0 q 1 q 2 . . . such that q 0 = q and for each i, 0 ≤ i < |ρ|, ∆(q i )(q i+1 ) > 0. When the run is finite ρ = q 0 q 1 . . . q n , we note q n = lst(ρ). The trace of ρ is the word tr(ρ) = L(q 0 )L(q 1 ) . . . ∈ Σ ∞ . We denote by Runs q (A) the set of infinite runs starting from q and we set Runs(A) = Runs q init (A), and Tr(A) = {tr(ρ) | ρ ∈ Runs(A)}, the set of traces of A. We also define FRuns q (A) the set of finite runs starting from q, and similarly FRuns(A) = FRuns q init (A) and FTr(A) = {tr(ρ) | ρ ∈ FRuns(A)}, the subset of Σ * of finite traces of A.

Recall [START_REF] Billingsley | Probability and Measure. 3rd edn[END_REF] that a probability measure P A can be defined on Runs(A): measurable sets are generated by cones, where the cone C ρ associated with a finite run ρ = q 0 q 1 . . . q n is the subset of infinite runs in Runs(A) having ρ as prefix. The probability of

C ρ is P A (C ρ ) = n-1 i=0 ∆(q i )(q i+1
). The cone of a word w ∈ Σ * is defined by C w = ρ∈tr -1 (w) C ρ . For an ω-regular language K, we denote by P A (K) the probability of K in A. This probability is well defined (since ω-regular sets are measurable [START_REF] Vardi | Automatic verification of probabilistic concurrent finite-state programs[END_REF]) and can be computed given a DPA for K [START_REF] Courcoubetis | The complexity of probabilistic verification[END_REF].

The specifications we consider here are given by Interval-valued Discrete Time Markov chains, introduced in [START_REF] Jonsson | Specification and refinement of probabilistic processes[END_REF] and further investigated in [START_REF] Chatterjee | Model-checking omega-regular properties of interval markov chains[END_REF][START_REF] Benedikt | LTL model checking of interval markov chains[END_REF] from a verification point of view. We denote by I the set of intervals in [0, 1].

Definition 2.3 (Interval-valued Discrete Time Markov Chains).

An Interval-valued Discrete Time Markov Chains (IDTMC) is a 4-tuple S = (S, s init , T, λ) where -S is a finite set of states, with s init ∈ S the initial state, -T : S → (S → I) associates with any state s ∈ S a mapping T (s) from S into I, λ : S → Σ is the labeling function.

By extension, f ∈ T (s) will denote any function

f : S → [0, 1] such that for all s ∈ S, f (s ) ∈ T (s)(s ) and s ∈S f (s ) = 1.
Several semantic interpretations for IDTMCs have been considered in [START_REF] Jonsson | Specification and refinement of probabilistic processes[END_REF][START_REF] Chatterjee | Model-checking omega-regular properties of interval markov chains[END_REF][START_REF] Benedikt | LTL model checking of interval markov chains[END_REF]. The simplest one is Uncertain Markov Chains, which corresponds to first choosing all distributions for the states, with probabilities belonging to the specified intervals. In this case, the resulting model is a PTS, with the same structure as the specification.

A richer semantics consists in choosing the distribution at each step, as in a Markov Decision Process, hence the name Interval Markov Decision Process (IMDP). Note that an IMDP can be translated into an exponentially larger MDP [START_REF] Chatterjee | Model-checking omega-regular properties of interval markov chains[END_REF], but the transformed MDP is ill-suited to model refinement.

Finally, the most general semantics is directly given by the satisfaction relation from [START_REF] Jonsson | Specification and refinement of probabilistic processes[END_REF] recalled later.

We first describe the IMDP semantics. A run of S starting from a state s is a sequence s

µ 1 -→ s 1 µ 2
-→ . . . where s i ∈ S and each µ i is a distribution over S such that ∀s ∈ S, µ i (s) ∈ T (s i-1 )(s). As before, we denote by Runs s (S) the set of runs starting from s, we set Runs(S) = Runs s init (S), FRuns(S) is the set of finite runs of S starting from s init , and for a run

ρ = s µ 1 -→ s 1 µ 2 -→ . . . s n-1 µn -→ s n in FRuns(S) we define lst(ρ) = s n .
To associate a probability measure with the runs, it is necessary to resolve the non determinism by a scheduler that chooses a distribution at each step. More precisely: Definition 2.4 (Scheduler). A scheduler A for an IDTMC specification S = (S, s init , T, λ), is a mapping A : FRuns(S) → Dist(S) such that for each run ρ with s = lst(ρ), A(ρ)(s ) ∈ T (s)(s ).

We denote by Sched(S) the set of schedulers for S. Like for Markov Decision Processes, scheduling S with A produces a PTS denoted by S(A) where states are finite runs: Q ⊆ FRuns(S), the initial state is the run containing only the initial state of S: q init = s init , and for ρ ∈ Q,

L(ρ) = λ(lst(ρ)) and ∆(ρ)(ρ ) = A(ρ)(s ) for ρ = ρ A(ρ) ---→ s . We note sat(S) = {S(A) | A ∈ Sched(S)}.
Note that the Uncertain Markov Chains semantics corresponds to the particular case of memoryless schedulers: there is a mapping B : S → Dist(S) such that A(ρ) = B(lst(ρ)). In this case the set of states of the PTS

S(A) is Q = S with ∆(s)(s ) = B(s)(s ) ∈ T (s)(s ).

Satisfaction relation

We now turn to the general satisfaction relation defined in [START_REF] Jonsson | Specification and refinement of probabilistic processes[END_REF].

Definition 2.5 (Satisfaction relation). A PTS

A = Q, q init , ∆, L satisfies IDTMC S = (S, s init , T, λ), written A S, if there exists a relation R ⊆ Q × S such that q init Rs init and if qRs then 1. L(q) = λ(s), 2. there exists a joint distribution δ ∈ Dist(Q × S) such that (a) δ(q , S) = ∆(q)(q ) for all q ∈ Q, (b) δ(Q, s ) ∈ T (s)(s ) for all s ∈ S, (c)
q Rs whenever δ(q , s ) > 0.

We write sat(S) = {A | A S} for the set of all PTSs that satisfy specification S; these are called implementations of S.

As a first result, we show that scheduling an IDTMC specification is a particular case of implementation: Proposition 2.6. Let S be an IDTMC specification. For each scheduler A of S, we have: S(A) S, hence sat(S) ⊆ sat(S).

Proof. The relation R ⊆ Q × S is defined by R = {(ρ, s) | lst(ρ) = s}.
We prove that the relation R is a satisfaction relation by defining δ (ρ,s) over Q × S as follows:

δ (ρ,s) (ρ , s ) = A(ρ)(s ) if ρ = ρ A(ρ) ---→ s , 0 otherwise. ( 1
)
The first condition results from the definition of the labeling and conditions 2 and 3 come from the fact that the joint distribution δ (ρ,s) is diagonal in this case.

2 (a) δ(ρ , S) = A(ρ)(s ) = ∆(ρ)(ρ ) with ρ = ρ A(ρ) ---→ s for all ρ ∈ Q. (b) δ(Q, s ) = A(ρ)(s ) ∈ T (s)(s ) with s = lst(ρ) for all s ∈ S.
3. ρ Rs whenever δ(ρ , s ) > 0 since s = lst(ρ ) by definition of R.

Indeed, for any scheduler A, S(A) is a kind of unfolding of S, which restricts the structure of S(A): at each step, the scheduler chooses a valid distribution among successor states. Hence not every implementation can be mapped to a scheduler. Said otherwise, not all implementations can be put in relation with S with a satisfaction relation where the joint distributions δ are diagonal. This means that the inclusion sat(S) ⊆ sat(S) is strict.

q0, a q1, b q2, b [ 1 2 , 1] [ 1 2 , 1] [1, 1] [1, 1] (a) A specification S0 q0, a q1, b q2, b 1 2 1 2 1 1 (b) A1, the only scheduling of S0 r0, a r1, b r2, b r3, b 1 3 1 3 1 3 1 1 1 (c) A2, an implementation
(not a scheduling) of S0 Fig. 2. A specification with an implementation that is not the result of scheduling.

For example, consider the specification S 0 of Fig. 2

(a).

There is a single possible scheduler for this specification: the one that picks in q 0 probability 1 2 to go to either q 1 or q 2 (A 1 in Fig. 2(b)). However, the PTS A 2 of Fig. 2(c) is also an implementation of this specification (A 2 |= S 0 ) where r 2 is split between q 1 and q 2 . The corresponding matrix is

δ(q 0 , r 0 ) =   r 0 r 1 r 2 r 3 q 0 1 0 0 0 q 1 0 1 3 1 6 0 q 2 0 0 1 6 1 3  
Finally, the refinement relation between specifications is simply defined as inclusion of the satisfaction sets: Definition 2.7 (Refinement). For two IDTMC specifications S 1 and S 2 , S 1 refines S 2 if sat(S 1 ) ⊆ sat(S 2 ).

Simulation relation

The notion of simulation relation between probabilistic specifications was introduced in [START_REF] Jonsson | Specification and refinement of probabilistic processes[END_REF], where it is proved to be a sufficient condition for refinement: S 2 simulates S 1 implies that all implementations of S 1 are implementations of S 2 . This notion is adapted to our setting in Definition 2.8 below. We then investigate the effect of simulation when implementations are considered with respect to schedulers only. Therefore we study the relations between sat(S 1 ) and sat(S 2 ) whenever S 2 simulates S 1 .

Definition 2.8 (Simulation relation).

For S 1 = (S 1 , s 1,init , T 1 , λ 1 ) and S 2 = (S 2 , s 2,init , T 2 , λ 2 ) two IDTMC specifications, S 2 simulates S 1 if there exists a relation R ⊆ S 1 × S 2 such that s 1,init Rs 2,init and if s 1 Rs 2 then:

1. λ 1 (s 1 ) = λ 2 (s 2 ), 2. there exists a function δ : S 1 → Dist(S 2 ) such that for all f ∈ T 1 (s 1 )
and

s 2 ∈ S 2 ,   s 1 ∈S 1 f (s 1 ) • δ(s 1 )(s 2 )   ∈ T 2 (s 2 )(s 2 ), (2)
3. s 1 Rs 2 whenever δ(s 1 )(s 2 ) > 0.

a q0

S1 : b q1 b q2 [ 1 3 , 2 3 ] [ 1 4 , 1 3 ] [1, 1] [1, 1] a r0 S2 : b r1 [0, 1] [1, 1] 1 1 1 Fig. 3. A simulation of S 1 by S 2 .
In Figure 3, dashed lines illustrate the simulation relation R of S 1 by S 2 labeled with δ(q i )(r j ) since for Condition (2), we may in this case uniformly use the function:

δ(q i )(r j ) = 1 if (q i , q j ) ∈ R 0 otherwise
Note that there is no simulation relation of S 2 by S 1 . Indeed, let f ∈ T 2 (r 0 ) defined as f (r 1 ) = 1. The only way to distribute f over S 1 in order to satisfy Eq. 2 is to distribute 2 3 of f to q 1 and 1 3 to q 2 . Hence, it forces to set δ(r 1 )(q 1 ) to 2 3 and δ(r 1 )(q 2 ) to 1 3 but this choice for δ is not uniform for any f ∈ T 2 (r 0 ) as it does not satisfy Eq. 2 for f (r 1 ) = 1 2 for instance. Let us notice that in the case of PTSs, Definition 2.8 is still valid but intervals reduce to points and Equation 2becomes

s 1 ∈S 1 ∆ 1 (s 1 )(s 1 ) • δ(s 1 )(s 2 ) = ∆ 2 (s 2 )(s 2 ).
(3)

Simulation vs satisfaction

Remark that not only simulation and satisfaction are defined over different kind of models, they express different requirements. Indeed, simulation is symmetrical in the models used but asymmetrical in its semantics since one model must contain the behavior of the other. In contrast, satisfaction concerns different models but the behavior of the PTS must exactly comply to the IDTMC specification: it can neither add behaviors nor introduce new ones. Nevertheless, these notions coincide when the simulated IDTMC is in fact a PTS: Proposition 2.9. Let A be a PTS satisfying an IDTMC specification S. Then S simulates A when seen as an IDTMC where intervals are reduced to a point.

Proof (Sketch). The core of the proof relies on building a function δ sim for the simulation relation, from function δ sat given by the satisfaction relation. For any pair of states q ∈ Q of PTS A and s ∈ S of IDTMC S, define δ sim (q, s) = δsat(q,s) δsat(q,S) . One can show that this δ sim satisfies Condition (2) of Definition 2.8. Also, as noted before, simulation implies inclusion of the set of implementations: Proposition 2.10 ( [START_REF] Jonsson | Specification and refinement of probabilistic processes[END_REF]). S 2 simulates S 1 implies that sat(S 1 ) ⊆ sat(S 2 ).

The original definition of opacity was given in [START_REF] Bryans | Opacity generalised to transition systems[END_REF] for (non probabilistic) transition systems, with respect to some observation function O and some predicate ϕ (the secret) on the runs of the system.

Opacity for probabilistic models

We consider an ω-regular set ϕ ⊆ Σ ω and we say that a run ρ of a PTS A satisfies ϕ if its trace belongs to ϕ. We consider also an observation function O : Σ ω → Σ ∞ ob , where Σ ob is a subset of Σ representing its visible part. If π ob is the standard projection from Σ ∞ onto Σ ∞ ob mapping any element a ∈ Σ \ Σ ob to ε, the observation function is defined on a word w by O(w) = π ob (w). Alternatively, we could consider a subset P ob of a set of observable atomic propositions P . Then, by setting P u = P \ P ob , Σ ob = 2 P ob and Σ u = 2 Pu , Σ could be viewed as the product Σ ob × Σ u . The observation function O would be then defined on a word w by O(w) = π 1 (w), where π 1 is the projection from (Σ ob × Σ u ) ∞ onto Σ ∞ ob mapping each element on its first component.

The observation class of a word w is [w] O = O -1 (O(w)): for the observer, each word in this class is undistinguishable from w. Then ϕ is opaque with respect to A and O if each time a word satisfies ϕ, another word in the same observation class does not. We denote by V(A, O, ϕ) the set of words violating this condition:

V(A, O, ϕ) = (Tr(A) ∩ ϕ) \ (O -1 (O(Tr(A) \ ϕ))).

Definition 3.1 (Opacity). Let A be a PTS, with observation function

O. A predicate ϕ is opaque in A for O if V(A, O, ϕ) = ∅.
Equivalently, ϕ is opaque if for any w satisfying ϕ, [w] O ϕ. Variants of opacity have been defined, with other observation functions and predicates, or by requiring symmetry: the predicate ϕ is symmetrically opaque in A for O if both ϕ and Σ ω \ ϕ are opaque.

The notion of probabilistic opacity [START_REF] Bérard | Quantifying opacity[END_REF] extends this boolean property by defining a measure of the set of runs violating opacity: For instance, recall systems A 1 and A 2 of Fig. 1. The secret predicate in this case is the set of runs ϕ b = abΣ ω and the observation function is the projection π {a,c,d} onto {a, c, d} ω . This predicate is not opaque since the run abd ω discloses the occurrence of b. This is measured by the disclosure: Disc(A 1 , π a,c,d , ϕ b ) = P A 1 (abd ω ) = 1 4 and Disc(A 2 , π a,c,d , ϕ b ) = P A 2 (abd ω ) = 3 4 . Note that dealing with symmetric opacity would simply require to add both measures for ϕ and Σ ω \ϕ. Also remark that disclosure only measures probabilities of the observer being sure that the run is in the secret. For example, one can model anonymity of an agent α initiating some protocol by defining ϕ α as the set of all runs initiated by α. Anonymity of α is then equivalent to opacity of ϕ α . In the case where anonymity is not guaranteed, disclosure provides a measure of the threat. In the case where anonymity holds, this measure will be 0 and does not give any insight on the "strength" of anonymity. Other notions measuring this strength were proposed in [START_REF] Chaum | The dining cryptographers problem: unconditional sender and recipient untraceability[END_REF][START_REF] Bhargava | Probabilistic anonymity[END_REF] and quantitative opacity for partial disclosure of the secret have also been defined in [START_REF] Bérard | Quantifying opacity[END_REF], although they are not linear hence do not fare well under standard optimization techniques.

In order to compare systems with respect to opacity, we consider two PTSs A 1 and A 2 over the same alphabet Σ, with a given observation function O. We say that A 1 is more opaque than

A 2 if Disc(A 1 , O, ϕ) ≤ Disc(A 2 , O, ϕ).
We lift the definition of probabilistic disclosure from PTSs to IDTMC specifications as follows:

Disc(S, O, ϕ) = sup A∈sat(S) Disc(A, O, ϕ)
From the results in [START_REF] Jonsson | Specification and refinement of probabilistic processes[END_REF] mentioned in Proposition 2.10, it is easy to see that if S 2 simulates S 1 , then Disc(S 1 , O, ϕ) ≤ Disc(S 2 , O, ϕ).

To obtain a similar result for the notion of satisfaction restricted to schedulers, we define the restriction of the disclosure to scheduled implementations:

Disc(S, O, ϕ) = sup A∈sat(S) Disc(A, O, ϕ) = sup A∈Sched(S)

Disc(S(A), O, ϕ)

Note that this notion differs from the similar one in [START_REF] Bérard | Probabilistic opacity for Markov decision processes[END_REF] for Markov Decision Processes. The notion presented here is finer since the set of runs measured by the disclosure depends on the scheduled implementation. In [START_REF] Bérard | Probabilistic opacity for Markov decision processes[END_REF], the set of runs of the disclosure is defined on the (unscheduled) MDP, and its probability is optimized afterwards. This would not be consistent in IDTMCs, since two scheduled implementations can have different sets of edges with non-null probability, as explained below.

Computing the probabilistic disclosure of a specification

When the interval of an edge of an IDTMC is non-punctual and closed on the left by 0, then this edge may be present or not in an implementation. Otherwise said, in the case of schedulers, this action can be completely blocked. In keeping with the terminology of [START_REF] Jonsson | Specification and refinement of probabilistic processes[END_REF], we call these edges modal edges, and IDTMCs that contain such edges are also called modal IDTMCs.

Definition 3.3 (Modal edge

). An edge T (s)(s ) in IDTMC S is modal if there exists a scheduler A such that in S(A), for any run ρ with lst(ρ) = s, ∆(ρ)(ρ

A(ρ) ---→ s ) = 0.
From a modeling point of view, modal edges add a lot of flexibility for refinement. This however means that the range of potential implementation is larger and so it will be harder to obtain meaningful properties. Therefore such edges are desirable in an early modeling phase but less so in the latest refinements. In the context of opacity, removing an edge drastically changes the disclosure, since it can remove ambiguities.

We illustrate the importance of modal edges when computing the disclosure of a specification. For example, consider the modal IDTMC S m of Fig. 4(a), with an observation function that observes a and b and a secret being the presence of c. An implementation of S m that blocks the direct edge from a to b (Fig. 4(c)) has a disclosure of 1, since the secret is guaranteed to be part of the only possible run. On the other hand, in the non-modal version of the IDTMC (Fig. 4(b)), such implementations are banned and only implementations that retain a small probability to avoid c are allowed. In these implementations, the disclosure is 0, since every run is observed as ab ω and it is possible that c did not occur.

a c b [0; 1] [0; 1] [1; 1] [1; 1] (a) A modal IDTMC Sm. a c b ]0; 1] ]0; 1] [1; 1] [1; 1] (b) A non-modal IDTMC Snm.
In the case of non-modal IDTMCs, disclosure can be computed. The proof relies on a translation from IMDP to MDP and synchronization with DPA; it can be found in Appendix A.

Theorem 3.4. Computing the value of disclosure for an IDTMC specification S without modal edges can be done in 2EXPTIME.

Remarks on modal edges. When a scheduler is faced with the choice to include or exclude a modal edge, it can produce several versions of PTSs, say A 1 and A 2 , with

Tr(A 1 ) = Tr(A 2 ), hence V(A 1 , O, ϕ) = V(A 2 , O, ϕ).
In addition, these choices may be history dependent, as in the example of Fig. 5, with ϕ = aΣ ω and only letters c and d being observed. Intuitively, a way for the scheduler to always disclose the presence of an initial a is to always follow an a by the same letter, say a c. However, this choice must be made after the first letter has been seen. Moreover, leaving the possibility of a run ad • • • to occur means that run ac • • • does not disclose ϕ. As a result, the scheduler should also take into account ϕ and the observation function before committing to a choice with respect to modal edges. So far, the general case of modal IDTMCs remains open.

Monotonicity of opacity under simulation

This section is devoted to the proof of the following result: Theorem 4.1. Let S 1 and S 2 be IDTMC specifications such that S 2 simulates S 1 . Then Disc(S 1 , O, ϕ) ≤ Disc(S 2 , O, ϕ).

Since scheduling is a restrictive way to derive implementations from a specification, it is not the case in general that sat(S 1 ) ⊆ sat(S 2 ): although any scheduling S 1 (A 1 ) of S 1 with A 1 is an implementation of S 2 (by Propositions 2.6 and 2.10), this implementation may not be a scheduling (as illustrated by the example of Fig. 2).

S 2 S 1 S 1 (A 1 ) S 2 (A 2 ) R sat 1 sat 1 • R R sat 2
Fig. 6. The result of Theorem 4.2. Relation sat 1 • R always exists but might not be a scheduling.

Instead, the proof builds a scheduler A 2 for S 2 that produces an implementation S 2 (A 2 ) that simulates S 1 (A 1 ) (Theorem 4.2, illustrated in Fig. 6). Then, this simulation is shown to ensure that the probabilities of (cones of) finite words coincide (Propositions 4.3 and 4.4). Disclosure being a measurable event, coincidence of probabilities on cones ensures coincidence of probabilities for the disclosure.

Notations. Given two specifications S 1 and S 2 such that S 2 simulates S 1 through relation R, we define the relation ∼ on FRuns(S 1 ) × FRuns(S 2 ) by:

ρ 1 ∼ ρ 2 if |ρ 1 | = |ρ 2 |
and at any intermediate step i, the corresponding states satisfy s 1,i Rs 2,i .

Let A 1 and A 2 be two schedulers of S 1 and S 2 , respectively. We set

A 1 = S 1 (A 1 ) and A 2 = S 2 (A 2 ), with respective sets of states Q 1 and Q 2 . For ρ 2 ∈ Q 2 , we set sim(ρ 2 ) = {ρ 1 ∈ Q 1 | ρ 1 ∼ ρ 2 }. We now define a measure µ ρ 2 over sim(ρ 2 ) by µ ρ 2 (ρ 1 ) = P A 1 (ρ 1 )
P A 1 (sim(ρ 2 )) (where the probability of finite run ρ is abusively written instead of the probability of its cone C ρ ).

We first show how to build a scheduler for S 2 that simulates the scheduling of S 1 . The proof of the theorem below is given in Appendix B. Theorem 4.2. Let S 1 and S 2 be IDTMC specifications such that S 2 simulates S 1 . Then for any A 1 ∈ Sched(S 1 ) there exists A 2 ∈ Sched(S 2 ) such that S 2 (A 2 ) simulates S 1 (A 1 ). Now we show that simulation between two PTSs is sufficient to compare their disclosure. Namely, we show that the probabilities of cones of words are equal in both systems. Note that although this property is well known to hold for paths, it needs to be lifted to words in order to compare disclosure.

We start by considering the sets of traces globally; although it is folklore that simulation implies trace inclusion, we provide a proof for completeness sake. Proof. We prove the proposition by induction on a strengthened statement. Namely, we claim that for every finite run in A 1 there exists a similar run in A 2 . Since an infinite run is the limit of the sequence of its finite prefixes, this claim is sufficient to prove the proposition. Assume by induction that the proposition holds for every word of length n. Let w ∈ FTr(A 1 ) of length n+1. We write w = w 0 a for some a ∈ Σ. Consider a run of A 1 that produces w. It is of the form ρ 0 s 1 where λ(s 1 ) = a; let s 1 = lst(ρ 0 ). Let ρ 0 be a run in A 2 , similar to ρ 0 , and s 2 = lst(ρ 0 ). By definition of simulation, there exists a function δ such that for any state

s 2 of A 2 , ∆ 2 (s 2 )(s 2 ) = σ 1 ∈S 1 ∆ 1 (s 1 )(σ 1 ) • δ(σ 1 )(s 2 ).
Moreover, whenever δ(σ 1 )(s 2 ) > 0, λ(s 1 ) = λ(s 2 ). Since δ(s 1 ) is a distribution over S 2 , δ(s 1 )(s 2 ) > 0 for at least one state s 2 . Hence ρ 0 s 2 is similar to ρ, which shows in particular that w ∈ FTr(A 2 ).

We additionally show that probabilities coincide: Proposition 4.4. Let A 1 and A 2 be PTSs such that A 2 simulates A 1 .

Then for all w ∈ Σ * ,

P A 1 (C w ) = P A 2 (C w ).
Since a given word may be produced by several paths, their probabilities should be considered altogether. Hence the proof of the above proposition is not immediate; it is quite technical and can be found in Appendix C.

Existing properties about simulation for PTSs can be retrieved as consequences of the above result. They were for example obtained as a particular case of sub-stochastic simulation in [START_REF] Baier | Comparative branching-time semantics for Markov chains[END_REF]. Although not necessary to prove the main theorem, these results illustrate how constraining simulation between PTSs is.

Recall that a probabilistic bisimulation [START_REF] Jonsson | Specification and refinement of probabilistic processes[END_REF] is a bisimulation that preserves transition probabilities, i.e. a bisimulation relation R on states such that for any equivalence class R of R, and any two related states sRs , ∆(s)(R) = ∆(s )(R).

Corollary 4.5 ([7]). Let A 1 and A 2 be PTSs such that A 2 simulates A 1 . Then there exists a probabilistic bisimulation over the union of both PTSs.

Corollary 4.6 ([7]). Let A 1 and A 2 be PTSs such that A 2 simulates A 1 . Then A 1 also simulates A 2 .

We are now ready to prove Theorem 4.1.

Proof. Let A 1 ∈ sat(S 1 ). By Theorem 4.2 there exists A 2 ∈ sat(S 2 ) that simulates A 1 . By Proposition 4.4, P A 1 (C w ) = P A 2 (C w ) for every word w ∈ FTr(A 1 ). Hence, for any ω-regular (hence measurable) language L, one has

P A 1 (L) = P A 2 (L). It is in particular the case for V(A 1 , O, ϕ) = V(A 2 , O, ϕ). Therefore, Disc(A 1 , O, ϕ) = Disc(A 2 , O, ϕ).
Consequently, the theorem holds.

Conclusion

This work investigates how refinement of probabilistic models impacts the security -modeled as opacity. We provide a procedure to compute the worst-case opacity for a subclass of IDTMCs, and we show that opacity is monotonic with respect to simulation when implementations are obtained through scheduling.

Directions for future work include computing disclosure for IDTMCs with modal edges. In addition, while we considered here only the worst case scenario, it would be interesting to handle both the worst and the best case, thus providing bounds on the disclosure of all possible implementations.

B Proof of Theorem 4.2

Let S 1 = (S 1 , s init,1 , T 1 , λ 1 ) and S 2 = (S 2 , s init,2 , T 2 λ 2 ) be interval-based specifications such that S 2 simulates S 1 with R. Let sat 1 be the satisfaction relation related to A 1 and A 1 = S 1 (A 1 ) = (Q 1 , q init,1 , ∆ 1 , L 1 ). Then we show that there exists A 2 ∈ Sched(S 2 ) and a simulation relation R such that sat 1 • R = R • sat 2 where sat 2 is the satisfaction relation related to A 2 . Then we define the scheduler A 2 by:

A 2 (ρ 2 )(s 2 ) = ρ 1 ∈sim(ρ 2 ) µ ρ 2 (ρ 1 ) s 1 ∈S 1 A 1 (ρ 1 )(s 1 ) • δ(s 1 )(s 2 ) for any s 2 ∈ S 2 , writing A 2 = S 2 (A 2 ) = (Q 2 , q init,2 , ∆ 2 , L 2 )
. Now the relation R can be defined as ∼ that relates runs that are similar "step by step", as defined above. To see that the conditions are satisfied, let ρ 1 and ρ 2 be runs in Q 1 and Q 2 respectively. Then the distribution δ is obtained by:

δ (ρ 1 )(ρ 2 ) = µ ρ 2 (ρ 1 )δ(lst(ρ 1 ))(lst(ρ 2 )) if ρ 1 ∼ ρ 2 , 0 otherwise.
Since A 1 and A 2 are PTSs, we just need to show that Equation (3) holds.

∆ 2 (ρ 2 )(ρ 2 ) = A 2 (ρ 2 )(s 2 ) = ρ 1 ∈sim(ρ 2 ) µ ρ 2 (ρ 1 ) s 1 ∈S 1 A 1 (ρ 1 )(s 1 ) • δ(s 1 )(s 2 ) and since ρ 2 = ρ 2 • s 2 = ρ 1 ∈sim(ρ 2 ) s 1 ∈S 1 A 1 (ρ 1 )(s 1 ) • δ (ρ 1 • s 1 )(ρ 2 ) = ρ 1 ∈Q 1 A 1 (ρ 1 )(s 1 ) • δ (ρ 1 )(ρ 2 )
by defining ρ 1 = ρ 1 • s 1 and remarking that δ = 0 if its arguments are not similar runs

∆ 2 (ρ 2 )(ρ 2 ) = ρ 1 ∈Q 1 ∆ 1 (ρ 1 )(ρ 1 ) • δ (ρ 1 )(ρ 2 ).

C Proof of Proposition 4.4

Assume by induction that the proposition holds for every word of length n. Let w ∈ FTr(A 1 ) = FTr(A 2 ) (recall Proposition 4.3) of length n + 1 with w = w 0 a for some a ∈ Σ. A run ρ of A 2 that produces w can be assumed to be of the form ρ = ρ 0 s 2 with tr(ρ 0 ) = w 0 and λ(s 2 ) = a.

Then P A 2 (C ρ ) = P A 2 (C ρ 0 )∆ 2 (s 2 )(s 2 )
where s 2 = lst(ρ 0 ) and hence

P A 2 (C w ) = ρ ∈FRuns(A 2 ) tr(ρ )=w P A 2 (C ρ ) = s 2 ,s 2 ∈S 2 ρ 0 ∈FRuns(A 2 ) tr(ρ 0 )=w 0 , lst(ρ 0 )=s 2 ,lst(ρ )=s 2 P A 2 (C ρ 0 )∆ 2 (s 2 )(s 2 ) Now let A 1 s.t. A 2 simulates A 1 then, as ρ 0 ∈FRuns(A 1 )
ρ 0 ∼ρ 0 lst(ρ 0 )=s 1 µ ρ 0 (ρ 0 ) = s 1 ∈S 1 ρ 0 ∈FRuns(A 1 ) ρ 0 ∼ρ 0 lst(ρ 0 )=s 1 µ ρ 0 (ρ 0 ) = 1 we get that

P A 2 (C w ) = s 2 ,s 2 ∈S 2 ρ 0 ∈FRuns(A 2 )
tr(ρ 0 )=w 0 , lst(ρ 0 )=s 2 ,lst(ρ )=s 2

P A 2 (C ρ 0 )∆ 2 (s 2 )(s 2 ) • s 1 ∈S 1 ρ 0 ∈FRuns(A 1 )
ρ 0 ∼ρ 0 lst(ρ 0 )=s 1 µ ρ 0 (ρ 0 )

P A 2 (C w ) = s 1 ∈S 1 s 2 ,s 2 ∈S 2
ρ 0 ∈FRuns(A 2 ) tr(ρ 0 )=w 0 , lst(ρ 0 )=s 2 ,lst(ρ )=s 2 P A 2 (C ρ 0 )∆ 2 (s 2 )(s 2 ) ρ 0 ∈FRuns(A 1 ) ρ 0 ∼ρ 0 lst(ρ 0 )=s 1 µ ρ 0 (ρ 0 )

As the terms are null if it is not the case that s 1 Rs 2 , we have:

Fig. 1 .

 1 Fig. 1. Probabilistic systems A 1 or A 2 implementing underspecified system S.

Definition 3 . 2 (

 32 Probabilistic Disclosure). Let A be a PTS, with observation function O and ω-regular predicate ϕ. The probabilistic disclosure of ϕ in A for O is Disc(A, O, ϕ) = P A (V(A, O, ϕ)).

  A non-disclosing implementation of Snm (and Sm), ε > 0.

Fig. 4 .

 4 Fig. 4. The influence of modal transitions on disclosure.

Fig. 5 .

 5 Fig. 5. IDTMC where the choice on modal edge requires history.

Proposition 4 . 3 .

 43 Let A 1 and A 2 be PTSs such that A 2 simulates A 1 . Then T r(A 1 ) = T r(A 2 ).

= s 1 2 P A 2 (C ρ 0 ) s 1 ∈S 1 ∆ 1 2 P A 2 (P A 2 (C ρ 0 ) = s 1 1 P A 1 ( 1 P A 1 (s 1 ∆ 1 (s 1 )(s 1 ) 1 P A 1 (C ρ 0 ) = s 1 1 P A 1 (C ρ 0 ) s 1

 122111222111111111111111 ∈S 1 s 2 ,s 2 ∈S 2 ρ 0 ∈FRuns(A 2 ) tr(ρ 0 )=w 0 , lst(ρ 0 )=s 2 ,lst(ρ )=s (s 1 )(s 1 ) • δ s 1 ,s 2 (s 1 )(s 2 )ρ 0 ∈FRuns(A 1 )ρ 0 ∼ρ 0 lst(ρ 0 )=s 1 µ ρ 0 (ρ 0 ) And as the terms are null if λ(s 1 ) = λ(s 2 ) = λ(lst(ρ)), we have:= s 1 ∈S 1 s 2 ,s 2 ∈S 2 ρ 0 ∈FRuns(A 2 ) tr(ρ 0 )=w 0 , lst(ρ 0 )=s 2 ,lst(ρ )=s 2 P A 2 (C ρ 0 ) s 1 ∈S 1 λ(s 1 )=λ(lst(ρ)) ∆ 1 (s 1 )(s 1 ) • δ s 1 ,s 2 (s 1 )(s 2 ) ρ 0 ∈FRuns(A 1 ) ρ 0 ∼ρ 0 lst(ρ 0 )=s 1 µ ρ 0 (ρ 0 ) = s 1 ∈S 1 s 1 ∈S 1 λ(s 1 )=λ(lst(ρ)) s 2 ∈S 2 s 2 ∈S 2 δ s 1 ,s 2 (s 1 )(s 2 ) ∈FRuns(A 2 ) tr(ρ 0 )=w 0 , lst(ρ 0 )=s 2 ,lst(ρ )=s 2 P A 2 (C ρ 0 )∆ 1 (s 1 )(s 1 ) ρ 0 ∈FRuns(A 1 ) ρ 0 ∼ρ 0 lst(ρ 0 )=s 1 µ ρ 0 (ρ 0 ) And since s 2 ∈S 2 δ s 1 ,s 2 (s 1 )(s 2 ) = 1, we have: = s 1 ∈S 1 s 1 ∈S 1 λ(s 1 )=λ(lst(ρ)) s 2 ∈S 2 ρ 0 ∈FRuns(A 2 ) tr(ρ 0 )=w 0 , lst(ρ 0 )=s C ρ 0 )∆ 1 (s 1 )(s 1 ) ρ 0 ∈FRuns(A 1 ) ρ 0 ∼ρ 0 lst(ρ 0 )=s 1 µ ρ 0 (ρ 0 ) P A 2 (C w ) = s 1 ∈S 1 s 1 ∈S 1 λ(s 1 )=λ(lst(ρ)) ρ 0 ∈FRuns(A 2 ) tr(ρ 0 )=w 0 P A 2 (C ρ 0 )∆ 1 (s 1 )(s 1 ) ρ 0 ∈FRuns(A 1 ) ρ 0 ∼ρ 0 lst(ρ 0 )=s 1 µ ρ 0 (ρ 0 ) P A 2 (C w ) = s 1 ∈S 1 s 1 ∈S 1 λ(s 1 )=λ(lst(ρ)) ∆ 1 (s 1 )(s 1 ) ρ 0 ∈FRuns(A 2 ) tr(ρ 0 )=w 0 ρ 0 ∈FRuns(A 1 ) ρ 0 ∼ρ 0 lst(ρ 0 )=s 1 P A 2 (C ρ 0 )µ ρ 0 (ρ 0 ) = s 1 ∈S 1 s 1 ∈S 1 λ(s 1 )=λ(lst(ρ)) ∆ 1 (s 1 )(s 1 ) ρ 0 ∈FRuns(A 2 ) tr(ρ 0 )=w 0 ρ 0 ∈FRuns(A 1 ) ρ 0 ∼ρ 0 lst(ρ 0 )=s 1 P A 2 (C ρ 0 ) P A 1 (C ρ 0 ) P A 1 (sim(ρ 0 )) = s 1 ∈S 1 s 1 ∈S 1 λ(s 1 )=λ(lst(ρ)) ∆ 1 (s 1 )(s 1 ) ρ 0 ∈FRuns(A 1 ) tr(ρ 0 )=w 0 lst(ρ 0 )=s 1 P A 1 (C ρ 0 ) P A 1 (sim(ρ 0 )) • ρ 0 ∈FRuns(A 2 ) tr(ρ 0 )=w 0 ∈S 1 s 1 ∈S 1 λ(s 1 )=λ(lst(ρ)) ∆ 1 (s 1 )(s 1 ) ρ 0 ∈FRuns(A 1 ) tr(ρ 0 )=w 0 lst(ρ 0 )=s C ρ 0 ) P A 1 (sim(ρ 0 )) • P A 2 (C w 0 )and by induction hypothesis, P A 2 (C w 0 ) = P A 1 (C w 0 ):= s 1 ∈S 1 s 1 ∈S 1 λ(s 1 )=λ(lst(ρ)) ∆ 1 (s 1 )(s 1 ) ρ 0 ∈FRuns(A 1 ) tr(ρ 0 )=w 0 lst(ρ 0 )=s C ρ 0 ) P A 1 (sim(ρ 0 )) • P A 1 (C w 0 ) and since P A 1 (sim(ρ 0 )) = P A 1 (C w 0 ): = ∈S 1 s 1 ∈S 1 λ(s 1 )=λ(lst(ρ))ρ 0 ∈FRuns(A 1 ) tr(ρ 0 )=w 0 lst(ρ 0 )=s ∈S 1 ρ 0 ∈FRuns(A 1 ) tr(ρ 0 )=w 0 lst(ρ 0 )=s ∈S 1 λ(s 1 )=λ(lst(ρ))∆ 1 (s 1 )(s 1 ) = ρ 0 ∈FRuns(A 1 ) tr(ρ 0 )=w 0 P A 1 (C ρ 0 )∆ 1 (lst(ρ 0 ))(lst(ρ))P A 2 (C w ) = P A 1 (C w )

Partially supported by a grant from Coopération France-Québec, Service Coopération et Action Culturelle 2012/26/SCAC (French Government), the NSERC Discovery Individual grant No. 13321 (Government of Canada), the FQRNT Team grant No. 167440 (Quebec's Government) and the CFQCU France-Quebec Cooperative grant No. 167671 (Quebec's Government). This research has been partially done while this author was visiting the LIP6, Université Pierre & Marie Curie.

A Computing the probabilistic disclosure of a specification

A.1 Detecting modal edges.

The detection of modal edges is the first step toward computation of the disclosure of an IDTMC.

Proposition A.1. The set of modal edges can be computed in time polynomial in the number of edges.

Proof. The decision procedure for each edge is as follows:

if an edge is not weighted by an interval containing 0, it is not modal; otherwise, compute the sum of maximal interval values of all other edges stemming from the same state;

• if this sum is > 1, the edge is modal;

• if this sum is < 1, the edge is not modal;

• otherwise (the sum is = 1), the edge is modal if, and only if, all intervals of other outgoing edges are closed on the right.

Note that the procedure does not rely entirely on the syntactic criterion of an interval closed on 0: it is sufficient but may lead to false positives. For example, consider a state with two outgoing edges e 1 , [ 1 4 ; 2 3 ] and e 2 , [0; 1]. The e 2 edge is not actually modal since any probability distribution satisfying the specification can give at most 2 3 to e 1 , hence must at least give weight 1 3 to e 2 . This is avoided by the pre-computation of the least possible probability that can be put on an edge.

A.2 IDTMC without modal edges.

We now prove Theorem 3.4.

Note that intervals may be closed or open on any non-zero bound, which is not the case of IDTMCs in [START_REF] Chatterjee | Model-checking omega-regular properties of interval markov chains[END_REF] where all intervals are closed. Hence although our procedure uses some of the ideas of Chatterjee et al [START_REF] Chatterjee | Model-checking omega-regular properties of interval markov chains[END_REF], it is adapted to deal with open intervals.

First remark that there exists a regular language K such that for any scheduler A, Tr(S(A)) = K. This is only true because S is assumed nonmodal. Let A K be a PTS such that Tr(A K ) = K; it can be chosen of size |S|. By the definition of disclosure, if the secret ϕ is ω-regular and the observation function O is a projection (see Section 3), then finding the supremum of the disclosure means finding the maximal probability to reach an ω-regular set of runs, namely

Then open intervals can be safely ignored when trying to optimize the probability of V(A K , O, ϕ), i.e. they are treated as closed ones. Indeed, if the optimal scheduler uses a value x which is the bound of an open interval, then one can build a family of schedulers using value x ± 1 2 n for the nth scheduler. The limit probability of reaching V(A K , O, ϕ) is therefore the one computed when using exact value x. Remark that using closed intervals may introduce intervals containing 0, although it is of no concern since the observation classes are already defined and may not change, only their probability may change. Said otherwise, this does not mean that we are computing disclosure of the closed version, since it is only a probability. On the example of Fig. 4(b), it means trying to compute the maximal probability of the empty set, which is indeed zero.

The procedure is hence as follows. Starting from a DPA A ϕ for ϕ, a DPA A V for V(A K , O, ϕ) can be built, with size exponential in the size of S and A ϕ (and with a number k of colors polynomial in the size of A and A ϕ ). This construction relies on intersections and complementations of DPA, with a determinization step that brings the exponential blowup [START_REF] Piterman | From nondeterministic Büchi and Streett automata to deterministic parity automata[END_REF].

The construction of [START_REF] Chatterjee | Model-checking omega-regular properties of interval markov chains[END_REF] yields a memoryless scheduler, although it is memoryless on the product, and hence is finite-memory on the original IDTMC. The procedure of [START_REF] Chatterjee | Model-checking omega-regular properties of interval markov chains[END_REF] is in EXPTIME with respect to the size of its input, hence computation of disclosure is doubly exponential: