Benoît Delahaye
email: benoit.delahaye@inria.fr

Uli Fahrenberg
email: ulrich.fahrenberg@inria.fr

Kim Guldstrand Larsen

Axel Legay
email: axel.legay@inria.fr

Refinement and Difference for Probabilistic Automata

come

Introduction

Probabilistic automata as promoted by Segala and Lynch [START_REF] Segala | Probabilistic simulations for probabilistic processes[END_REF] are a widely-used formalism for modeling systems with probabilistic behavior. These include randomized security and communication protocols, distributed systems, biological processes and many other applications. Probabilistic model checking [START_REF] Hinton | PRISM: A tool for automatic verification of probabilistic systems[END_REF][START_REF] Baier | Principles of Model Checking[END_REF][START_REF] Vardi | Automatic verification of probabilistic concurrent finite-state programs[END_REF] is then used to analyze and verify the behavior of such systems. Given the prevalence of applications of such systems, probabilistic model checking is a field of great interest. However, and similarly to the situation for non-probabilistic model checking, probabilistic model checking suffers from state space explosion, which hinders its applicability considerably.

One generally successful technique for combating state space explosion is the use of compositional techniques, where a (probabilistic) system is model checked by verifying its components one by one. This compositionality can be obtained by decomposition, that is, to check whether a given system satisfies a property, the system is automatically decomposed into components which are then verified. Several attempts at such automatic decomposition techniques have been made [START_REF] Cobleigh | Learning assumptions for compositional verification[END_REF][START_REF] Kwiatkowska | Assume-guarantee verification for probabilistic systems[END_REF], but in general, this approach has not been very successful [START_REF] Cobleigh | Breaking up is hard to do: An evaluation of automated assume-guarantee reasoning[END_REF].

As an alternative to the standard model checking approaches using logical specifications, such as e.g. LTL, MITL or PCTL [START_REF] Manna | The Temporal Logic of Reactive and Concurrent Systems[END_REF][START_REF] Alur | The benefits of relaxing punctuality[END_REF][START_REF] Hansson | A logic for reasoning about time and reliability[END_REF], automata-based specification theories have been proposed, such as Input/Output Automata [START_REF] Lynch | An introduction to Input/Output automata[END_REF], Interface Automata [START_REF] Alfaro | Interface automata[END_REF], and Modal Specifications [START_REF] Larsen | Modal specifications[END_REF][START_REF] Raclet | Quotient de spécifications pour la réutilisation de composants[END_REF][START_REF] Bauer | General quantitative specification theories with modalities[END_REF]. These support composition at specification level; hence a model which naturally consists of a composition of several components can be verified by model checking each component on its own, against its own specification. The overall model will then automatically satisfy the composition of the component specifications. Remark that this solves the decomposition problem mentioned above: instead of trying to automatically decompose a system for verification, specification theories make it possible to verify the system without constructing it in the first place. exact difference is zero: hence any superfluous PAs which are captured by the overapproximation are infinitesimally close to the real difference. Taken together, these approximations hence solve the problem of assessing the precise difference between deterministic APAs in case of failing refinement.

We restrict ourselves to the subclass of deterministic APAs, as it allows syntactic reasoning to decide and compute refinement. Indeed, for deterministic APAs, syntactic refinement coincides with semantic refinement, hence allowing for efficient procedures. Note that although the class of APAs we consider is called "deterministic", it still offers non-determinism in the sense that one can choose between different actions in a given state.

Related work. This paper embeds into a series of articles on APA as a specification theory [14][START_REF] Delahaye | New results on abstract probabilistic automata[END_REF][START_REF] Delahaye | APAC: A tool for reasoning about abstract probabilistic automata[END_REF]. In [14] we introduce deterministic APA, generalizing earlier work on interval-based abstractions of probabilistic systems [START_REF] Fecher | Don't know in probabilistic systems[END_REF][START_REF] Jonsson | Specification and refinement of probabilistic processes[END_REF][START_REF] Katoen | Three-valued abstraction for continuous-time Markov chains[END_REF], and define notions of refinement, logical composition, and structural composition for them. We also introduce a notion of compositional abstraction for APA. In [START_REF] Delahaye | New results on abstract probabilistic automata[END_REF] we extend this setting to nondeterministic APA and give a notion of (lossy) determinization, and in [START_REF] Delahaye | APAC: A tool for reasoning about abstract probabilistic automata[END_REF] we introduce the tool APAC. The distance and difference we introduce in the present paper complement the refinement and abstraction from [14].

Compositional abstraction of APA is also considered in [START_REF] Sher | Compositional abstraction techniques for probabilistic automata[END_REF], but using a different refinement relation. Differences between specifications are developed in [START_REF] Sassolas | Exploring inconsistencies between modal transition systems[END_REF] for the formalism of modal transition systems, and distances between specifications, in the variant of weighted modal automata, have been considered in [START_REF] Bauer | General quantitative specification theories with modalities[END_REF]. Distances between probabilistic systems have been introduced in [START_REF] De Alfaro | Game relations and metrics[END_REF][START_REF] Desharnais | Metrics for labelled Markov processes[END_REF][START_REF] Van Breugel | An intrinsic characterization of approximate probabilistic bisimilarity[END_REF].

The originality of our present work is, then, the ability to measure how far away one probabilistic specification is from being a refinement of another, using distances and our new difference operator. Both are important in assessing precisely how much one APA differs from another.

Acknowledgement. The authors wish to thank Joost-Pieter Katoen for interesting discussions and insightful comments on the subject of this work.

Background

Let Dist(S) denote the set of all discrete probability distributions over a finite set S and B 2 = {⊤, ⊥}. Definition 1. A probabilistic automaton (PA) [START_REF] Segala | Probabilistic simulations for probabilistic processes[END_REF] is a tuple (S, A, L, AP, V, s 0 ), where S is a finite set of states with the initial state s 0 ∈ S, A is a finite set of actions, L: S × A × Dist(S) → B 2 is a (two-valued) transition function, AP is a finite set of atomic propositions and V : S → 2 AP is a state-labeling function. Consider a state s, an action a, and a probability distribution µ. The value of L(s, a, µ) is set to ⊤ in case there exists a transition from s under action a to a distribution µ on successor states. In other cases, we have L(s, a, µ) = ⊥. We now introduce Abstract Probabilistic Automata (APA) [14], that is a specification theory for PAs. For a finite set S, we let C(S) denote the set of constraints over discrete probability distributions on S. Each element ϕ ∈ C(S) describes a set of distributions: Sat(ϕ) ⊆ Dist(S). Let B 3 = {⊤, ?, ⊥}. APAs are formally defined as follows.

We write µ ⋐ δ R µ ′ if µ is simulated by µ ′ w.r.t R and δ, and µ ⋐ R µ ′ if there exists δ with µ ⋐ δ R µ ′ .

We will also need distribution simulations without the requirement of a relation R ⊆ S × S ′ (hence also without claim 3 above); these we denote by µ ⋐ δ µ ′ . Definition 4 ( [14]).

Let N 1 = (S 1 , A, L 1 , AP, V 1 , S 1 0 ) and N 2 = (S 2 , A, L 2 , AP, V 2 , S 2 0 ) be APAs. A relation R ⊆ S 1 × S 2 is a refinement relation if and only if, for all (s 1 , s 2 ) ∈ R, we have V 1 (s 1 ) ⊆ V 2 (s 2 ) and 1. ∀a ∈ A, ∀ϕ 2 ∈ C(S 2 ), if L 2 (s 2 , a, ϕ 2 ) = ⊤, then ∃ϕ 1 ∈ C(S 1 ) : L 1 (s 1 , a, ϕ 1 ) = ⊤ and ∀µ 1 ∈ Sat(ϕ 1 ), ∃µ 2 ∈ Sat(ϕ 2 ) such that µ 1 ⋐ R µ 2 , 2. ∀a ∈ A, ∀ϕ 1 ∈ C(S 1 ), if L 1 (s 1 , a, ϕ 1 ) = ⊥, then ∃ϕ 2 ∈ C(S 2 ) such that L 2 (s 2 , a, ϕ 2 ) = ⊥ and ∀µ 1 ∈ Sat(ϕ 1 ), ∃µ 2 ∈ Sat(ϕ 2 ) such that µ 1 ⋐ R µ 2 .
We say that N 1 refines N 2 , denoted N 1 N 2 , iff there exists a refinement relation such that ∀s 1 0 ∈ S 1 0 , ∃s 2 0 ∈ S 2 0 : (s 1 0 , s 2 0 ) ∈ R. Since any PA P is also an APA, we say that P satisfies N (or equivalently P implements N ), denoted P |= N , iff P N . In [14], it is shown that for deterministic APAs N 1 , N 2 , we have

N 1 N 2 ⇐⇒ [[N 1 ]] ⊆ [[N 2 ]], where [[N i ]] denotes the set of implementations of APA N i . Hence for deterministic APAs, the difference [[N 1 ]] \ [[N 2 ]] is non-empty iff N 1 N 2 .
This equivalence breaks for non-deterministic APAs [14], whence we develop our theory only for deterministic APAs.

To show a convergence theorem about our difference construction in Sect. 4.2 below, we need a relaxed notion of refinement which takes into account that APAs are a quantitative formalism. Indeed, refinement as of Def. 4 is a purely qualitative relation; if both N 2 N 1 and N 3 N 1 , then there are no criteria to compare N 2 and N 3 with respect to N 1 , saying which one is the closest to N 1 . We provide such a relaxed notion by generalizing refinement to a discounted distance which provides precisely such criteria. In Sect. 4.2, we will show how those distances can be used to prove that increasingly precise difference approximations between APAs converge to the real difference. The next definition shows how a distance between states is lifted to a distance between constraints.

Definition 5. Let d : S 1 × S 2 → R + and ϕ 1 ∈ C(S 1 ), ϕ 2 ∈ C(S 2 ) be constraints in N 1 and N 2 . Define the distance D N1,N2 between ϕ 1 and ϕ 2 as follows:

D N1,N2 (ϕ 1 , ϕ 2 , d) = sup µ1∈Sat(ϕ1) inf µ2∈Sat(ϕ2) inf δ:µ1⋐ δ µ2 (s1,s2)∈S1×S2 µ 1 (s 1 )δ(s 1 )(s 2 )d(s 1 , s 2 )
For the definition of d below, we say that states

s 1 ∈ S 1 , s 2 ∈ S 2 are not compatible if either (1) V 1 (s 1 ) = V 2 (s 2 ), (2
) there exists a ∈ A and ϕ 1 ∈ C(S 1 ) such that L 1 (s 1 , a, ϕ 1 ) = ⊥ and for all ϕ 2 ∈ C(S 2 ), L 2 (s 2 , a, ϕ 2 ) = ⊥, or (3) there exists a ∈ A and ϕ 2 ∈ C(S 2 ) such that L 2 (s 2 , a, ϕ 2 ) = ⊤ and for all ϕ 1 ∈ C(S 1 ), L 1 (s 1 , a, ϕ 1 ) = ⊤. For compatible states, their distance is similar to the accumulating branching distance on modal transition systems as introduced in [START_REF] Bauer | General quantitative specification theories with modalities[END_REF][START_REF] Thrane | Quantitative analysis of weighted transition systems[END_REF], adapted to our formalism. In the rest of the paper, the real constant 0 < λ < 1 represents a discount factor. Formally, d : S 1 × S 2 → [0, 1] is the least fixpoint to the following system of equations:

d(s 1 , s 2 ) = (1)        1 if s 1 is not compatible with s 2 max    max {a,ϕ1:L1(s1,a,ϕ1) =⊥} min {ϕ2:L2(s2,a,ϕ2) =⊥} λD N1,N2 (ϕ 1 , ϕ 2 , d) max {a,ϕ2:L2(s2,a,ϕ2)=⊤} min {ϕ1:L1(s1,a,ϕ1)=⊤} λD N1,N2 (ϕ 1 , ϕ 2 , d) otherwise
Since the above system of linear equations defines a contraction, the existence and uniqueness of its least fixpoint is ensured, cf. [START_REF] Larsen | Metrics for weighted transition systems: Axiomatization and complexity[END_REF]. This definition intuitively extends to PAs, which allows us to propose the two following notions of distance:

Definition 6. Let N 1 = (S 1 , A, L 1 , AP, V 1 , S 1 0 ) and N 2 = (S 2 , A, L 2 , AP, V 2 , S 2
0 ) be APAs in SVNF. The syntactic distance and thorough distances between N 1 and N 2 are defined as follows:

-Syntactic distance.

d(N 1 , N 2 ) = max s 1 0 ∈S 1 0 min s 2 0 ∈S 2 0 d(s 1 0 , s 2 0 ) . -Thorough distance. d t (N 1 , N 2 ) = sup P1∈[[N1]] inf P2∈[[N2]] d(P 1 , P 2 ) .
Note that the notion of thorough distance defined above intuitively extends to sets of PAs: given two sets of PAs S 1 , S 2 , we have

d t (S 1 , S 2 ) = sup P1∈S1 inf P2∈S2 d(P 1 , P 2 ) .
The intuition here is that d(s 1 , s 2 ) compares not only the probability distributions at s 1 and s 2 , but also (recursively) the distributions at all states reachable from s 1 and s 2 , weighted by their probability. Each step is discounted by λ, hence steps further in the future contribute less to the distance. We also remark that N 1 N 2 implies d(N 1 , N 2 ) = 0. It can easily be shown, cf. [START_REF] Thrane | Quantitative analysis of weighted transition systems[END_REF], that both d and d t are asymmetric pseudometrics (or hemimetrics), i.e. satisfying d(N 1 , N 1 ) = 0 and d(N 1 , N 2 ) + d(N 2 , N 3 ) ≥ d(N 1 , N 3 ) for all APAs N 1 , N 2 , N 3 (and similarly for d t ). The fact that they are only pseudometrics, i.e. that d(N 1 , N 2 ) = 0 does not imply N 1 = N 2 , will play a role in our convergence arguments later. The following proposition shows that the thorough distance is bounded above by the syntactic distance. Hence we can bound distances between (sets of) implementations by the syntactic distance between their specifications. Proposition 1. For all APAs N 1 and N 2 in SVNF, it holds that

d t (N 1 , N 2 ) ≤ d(N 1 , N 2 ).

Difference Operators for Deterministic APAs

The difference N 1 \ N 2 of two APAs N 1 , N 2 is meant to be a syntactic representation of all counterexamples, i.e. all PAs P for which

P ∈ [[N 1 ]] but P / ∈ [[N 2 ]
]. We will see later that such difference cannot be an APA itself; instead we will approximate it using APAs.

Because N 1 and N 2 are deterministic, we know that the difference

[[N 1 ]] \ [[N 2 ]] is non-empty if and only if N 1 N 2 .
So let us assume that N 1 N 2 , and let R be a maximal refinement relation between N 1 and N 2 . Since N 1 N 2 , we know that (s 1 0 , s 2 0 ) ∈ R. Given (s 1 , s 2 ) ∈ S 1 × S 2 , we can distinguish between the following cases:

1. (s 1 , s 2 ) ∈ R 2. V 1 (s 1 ) = V 2 (s 2 ), 3. (s 1 , s 2 ) ∈ R and V 1 (s 1 ) = V 2 (s 2 ),
∈ C(S 1 ) : L 1 (s 1 , e, ϕ 1 ) = ⊥, ϕ2 s2 s1 e e, ⊤ (e)
there exists e ∈ A and

ϕ 2 ∈ C(S 2 ) such that L 2 (s 2 , e, ϕ 2 ) = ⊤ and ∃ϕ 1 ∈ C(S 1 ) : L 1 (s 1 , e, ϕ 1 ) =?, ϕ2 s2 ϕ1 s1 e, ? e, ⊤
(f) there exists e ∈ A and

ϕ 2 ∈ C(S 2 ) such that L 2 (s 2 , e, ϕ 2 ) = ⊤, ∃ϕ 1 ∈ C(S 1 ) : L 1 (s 1 , e, ϕ 1 ) = ⊤ and ∃µ ∈ Sat(ϕ 1 ) such that ∀µ ′ ∈ Sat(ϕ 2 ) : µ ⋐ R µ ′ . s2 s1 ϕ1 ϕ2 = e, ⊤ e, ⊤
Remark that because of the determinism and SVNF of APAs N 1 and N 2 , cases 1, 2 and 3 cannot happen at the same time. Moreover, although the cases in 3 can happen simultaneously, they cannot be "triggered" by the same action. In order to keep track of these "concurrent" situations, we define the following sets.

Given a pair of states (s 1 , s 2 ), let us define B a (s 1 , s 2 ) to be the set of actions in A such that case 3.a above holds. If there is no such action, then

B a (s 1 , s 2 ) = ∅. Similarly, we define B b (s 1 , s 2 ), B c (s 1 , s 2 ), B d (s 1 , s 2 ), B e (s 1 , s 2 ) and B f (s 1 , s 2 )
to be the sets of actions such that cases 3.b, c, d, e and 3.f holds respectively. Given a set

X ⊆ {a, b, c, d, e, f }, let B X (s 1 , s 2 ) = ∪ x∈X B x (s 1 , s 2 ). In addition, let B(s 1 , s 2 ) = B {a,b,c,d,e,f } (s 1 , s 2 ).

Over-Approximating Difference

We now try to compute an APA that represents the difference between the sets of implementations of two APAs. We first observe that such a set may not be representable by an APA, then we will propose over-and under-approximations. Consider the APAs N 1 and N 2 given in Figures 1a and1b, where α = β = γ. Consider the difference of their sets of implementations. It is easy to see that this set contains all the PAs that can finitely loop on valuation α and then move into a state with valuation β. Since there is no bound on the time spent in the loop, there is no finite-state APA that can represent this set of implementations.

1 2 {{α}} {{β}} a, ϕ1, ⊤ (µ(1) = 1) ∨ (µ(2) = 1) µ ∈ Sat(ϕ1) ⇐⇒ (a) APA N1 A B {{α}} {{γ}} a, ϕ2, ⊤ µ ∈ Sat(ϕ2) ⇐⇒ (µ(A) = 1) ∨ (µ(B) = 1) (b) APA N2 Fig. 1: APAs N1 and N2 such that [[N1]] \ [[N2]
] cannot be represented using a finite-state APA.

Now we propose a construction \ * that over-approximates the difference between APAs in the following sense: given two deterministic APAs

N 1 = (S 1 , A, L 1 , AP, V 1 , {s 1 0 }) and N 2 = (S 2 , A, L 2 , AP, V 2 , {s 2 0 }) in SVNF, such that N 1 N 2 , we have [[N 1 ]] \ [[N 2 ]] ⊆ [[N 1 \ * N 2 ]]. We first observe that if V 1 (s 1 0 ) = V 2 (s 2 0 ), i.e. (s 1 0 , s 2 0 ) in case 2, then [[N 1 ]] ∩ [[N 2 ]] = ∅. In such case, we define N 1 \ * N 2 as N 1 .
Otherwise, we build on the reasons for which refinement fails between N 1 and N 2 . Note that the assumption N 1 N 2 implies that the pair (s 1 0 , s 2 0 ) can never be in any refinement relation, hence in case 1. We first give an informal intuition of how the construction works and then define it formally.

In our construction, states in N 1 \ * N 2 will be elements of S 1 ×(S 2 ∪{⊥})×(A∪{ε}). Our objective is to ensure that any implementation of our constructed APA will satisfy N 1 and not N 2 . In (s 1 , s 2 , e), states s 1 and s 2 keep track of executions of N 1 and N 2 . Action e is the action of N 1 that will be used to break satisfaction with respect to N 2 , i.e. the action that will be the cause for which any implementation of (s 1 , s 2 , e) cannot satisfy N 2 . Since satisfaction is defined recursively, the breaking is not necessarily immediate and can be postponed to successors. ⊥ is used to represent states that can only be reached after breaking the satisfaction relation to N 2 . In these states, we do not need to keep track of the corresponding execution in N 2 , thus only focus on satisfying N 1 . States of the form (s 1 , s 2 , ε) with s 2 = ⊥ are states where the satisfaction is broken by a distribution that does not match constraints in N 2 (cases 3.c and 3.f). In order to invalidate these constraints, we still need to keep track of the corresponding execution in N 2 , hence the use of ε instead of ⊥.

The transitions in our construction will match the different cases shown in the previous section, ensuring that in each state, either the relation is broken immediately or reported to at least one successor. Since there can be several ways of breaking the relation in state (s 1 0 , s 2 0 ), each corresponding to an action e ∈ B(s 1 0 , s 2 0 ), the APA N 1 \ * N 2 will have one initial state for each of them. Formally, if (s 1 0 , s 2 0 ) is in case 3, we define the over-approximation of the difference of N 1 and N 2 as follows. -If s 2 = ⊥ or e = ε or (s 1 , s 2 ) in case 1 or 2, then for all a ∈ A and ϕ ∈ C(S 1 ) such that L 1 (s 1 , a, ϕ) = ⊥, let L((s 1 , s 2 , e), a, ϕ ⊥ ) = L 1 (s 1 , a, ϕ), with ϕ ⊥ defined below. For all other b ∈ A and ϕ ∈ C(S), let L((s 1 , s 2 , e), b, ϕ) = ⊥. -Else, we have (s 1 , s 2 ) in case 3 and B(s 1 , s 2 ) = ∅ by construction. The definition of L is given in Table 1, with the constraints ϕ ⊥ and ϕ B 12 defined hereafter.

Given ϕ ∈ C(S 1 ), ϕ ⊥ ∈ C(S) is defined as follows: µ ∈ Sat(ϕ ⊥ ) iff ∀s 1 ∈ S 1 , ∀s 2 = ⊥, ∀b = ε, µ(s 1 , s 2 , b) = 0 and the distribution (µ ↓ 1 : s 1 → µ(s 1 , ⊥, ε)) is in Sat(ϕ).
Given a state (s 1 , s 2 , e) ∈ S with s 2 = ⊥ and e = ε and two constraints

ϕ 1 ∈ C(S 1 ), ϕ 2 ∈ C(S 2 ) such that L 1 (s 1 , e, ϕ 1 ) = ⊥ and L 2 (s 2 , e, ϕ 2 ) = ⊥, the constraint ϕ B 12 ∈ C(S) is defined as follows: µ ∈ Sat(ϕ B 12 ) iff (1) for all (s ′ 1 , s ′ 2 , c) ∈ S, we have µ(s ′ 1 , s ′ 2 , c) > 0 ⇒ s ′ 2 = ⊥ if succ s2,e (s ′ 1 ) = ∅ and {s ′ 2 } = succ s2,e (s ′ 1 ) otherwise, and c ∈ B(s ′ 1 , s ′ 2 ) ∪ {ε}, (2) the distribution µ 1 : s ′ 1 → c∈A∪{ε},s ′ 2 ∈S2∪{⊥} µ(s ′ 1 , s ′ 2 , c) satisfies ϕ 1 , and (3) either (a) there exists (s ′ 1 , ⊥, c) such that µ(s ′ 1 , ⊥, c) > 0 or (b) the distribution µ 2 : s ′ 2 → c∈A∪{ε},s ′ 1 ∈S1 µ(s ′ 1 , s ′ 2 , c) does not satisfy ϕ 2 , or (c) there 1, A, a 2, ⊥, ε 1, ⊥, ε 1, A, ε {{α}} {{α}} {{α}} {{β}} a, ϕ ⊥ 1 , ⊤ a, ϕ B 12 , ⊤ a, ϕ ⊥ 1 , ⊤ a, ϕ ⊥ 1 , ⊤ µ ∈ Sat(ϕ B 12 ) ⇐⇒ (µ(1, A, a) + µ(1, A, ε) = 1) ∧ (µ(1, A, a) > 0) ∨(µ(2, ⊥, ε) = 1) (a) N1 \ * N2 Ω {α} a, 1 (b)
exists s ′ 1 ∈ S 1 , s ′ 2 ∈ S 2 and c = ε such that µ(s ′ 1 , s ′ 2 , c) > 0. Informally, distributions in ϕ B
12 must (1) follow the corresponding execution is N 1 and N 2 if possible, (2) satisfy ϕ 1 and (3) either (a) reach a state in N 1 that cannot be matched in N 2 or (b) break the constraint ϕ 2 , or (c) report breaking the relation to at least one successor state.

The following theorem shows that N 1 \ * N 2 is an over-approximation of the difference of N 1 and N 2 in terms of sets of implementations.

Theorem 1. For all deterministic APAs N 1 and

N 2 in SVNF such that N 1 N 2 , we have [[N 1 ]] \ [[N 2 ]] ⊆ [[N 1 \ * N 2 ]].
The reverse inclusion unfortunately does not hold. Intuitively, as explained in the construction of the constraint ϕ B 12 above, one can postpone the breaking of the satisfaction relation for N 2 to the next state (condition (3.c)). This assumption is necessary in order to produce an APA representing all counterexamples. However, when there are cycles in the execution of N 1 \ * N 2 , this assumption allows to postpone forever, thus allowing for implementations that will ultimately satisfy N 2 . This is illustrated in the following example.

Example 1. Consider the APAs N 1 and N 2 given in Fig. 1. Their over-approximating difference N 1 \ * N 2 is given in Fig. 2a. One can see that the PA P in Fig. 2b satisfies both N 1 \ * N 2 and N 2 .

We will later see in Corollary 1 that even though N 1 \ * N 2 may be capturing too many counterexamples, the distance between N 1 \ * N 2 and the real set of counterexamples

[[N 1 ]] \ [[N 2 ]
] is zero. This means that the two sets are infinitesimally close to each other, so in this sense, N 1 \ * N 2 is the best possible over-approximation.

Under-Approximating Difference

We now propose a construction that instead under-estimates the difference between APAs. This construction resembles the over-approximation presented in the previous section, the main difference being that in the under-approximation, states are indexed with an integer that represents the maximal depth of the unfolding of counterexamples. The construction is as follows.

Let

N 1 = (S 1 , A, L 1 , AP, V 1 , {s 1 0 }) and N 2 = (S 2 , A, L 2 , AP, V 2 , {s 2 0 }) be two deterministic APAs in SVNF such that N 1 N 2 . Let K ∈ N be the parameter of our construction. As in Section 4.1, if V 1 (s 1 0 ) = V 2 (s 2 0 ), i.e. (s 1 0 , s 2 0 ) in case 2, then [[N 1 ]] ∩ [[N 2 ]] = ∅.
In this case, we define N 1 \ K N 2 as N 1 . Otherwise, the underapproximation is defined as follows.

Definition 8. Let N 1 \ K N 2 = (S, A, L, AP, V, S K 0 ), where S = S 1 × (S 2 ∪ {⊥}) × (A ∪ {ε}) × {1, . . . , K}, V (s 1 , s 2 , a, k) = V (s 1 ) for all s 2 , a, k < K, S K 0 = {(s 1 0 , s 2 0 , f, K) | f ∈ B(s 1 0 , s 2
0 )}, and L is defined by: -If s 2 = ⊥ or e = ε or (s 1 , s 2 ) in case 1 or 2, then for all a ∈ A and ϕ ∈ C(S 1 ) such that L 1 (s 1 , a, ϕ) = ⊥, let L((s 1 , s 2 , e, k), a, ϕ ⊥ ) = L 1 (s 1 , a, ϕ), with ϕ ⊥ defined below. For all other b ∈ A and ϕ ∈ C(S), let L((s 1 , s 2 , e, k), b, ϕ) = ⊥. -Else we have (s 1 , s 2 ) in case 3 and B(s 1 , s 2 ) = ∅ by construction. The definition of L is given in Table 2. The constraints ϕ ⊥ and ϕ B,k 12 are defined hereafter.

{{α}} {{α}} {{β}} a, ϕ ⊥ 1 , ⊤ a, ϕ ⊥ 1 , ⊤ 1, A, a, 1 1, ⊥, ε, 1 2, ⊥, ε, 1 a, ϕ B,1 12 , ⊤ µ ∈ Sat(ϕ B,1 12 ) ⇐⇒ (µ(2, ⊥, ε, 1) = 1) (a) N1 \ 1 N2 1, A, a, 2 1, A, a, 1 {{α}} {{α}} {{α}} {{β}} a, ϕ ⊥ 1 , ⊤ a, ϕ ⊥ 1 , ⊤ a, ϕ ⊥ 1 , ⊤ 1, A, ε, 1 2, ⊥, ε, 1 1, ⊥, ε, 1 a, ϕ ⊥ 1 , ⊤ a, ϕ B,1 12 , ⊤ {{α}} a, ϕ B,2 12 , ⊤ µ ∈ Sat(ϕ B,2 12 ) ⇐⇒ (µ(1, A, a, 2) + µ(1, A, a, 1) + µ(1, A, ε, 1) = 1) ∧(µ(1, A, a, 1) > 0) ∨(µ(2, ⊥, ε, 1) = 1) µ ∈ Sat(ϕ B,1 12 ) ⇐⇒ (µ(2, ⊥, ε, 1) = 1) (b) N1 \ 2 N2
Fig. 3: Under-approximations at level 1 and 2 of the difference of APAs N1 and N2 from Figure 1.

Given a constraint ϕ ∈ C(S 1 ), the constraint ϕ ⊥ ∈ C(S) is defined as follows:

µ ∈ Sat(ϕ ⊥ ) iff ∀s 1 ∈ S 1 , ∀s 2 = ⊥, ∀b = ε, ∀k = 1, µ(s 1 , s 2 , b, k) = 0 and the distribution (µ ↓ 1 : s 1 → µ(s 1 , ⊥, ε, 1)) is in Sat(ϕ).
Given a state (s 1 , s 2 , e, k) ∈ S with s 2 = ⊥ and e = ε and two constraints ϕ 1 ∈ C(S 1 ) and

ϕ 2 ∈ C(S 2 ) such that L 1 (s 1 , e, ϕ 1 ) = ⊥ and L 2 (s 2 , e, ϕ 2 ) = ⊥, the constraint ϕ B,k 12 ∈ C(S) is defined as follows: µ ∈ Sat(ϕ B,k 12 ) iff (1) for all (s ′ 1 , s ′ 2 , c, k ′ ) ∈ S, if µ(s ′ 1 , s ′ 2 , c, k ′ ) > 0, then c ∈ B(s ′ 1 , s ′ 2 ) ∪ {ε} and either succ s2,e (s ′ 1 ) = ∅, s ′ 2 = ⊥ and k ′ = 1, or {s ′ 2 } = succ s2,e (s ′ 1 ), (2) the distribution µ 1 : s ′ 1 → c∈A∪{ε},s ′ 2 ∈S2∪{⊥},k ′ ≥1 µ(s ′ 1 , s ′ 2 , c, k ′ ) satisfies ϕ 1 , and (3) either (a) there exists (s ′ 1 , ⊥, c, 1) such that µ(s ′ 1 , ⊥, c, 1) > 0 , or (b) the distribution µ 2 : s ′ 2 → c∈A∪{ε},s ′ 1 ∈S1,k ′ ≥1 µ(s ′ 1 , s ′ 2 , c, k ′ ) does not satisfy ϕ 2 , or (c) k = 1 and there exists s ′ 1 ∈ S 1 , s ′ 2 ∈ S 2 , c = ε and k ′ < k such that µ(s ′ 1 , s ′ 2 , c, k ′ ) > 0.
The construction is illustrated in Figure 3.

Properties

We already saw in Theorem 1 that N 1 \ * N 2 is a correct over-approximation of the difference of N 1 by N 2 in terms of sets of implementations. The next theorem shows that, similarly, all N 1 \ K N 2 are correct under-approximations. Moreover, for increasing K the approximation is improving, and eventually all PAs in

[[N 1 ]] \ [[N 2 ]] are getting caught. (Hence in a set-theoretic sense, lim K→∞ [[N 1 \ K N 2 ]] = [[N 1 ]] \ [[N 2 ]].)
Theorem 2. For all deterministic APAs N 1 and N 2 in SVNF such that N 1 N 2 :

1. for all K ∈ N, we have

N 1 \ K N 2 N 1 \ K+1 N 2 , 2. for all K ∈ N, [[N 1 \ K N 2 ]] ⊆ [[N 1 ]] \ [[N 2 ]], and 3. for all PA P ∈ [[N 1 ]] \ [[N 2 ]], there exists K ∈ N such that P ∈ [[N 1 \ K N 2 ]].
Note that item 3 implies that for all PA P ∈

[[N 1 ]]\[[N 2 ]], there is a finite specification capturing [[N 1 ]] \ [[N 2 ]] "up to" P .
Using our distance defined in Section 3, we can make the above convergence result more precise. The next proposition shows that the speed of convergence is exponential in K; hence in practice, K will typically not need to be very large.

Proposition 2. Let N 1 and N 2 be two deterministic APAs in SVNF such that N 1 N 2 , and let

K ∈ N. Then d t ([[N 1 ]] \ [[N 2 ]], [[N 1 \ K N 2 ]]) ≤ λ K (1 -λ) -1 .
For the actual application at hand however, the particular accumulating distance d we have introduced in Section 3 may have limited interest, especially considering that one has to choose a discounting factor for actually calculating it.

What is more interesting are results of a topological nature which abstract away from the particular distance used and apply to all distances which are topologically equivalent to d. The results we present below are of this nature.

It can be shown, c.f. [START_REF] Thrane | Quantitative analysis of weighted transition systems[END_REF], that accumulating distances for different choices of λ are topologically equivalent (indeed, even Lipschitz equivalent), hence the particular choice of discounting factor is not important. Also some other system distances are Lipschitz equivalent to the accumulating one, in particular the so-called point-wise and maximum-lead ones, see again [START_REF] Thrane | Quantitative analysis of weighted transition systems[END_REF]. Theorem 3. Let N 1 and N 2 be two deterministic APAs in SVNF such that N 1 N 2 .

1. The sequence (N 1 \ K N 2 ) K∈N converges in the distance d, and

lim K→∞ d(N 1 \ * N 2 , N 1 \ K N 2 ) = 0. 2. The sequence ([[N 1 \ K N 2 ]]) K∈N converges in the distance d t , and lim K→∞ d t ([[N 1 ]]\ [[N 2 ]], [[N 1 \ K N 2 ]]) = 0.
Recall that as d and d t are not metrics, but only (asymmetric) pseudometrics (i.e. hemi-metrics), the above sequences may have more than one limit; hence the particular formulation. The theorem's statements are topological as they only allure to convergence of sequences and distance 0; topologically equivalent distances obey precisely the property of having the same convergence behaviour and the same kernel, c.f. [1].

The next corollary, which is easily proven from the above theorem by noticing that its first part implies that also lim

K→∞ d t ([[N 1 \ * N 2 ]], [[N 1 \ K N 2 ]]) = 0,
shows what we mentioned already at the end of Section 4.1:

N 1 \ * N 2 is the best possible over-approximation of [[N 1 ]] \ [[N 2 ]]. Corollary 1. Let N 1 and N 2 be two deterministic APAs in SVNF such that N 1 N 2 . Then d t ([[N 1 \ * N 2 ]], [[N 1 ]] \ [[N 2 ]]) = 0.
Again, as d t is not a metric, the distance being zero does not imply that the sets

[[N 1 \ * N 2 ]] and [[N 1 ]] \ [[N 2 ]
] are equal; it merely means that they are indistinguishable by the distance d t , or infinitesimally close to each other.

Conclusion

We have in this paper added an important aspect to the specification theory of Abstract Probabilistic Automata, in that we have shown how to exhaustively characterize the difference between two deterministic specifications. In a stepwise refinement methodology, difference is an important tool to gauge refinement failures.

We have also introduced a notion of discounted distance between specifications which can be used as another measure for how far one specification is from being a refinement of another. Using this distance, we were able to show that our sequence of under-approximations converges, semantically, to the real difference of sets of implementations, and that our over-approximation is infinitesimally close to the real difference.

There are many different ways to measure distances between implementations and specifications, allowing to put the focus on either transient or steady-state behavior. In this paper we have chosen one specific discounted distance, placing the focus on transient behavior. Apart from the fact that this can indeed be a useful distance in practice, we remark that the convergence results about our under-and over-approximations are topological in nature and hence apply with respect to all distances which are topologically equivalent to the specific one used here, typically discounted distances. Although the results presented in the paper do not hold in general for the accumulating (undiscounted) distance, there are other notions of distances that are more relevant for steady-state behavior, e.g. limit-average. Whether our results hold in this setting remains future work.

We also remark that we have shown that it is not more difficult to compute the difference of two APAs than to check for their refinement. Hence if a refinement failure is detected (using e.g. the methods presented in our APAC tool), it is not difficult to also compute the difference for information about the reason for refinement failure.

One limitation of our approach is the use of deterministic APAs. Even though deterministic specifications are generally considered to suffice from a modeling point of view [START_REF] Larsen | Modal specifications[END_REF], non-determinism may be introduced e.g. when composing specifications. Indeed, our constructions themselves introduce non-determinism: for deterministic APAs N 1 , N 2 , both N 1 \ * N 2 and N 1 \ K N 2 may be non-deterministic. Hence it is of interest to extend our approach to non-deterministic specifications. The problem here is, however, that for non-deterministic specifications, the relation between refinement and inclusion of sets of implementations

N 1 N 2 ⇐⇒ [[N 1 ]] ⊆ [[N 2 ]
] breaks: we may well have

N 1 N 2 but [[N 1 ]] ⊆ [[N 2 ]],
cf. [14]. So the technique we have used in this paper to compute differences will not work for non-deterministic APAs, and techniques based on thorough refinement will have to be used.

As a last note, we wish to compare our approach of difference between APA specifications with the use of counterexamples in probabilistic model checking. Counterexample generation is studied in a number of papers [START_REF] Aljazzar | Directed explicit state-space search in the generation of counterexamples for stochastic model checking[END_REF][START_REF] Han | Counterexample generation in probabilistic model checking[END_REF][START_REF] Wimmer | Counterexample generation for discrete-time Markov chains using bounded model checking[END_REF][START_REF] Andrés | Significant diagnostic counterexamples in probabilistic model checking[END_REF][START_REF] Jansen | Hierarchical counterexamples for discrete-time Markov chains[END_REF][START_REF] Schmalz | Counterexamples in probabilistic LTL model checking for Markov chains[END_REF][START_REF] Hermanns | Probabilistic CEGAR[END_REF][START_REF] Wimmer | Minimal critical subsystems for discrete-time Markov models[END_REF][START_REF] Chadha | A counterexample-guided abstraction-refinement framework for Markov decision processes[END_REF][START_REF] Komuravelli | Assume-guarantee abstraction refinement for probabilistic systems[END_REF], typically with the purpose of embedding it into a procedure of counterexample guided abstraction refinement (CEGAR). The focus typically is on generation of one particular counterexample to refinement, which can then be used to adapt the abstraction accordingly.

In contrast, our approach at computing APA difference generates a representation of all counterexamples. Our focus is not on refinement of abstractions at system level, using counterexamples, but on assessment of specifications. This is, then, the reason why we want to compute all counterexamples instead of only one. We remark, however, that our approach also can be used, in a quite simplified version, to generate only one counterexample; details of this are in the appendix. Our work is hence supplementary and orthogonal to the CEGAR-type use of counterexamples: CEGAR procedures can be used also to refine APA specifications, but only our difference can assess the precise distinction between specifications.

Appendix: Counter-Example Generation

Here we show how some techniques similar to the ones we have introduced can be used to generate one counterexample to a failed refinement N 1 N 2 . Note that when we compute the approximating differences N 1 \ * N 2 and N 1 \ K N 2 , we are in principle generating (approximations to) the set of all counterexamples, hence what we do in Section 4 is much more general than what we will present below. Generating only one counterexample may still be interesting however, as it is somewhat easier than computing the differences N 1 \ * N 2 , N 1 \ K N 2 and is all that is needed e.g. in a CEGAR approach.

First remark that Definition 4 can be trivially turned into an algorithm for checking refinement. Let

N 1 = (S 1 , A, L 1 , AP, V 1 , {s 1 0 }) and N 2 = (S 2 , A, L 2 , AP, V 2 , {s 2 0 }) be two deterministic APAs in SVNF. Consider the initial relation R 0 = S 1 ×S 2 . Compute R k+1
by removing all pairs of states not satisfying Definition 4 for R k . The sequence (R n ) n∈N is then strictly decreasing and converges to a fixpoint within a finite number of steps K ≤ |S 1 × S 2 |. This fixpoint R K coincides with the maximal refinement relation R between N 1 and N 2 . Let the index of this fixpoint be denoted with

Ind(R) = K; hence Ind R (s 1 , s 2 ) = min(max({k | (s 1 , s 2 ) ∈ R k }), K).
We now observe that if a pair of states (s 1 , s 2 ) is removed from the relation R by case 3, then we need to keep track of the actions that lead to this removal in order to use them in our counterexample. Whenever a pair of states is in cases 3.a, 3.b, 3.d or 3.e, we have that Ind R (s 1 , s 2 ) = 0 and the counterexample can be easily produced by allowing or disallowing the corresponding transitions from N 1 and N 2 . Cases 3.c and 3.f play a different role: due to the fact that they exploit distributions, they are the only cases in which refinement can be broken by using its recursive axiom. In these cases, producing a counterexample can be done in two ways: either by using a distribution that does not satisfy the constraints in N 2 (if such a distribution exists, then Ind R (s 1 , s 2 ) = 0), or by using a distribution that reaches a pair of states (s ′ 1 , s ′ 2 ) / ∈ R. When 0 < Ind R (s 1 , s 2 ) < Ind(R), only the latter is possible. This recursive construction has disadvantages: it allows us to produce loops that may lead to incorrect counterexamples. In order to prevent these loops, we propose to use only those distributions that decrease the value of Ind in this particular case. The set Break(s 1 , s 2 ) defined hereafter allows us to distinguish the actions for which the value of Ind decreases, hence ensuring (by Lemma 1 below) the correctness of our counterexample construction. Let (s 1 , s 2 ) ∈ S 1 × S 2 be such that V 1 (s 1 ) ⊆ V 2 (s 2 ) and Ind R (s 1 , s 2 ) = k < Ind(R). We define Break(s 1 , s 2 ) to be the set {a ∈ A | either a ∈ B a,b,d,e (s 1 , s 2 ) or there exists ϕ 1 ∈ C(S 1 ) such that

L 1 (s 1 , a, ϕ 1 ) = ⊥, ϕ 2 ∈ C(S 2 ) such that L 2 (s 2 , a, ϕ 2 ) = ⊥ and µ 1 ∈ Sat(ϕ 1 ) such that ∀µ 2 ∈ Sat(ϕ 2 ), µ 1 ⋐ R k µ 2 }.
Remark that the conditions defined above are exactly the conditions for removing a pair of states (s 1 , s 2 ) at step k of the algorithm for computing R defined above. Under the assumption that V 1 (s 1 ) ⊆ V 2 (s 2 ) and Ind R (s 1 , s 2 ) = k < Ind(R), we can be sure that the set Break(s 1 , s 2 ) is not empty. Moreover, we have the following lemma.

Lemma 1. For all pairs of states (s 1 , s 2 ) in case 3 and for all actions e ∈ (B c (s 1 , s 2 ) ∪ B f (s 1 , s 2 )) ∩ Break(s 1 , s 2 ), there exist constraints ϕ 1 and ϕ 2 such that L 1 (s 1 , e, ϕ 1 ) = ⊥ and L 2 (s 2 , e, ϕ 2 ) = ⊥ and a distribution µ 1 ∈ Sat(ϕ 1 ) such that either

1. ∃s ′ 1 ∈ S 1 such that µ 1 (s ′ 1 ) > 0 and succ s2,e (s ′ 1 ) = ∅, or 2. µ 2 1 : s ′ 2 → {s ′ 1 ∈S1 | s ′ 2 =succs 2 ,e (s ′ 1 )} µ 1 (s ′ 1 ) / ∈ Sat(ϕ 2 ), 3. ∃s ′ 1 ∈ S 1 , s ′ 2 ∈ S 2 such that µ 1 (s ′ 1 ) > 0, s ′ 2 = succ s2,e (s ′ 1 ) and Ind R (s ′ 1 , s ′ 2 ) < Ind R (s 1 , s 2 ).
Proof. Let R be the maximal refinement relation between N 1 and N 2 and let (s

1 , s 2 ) ∈ S 1 × S 2 such that (s 1 , s 2 ) is in case 3, i.e. (s 1 , s 2 ) / ∈ R and V 1 (s 1 ) = V 2 (s 2 ). Let e ∈ A such that e ∈ (B c (s 1 , s 2 ) ∪ B f (s 1 , s 2 )) ∩ Break(s 1 , s 2 ).
Since e ∈ B c (s 1 , s 2 ) ∪ B f (s 1 , s 2 ), there exists ϕ 1 ∈ C(S 1 ) and ϕ 2 ∈ C(S 2 ) such that either L 2 (s 2 , e, ϕ 2 ) = ⊤ and L 1 (s 1 , e, ϕ 1 ) = ⊤ or L 2 (s 2 , e, ϕ 2 ) =? and L 1 (s 1 , e, ϕ 1 ) = ⊥. As a consequence, since e ∈ Break(s 1 , s 2 ), we have that

∃µ 1 ∈ Sat(ϕ 1 ), ∀µ 2 ∈ Sat(ϕ 2 ), µ 1 ⋐ R k µ 2 .
(

) 2
Let K be the smallest index such that R K = R. By construction, we know that Ind R (s 1 , s 2 ) = k < K, i.e. (s 1 , s 2 ) ∈ R k and (s 1 , s 2 ) / ∈ R k+1 . Consider the distribution µ 1 given by ( 2) above. We have that ∀µ

2 ∈ Sat(ϕ 2 ), ∀ corresp. δ, µ 1 ⋐ δ R k µ 2 . Consider the function δ such that δ(s ′ 1 , s ′ 2 ) = 1 if s ′ 2 = succ s2,e (s ′ 1
) and 0 otherwise. There are several cases.

-If there exists s ′ 1 ∈ S 1 such that µ 1 (s ′ 1 ) > 0 and succ s2,e (s ′ 1 ) = ∅, then the lemma is proven.

-Else, δ is a correspondence function. Since ∀µ 2 ∈ Sat(ϕ 2 ), µ 1 ⋐ R k µ 2 , we know that either (1) µ 2 : s ′ 2 → s ′ 1 ∈S1 µ 1 (s ′ 1 )δ(s ′ 1 , s ′ 2 ) does not satisfy ϕ 2 , or (2) there exists s ′ 1 and s ′ 2 such that µ 1 (s ′ 1 ) > 0, δ(s ′ 1 , s ′ 2 ) > 0 and (s ′ 1 , s ′ 2 ) / ∈ R k . 1. Assume that µ 2 : s ′ 2 → s ′ 1 ∈S1 µ 1 (s ′ 1 )δ(s ′ 1 , s ′ 2 )
does not satisfy ϕ 2 . Remark that the function µ 2 1 from Lemma 1 is equal to µ 2 defined above. As a consequence, µ 2 1 / ∈ ϕ 2 . 2. Otherwise, assume that there exists s ′ 1 and s ′ 2 such that µ

1 (s ′ 1 ) > 0, δ(s ′ 1 , s ′ 2 ) > 0 and (s ′ 1 , s ′ 2 ) / ∈ R k . Since (s ′ 1 , s ′ 2 ) / ∈ R k , we have that Ind R (s ′ 1 , s ′ 2 ) < k. As a consequence, there exists s ′ 1 ∈ S 1 , s ′ 2 ∈ S 2 such that µ 1 (s ′ 1 ) > 0, s ′ 2 = succ s2,e (s ′ 1 ) and Ind R (s ′ 1 , s ′ 2 ) < Ind R (s 1 , s 2 ).
In other words, the above lemma ensures that a pair (s ′ 1 , s ′ 2 ) such that Ind R (s ′ 1 , s ′ 2 ) = 0 can be reached within a bounded number of transitions for all pairs of states (s 1 , s 2 ) in case 3. As explained above, this is a prerequisite for the correctness of the counterexample construction defined hereafter.

We now propose the main contribution of the section: a construction to build counterexamples. Let

N 1 = (S 1 , A, L 1 , AP, V 1 , {s 1 0 }) and N 2 = (S 2 , A, L 2 , AP, V 2 , {s 2 0 }) be deterministic APAs in SVNF such that N 1 N 2 .
Let R be the maximal refinement relation between N 1 and N 2 .. Definition 9. The counterexample P = (S, A, L, AP, V, s 0 ) is computed as follows:

- -If e ∈ Break(s1, s2), then let µ1 be the distribution given in Lemma 1. -Else, let µ1 be an arbitrary distribution in Sat(ϕ1) such that ∀µ2 ∈ Sat(ϕ2), µ1 ⋐R µ2.

S = S 1 × (S 2 ∪ {⊥}), -s 0 = (s 1 0 , s 2
In both cases, let L((s1, s2), e, c µ1) = ⊤. -V (s 1 , s 2 ) = v ∈ 2 AP such that V 1 (s 1 ) = {v} for all (s 1 , s 2 ) ∈ S, and -L is defined as follows. Let (s 1 , s 2 ) ∈ S.

B f (s1, s2) s2 s1 ϕ1 ϕ2 = e, ⊤ e, ⊤
• If (s 1 , s 2 ) in case 1 or 2 or s 2 = ⊥, then for all a ∈ A and ϕ 1 ∈ C(S 1 ) such that L 1 (s 1 , a, ϕ 1 ) = ⊤, let µ 1 be an arbitrary distribution in Sat(ϕ 1 ) and let

L((s 1 , s 2 ), a, µ ⊥ 1 ) = ⊤ with µ ⊥ 1 ∈ Dist(S) such that µ ⊥ 1 (s ′ 1 , s ′ 2 ) = µ 1 (s ′ 1 ) if s ′ 2 = ⊥ and 0 otherwise. • Else, (s 1 , s 2 ) is in case 3 and B(s 1 , s 2 ) = ∅. For all a ∈ A \ B(s 1 , s 2 ) and ϕ 1 ∈ C(S 1
) such that L 1 (s 1 , a, ϕ 1 ) = ⊤, let µ 1 be an arbitrary distribution in Sat(ϕ 1 ) and let L((s 1 , s 2 ), a, µ ⊥ 1 ) = ⊤, with µ ⊥ 1 defined as above. In addition, for all e ∈ B(s 1 , s 2 ), let L((s 1 , s 2 ), e, .) be defined as in Table 3. In the table, given constraints ϕ 1 ∈ C(S 1 ) and ϕ 2 ∈ C(S 2 ) such that L 1 (s 1 , e, ϕ 1 ) = ⊥ and L 2 (s 2 , e, ϕ 2 ) = ⊥, and a distribution µ 1 ∈ Sat(ϕ 1 ), the distribution µ 1 ∈ Dist(S) is defined as follows:

µ 1 (s ′ 1 , s ′ 2 ) = µ 1 (s 1 ) if s ′ 2 = succ s2,e (s ′ 1
) or succ s2,e (s ′ 1 ) = ∅ and s ′ 2 = ⊥, and 0 otherwise. Proof. Let N 1 = (S 1 , A, L 1 , AP, V 1 , {s 1 0 }) and N 2 = (S 2 , A, L 2 , AP, V 2 , {s 2 0 }) be deterministic APAs in SVNF such that N 1 N 2 . Let P = (S, A, L, AP, V, s 0 ) be the counterexample defined as above. We prove that P |= N 1 and P |= N 2 .

P |= N 1 . Consider the relation R s ⊆ S × S 1 such that (s 1 , s 2 ) R s s ′ 1 iff s 1 = s ′ 1 .
We prove that R s is a satisfaction relation. Let t = (s 1 , s 2 ) ∈ S and consider (t, s 1 ) ∈ R s .

-By construction, we have V (s 1 , s 2 ) ⊆ V 1 (s 1 ).

-Let a ∈ A and ϕ 1 ∈ C(S 1 such that L 1 (s 1 , a, ϕ 1 ) = ⊤. There are several cases.

• If (s 1 , s 2 ) in case 1 or 2 or s 2 = ⊥, then by construction there exists µ ⊥ 1 ∈ Dist(S) such that L((s 1 , s 2 ), a, µ ⊥ 1 ) = ⊤. By construction, we have that there exists µ

1 ∈ Sat(ϕ 1 ) such that µ ⊥ 1 ⋐ Rs µ 1 . • Else, (s 1 , s 2 ) is in case 3 and B(s 1 , s 2 ) = ∅. If a / ∈ B(s 1 , s 2
), the result follows as above. Else, either a ∈ B a (s 1 , s 2 ) ∪ B b (s 1 , s 2 ) and the result follows again by construction, or a ∈ B c (s 1 , s 2 ) ∪ B f (s 1 , s 2 ). In this case, there exists a distribution µ 1 ∈ Dist(S) such that L((s 1 , s 2 ), a, µ 1 ) = ⊤. By construction, µ 1 is defined as follows:

µ 1 (s ′ 1 , s ′ 2 ) =    µ 1 (s 1 ) if s ′ 2 = succ s2,e (s ′ 1
) or succ s2,e (s ′ 1 ) = ∅ and s ′ 2 = ⊥ 0 otherwise

, where µ 1 is either the distribution given by Lemma 1 if a ∈ Break(s 1 , s 2 ) or an arbitrary distribution in Sat(ϕ 1 ). In both cases, µ 1 ∈ Sat(ϕ 1 ). Consider the function δ : S × S 1 → [0, 1] such that δ((s ′ 1 , s ′ 2 ), s ′′ 1 ) = 1 if s ′ 1 = s ′′ 1 and 0 otherwise. Using standard techniques, on can verify that δ is a correspondence function and that µ 1 ⋐ Rs µ 1 .

-Let a ∈ A and µ ∈ Dist(S) such that L((s 1 , s 2 ), a, µ) = ⊤. By construction of P , there must exists ϕ 1 ∈ C(S 1 ) such that L 1 (s 1 , a, ϕ 1 ) = ⊥ and µ is either of the form µ ⊥ 1 or µ 1 for some µ 1 ∈ Sat(ϕ 1 ). As above, we can prove that in all cases, µ ⋐ Rs µ 1 .

Finally R s is a satisfaction relation. Moreover, we have ((s 1 0 , s 2 0 ), s 1 0 ) ∈ R s , thus P |= N 1 . P |= N 2 . Let R s ⊆ S × S 2 be the maximal satisfaction relation between P and N 2 , and assume that R s is not empty. Let R ⊆ S 1 × S 2 be the maximal refinement relation between N 1 and N 2 and let K be the smallest index such that R K = R. We prove that for all (s 1 , s 2 ) ∈ S 1 × S 2 , if Ind R (s 1 , s 2 ) < K, then ((s 1 , s 2 ), s 2 ) / ∈ R s . The proof is done by induction on k = Ind R (s 1 , s 2 ). Let (s 1 , s 2 ) ∈ S 1 × S 2 .

-Base case. If Ind R (s 1 , s 2 ) = 0, then there are several cases.

• If (s 1 , s 2 ) in case 2, i.e. V 1 (s 1 ) = V 2 (s 2 ). In this case, we know that V ((s 1 , s 2 )) ∈ V 1 (s 1 ). Thus, by SVNF of N 1 and N 2 , we have that V ((s 1 , s 2 )) / ∈ V 2 (s 2 ) and ((s 1 , s 2 ), s 2 ) / ∈ R s . • Else, if (s 1 , s 2 ) in cases 3.a or 3.b, then there exists a ∈ A and µ ⊥ 1 ∈ Dist(S) such that L((s 1 , s 2 ), a, µ ⊥ 1 ) = ⊤ and ∀ϕ 2 ∈ C(S 2 ), we have L 2 (s 2 , a, ϕ 2 ) = ⊥. As a consequence, ((s 1 , s 2 ), s 2 ) / ∈ R s .

d ′ is a pre-fixpoint to (1). Indeed, for s ′ 1 and s 2 compatible, we have

d ′ (

Proof of Theorem 1

For all deterministic APAs N 1 and N 2 in SVNF such that N 1 N 2 , we have

[[N 1 ]] \ [[N 2 ]] ⊆ [[N 1 \ * N 2 ]].
Proof. Let N 1 = (S 1 , A, L 1 , AP, V 1 , {s 1 0 }) and N 2 = (S 2 , A, L 2 , AP, V 2 , {s 2 0 }) be deterministic APAs in single valuation normal form such that N 1 N 2 . Let R be the maximal weak refinement relation between N 1 and N 2 . Let P = (S P , A, L P , AP, V P , s P 0 ) be a PA such that P |= N 1 and P |= N 2 . We prove that P |= N 1 \ * N 2 . Let R 1 ⊆ S P × S 1 be the relation witnessing P |= N 1 and let R 2 be the maximal satisfaction relation in S P × S 2 . By construction, (s P 0 , s 2 ) / ∈ R 2 . If V 1 (s 1 0 ) = V 2 (s 2 0 ), then by construction N 1 \ * N 2 = N 1 and thus P |= N 1 \ * N 2 . Else, we have (s 1 0 , s 2 0 ) in case 3, thus N 1 \ * N 2 = (S, A, L, AP, V, S 0 ) is defined as in Section 4.1. By construction, we also have (s P 0 , s 2 0 ) in case 3, thus there must exist f ∈ B(s P 0 , s 2 0 ). Remark that by construction, we must have B(s P 0 , s 2 0 ) ⊆ B(s 1 0 , s 2 0 ). We will prove that P |= N 1 \ * N 2 .

Define the following relation R \ ⊆ S P × S:

1 eTable 1 :

 11 s2, e)For all a = e ∈ A and ϕ ∈ C(S1) such that L1(s1, a, ϕ) = ⊥, let L((s1, s2, e), a, ϕ ⊥ ) = L1(s1, a, ϕ). In addition, let L((s1, s2, e), e, ϕ ⊥ 1 ) = ⊤. For all other b ∈ A and ϕ ∈ C(S), let L((s1, s2, e), b, ϕ) = ⊥. B b (s1, s2) s2, e)For all a ∈ A and ϕ ∈ C(S1) such that L1(s1, a, ϕ) = ⊥, let L((s1, s2, e), a, ϕ ⊥ ) = L1(s1, a, ϕ). For all other b ∈ A and ϕ ∈ C(S), let L((s1, s2, e), b, ϕ) = ⊥.Be(s1, s2) s2, e)For all a = e ∈ A and ϕ ∈ C(S1) such that L1(s1, a, ϕ) = ⊥, let L((s1, s2, e), a, ϕ ⊥ ) = L1(s1, a, ϕ). In addition, let L((s1, s2, e), e, ϕ B 12 ) =?. For all other b ∈ A and ϕ ∈ C(S), let L((s1, s2, e), b, ϕ) = ⊥.Bc(s1, s2) , {?, ⊤}For all a ∈ A and ϕ ∈ C(S1) such that L1(s1, a, ϕ) = ⊥ (including e and ϕ1), let L((s1, s2, e), a, ϕ ⊥ ) = L1(s1, a, ϕ). In addition, let L((s1, s2, e), e, ϕ B 12 ) = ⊤. For all other b ∈ A and ϕ ∈ C(S), let L((s1, s2, e), b, ϕ) = ⊥. B f (s1, s2) Definition of the transition function L in N1 \ * N2. Definition 7. Let N 1 \ * N 2 = (S, A, L, AP, V, S 0 ), where S = S 1 × (S 2 ∪ {⊥}) × (A ∪ {ε}), V (s 1 , s 2 , a) = V (s 1 ) for all s 2 and a, S 0 = {(s 1 0 , s 2 0 , f ) | f ∈ B(s 1 0 , s 2 0 )}, and L is defined by:

PFig. 2 :

 2 Fig. 2: Over-approximating difference N1 \ * N2 of APAs N1 and N2 from Figure 1 and PA P such that P |= N1 \ * N2 and P |= N2.

Table 2 :

 2 s2, e, k)For all a = e ∈ A and ϕ ∈ C(S1) such that L1(s1, a, ϕ) = ⊥, let L((s1, s2, e, k), a, ϕ ⊥ ) = L1(s1, a, ϕ). In addition, let L((s1, s2, e, k), e, ϕ ⊥ 1 ) = ⊤. For all other b ∈ A and ϕ ∈ C(S), let L((s1, s2, e, k), b, ϕ) = ⊥. B b (s1, s2) s2, e, k) For all a ∈ A and ϕ ∈ C(S1) such that L1(s1, a, ϕ) = ⊥, let L((s1, s2, e, k), a, ϕ ⊥ ) = L1(s1, a, ϕ). For all other b ∈ A and ϕ ∈ C(S), let L((s1, s2, e, k), b, ϕ) = ⊥. Be(s1, s2) s2, e, k)For all a = e ∈ A and ϕ ∈ C(S1) such that L1(s1, a, ϕ) = ⊥, let L((s1, s2, e, k), a, ϕ ⊥ ) = L1(s1, a, ϕ). In addition, let L((s1, s2, e, k), e, ϕ B,k 12 ) = ?. For all other b ∈ A and ϕ ∈ C(S), let L((s1, s2, e, k), b, ϕ) = ⊥.Bc(s1, s2)For all a ∈ A and ϕ ∈ C(S1) such that L1(s1, a, ϕ) = ⊥ (including e and ϕ1), let L((s1, s2, e, k), a, ϕ ⊥ ) = L1(s1, a, ϕ). In addition, let L((s1, s2, e, k), e, ϕ B,k 12 ) = ⊤. For all other b ∈ A and ϕ ∈ C(S), let L((s1, s2, e, k), b, ϕ) = ⊥. B f (s1, s2) Definition of the transition function L in N1 \ K N2.

  Let ϕ1 ∈ C(S1) such that L1(s1, e, ϕ1) = ⊥ and let µ1 be an arbitrary distribution in Sat(ϕ1). Define L((s1, s2), e, µ ⊥ 1 ) = ⊤. B b (s1, s2) For all µ ∈ Dist(S), let L((s1, s2), e, µ) = ⊥. Let ϕ1 ∈ C(S1) and ϕ2 ∈ C(S2) such that L1(s1, e, ϕ1) = ⊥ and L2(s2, e, ϕ2) = ⊥.

Theorem 4 .

 4 The counterexample PA P defined above is such that P |= N 1 and P |= N 2 .

  ∈ A and ϕ 1 ∈ C(S 1 ) such that L 1 (s 1 , e, ϕ 1 ) ≥? and ∃ϕ 2 ∈ C(S 2 ) : L 2 (s 2 , e, ϕ 2 ) = ?, ∃µ ∈ Sat(ϕ 1 ) such that ∀µ ′ ∈ Sat(ϕ 2 ) : µ ⋐ R µ ′ ,

	and
	(a) there exists e ∈ A and ϕ 1 ∈ C(S 1 ) such that L 1 (s 1 , e, ϕ 1 ) = ⊤ and ∀ϕ 2 ∈ C(S 2 ) : L 2 (s 2 , e, ϕ 2 ) = ⊥,	s1	e, ⊤	s2 e
		ϕ1
	(b) there exists e ∈ A and ϕ 1 ∈ C(S 1 ) such that L 1 (s 1 , e, ϕ 1 ) =? and ∀ϕ 2 ∈ C(S 2 ) : L 2 (s 2 , e, ϕ 2 ) = ⊥,	s1	e, ?	s2 e
		ϕ1
	s2 (c) there exists e ϕ2 ϕ1 s1 = e, {?, ⊤} e, ?
	(d) there exists e ∈ A and ϕ 2 ∈ C(S 2 ) such that
	L

2 (s 2 , e, ϕ 2 ) = ⊤ and ∀ϕ 1

Table 3 :

 3 Definition of the transition function L in P .

  s ′ 1 , s 2 ) = d(s ′ 1 , s 2 ) + η P1,P2 (µ 1 , µ 2 , d) + η ,due to the construction of P 2 and the fact that the sup µ1∈Sat(µ1) is trivial in the formula forD P1,N2 (µ 1 , ϕ 2 , d), P1,P2 (µ 1 , µ 2 , d ′ ) ,where the last inequality is a consequence of λD P1,P2 (µ 1 , µ 2 , d ′ ) = λ

	= max = max	   a,µ1:L ′ 1 (s ′ max 1 ,a,µ1)=⊤   max a,ϕ2:L2(s2,a,ϕ2)=⊤    max a,µ1:L ′ 1 (s ′ 1 ,a,µ1)=⊤   max a,µ2:L ′ 2 (s2,a,µ2)=⊤	min ϕ2:L2(s2,a,ϕ2) =⊥ min µ1:L ′ 1 (s ′ 1 ,a,µ1)=⊤ min µ2:L ′ 2 (s2,a,µ2)=⊤ min µ1:L ′ 1 (s ′ 1 ,a,µ1)=⊤	λD P1,N2 (µ 1 , ϕ 2 , d) + η λD P1,N2 (µ 1 , ϕ 2 , d) + η λD P1,P2 (µ 1 , µ 2 , d) + η
	≥ max	   a,µ1:L ′ 1 (s ′ max 1 ,a,µ1)=⊤   max a,µ2:L ′ 2 (s2,a,µ2)=⊤	min 2 (s2,a,µ2)=⊤ µ2:L ′ min µ1:L ′ 1 (s ′ 1 ,a,µ1)=⊤	λD P1,P2 (µ 1 , µ 2 , d ′ )
		t ′ 1 ,t2

λD λD µ 1 (t ′ 1 )δ(t ′ 1 , t 2 )(d(t ′ 1 , t 2 ) + η) = λ t ′ 1 ,t2 µ 1 (t ′ 1 )δ(t ′ 1 , t 2 )d(t ′ 1 , t 2 ) + λη.

• Else, if (s 1 , s 2 ) in cases 3.d or 3.d, then there exists a ∈ A and ϕ 2 ∈ C(S 2 ) such that L 2 (s 2 , a, ϕ 2 ) = ⊤ and for all µ ∈ Dist(S), we have L((s 1 , s 2 ), a, µ) = ⊥. As a consequence, ((s 1 , s 2 ), s 2 ) / ∈ R s . • Finally, if (s 1 , s 2 ) in cases 3.c or 3.f , there exists e ∈ (B c (s 1 , s 2 )∪B f (s 1 , s 2 ))∩ Break(s 1 , s 2 ). By Lemma 1, there exists constraints ϕ 1 and ϕ 2 such that L 1 (s 1 , e, ϕ 1 ) = ⊥ and L 2 (s 2 , e, ϕ 2 ) = ⊥ and a distribution µ 1 ∈ Sat(ϕ 1 ) such that either (I) ∃s ′ 1 ∈ S 1 such that µ 1 (s ′ 1 ) > 0 and succ s2,e (s ′ 1 ) = ∅, or (II) µ 2 1 :

. By construction, we have that L((s 1 , s 2 ), e, µ 1 ) = ⊤ for µ 1 given above. Since Ind R (s 1 , s 2 ) = 0, case (III) above is not possible. From cases (I) and (II), we can deduce that for all µ 2 ∈ Sat(ϕ 2 ), we have µ 1 ⋐ Rs µ 2 . Moreover, by determinism of N 2 , ϕ 2 is the only constraint such that L 2 (s 2 , e, ϕ 2 ) = ⊥. As a consequence, ((s 1 , s 2 ), s 2 ) / ∈ R s .

-Inductive step. Let 0 < k < K and assume that for all k ′ < k and for all (s ′ 1 , s 2 ) ∈ § 1 × S 2 , if Ind R (s 1 , s 2 ) = k ′ , then ((s 1 , s 2 ), s 2 ) / ∈ R s . Assume that Ind R (s 1 , s 2 ) = k. There are two cases.

• If (s 1 , s 2 ) in cases 2, 3.a, 3.b, 3.d or 3.d, the same reasoning applies as for the base case. We thus deduce that ((s 1 , s 2 ), s 2 ) / ∈ R s . • Otherwise, if (s 1 , s 2 ) in cases 3.c or 3.f , then, as above, there exists e ∈ (B c (s 1 , s 2 )∪B f (s 1 , s 2 ))∩Break(s 1 , s 2 ). By Lemma 1, there exists constraints ϕ 1 and ϕ 2 such that L 1 (s 1 , e, ϕ 1 ) = ⊥ and L 2 (s 2 , e, ϕ 2 ) = ⊥ and a distribution µ 1 ∈ Sat(ϕ 1 ) such that either (I) ∃s ′ 1 ∈ S 1 such that µ 1 (s ′ 1 ) > 0 and succ s2,e (s ′ 1 ) = ∅, or (II) µ 2 1 : s ′ 2 → {s ′ 1 ∈S1 | s ′ 2 =succs 2 ,e (s ′ 1 )} µ 1 (s ′ 1 ) / ∈ Sat(ϕ 2 ), (III) ∃s ′ 1 ∈ S 1 , s ′ 2 ∈ S 2 such that µ 1 (s ′ 1 ) > 0, s ′ 2 = succ s2,e (s ′ 1 ) and Ind R (s ′ 1 , s ′ 2 ) < Ind R (s 1 , s 2 ). By construction, we have that L((s 1 , s 2 ), e, µ 1 ) = ⊤ for µ 1 given above. As above, if cases (I) or (II) apply, then we can deduce that ((s 1 , s 2 ), s 2 ) / ∈ R s . If case (III) applies, then there exists (s ′ 1 , s ′ 2 ) ∈ S such that µ 1 (s ′ 1 , s ′ 2 ) > 0, s ′ 2 = succ s2,e (s ′ 1 ) and Ind R (s ′ 1 , s ′ 2 ) < Ind R (s 1 , s 2 ). Since s ′ 2 = succ s2,e (s ′ 1 ), then, by determinism of N 2 , all correspondence functions δ will be such that δ((s ′ 1 , s ′ 2 ), s ′ 2 ) = 1. However, we have that Ind R (s ′ 1 , s ′ 2 ) < k, thus by induction

As a consequence, we have that for all µ 2 ∈ Sat(ϕ 2 ), we have µ 1 ⋐ Rs µ 2 . We can thus deduce that

Finally, we know that Ind R (s 1 0 , s 2 0 ) < k. As a consequence, we have ((s 1 0 , s 2 0 ), s 2 0 ) / ∈ R s and thus P |= N 2 .

Appendix: Proofs

Proof of Proposition 1

For all APAs N 1 and N 2 in SVNF, it holds that d t (N 1 , N 2 ) ≤ d(N 1 , N 2 ). For a distribution µ 1 and a constraint ϕ 2 , we denote by

the set of all simulations between µ 1 and distributions satisfying ϕ 2 .

Proof. If d(N 1 , N 2 ) = 1, we have nothing to prove. Otherwise, write N i = (S i , A, L i , AP, V i , S i 0 ) for i = 1, 2, and let

so there must exist a redistribution δ ∈ RD(µ 1 , ϕ 2 ) for which

and (s 2 = ⊥) and (e = ε) or (p R 1 s 1 ) and (p, s 2 ) in case 1 or 2 and and (e = ε) or (p R 1 s 1 ) and (p, s 2 ) in case 3 and (e ∈ B(p, s 2 ))

We now prove that R \ is a satisfaction relation. Let (p, (s 1 , s 2 , e)) ∈ R \ . If s 2 = ⊥ or e = ε, then since p R 1 s 1 , R \ satisfies the axioms of a satisfaction relation by construction. Else we have s 2 ∈ S 2 and e = ε, thus, by definition of R \ , we know that (p, s 2 ) is in case 3.

-By construction, we have

-Let a ∈ A and µ P ∈ Dist(S P ) such that L P (p, a, µ P ) = ⊤. There are several cases.

• If a = e, then since p R 1 s 1 , there exists ϕ 1 ∈ C(S 1 ) such that L 1 (s 1 , a, ϕ 1 ) = ⊥ and there exists µ 1 ∈ Sat(ϕ 1 ) such that µ P ⋐ R \ µ 1 . By construction, we have L((s 1 , s 2 , e), a, ϕ ⊥ 1 ) = ⊥ and there obviously exists µ ∈ Sat(ϕ ⊥ 1 ) such that µ P ⋐ R \ µ.

• If a = e ∈ B a (p, s 2 ), then, as above, there exists ϕ ∈ C(S) such that L((s 1 , s 2 , e), a, ϕ) = ⊥ and there exists µ ∈ Sat(ϕ) such that

Remark that for all p ′ ∈ S P such that µ P (p ′ ) > 0, there exists a unique

). As a consequence, we have that µ ′ 1 = µ 1 ∈ Sat(ϕ 1 ). 3. Assume that for all p ′ ∈ S P such that µ P (p ′ ) > 0, we have succ s2,e (p ′ ) = ∅ (the other case being trivial). Consider the distribution µ 2 :

). We thus conclude that there exists µ ∈ Sat(ϕ B 12 ) such that µ P ⋐ R \ µ. Finally, in all cases, there exists ϕ ∈ C(S) such that L((s 1 , s 2 , e), a, ϕ) = ⊥ and there exists µ ∈ Sat(ϕ) such that

As above, there are several cases.

The rest of the proof is then as above.

• If a = e ∈ B a (p, s 2 ), then there exists µ P ∈ Dist(S P ) such that L P (p, e, µ P ) = ⊤. The rest of the proof is then as above. Recall that B a (s

. Thus, there exists µ P ∈ Dist(S P ) and

, there also exist ϕ 1 ∈ C(S 1 ) such that L 1 (s 1 , e, ϕ 1 ) = ⊥. By determinism, ϕ 1 and ϕ 2 are unique. The rest of the proof follows as above. Thus, in all cases, there exists µ P ∈ Dist(S P ) such that L P (p, a, µ P ) = ⊤ and there exists µ ∈ Sat(ϕ) such that µ P ⋐ R \ µ.

Finally, R \ is a satisfaction relation. Moreover, we have s P 0 R 1 s 1 0 , (s P 0 , s 2 0 ) in case 3 and f ∈ B(s P 0 , s 2 0 ) by construction, thus

Proof of Theorem 2

For all deterministic APAs N 1 and N 2 in SVNF such that N 1 N 2 , we have that

0 , s 2 0 , e, K), (s 1 0 , s 2 0 , e, K+1)) | e ∈ B(s 1 0 , s 2 0 )}∪R id , where R id denotes the identity relation. One can verify that, by construction, R is a refinement relation witnessing

Let

Let R be the maximal weak refinement relation between N 1 and N 2 .

1. We first prove that for all

and the result holds. Otherwise, assume that (s 1 0 , s 2 0 ) is in case 3 and let K ∈ N. We have N 1 \ K N 2 = (S, A, L, AP, V, S K 0 ) defined as in Section 4.2. Let P = (S P , A, L P , AP, V P , s P 0 ) be a PA such that P |= N 1 \ K N 2 . Let R \ ⊆ S P × S be the associated satisfaction relation and let f ∈ B(s 1 0 , s 2 0 ) be such that s P 0 R \ (s 1 0 , s 2 0 , f, K). We show that P |= N 1 and P |= N 2 .

We start by proving that

-By construction, we have

-Let a ∈ A and µ P ∈ Dist(S P ) be such that L P (p, a, µ P ) = ⊤. By R \ , there exists ϕ ∈ C(S) such that L((s 1 , s 2 , e, n), a, ϕ) = ⊥ and there exists µ ∈ Sat(ϕ) such that µ P ⋐ R \ µ.

If s 2 = ⊥ or e = ε or a = e, then by construction of N 1 \ K N 2 , there exists ϕ 1 ∈ C(S 1 ) such that ϕ = ϕ ⊥ 1 and L 1 (s 1 , a, ϕ 1 ) = ⊥. As a consequence, the distribution

) and it follows that µ P ⋐ R1 µ ↓ 1 . Otherwise, assume that s 2 ∈ S 2 , e ∈ A and a = e. There are several cases.

• If e ∈ B a (s 1 , s 2 ) ∪ B b (s 1 , s 2 ), then by construction of N 1 \ K N 2 , there exists

As above, we thus have

• Else, if e ∈ B e (s 1 , s 2 ), then there exists ϕ 1 ∈ C(S 1 ) and ϕ 2 ∈ C(S 2 ) such that L 1 (s 1 , e, ϕ 1 ) =? and L 2 (s 2 , e, ϕ 2 ) = ⊤. Moreover, ϕ is of the form ϕ B 12 , and

) and 0 otherwise. By construction, δ 1 is a correspondence function and we have µ P δ 1 = µ 1 . Thus there exists

, then there exists ϕ 1 ∈ C(S 1 ) such that L(s 1 , e, ϕ 1 ) = ⊥, and either ϕ = ϕ ⊥ 1 or ϕ = ϕ B 12 as in the case above. In both cases, as proven before, there exists µ 1 ∈ Sat(ϕ 1 ) such that µ P ⋐ R1 µ 1 .

-Let a ∈ A and ϕ 1 ∈ C(S 1 ) such that L 1 (s 1 , a, ϕ 1 ) = ⊤.

If s 2 = ⊥ or e = ε or a = e, then by construction of N 1 \ K N 2 , the constraint ϕ ⊥ 1 is such that L((s 1 , s 2 , e, n), a, ϕ ⊥ 1 ) = ⊤. As a consequence, there exists a distribution µ P ∈ Dist(S P ) such that L P (p, a, µ P ) = ⊤ and there exists µ ∈ Sat(ϕ ⊥ 1 ) such that µ P ⋐ R \ µ. Moreover, by construction of ϕ ⊥ 1 , the distribution µ ↓ 1 :

) and it follows that µ P ⋐ R1 µ ↓ 1 . Otherwise, assume that s 2 ∈ S 2 , e ∈ A and a = e. Since L 1 (s 1 , a, ϕ 1 ) = ⊤, (s 1 , s 2 ) can only be in cases 3.a, 3.c or 3.f . As a consequence, e ∈ B a (s

. By construction, in all of these cases, we have L((s 1 , s 2 , e, n), a, ϕ ⊥ 1 ) = ⊤. Thus, there exists a distribution µ P ∈ Dist(S P ) such that L P (p, a, µ P ) = ⊤ and there exists µ ∈ Sat(ϕ ⊥ 1 ) such that µ P ⋐ R \ µ. As above, it follows that µ P ⋐ R1 µ ↓ 1 .

Finally, R 1 is a satisfaction relation. Moreover, by hypothesis, we have

We now prove that P |= N 2 . Assume the contrary and let R 2 ⊆ S P × S 2 be the smallest satisfaction relation witnessing P |= N 2 (i.e. containing only reachable states). We prove the following by induction on the value of n, for 1 ≤ n ≤ K: ∀p ∈ S P , s 2 ∈ S 2 , if there exists

-Base Case (n = 1). Let p, s 1 , s 2 , e such that p R \ (s 1 , s 2 , e, 1).

, then by construction there is an e transition in either P or N 2 that cannot be matched by the other. Thus (p, s 2 ) / ∈ R 2 . The same is verified if e ∈ B e (s 1 , s 2 ) and there is no distribution µ P ∈ Dist(S P ) such that L P (p, e, µ P ) = ⊤. Else, e ∈ B e (s 1 , s 2 ) ∪ B c (s 1 , s 2 ) ∪ B f (s 1 , s 2 ) and there exists µ P ∈ Dist(S P ) such that L P (p, e, µ P ) = ⊤. Let ϕ 1 ∈ C(S 1 ) and ϕ 2 ∈ C(S 2 ) be the corresponding constraints in N 1 and N 2 . Consider the corresponding constraint ϕ B, 1 12 ∈ C(S). By R \ , there exists µ ∈ Sat(ϕ B, 1 12 ) such that µ P ⋐ R \ µ. By construction of ϕ B,1 12 , we know that either (3.a) there exists

does not satisfy ϕ 2 . If there exists (s ′ 1 , ⊥, ε, 1) such that µ(s ′ 1 , ⊥, ε, 1) > 0, then there exists p ′ ∈ S P such that µ P (p ′ ) > 0 and succ s2,e (p ′ ) = ∅. Thus there cannot exists µ ′ 2 ∈ Sat(ϕ 2 ) such that µ P ⋐ R2 µ ′ 2 . Otherwise, by determinism of N 2 , we know that the only possible correspondence function for µ P and R 2 is δ 2 :

) and 0 otherwise. By construction, we have µ P δ 2 = µ 2 and thus there is no distribution µ

-Induction. Let 1 < n ≤ K and assume that for all k < n, for all p ′ ∈ S P , s ′ 2 ∈ S 2 , whenever there exists s

then by construction there is an e transition in either P or N 2 that cannot be matched by the other. Thus (p, s 2 ) / ∈ R 2 . The same is verified if e ∈ B e (s 1 , s 2 ) and there is no distribution µ P ∈ Dist(S P ) such that L P (p, e, µ P ) = ⊤. Else, e ∈ B e (s 1 , s 2 ) ∪ B c (s 1 , s 2 ) ∪ B f (s 1 , s 2 ) and there exists µ P ∈ Dist(S P ) such that L P (p, e, µ P ) = ⊤. Let ϕ 1 ∈ C(S 1 ) and ϕ 2 ∈ C(S 2 ) be the corresponding constraints in N 1 and N 2 .

Consider the corresponding constraint ϕ B,n 12 ∈ C(S). By R \ , there exists µ ∈ Sat(ϕ B,n 12 ) such that µ P ⋐ R \ µ. By construction of ϕ B,n 12 , we know that either (3.a) there exists

By hypothesis, we have s P 0 R \ (s 1 0 , s 2 0 , f, K). As a consequence, we have that

2. We now prove that for all PA P ∈

Otherwise, assume that (s 1 0 , s 2 0 ) is in case 3. Let P = (S P , A, L P , AP, V P , s P 0 ) be a PA such that P |= N 1 and P |= N 2 . Let R 1 be the satisfaction relation witnessing P |= N 1 and R 2 be the maximal satisfaction relation between P and N 2 . Assume that R 2 is computed as described in Section 5. Let Ind R2 be the associated index function and let K be the minimal index such that R 2K = R 2 . We show that P |= N 1 \ K N 2 . Let N 1 \ K N 2 = (S, A, L, AP, V, S 0 ) be defined as in Section 4.2.

Let R \ ⊆ S P × S 2 be the relation such that Remark that whenever (p, s 2 ) is in case 3, we know that Ind R2 (p, s 2 ) < K, thus

the axioms of a satisfaction relation by construction. Else we have s 2 ∈ S 2 and e = ε, thus, by definition of R \ , we know that (p, s 2 ) is in case 3. The rest of the proof is almost identical to the proof of Theorem 1. In the following, we report to this proof and only highlight the differences.

-By construction, we have

-Let a ∈ A and µ P ∈ Dist(S P ) such that L P (p, a, µ P ) = ⊤. There are several cases.

• If a = e, or a = e ∈ B a (p, s 2 ), the proof is identical to the proof of Theorem 1.

• Else, we necessarily have

) such that L 1 (s 1 , e, ϕ 1 ) = ⊥ and there exists µ 1 ∈ Sat(ϕ 1 ) and a correspondence function δ 1 :

12 is such that L((s 1 , s 2 , e, k), e, ϕ B,k 12 ) = ⊤. We now prove that there exists µ ∈ Sat(ϕ B,k 12 ) such that µ P ⋐ R \ µ. Consider the function δ : S P → (S → [0, 1]) defined as follows: Let p ′ ∈ S P such that µ P (p ′ ) > 0 and let s ′ 1 = succ s1,e (p ′ ), which exists by

). As a consequence, we have that µ ′ 1 = µδ 1 = µ 1 ∈ Sat(ϕ 1 ). 3. Depending on k, there are 2 cases.

* If k > 1, assume that for all p ′ ∈ S P such that µ P (p ′ ) > 0, we have succ s2,e (p ′ ) = ∅ (the other case being trivial). Since c

). In the first case (2), consider the distribution µ 2 defined as follows:

We have the following: for all s ′ 2 ∈ S 2 ,

). In the second case (3), we have

). * On the other hand, if k = 1, then Ind R2 (p, s 2 ) = 0 and either (1) there exists p ′ ∈ S P such that µ P (p ′ ) > 0 and succ s2,e (p ′ ) = ∅, or (2) the distribution the distribution µ 2 1 such that

In both cases, as above, we can prove that µ ∈ Sat(ϕ12 B,k . In both cases, we have µ ∈ Sat(ϕ B,k 12 ). We thus conclude that there exists µ ∈ Sat(ϕ B,k 12 ) such that µ P ⋐ R \ µ. -Let a ∈ A and ϕ ∈ C(S) such that L((s 1 , s 2 , e), a, ϕ) = ⊤. As in the proof of Theorem 1, there are several cases that all boil down to the same arguments as above.

Finally, R \ is a satisfaction relation.

Let c ∈ Break R2 (s P 0 , s 2 0 ) and consider the relation R \ ′ = R \ ∪{(s P 0 , (s 1 0 , s 2 0 , c, K))}. Due to the fact that K ≥ Ind R2 (s P 0 , s 2 0 ), one can verify that the pair (s P 0 , (s 1 0 , s 2 0 , c, K)) also satisfies the axioms of a satisfaction relation. The proof is identical to the one presented above. As a consequence, R \ ′ is also a satisfaction relation. Moreover, we now have that (s P 0 , (s

Proof of Proposition 2

Let N 1 and N 2 be two deterministic APAs in SVNF such that N 1 N 2 , and let K ∈ N.

Proof. By Lemma 2, we know that d(N

for each L by Proposition 1. Applying the triangle inequality for d t , we see that

Let N 1 and N 2 be two deterministic APAs in SVNF such that N 1 N 2 . The following holds:

1. the sequences

1. The proof of the convergence of both sequences

is done as follows. We show in Lemma 2 that the sequence (N 1 \ K N 2 ) K is bi-Cauchy (i.e. both forward-Cauchy and backwards-Cauchy) in the sense of [START_REF] Bonsangue | Generalized metric spaces: Completion, topology, and powerdomains via the Yoneda embedding[END_REF]).

. The proof is in several steps.

-We first remark that for all (s 1 , s 2 , e) ∈ S 1 × (S 2 ∪ ⊥) × (A ∪ ε) and for all k ≤ K 1 , the distance between State (s 1 , s 2 , e, k)

Moreover, we know by construction that D N 2 ,N 1 (ϕ ′ , ϕ, d) ≤ 1 for all ϕ ′ and ϕ. As a consequence, d(t 2 , t 1 ) ≤ λ = λ k1 .

• Induction. Let t 1 = (s 1 , s 2 , e, k 1 ) 1 and t

), then t 1 and t 2 are identical by construction and the result holds. Otherwise, the pair of constraints for which the distance is maximal will be constraints ϕ B,k1 12 ∈ C(S 1 ) and ϕ B,k2

By definition, we have

)

)

). One can verify that δ ∈ RD(µ 2 , ϕ B,k1 12 ) as follows: Finally, we have d(t 2 , t 1 ) ≤ λλ k1-1 = λ k , which proves the induction.

-For all state t 2 0 = (s 1 0 , s 2 0 , e, K 2 ) ∈ T 2 0 , there exists a state t 1 0 = (s 1 0 , s 2 0 , e, K 1 ) ∈ T 1 0 such that d(t 2 0 , t 1 0 ) ≤ λ K1 . As a consequence, we have d(N 1 \ K2 N 2 , N 1 \ K1 N 2 ) ≤ λ K1 .

Let ε > 0. Since λ < 1, there exists K ∈ N such that λ K < ε. As a consequence, by the above lemma, we have that for all K ≤ K 1 ≤ K 2 ,

The sequence (N 1 \ K N 2 ) K is thus bi-Cauchy. Hence, because of Proposition 1, the sequence (of sets of PA) ([[N 1 \ K N 2 ]]) K is also bi-Cauchy. The other two items show that they converge.

2.

Theorem 2 shows that the sequence ([[N 1 \ K N 2 ]]) K converges in a set-theoretic sense (as a direct limit), and that lim

] = 0, and by continuity of

3. Finally, we prove that lim K→∞ d(N 1 \ * N 2 , N 1 \ K N 2 ) = 0. This proof is very similar to the proof of Lemma 2 above: we can show that the distance between N 1 \ * N 2 and N 1 \ K N 2 is bounded as follows:

Let N 1 \ K N 2 = N K = (S K , A, L K , AP, V K , T K 0 ) and N 1 \ * N 2 = N * = (S * , A, L * , AP, V * , T * 0 ). We start by proving by induction on 1 ≤ k ≤ K that for all (s 1 , s 2 , e) ∈ S 1 × (S 2 ∪ ⊥) × (A ∪ ε), we have d((s 1 , s 2 , e) * , (s 1 , s 2 , e, k)) ≤ λ k . The only difference with the proof of Lemma 2 is in the choice of the function δ : S * ×S K → [0, 1] in the induction part. Here, we choose δ as follows:

The rest of the proof is identical, and we obtain that for all 1 ≤ k ≤ K and for all (s 1 , s 2 , e) ∈ S 1 × (S 2 ∪ ⊥) × (A ∪ ε), we have d((s 1 , s 2 , e) * , (s 1 , s 2 , e, k)) ≤ λ k . In particular, this is also true for initial states. As a consequence, for all state t * 0 = (s 2 0 , s 1 0 , e) ∈ T * 0 , there exists a state t K 0 = (s 1 0 , s 2 0 , e, K) ∈ T K 0 such that d(t * 0 , t K 0 ) ≤ λ K . As a consequence, we have d(N

As a consequence, we obtain: