Bettina Braitling

Ralf Wimmer

Bernd Becker

Nils Jansen

Erika Ábrahám

Counterexample Generation for Markov Chains Using SMT-Based Bounded Model Checking

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

Introduction

The verification of formal systems has gained great importance both in research and industry. Model checking proves or refutes automatically (i. e. without user interaction) that a system exhibits a given set of properties (see, e. g., [START_REF] Baier | Principles of Model Checking[END_REF]). In many cases model checking also provides helpful diagnostic information; in case of a defective system a counterexample in form of a witnessing run is returned. The usage of symbolic representations like ordered binary decision diagrams (OBDDs) [START_REF] Bryant | Graph-based algorithms for boolean function manipulation[END_REF] assures the usability of model checking for many kinds of large systems. However, there are classes of practically relevant systems for which even these OBDD-based methods fail. To fill this gap, bounded model checking (BMC) was developed [START_REF] Clarke | Bounded model checking using satisfiability solving[END_REF]. Thereby the existence of a path of fixed length that refutes the property under consideration is formulated as a satisfiability (SAT) problem.

As the size of the corresponding formula is relatively small and as modern SATsolvers have strongly evolved over the last 15 years, it is not surprising that this approach is very successful.

To model real-life scenarios it is often necessary to cope with specific uncertainties using probabilities. For instance, properties can be formulated in probabilistic computation tree logic (PCTL) [START_REF] Hansson | A logic for reasoning about time and reliability[END_REF] for models called discrete-time Markov chains (DTMCs). The classical model checking approach for this setting is based on the solution of a linear equation system [START_REF] Hansson | A logic for reasoning about time and reliability[END_REF]. However, it lacks the generation of counterexamples, since the solution of the equation system yields only the mere probabilities without further information.

To provide a user with such diagnostic information for probabilistic systems, there have been some recent developments during the last few years [START_REF] Andrés | Significant diagnostic counterexamples in probabilistic 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] Aljazzar | Directed explicit state-space search in the generation of counterexamples for stochastic model checking[END_REF][START_REF] Ábrahám | DTMC model checking by SCC reduction[END_REF]. Contrary to, e. g., LTL model checking for digital systems, counterexamples for a PCTL property may consist of a large number of paths to reach certain probability bounds. Various techniques have been proposed to obtain compact representations: incrementally adding the paths with the highest probability [START_REF] Han | Counterexample generation in probabilistic model checking[END_REF][START_REF] Aljazzar | Directed explicit state-space search in the generation of counterexamples for stochastic model checking[END_REF], reducing the strongly connected components of the underlying digraph of a DTMC [START_REF] Andrés | Significant diagnostic counterexamples in probabilistic model checking[END_REF][START_REF] Ábrahám | DTMC model checking by SCC reduction[END_REF], and using regular expressions to describe whole sets of counterexamples [START_REF] Han | Counterexample generation in probabilistic model checking[END_REF]. All these techniques rely on an explicit representation of the state space.

Bounded model checking for probabilistic systems in the context of counterexample generation was introduced in [START_REF] Wimmer | Counterexample generation for discrete-time Markov chains using bounded model checking[END_REF], which represents the state space symbolically. This procedure can be used to refute probabilistic reachability problems. They can be formulated in PCTL [START_REF] Hansson | A logic for reasoning about time and reliability[END_REF] as P ≤p (a U b) with atomic propositions a and b. The meaning of this formula is that the probability to reach a b-state, passing only a-states, may be at most p. The refutation is shown by using a SAT-solver to find paths satisfying the property whose joint probability measure exceeds the bound p. The input of the solver are propositional formulae that are satisfied iff the assignment of the variables corresponds to a sequence of states of the DTMC that represents a path to a target state. This process is significantly accelerated by a loop-detection mechanism, which is used to handle sets of paths which differ only in the number of unfoldings of the same loops.

A drawback of the state-of-the-art BMC procedure for DTMCs is that paths are found in an arbitrary order while for the size of counterexamples it is often advantageous to start with paths of high probability. Moreover, it is desirable to use this procedure for Markov reward models (MRMs), which extend DTMCs by the possibility to model costs (or dually rewards) of operations. MRMs allow to verify properties like "The probability to finish the computation with costs larger than c is at most 10 -3 ."

In this paper we therefore extend stochastic BMC in order to handle these problems. Instead of using a SAT-solver, we use the more powerful approach of SMT-solving. SMT stands for satisfiability modulo theories and is a generalization of SAT [START_REF] Nelson | Simplification by cooperating decision procedures[END_REF]. It allows to express propositional formulae representing paths to target states together with conditions on the probability of such paths. Furthermore, real numbers that are allocated to the states by a cost-function can be added up and restrictions on the accumulated costs of paths can be imposed. We will also show how this counterexample generation can be combined with minimization techniques for Markov chains in order not only to speed up the counterexample generation but also to obtain more abstract counterexamples.

Organization of the paper. At first, we give a brief introduction to the foundations of DTMCs, counterexamples, Markov reward models, and bisimulation minimization. Section 3 then explains the concept of SMT-solving for this context. In Sect. 4 we describe the results of some experiments we did on well-known test cases. In Sect. 5 we draw a short conclusion and give an outlook to future work on this approach.

Foundations

In this section we take a brief look at the basics of discrete-time Markov chains, Markov reward models, and bisimulation minimization.

Stochastic Models

Definition 1. Let AP be a set of atomic propositions. A discrete-time Markov chain (DTMC) is a tuple M = (S, s I , P, L) such that S is a finite, non-empty set of states; s I ∈ S, the initial state; P : S × S → [0, 1], the matrix of the one-step transition probabilities; and L : S → 2 AP a labeling function that assigns each state the set of atomic propositions which hold in that state.

P has to be a stochastic matrix that satisfies s ∈S P (s, s ) = 1 for all s ∈ S. A (finite or infinite) path π is a (finite or infinite) sequence π = s 0 s 1 . . . of states such that P (s i , s i+1 ) > 0 for all i ≥ 0. A finite path π = s 0 s 1 . . . s n has length |π| = n; for infinite paths we set |π| = ∞. For i ≤ |π|, π i denotes the i th state of π, i. e., π i = s i . The i th prefix of a path π is denoted by π↑ i = s 0 s 1 . . . s i . The set of finite (infinite) paths starting in state s is called Path fin s (Path inf s ). In order to obtain a probability measure for sets of infinite paths we first need to define a probability space for DTMCs: Definition 2. Let M = (S, s I , P, L) be a DTMC and s ∈ S. We define a probability space Ψ s = (Path inf s , ∆ s , Pr s ) such that -∆ s is the smallest σ-algebra generated by Path inf s and the set of basic cylinders of the paths from Path fin s . Thereby, for a finite path π ∈ Path fin s , the basic cylinder over π is defined as

∆(π) = {λ ∈ Path inf s | λ↑ |π| = π}.
-Pr s is the uniquely defined probability measure that satisfies the equation Pr s (∆(ss

1 s 2 . . . s n )) = P (s, s 1 ) • P (s 1 , s 2 ) • • • • • P (s n-1 , s n ) for all basic cylinders ∆(ss 1 s 2 . . . s n ).
The properties we want to consider are formulated in PCTL [START_REF] Hansson | A logic for reasoning about time and reliability[END_REF] and are of the form P ≤p (a U b) with a, b ∈ AP. This means that the probability to walk along a path from the initial state to a state in which b holds, with all intermediate states satisfying a, is less than or equal to p. More formally: A path π satisfies Han and Katoen have shown that there is always a finite counterexample if P ≤p (a U b) is violated [START_REF] Han | Counterexamples in probabilistic model checking[END_REF].

a U b, written π a U b, iff ∃i ≥ 0 : b ∈ L(π i ) ∧ ∀ 0 ≤ j < i : a ∈ L(π j ) . A
In order to be able to express properties like "The probability to reach a target state with costs larger than c is at most p", Markov chains have to be extended by so-called reward functions. Rewards can be used to model costs of certain operations, to count steps or to measure given gratifications. The variant of rewards we use here are state rewards. One could also assign reward values to transitions instead of states (so-called transition rewards). We restrict ourselves to state rewards; all techniques that are developed in this paper can also be applied to transition rewards.

Let π ∈ Path fin s be a finite path and R a reward function. The accumulated reward of π is given by R(π) = |π|-1 i=0 R(π i ). Note that the reward is granted when leaving a state.

We extend the PCTL-properties from above to Markov reward models. For a (possibly unbounded) interval I ⊆ R, a path π satisfies the property a U I b, written π a U I b, if there is 0 ≤ i ≤ |π| such that b ∈ L(π i ), R(π↑ i ) ∈ I, and a ∈ L(π j ) for all 0 ≤ j < i. A state s ∈ S satisfies P ≤p (a

U I b) if Pr s {π ∈ Path inf s | π a U I b} ≤ p.
Our techniques can be extended in a straightforward way to I being the union of a finite set of intervals. Please note that the bounded until operator of PCTL is a special case of a reward condition.

Our goal is to compute counterexamples to refute such reward properties using bounded model checking (BMC).

Bisimulation Minimization

For the generation of counterexamples we work with a symbolic representation of the DTMC and the reward function. Symbolic representations have the advantage that the size of the representation is not directly correlated with the size of the represented system. The representation can be smaller by orders of magnitude. By using algorithms whose running time only depends on the size of the representation, very large state spaces can be handled.

But even if the symbolic representation of a system is small, the number of paths that are needed for a counterexample can be very large. In order to reduce the number of paths, we first compute the smallest system that has the same behavior w. r. t. probabilities and rewards as the original one. This in general not only reduces the number of states, but also the number of paths, because all paths that stepwise consist of equivalent states are mapped onto a single path in the minimized system.

The methods for computing such minimal systems are based on bisimulation relations. A bisimulation groups states whose behavior is indistinguishable into equivalence classes [START_REF] Katoen | Bisimulation Minimisation Mostly Speeds Up Probabilistic Model Checking[END_REF]: Definition 5. Let M = (S, s I , P, L) be a DTMC and R : S → R a reward function for M . A partition P of S is a bisimulation if the following holds for all equivalence classes C of P and for all s, t ∈ S such that s and t are contained in the same block of P:

L(s) = L(t), R(s) = R(t)
, and P (s, C) = P (t, C), where P (s, C) = s ∈C P (s, s ). Two states s, t ∈ S are bisimilar (s ∼ t) if there exists a bisimulation P such that s and t are contained in the same block of P. The quotient can be considerably smaller than the original system. At the same time it still satisfies the same PCTL and reward properties. All analyses can therefore be carried out on the quotient system instead of the larger original Markov model. For symbolic algorithms to compute the bisimulation quotient of a DTMC or MRM, we refer the reader to, e. g., [START_REF] Derisavi | Signature-based symbolic algorithm for optimal Markov chain lumping[END_REF][START_REF] Wimmer | Symbolic partition refinement with automatic balancing of time and space[END_REF].

SMT-based Bounded Model Checking for Counterexample Generation

In this section we show how counterexamples can be computed using an SMTbased formulation of bounded model checking (BMC). BMC has already been applied in [START_REF] Wimmer | Counterexample generation for discrete-time Markov chains using bounded model checking[END_REF] for this purpose but in a purely propositional variant. The main drawback of the existing approach is that the propositional BMC formula only contains information about the mere existence of a path, but not about its probability measure. Hence there is no direct possibility to control the SAT-solver such that paths with high probability measure are preferred.

Here we propose the usage of a more powerful formulation than purely propositional logic. The satisfiability modulo theories (SMT) problem is a generalization of the propositional satisfiability (SAT) problem. It combines propositional logic with arithmetic reasoning. Using SMT we can create a formula that is only satisfied by paths with a certain minimal probability. This enables us to apply binary search to find paths first whose probability measures differ from the probability of the most probable path of the current unrolling depth by at most a constant ε > 0. Furthermore, this formulation allows us to compute counterexamples for Markov reward models.

Since often even counterexamples of minimal size are too large to be useful, we minimize the DTMC or MRM before determining a counterexample. The counterexample obtained for the minimized system is much more compact since all equivalent evidences of the original system are merged into a single path of the minimized system. Given a counterexample of the minimized system, it can easily be translated back to the original system -either resulting in an ordinary counterexample or in one representative evidence per equivalence class.

We first describe the SMT-based BMC formula and compare it to the SATbased approach of [START_REF] Wimmer | Counterexample generation for discrete-time Markov chains using bounded model checking[END_REF]. Then we show how to handle Markov reward models with an arbitrary number of reward functions. Finally we demonstrate how minimization can be applied to make the counterexample generation more efficient.

SMT-based and SAT-based SBMC

Stochastic bounded model checking (SBMC) as proposed in [START_REF] Wimmer | Counterexample generation for discrete-time Markov chains using bounded model checking[END_REF] is based on the formulation as a (propositional) satisfiability problem that a path of a certain length exists which exhibits a given property. To handle formulae of the form P ≤p (a U b), states that satisfy either ¬a or b are made absorbing by removing all out-going edges. This reduces the problem to reaching a b-state.

After this preprocessing step, SBMC uses a SAT-solver to determine satisfying solutions for the BMC formula, which has the following structure:

SBMC(k) := I(s 0 ) ∧ k-1 i=0 T SAT (s i , s i+1 ) ∧ L b (s k ). (1)
I(s 0 ) is a formula that is satisfied iff the assignment of s 0 corresponds to the initial state s I . Accordingly, T SAT (s i , s i+1 ) represents the transition from a state s i to a successor s i+1 , such that T SAT (s i , s i+1 ) is satisfied iff P (s i , s i+1 ) > 0, and L b (s k ) is the property which holds for s k iff b ∈ L(s k ). Each satisfying assignment of formula (1) corresponds to a path of length k that is an evidence for a U b. The authors of [START_REF] Wimmer | Counterexample generation for discrete-time Markov chains using bounded model checking[END_REF] describe how this formula can efficiently be constructed from a BDD-based representation of the Markov chain. First they construct an OBDD for the underlying directed graph by mapping positive probabilities in the MTBDD representation of the probability matrix to 1. Then they apply Tseitin-transformation [START_REF] Tseitin | On the complexity of derivation in propositional calculus[END_REF] to the OBDDs to construct the different parts of the BMC formula. Fig. 1 gives a rough overview of the BMC procedure for a DTMC M = (S, s I , P, L) and a formula ϕ = P ≤p (a U b).

The probability measure of a path, however, is not considered within this formula. The probability measure has to be computed after the path has been found. Using an SMT-based formulation we can create a modified version of the BMC formula that allows us to put restrictions on the probability measure of evidences. We define an extended transition formula T SMT (s i , s i+1 , pi ) that is satisfied iff P (s i , s i+1 ) > 0 and the variable pi is assigned the logarithm of this probability. Following [START_REF] Han | Counterexample generation in probabilistic model checking[END_REF], the logarithm is used in order to turn the multiplication of the probabilities along a path into a summation. This leads to SMT formulae over linear real arithmetic that can be decided efficiently. This variant of the transition predicate can also be generated from an MTBDD representation of the matrix P (s, s ) of transition probabilities using Tseitin-transformation. In contrast to the propositional case, where 'true' and 'false' are used as atomic formulae for the terminal nodes, we use 'p = log v' for leaves with value v > 0 and 'false' for the leaf 0.

procedure Counterexample preprocess(M, ϕ); C ← ∅; k ← 0; Pr(C) ← 0; ϕ ← BMCformula(k, M, ϕ); while Pr(C) ≤ p do solution ← solve(ϕ) if solution = UNSAT then k ← k + 1; ϕ ← BMCformula(k, M, ϕ); else π ← CreatePath(solution); C ← C ∪ {π}; Pr(C) ← Pr(C) + Pr(π); ϕ ← ϕ ∧ ExcludePath(π); end if end while return C end procedure
To let the solver find only evidences with a probability measure of at least p t ∈ [0, 1], we add the condition k-1 i=0 pi > log p t to the BMC formula:

SSBMC(k) := I(s 0 ) ∧ k-1 i=0 T SMT (s i , s i+1 , pi ) ∧ L b (s k ) ∧ k-1 i=0 pi ≥ log p t . (2)
This formula is given to an SMT-solver. If the solver returns SAT, the satisfying assignment represents an evidence with a probability measure of at least p t . If we get UNSAT, there is no such path of the current length.

This enables us to do a binary search for evidences with a high probability measure in Path fin s I . In principle we could determine the most probable path of the current unrolling depth first, then the one with the second highest probability, and so on. For efficiency reasons we apply a different strategy: First, we look for paths which already exceed our probability threshold p. If this fails, we search for paths with a probability greater or equal to p / 2 . If we have found all existing paths with such a probability and the accumulated probability mass is still less than p, we start looking for paths with a probability greater or equal p / 4 , and so on. The value p t is decreased, until either all paths with length k have been found or the accumulated probability of the set of evidences is high enough. If the latter is not the case, we proceed to depth k + 1.

The optimizations for SBMC -exploiting loops and improvements of the clauses to exclude paths from the search space -, which are proposed in [START_REF] Wimmer | Counterexample generation for discrete-time Markov chains using bounded model checking[END_REF], work for SSBMC as well and without further modification.

Counterexamples for MRMs

With the proposed method, we are not only able to handle DTMCs, but to handle MRMs as well. To consider the reward structure of an MRM during the search for paths, we need to integrate the rewards into the transition relation. In the preprocessing step, which is needed to turn the PCTL-Until property P ≤p (a U I b) into a reachability property, we must not cut the transitions from all b-states. There must be the possibility to extend a path if its accumulated reward is not within I. Thus we cut the transitions only from states s with a ∈ L(s).

After that we extend the transition formula by a formula for the rewards in a similar way as we have done for the probabilities. For each time frame 0 ≤ i < k we introduce a variable ri such that the formula R(s i , ri ) is satisfied iff ri carries the value R(s i ). This formula can be created from an MTBDD representation of the reward function using Tseitin-transformation. The resulting SMT-formula, which takes rewards into account, has the following structure: R-SSBMC(k) := SSBMC(k)

∧ k-1 i=0 R(s i , ri ) ∧ min(I) ≤ k-1 i=0 ri ≤ max(I) . (3)
Since b-states are no longer absorbing when using this formula, we have to make sure that we do not find paths of which we have already found a proper prefix. This can be guaranteed by adding clauses to the formula that exclude all paths that were found in previous iterations. Using this technique it is possible to handle an arbitrary number of reward functions at the same time. We just add distinct variables for each reward function and build several reward sums which are checked against the corresponding intervals.

Bisimulation Minimization

We can use bisimulation minimization (cf. Sec. 2.2) as a further preprocessing step after cutting unnecessary transitions, but before constructing a counterexample. Since in many cases the quotient system is considerably smaller than the original system, fewer paths are needed for a counterexample.

Every path in the bisimulation quotient represents a set of paths in the original system. To be more precise, let π, π ∈ Path fin (s) be two evidences in a DTMC M = (S, s I , P, L). They are equivalent if |π| = |π | and for all 0 ≤ i ≤ |π|: π i ∼ π i . All equivalent paths correspond to the same path in the quotient system, namely to the path

π Q = [π 0 ] ∼ [π 1 ] ∼ . . . [π |π| ] ∼ .
The probability of π Q is the sum of the probabilities of the represented original paths that start in s I . Therefore in general fewer paths are needed in the quotient system for a counterexample.

Once a counterexample has been determined for the quotient DTMC, its paths can be translated back to the original system. The result is a tree that contains all evidences that are stepwise equivalent to the given path. Let us assume that

π Q = C 0 C 1 . . . C n with C 0 = [s I ]
∼ is such a path in the quotient system. We set succ(s) = {s ∈ S | P (s, s ) > 0}. The root of the tree is the initial state s I that corresponds to C 0 on π Q . If s i is a node of the tree that corresponds to C i on π Q , its successor nodes in the tree are succ(s) ∩ C i+1 . They correspond to C i+1 . The probability measures of the resulting tree and of π Q coincide.

In the next section we show the effectiveness of SMT-based counterexample generation and of this optimization on a set of example benchmarks.

Experimental Results

We have implemented the SSBMC-tool in C ++ with the refinements we presented above, including the optimizations from [START_REF] Wimmer | Counterexample generation for discrete-time Markov chains using bounded model checking[END_REF]. We used Yices [START_REF] Dutertre | A fast linear-arithmetic solver for DPLL(T)[END_REF] as the underlying SMT-solver.

Our benchmarks are instances of the following four case studies:

(1) The contract signing protocol [START_REF] Even | A randomized protocol for signing contracts[END_REF][START_REF] Norman | Analysis of probabilistic contract signing[END_REF] (contract) provides a fair exchange of signatures between two parties A and B over a network. If B has obtained the signature of A, the protocol ensures that A will receive the signature of B as well. In our experiments we examine the violation of this property.

(2) The task of the crowds protocol [START_REF] Reiter | Crowds: Anonymity for web transactions[END_REF] (crowds) is to provide a method for anonymous web browsing. The communication of a single user is hidden by routing it randomly within a group of similar users. The model contains corrupt group members who try to discern the source of a message. We explore the probability that these corrupt members succeed.

(3) The leader election protocol [START_REF] Itai | Symmetry breaking in distributed networks[END_REF] (leader) consists of N processors in a synchronous ring. Every processor chooses a random number from {0, . . . , M }. The numbers are passed around the ring, the processor with the highest number becomes the leader if this number is unique. If this fails, a new round starts. We provide a certificate that the probability to eventually elect a leader exceeds a given bound.

(4) The self-stabilizing minimal spanning tree algorithm [START_REF] Collin | Self-stabilizing depth-first search[END_REF] (mst) computes a minimal spanning tree in a network with N nodes. Due to, e. g., communication failures the system may leave the state where a result has been computed, and recover after some time. For our experiments we explore the probability that the algorithm does not recover within a given number of k steps. This model is of particular interest to us, because it has a large number of paths, but only a few have a notable probability mass. Because SAT-based BMC does not find paths with high probability first, the hope is that the SMT approach finds much smaller counterexamples in less time.

We used the probabilistic model checker PRISM [START_REF] Hinton | PRISM: A tool for automatic verification of probabilistic systems[END_REF] to generate symbolic representations of these case studies. All experiments were run on a Dual Core AMD Opteron processor with 2.4 GHz per core and 4 GB of main memory. Any computation which took more than two hours ("-TO -") or needed more than 2 GB of memory ("-MO -") was aborted.

In order to compare the results we ran the same benchmarks under the same conditions also with the SBMC-tool from [START_REF] Wimmer | Counterexample generation for discrete-time Markov chains using bounded model checking[END_REF].

Counterexamples for DTMCs

In this section we present the results for the SSBMC procedure. The evaluation of bisimulation minimization and counterexamples for MRMs follows in subsequent sections.

Table 1 contains the results for counterexample generation for DTMCs using the SMT-and the SAT-approach. The first and the second column contain the names of the model and the probability threshold p. In the third column the maximal unrolling depth k max is listed. The blocks titled "SSBMC" and "SBMC" present the results for SMT-based approach and the SAT-based approach, respectively. The columns "#paths", "time", and "memory" contain the number of paths in the counterexample, the needed computation time in seconds, and the memory consumption in megabytes.

Both tools are able to solve a subset of the instances within the given limits. The SSBMC-tool was aborted due to the memory limit for one instance of the contract benchmark, most instances of the crowds benchmark, and some instances of the leader protocol. The reason is the high memory consumption of the SMT-solver Yices compared to the SAT-solver MiniSAT, which is used in SBMC. The contract and leader benchmarks exhibit the property that all evidences of the same length have the same probability. Therefore the number of paths coincide for both tools. The running time of SSBMC for these instances is slightly higher due to the modified binary search (cf. Sec. 3.1) which increases the number of calls to the solver. The search strategy is also the reason why SSBMC may need slightly more evidences than SBMC, which is the case here for crowds02 07, where the probabilities of the different evidences differ only by a small amount.

Notable are the mst instances. They contain a large number of evidences with very different probabilities. SBMC is not able to compute a counterexample within the given time limit, while SSBMC returns less than 5000 paths in under 3 minutes. A more detailed look showed that SBMC had computed 633 729 paths for mst-14 before the timeout occurred. This is because the SMT-approach is able to compute the more probable evidences first, only few of which are needed for a counterexample.

Bisimulation

In Table 2 we evaluate the impact of bisimulation minimization on running time and memory consumption for SSBMC and SBMC. In Table 3 we show the results of bisimulation with subsequent back-translation of the abstract evidences. In the latter case, we converted the minimized paths completely, i. e., we obtained all original paths which were represented by an abstract path. The running time listed in Table 2 and Table 3 include the time for bisimulation minimization, counterexample generation, and, in Table 3, path conversion. Again, the block titled "SSBMC" ("SBMC") contains the result for the SMT-based (SAT-based) approach.

As we can see, bisimulation minimization causes in most cases a significant decrease in computation time and required memory of SSBMC and SBMC. This effect is somewhat alleviated when the paths are translated back to the original system, although not dramatically. Some instances of the contract and the crowds protocol which could not be solved by SSBMC within the given time and memory bounds become actually solvable, even with path conversion.

However, there is also an exception to this trend: The path conversion for the minimal spanning tree benchmark cannot be done within the given memory bounds. This is due to the fact that one abstract path in these benchmarks represents a great number of original paths, too many to convert them all. While the SMT-based approach without bisimulation minimization can pick the paths with the highest probability, leading to a small counterexample, this is not possible after bisimulation minimization. If we compute the most probable paths in the minimized system, they can correspond to huge numbers of paths in the original system each of which has only negligible probability.

Rewards

For the reward model checking we integrated rewards into the leader election protocol. A reward of 1 is granted whenever a new round starts, i. e., when each processor chooses a new ID. We want to analyze how high the probability measure is that at least three rounds are needed until a leader has been elected. For the experiments we restricted our search to a maximal path length of depth max . We computed all paths with the given property up to this length. The results are shown in Table 4. The first column contains the name of the model, the second the maximal depth depth max . The subsequent columns contain the accumulated probability measure p, the number of found paths, the computation time (in seconds) and the required memory (in megabytes).

Compared to the results in Section 4.1 we need more and longer paths to get a noteworthy probability measure. The computation time and the amount of consumed memory are higher accordingly.

We also integrated bisimulation minimization for Markov reward models with state rewards. In this case only an appropriate initial partition has to be provided for bisimulation computation. The results are shown in Table 5. For the leader benchmarks bisimulation minimization results in a enormous compression of the state space and a respective reduction of the number of evidences. Since the back-translation can be done efficiently and yields for the leader benchmark the same counterexample as the version without minimization, using bisimulation minimization as a preprocessing and back-translation as a postprocessing step reduces the overall computation time and memory consumption.

Conclusion

In our paper we showed how SMT and BMC can be combined to efficiently generate counterexamples for DTMCs. Our SSBMC method can handle systems which could not be handled with the previously presented SAT-based approach [START_REF] Wimmer | Counterexample generation for discrete-time Markov chains using bounded model checking[END_REF]. With SSBMC it is also possible to analyze Markov reward models with an arbitrary number of reward functions. This enables us to refute reachability properties which impose restrictions on the accumulated reward of paths. Furthermore we presented bisimulation minimization as a preprocessing step for SSBMC. It reduces the number of evidences needed for a counterexample by merging equivalent paths. This way the counterexample generation is accelerated and the memory consumption is reduced. We are able to convert these minimized paths back to the original ones. As future work we will carry out a more detailed experimental evaluation of our methods on appropriate models. Furthermore, there are still many possible optimizations for our tool. So far, reward model checking and bisimulation minimization only work without the loop detection optimization from [START_REF] Wimmer | Counterexample generation for discrete-time Markov chains using bounded model checking[END_REF]. These combinations have to be implemented.

We plan to optimize the search for paths with higher probabilities. We want to include the BDD-based method from [START_REF] Günther | Symbolic calculation of k-shortest paths and related measures with the stochastic process algebra tool Caspa[END_REF], which applies Dijkstra's shortest path algorithm to compute the most probable evidences, into our tool as another preprocessing step. The advantage of this method is that it yields counterexamples of minimal size. Preliminary experiments have shown that this method is efficient as long as the number of paths is small. Since the BDD sizes grow with each path that has been found, memory consumption and running time grow accordingly. We want to combine this approach with the SMT-approach by using the BDDbased method as long as it is efficient and switch to the SMT-approach when the BDD-approach becomes too expensive.

Definition 4 .

 4 A Markov reward model (MRM) is a pair (M, R) where M = (S, s I , P, L) is a DTMC and R : S → R a real-valued reward function.

  The equivalence classes of bisimilarity and the coarsest bisimulation partition coincide. The equivalence class of a state s ∈ S w. r. t. a bisimulation P is denoted by [s] P . The classes of the bisimulation now become the states of a new DTMC. Definition 6. Let M = (S, s I , P, L) be a DTMC, R a reward function for M , and P be a bisimulation. The bisimulation quotient is the DTMC (P, C I , P , L ) with reward function R such that -For all C, C ∈ P: P (C, C ) = P (s, C ) for an arbitrary s ∈ C, -C I is the block that contains the initial state s I of M , -∀ C ∈ P : L (C) = L(s) for an arbitrary state s ∈ C, and -∀ C ∈ P : R (C) = R(s) for an arbitrary state s ∈ C.

Fig. 1 .

 1 Fig. 1. Counterexample generation

  state s ∈ S satisfies the formula P ≤p (a U b) (written s P ≤p (a U b)) iff Pr s {π ∈ Path inf s |π a U b} ≤ p. Let us assume that such a formula P ≤p (a U b) is violated by a DTMC M . That means Pr s I {π ∈ Path inf s |π a U b} > p.In this case we want to compute a counterexample which certifies that the formula is indeed violated. Hence a counterexample is a set of paths that satisfy a U b and whose joint probability measure exceeds the bound p. Definition 3. Let M = (S, s I , P, L) be a discrete-time Markov chain for which the property ϕ = P ≤p (a U b) is violated in state s I . An evidence for ϕ is a finite path π ∈ Path fin s I such that π a U b, but no proper prefix of π satisfies this formula. A counterexample is a set C ⊆ Path fin s I of evidences such that Pr s I (C) > p.

Table 1 .

 1 Counterexample generation for DTMCs using SMT-and SAT-based BMC

					SSBMC			SBMC
	Name	p	kmax #paths	time	mem. #paths	time	mem.
	contract05 03 0.500 37	513	14.85 124.72	513	25.04	74.84
	contract05 08 0.500 87	513 134.92 889.32	513 399.08 694.71
	contract06 03 0.500 44	2049	70.21 388.81	2049 140.36 124.79
	contract06 08 0.500 92		-MO -		2049 2620.12 1181.76
	contract07 03 0.500 51	8193 474.59 1510.28	8193 627.56 198.27
	crowds02 07	0.100 39	21306 1006.05 1394.26	21116 417.89	96.11
	crowds04 06	0.050 34		-MO -		80912 1468.94 278.17
	crowds04 07	0.050 34		-MO -		80926 1773.83 286.38
	crowds05 05	0.050 36		-MO -			-MO -
	crowds10 05	0.025 27		-MO -		52795 1654.83 188.51
	leader03 04	0.990	8	276	0.70	27.45	276	0.76	14.55
	leader03 08	0.990	8	1979	28.21 101.41	1979	25.76	66.48
	leader04 03	0.990 20		-MO -		347454 3959.88 720.56
	leader05 02	0.900 42		-MO -			-MO -
	leader06 02	0.900 84		-MO -			-TO -
	mst14	0.990 14	426	11.64	42.99		-TO -
	mst15	0.049 15	4531	98.58 148.82		-TO -
	mst16	0.047 16	4648 107.27 158.25		-TO -
	mst18	0.036 18	4073 109.26 164.24		-TO -
	mst20	0.034 20	452	19.57	58.21		-TO -

Table 2 .

 2 Counterexample generation with bisimulation minimization

					SSBMC		SBMC
	Name	p	kmax #paths	time mem. #paths	time mem.
	contract05 03 0.500 37	7	23.41 61.42	7	48.50 54.55
	contract05 08 0.500 87	7 467.88 179.29	7 829.43 94.72
	contract06 03 0.500 44	8	57.75 84.94	8 144.06 64.56
	contract06 08 0.500 97	8 1205.37 209.47	8 2213.94 120.83
	contract07 03 0.500 51	9 169.37 123.93	9 407.63 79.13
	crowds02 07	0.100 39	21069 629.24 633.34	21279 191.31 101.34
	crowds04 06	0.050 34	3459 106.17 164.95	3624	44.19 48.76
	crowds04 07	0.050 34	3459 123.32 167.61	3555	46.97 50.67
	crowds05 05	0.050 36	6347 184.06 251.70	8435	55.20 50.47
	crowds10 05	0.025 27	251	12.74 71.20	347	10.22 47.84
	leader03 04	0.990	8	2	0.12 21.68	2	0.10 12.06
	leader03 08	0.990	8	2	0.64 33.93	2	0.68 24.31
	leader04 03	0.990 20	4	0.31 25.12	4	0.32 15.50
	leader05 02	0.900 42	7	0.24 22.94	7	0.24 12.05
	leader06 02	0.900 84	12	0.79 26.19	12	0.89 14.09
	mst14	0.990 14	9	2.28 38.10	396	0.78 16.85
	mst15	0.049 15	13	1.85 39.36	1648	1.40 17.92
	mst16	0.047 16	13	2.19 39.73	5632	4.00 25.99
	mst18	0.036 18	9	3.57 43.64	27475	30.82 69.69
	mst20	0.034 20	7	5.02 44.91	20290	25.83 56.63

Table 3 .

 3 Counterexample generation with bisimulation and path conversion

				SSBMC			SBMC
	Name	p kmax #paths	time mem. #paths	time mem.
	contract05 03 0.500 37	520	27.87	72.87	520	50.86	54.36
	contract05 08 0.500 87	520 859.34 182.64	520 1259.94	98.06
	contract06 03 0.500 44	2064	72.27	91.44	2064 168.28	75.50
	contract06 08 0.500 97	2064 4181.45 224.31	2064 5927.5 131.68
	contract07 03 0.500 51	8224 230.69 149.60	8224 450.20 103.13
	crowds02 07 0.100 39	21069 812.51 699.80 21279 313.99 168.42
	crowds04 06 0.050 34	81227 408.69 406.16 81138 218.81 289.62
	crowds04 07 0.050 34	81227 426.69 409.29 80705 221.80 290.00
	crowds05 05 0.050 36		-MO -			-MO -
	crowds10 05 0.025 27	54323 198.30 194.38 53507 119.83 168.93
	leader03 04	0.990 8	300	0.21	21.68	300	0.16	12.06
	leader03 08	0.990 8	4536	4.12	33.93	4536	3.67	24.31
	leader04 03	0.990 20 583440 483.99 1123.74 583440 300.24 1108.83
	leader05 02	0.900 42		-MO -			-MO -
	leader06 02	0.900 84		-MO -			-MO -
	mst14	0.990 14		-MO -			-MO -
	mst15	0.049 15		-MO -			-MO -
	mst16	0.047 16		-MO -			-MO -
	mst18	0.036 18		-MO -			-MO -
	mst20	0.034 20		-MO -			-MO -

Table 4 .

 4 Counterexample generation for MRMs using SMT-based BMC

	Model	depth max	p	#paths	time	mem.
	leader03 04	23	0.00391	20160	290.62	434.45
	leader03 05	19	0.00160	18000	290.16	379.25
	leader03 06	19	0.00077	52920 2134.05 1147.73
	leader03 08	15	0.00024	32256 1050.96	709.98
	leader04 02	25	0.21875	37376	912.11 1110.54
	leader04 03	19	0.04979	26460	589.94	761.34
	leader05 02	23	0.14771	4840	40.16	163.06
	leader06 02	25	0.12378	32448	907.33 1360.11
	leader08 02	28		-MO -

Table 5 .

 5 Counterexample generation for MRMs with bisimulation minimization

			without conv.		with conv.
	Model	depth max	p	#paths time mem.	p	#paths time mem.
	leader03 04	23	0.00391	3	0.15 21.70 0.00391 20160 9.37 59.36
	leader03 05	19	0.00160	2	0.25 24.84 0.00160 18000 10.68 54.93
	leader03 06	19	0.00077	2	0.38 26.96 0.00077 52920 34.30 119.10
	leader03 08	15	0.00024	1	0.66 33.96 0.00024 32256 25.95 69.56
	leader04 02	25	0.21875	3	0.11 21.29 0.21875 37376 20.43 92.57
	leader04 03	19	0.04979	1	0.29 25.15 0.04979 26460 18.55 72.67
	leader05 02	23	0.14771	1	0.18 22.12 0.14771	4840 3.23 31.45
	leader06 02	25	0.12378	1	0.30 23.74 0.12378 32448 31.71 87.96
	leader08 02	28	0.05493	1	0.98 31.33		-MO -

This work was partly supported by the German Research Council (DFG) as part of the Transregional Collaborative Research Center "Automatic Verification and Analysis of Complex Systems" (SFB/TR 14 AVACS) and the DFG-Project "CEBug -CounterExample Generation for Stochastic Systems using Bounded Model Checking"


John Derrick

Eerke Boiten

Relational Concurrent Refinement: timed refinement

Keywords: Data refinement, Z, simulations, timed-refinement

Data refinement in a state-based language such as Z is defined using a relational model in terms of the behaviour of abstract programs. Downward and upward simulation conditions form a sound and jointly complete methodology to verify relational data refinements, which can be checked on an event-byevent basis rather than per trace. In models of concurrency, refinement is often defined in terms of sets of observations, which can include the events a system is prepared to accept or refuse, or depend on explicit properties of states and transitions. By embedding such concurrent semantics into a relational one, eventwise verification methods for such refinement relations can be derived. In this paper we continue our program of deriving simulation conditions for process algebraic refinement by considering how notions of time should be embedded into a relational model, and thereby deriving relational notions of timed refinement.

Introduction

The modelling and understanding of time is important in computer science. It plays an especially important role in refinement, where how time is modelled and how it is treated in a development step lead to important differences and subtleties in notions of refinement. These distinctions are more prominent in a process algebra or behavioural setting where many refinement preorders have been defined, reflecting different choices of what is taken to be observable and different choices of how time is modelled.

In a process algebra such as CSP [START_REF] Hoare | Communicating Sequential Processes[END_REF] a system is defined in terms of actions (or events) which represent the interactions between a system and its environment. The exact way in which the environment is allowed to interact with the system varies between different semantics. Typical semantics are set-based, associating one or more sets with each process, for example traces, refusals, divergences. Refinement is then defined in terms of set inclusions and equalities between the corresponding sets for different processes. A survey of many prominent untimed process algebraic refinement relations is given in [START_REF] Van Glabbeek | The linear time -branching time spectrum I. The semantics of concrete sequential processes[END_REF][START_REF] Van Glabbeek | The linear time -branching time spectrum II; the semantics of sequential systems with silent moves[END_REF]. The addition of time adds further complications, and there are important choices as to how time is modelled, and the assumptions one makes. These choices all affect any associated refinement relations.

In a state-based system, e.g., one specified in Z, specifications are considered to define abstract data types (ADTs), consisting of an initialisation, a collection of operations and a finalisation. A program over an ADT is a sequential composition of these elements. Refinement is defined to be the subset relation over program behaviours for all possible programs, where what is deemed visible is the input/output relation. The accepted approach to make verification of refinements tractable is through downward and upward simulations which are sound and jointly complete [START_REF] De Roever | Data Refinement: Model-Oriented Proof Methods and their Comparison[END_REF]. Although there has been some work on modelling time relationally (eg see work on duration calculus and its integration with state-based languages [START_REF] Yuan | Duration calculus in COOZ[END_REF]), there has been less work on associated refinement relations, and none on how to model the various choices that arise in a process algebraic setting.

In integrated notations, for both practical and theoretical reasons, it is important to understand how time is modelled, whether from the process algebraic or statebased angle, and how this impacts on refinement. Our ongoing research on relational concurrent refinement [START_REF] Derrick | Relational concurrent refinement[END_REF][START_REF] Boiten | Relational concurrent refinement II: Internal operations and outputs[END_REF][START_REF] Derrick | More relational refinement: traces and partial relations[END_REF][START_REF] Boiten | Modelling divergence in relational concurrent refinement[END_REF][START_REF] Derrick | Relational concurrent refinement: Automata[END_REF] contributes to this agenda, by explicitly recording in a relational setting the observations characterising process algebraic models. This allows the verification of concurrent refinement through the standard relational method of simulations, and to interpret relational formalisms like Z in a concurrency model.

We derived simulation rules for process algebraic refinement (such as trace, failuresdivergences, readiness [START_REF] Derrick | Relational concurrent refinement[END_REF] etc), including also outputs and internal operations [START_REF] Boiten | Relational concurrent refinement II: Internal operations and outputs[END_REF], for different models of divergence [START_REF] Boiten | Modelling divergence in relational concurrent refinement[END_REF], as well as automaton-based refinements [START_REF] Derrick | Relational concurrent refinement: Automata[END_REF]. The current paper extends this by considering how time can be modelled in a relational context, and thus we derive simulation rules for some of the timed refinement preorders. In Section 2 we provide the basic definitions and background. In Section 3 we provide the simulation rules for a number of process algebraic preorders. In Section 4 we introduce time and timed refinements, and derive their relational simulation rules. We conclude in Section 5.

Background

The standard refinement theory of Z [START_REF] Woodcock | Using Z: Specification, Refinement, and Proof[END_REF][START_REF] Derrick | Refinement in Z and Object-Z[END_REF] is based on a relational model of data refinement where all operations are total, as described in [START_REF] He | Data refinement refined[END_REF]. However, the restriction to total relations can be dropped, see [START_REF] Jifeng | Prespecification and data refinement[END_REF], and soundness and joint completeness of the same set of simulation rules in the more general case can be shown.

A partial relational model

A program (defined here as a sequence of operations) is given as a relation over a global state G, implemented using a local state State. The initialisation of the program takes a global state to a local state, on which the operations act, a finalisation translates back from local to global. In order to distinguish between relational formulations (which use Z as a meta-language) and expressions in terms of Z schemas etc., we use the convention that expressions in the relational data types are typeset in a sans serif font.

Definition 1 (Data type)

A (partial) data type is a quadruple (State, Init, {Op i } i∈J , Fin). The operations {Op i }, indexed by i ∈ J , are relations on the set State; Init is a total relation from G to State; Fin is a total relation from State to G. If the operations are all total relations, we call it a total data type.

2

Insisting that Init and Fin be total merely records the facts that we can always start a program sequence and that we can always make an observation. Downward and upward simulations form a sound and jointly complete [START_REF] He | Data refinement refined[END_REF][START_REF] De Roever | Data Refinement: Model-Oriented Proof Methods and their Comparison[END_REF] proof method for verifying refinements. In a simulation a step-by-step comparison is made of each operation in the data types, and to do so the concrete and abstract states are related by a retrieve relation.

Definition 4 (Downward and upward simulations)

Let A = (AState, AInit, {AOp i } i∈J , AFin) and C = (CState, CInit, {COp i } i∈J , CFin). A downward simulation is a relation R from AState to CState satisfying CInit ⊆ AInit o 9 R R o 9 CFin ⊆ AFin ∀ i : J • R o 9 COp i ⊆ AOp i o 9 R An upward simulation is a relation T from CState to AState such that CInit o 9 T ⊆ AInit CFin ⊆ T o 9 AFin ∀ i : J • COp i o 9 T ⊆ T o 9 AOp i 2.2 Refinement in Z
The definition of refinement in a specification language such as Z is usually based on the relational framework described above, using an additional intermediate step (not used in the rest of this paper) where partial relations are embedded into total relations ("totalisation", see [START_REF] Woodcock | Using Z: Specification, Refinement, and Proof[END_REF][START_REF] Derrick | Refinement in Z and Object-Z[END_REF] for details). Specifically, a Z specification can be thought of as a data type, defined as a tuple (State, Init, {Op i } i∈J ). The operations Op i are defined in terms of (the variables of) State (its before-state) and State (its after-state). The initialisation is also expressed in terms of an after-state State . In addition to this, operations can also consume inputs and produce outputs. As finalisation is implicit in these data types, it only has an occasional impact on specific refinement notions. If specifications have inputs and outputs, these are included in both the global and local state of the relational embedding of a Z specification. See [START_REF] Derrick | Refinement in Z and Object-Z[END_REF] for the full details on this -in this paper we only consider data types without inputs and outputs. In concurrent refinement relations, inputs add little complication; outputs particularly complicate refusals as described in [START_REF] Boiten | Relational concurrent refinement II: Internal operations and outputs[END_REF]. In a context where there is no input or output, the global state contains no information and is a one point domain, i.e., G == { * }, and the local state is State == State. In such a context the other components of the embedding are as given below.

Definition 5 (Basic embedding of Z data types) The Z data type (State, Init, {Op i } i∈J ) is interpreted relationally as (State, Init, {Op i } i∈J , Fin) where

Init == {Init • * → θState } Op == {Op • θState → θState } Fin == {State • θState → * }
Given these embeddings, we can translate the relational refinement conditions of downward simulations for totalised relations into the following refinement conditions for Z ADTs.

Definition 6 (Standard downward simulation in Z)

Given Z data types A = (AState, AInit, {AOp i } i∈J ) and C = (CState, CInit, {COp i } i∈J ). The relation R on AState ∧ CState is a downward simulation from A to C in the nonblocking model if

∀ CState • CInit ⇒ ∃ AState • AInit ∧ R ∀ i : J ; AState; CState • pre AOp i ∧ R ⇒ pre COp i ∀ i : J ; AState; CState; CState • pre AOp i ∧ R ∧ COp i ⇒ ∃ AState • R ∧ AOp i
In the blocking model, the correctness (last) condition becomes

∀ i : J ; AState; CState; CState • R ∧ COp i ⇒ ∃ AState • R ∧ AOp i 2
The translation of the upward simulation conditions is similar, however this time the finalisation produces a condition that the simulation is total on the concrete state.

Definition 7 (Standard upward simulation in Z)

For Z data types A and C , the relation T on AState ∧ CState is an upward simulation from A to C in the non-blocking model if

∀ AState ; CState • CInit ∧ T ⇒ AInit ∀ i : J ; CState • ∃ AState • T ∧ (pre AOp i ⇒ pre COp i ) ∀ i : J ; AState ; CState; CState • (COp i ∧ T ) ⇒ (∃ AState • T ∧ (pre AOp i ⇒ AOp i ))
In the blocking model, the correctness condition becomes

∀ i : J ; AState ; CState; CState • (COp i ∧ T ) ⇒ ∃ AState • T ∧ AOp i 2
3 Process algebraic based refinement

The semantics of a process algebra [START_REF] Hoare | Communicating Sequential Processes[END_REF][START_REF] Milner | Communication and Concurrency[END_REF][START_REF]Handbook of Process Algebra[END_REF] is often given by associating a labelled transition system (LTS) to each term. Equivalence, and preorders, can be defined over the semantics where two terms are identified whenever no observer can notice any difference between their external behaviours. Varying how the environment interacts with a process leads to differing observations and therefore different preorders (i.e., refinement relations) -an overview and comprehensive treatment is provided by van Glabbeek in [START_REF] Van Glabbeek | The linear time -branching time spectrum I. The semantics of concrete sequential processes[END_REF][START_REF] Van Glabbeek | The linear time -branching time spectrum II; the semantics of sequential systems with silent moves[END_REF]. We will need the usual notation for labelled transition systems: Every state in the LTS itself represents a process -namely the one representing all possible behaviour from that point onwards. Specific notation needed includes the usual notation for writing transitions as p a -→ q for (p, a, q) ∈ T and the extension of this to traces (written p tr -→ q) and the set of enabled actions of a process which is defined

as: next(p) = {a ∈ Act | ∃ q • p a -→ q}.
To relate refinements in process algebras to those in a relational model, the methodology (as described in earlier papers [START_REF] Derrick | Relational concurrent refinement[END_REF][START_REF] Boiten | Relational concurrent refinement II: Internal operations and outputs[END_REF][START_REF] Derrick | More relational refinement: traces and partial relations[END_REF][START_REF] Derrick | Relational concurrent refinement: Automata[END_REF]) is as illustrated in the following subsection. As an example in an untimed context we give the embedding of the trace semantics and trace preorder as follows.

Trace preorder

We first define the trace refinement relation.

Definition 9 σ ∈ Act * is a trace of a process p if ∃ q • p σ -→ q.
T (p) denotes the set of traces of p. The trace preorder is defined by p tr q iff T (q) ⊆ T (p).

2

We then define a relational embedding of the Z data type, that is, define a data type (specifically define the finalisation operation) so as to facilitate the proof that data refinement equals the event based semantics. The choice of finalisation is taken so that we observe the characteristics of interest. Thus in the context of trace refinement we are interested in observing traces, but in that of failures refinement we need to observe more. So here possible traces lead to the single global value; impossible traces have no relational image.

Definition 10 (Trace embedding)

A Z data type (State, Init, {Op i } i∈J ) has the following trace embedding into the relational model.

G == { * } State == State Init == {Init • * → θState } Op == {Op • θState → θState } Fin == {State • (θState, * )}
To distinguish between the different embeddings we denote the trace embedding of a data type A as A | tr . We drop the | tr if the context is clear.

2

We then describe how to calculate the relevant LTS aspect from the Z data type. For example, for trace refinement what denotes traces (as in Definition 9) in the Z data type.

Definition 11

The traces of a Z data type (State, Init, {Op i } i∈J ) are all sequences i 1 , . . . , i n such that

∃ State • Init o 9 Op i1 o 9 . . . o 9
Op in We denote the traces of an ADT A by T (A).

2

We now prove that data refinement equals the relevant event based definition of refinement:

Theorem 1. With the trace embedding, data refinement corresponds to trace preorder. That is, when Z data types A and C are embedded as A and C,

A | tr data C | tr iff T (C ) ⊆ T (A)
Finally, we extract a characterisation of refinement as simulation rules on the operations of the Z data type. These are of course the rules for standard Z refinement but omitting applicability of operations, as used also e.g., in Event-B.

CInit ⊆ AInit o 9 R R o 9 CFin ⊆ AFin ∀ i : I • R o 9 COp i ⊆ AOp i o 9 R
We thus have the following conditions for the trace embedding.

Definition 12 (Trace simulations in Z)

A relation R on AState ∧ CState is a trace downward simulation from A to C if

∀ CState • CInit ⇒ ∃ AState • AInit ∧ R ∀ i ∈ J • ∀ AState; CState; CState • R ∧ COp i ⇒ ∃ AState • R ∧ AOp i
The relation T on AState ∧ CState is a trace upward simulation from A to C if it is total on CState and

∀ AState ; CState • CInit ∧ T ⇒ AInit ∀ i : J • ∀ AState ; CState; CState • (COp i ∧ T ) ⇒ (∃ AState • T ∧ AOp i ) 2
4 Timed models

We now add in the consideration of time into our framework. We adapt our definitions of data type, refinement and simulations given above for the untimed case, and again consider different refinement relations based upon differing semantics.

A timed relational model

We do not consider internal or silent actions, as their consideration complicates some of the timing based issues and these are discussed below. The model we define is essentially that of timed automaton [START_REF] Lynch | Forward and backward simulations Part II: timing-based systems[END_REF], and we make the following assumptions:

-We use a continuous time domain R + , although we could parameterize the theory by a time domain T . -We have a single global clock.

-We impose no constraints about Zeno behaviour or its absence.

-We have no internal events.

-We have no timelocks, time can always progress.

-Time additivity: If time can advance by a particular amount d in two steps, then it can also advance by d in a single step. This corresponds to the axiom S1 in [START_REF] Lynch | Forward and backward simulations Part II: timing-based systems[END_REF]. -Time interpolation: which is the converse of time additivity, that is, for any time progression there is an intermediate state at any instant during that progression. This corresponds to the axiom S2 in [START_REF] Lynch | Forward and backward simulations Part II: timing-based systems[END_REF].

Additional constraints can be placed as is done in many models. For example, constancy of offers [START_REF] Schneider | Concurrent and Real Time Systems: The CSP Approach[END_REF] states that the progression of time does not introduce any new events as possibilities, nor allows the withdrawal of any offers. Another axiom which is commonly included is that of time determinism, that is, that if time evolves but no internal or other visible action takes place then the new state is uniquely determined.

Our relational model will then be constructed with the following in mind:

-We assume the specifications contain a reserved variable t (of type R + ) representing the current time which is part of the local state State, which also serves as the relational local state State. -Atomic operations can refer to t but not change it, that is, they are instantaneous.

-The time passing operation Op τ advances t by τ as well as possibly having other effects. -A variable t representing time is also added to the global state G. Since time can always progress, these time passing operations are total.

-The finalisation Fin maps t in State to t in G, that is, it makes time visible at the end of a computation. -Programs are then, as before, finite sequences of time passing or atomic operations.

With this construction (which is just an embedding of time into our relational model) Definitions 1 and 2 define notions of data type and program, and Definitions 3 and 4 give us definitions of refinement and simulations for use on the timed relational model. Furthermore, the assumption of a global clock holds for both abstract and concrete systems, and simulation conditions on the given finalisation imply that the retrieve relation has to be the identity as far as time t is concerned.

A timed behavioural model

To relate the simulations with differing refinement preorders we need a timed semantics such as provided by timed automaton, e.g., [START_REF] Lynch | Forward and backward simulations Part II: timing-based systems[END_REF], or the semantics for a timed process algebra, e.g., [START_REF] Reed | The timed failures-stability model for CSP[END_REF][START_REF] Schneider | Concurrent and Real Time Systems: The CSP Approach[END_REF]. To do so we will augment our LTSs with visible time passing actions, and will not make a fundamental distinction between a transition due to time and one due to another atomic action as is done in some process algebraic semantics (i.e., we do not have two types of transitions). Similarly we do not, at this stage, make a distinction between visible time actions and other external actions as is done in, say, [START_REF] Schneider | Concurrent and Real Time Systems: The CSP Approach[END_REF] (i.e., we do not have two types of actions or events), c.f. pp3 of [START_REF] Lynch | Forward and backward simulations Part II: timing-based systems[END_REF].

Example 1. The automaton A in Figure 1 represents a system that places no timing constraints on the sequential ordering of the events a then b then stop. In this, and subsequent figures, we denote arbitrary time passing by the transition d -→.

In Figure 1 B adapts the above to introduce a specific time delay of at least 1 time units (assumed here to be secs) between a and b. This system corresponds to the timed CSP behaviour of a Timed traces, which consist of a trace of action-time pairs (the time component recording the time of occurrence of the action), are often used as the representation of visible executions in a timed model (e.g., as in [START_REF] Lynch | Forward and backward simulations Part II: timing-based systems[END_REF][START_REF] Reed | The timed failures-stability model for CSP[END_REF][START_REF] Schneider | Concurrent and Real Time Systems: The CSP Approach[END_REF]). However, in order that we can reuse results from Section 3 we take timed traces to be simply traces over the visible actions, which here includes time and other atomic actions. Thus a timed trace here will be of the form t 1 , a 1 , t 2 , a 2 , . . . , where the strict alternation can be assumed without loss of generality. In [START_REF] Lynch | Forward and backward simulations Part II: timing-based systems[END_REF] a mapping is defined between the set of traces given as action-time pairs and those consisting of traces over time and other atomic actions, thus there is no loss of generality in our assumption of the form of timed traces.

Init == {t 0 : R + • t 0 → t = t 0 , x = 0, t a = 0 } Op τ == [∆State | x = x ∧ t a = t a ∧ t = t + τ ] a == [∆State | x = 0 ∧ x = 1 ∧ t a = t ∧ t = t] b == [∆State | x = 1 ∧ x = 2 ∧ t ≥ t a + 1 ∧ t = t] Fin == λ s : State • s.t
Timed trace preorder We now consider the first preorder: the timed trace preorder.

Definition 13 Let Act be the atomic (non-time passing) actions, and t-Act = Act ∪ {Op τ | τ ∈ R + }. Let us denote the set of timed traces of p by T t (p) ⊆ (t-Act) * . The timed trace preorder, t-tr , is defined by p t-tr q iff T t (q) ⊆ T t (p). 2

Example 3. Figure 1 defines A and B with A t-tr B but B t-tr A. However, A and B have the same underlying untimed behaviour even though A = t-tr B . 2

Because of the construction of our timed relational model, and in particular, the consideration of timed actions as visible actions, the embeddings and correspondence given in Definitions 10 and 11 and Theorem 1 carry over directly to the timed case. Thus all that remains to be done is to derive the consequences for the simulation rules.

In fact, the derivations given in Definition 12 still hold providedt the quantification ∀ i : I includes quantification over the time passing events. All that remains is thus to articulate the precise consequences of this with regards to time. We consider these in turn.

Initialisation: the consequence here is, since the retrieve relation is the identity on time, the times at initialisation must be the same.

Non-time passing actions: the correctness condition falls apart into two parts: the usual correctness condition as in Definition 12 for the untimed aspects of the behaviour, with the additional consequence that

R ∧ pre COp i ⇒ pre AOp i
where the preconditions include reference to t -this in particular implies that in linked states, at the same time t, COp i can only be enabled if AOp i is.

Time passing actions: Since by assumption the time passing actions are total, the correctness condition in the blocking model thus becomes (for a downward simulation):

∀ τ ∈ R + • ∀ AState; CState; CState • R ∧ COp τ ⇒ ∃ AState • R ∧ AOp τ
if the time passing actions do not change the rest of the state space (i.e., we have time determinism), then this is vacuously satisfied. corresponding to P = (a → stop) and Q = (WAIT 2; a → stop) have the same untimed behaviour and P t-tr Q but Q t-tr P since 1, a is a timed trace of P but not of Q.

2

The above simulations agrees with those presented in [START_REF] Lynch | Forward and backward simulations Part II: timing-based systems[END_REF], where Lynch and Vaandrager derive simulations for timed automata in a fashion similar to those presented in [START_REF] Lynch | Forward and backward simulations I.: untimed systems[END_REF] for untimed automata (see also results in [START_REF] Derrick | Relational concurrent refinement: Automata[END_REF]). Specifically, they present a notion of timed refinement and the corresponding timed forward simulation and timed backward simulation. As in the untimed case, their notion of timed refinement corresponds to timed trace preorder, and their timed simulations to those given by the simulations defined here.

Many of the results in [START_REF] Lynch | Forward and backward simulations Part II: timing-based systems[END_REF] are derived via their untimed counterpart using the idea of a closure automaton which embeds a timed automaton into one with explicit time passing steps. Definitions and results on the closure automata can be translated directly to definitions and results on the underlying timed automata. In terms of our relational construction, such a closure corresponds to our basic definition since we consider time passing to be visible (in order that our results concerning simulations carry over to the timed case).

Our motivation for considering time passing to be a visible action here, though is twofold. Not only does it allow one to use the results of the preceding sections concerning simulations, but moreover, the view that time passing is indeed visible. Since we are less concerned with the parallel composition of two components in our relational framework, we do not need to stress the component-environment boundary and interface in a way that comes to the fore in, say, a process algebra. Thus we can either consider time to be visible, yet not under the control of the environment or even to be visible and under the control of an environment that will always offer time passing as one of its behaviours.

Completed timed trace preorder In an untimed setting, σ ∈ Act * is a completed trace of a process p if ∃ q • p σ -→ q and next(q) = ∅. CT (p) denotes the set of completed traces of p. The completed trace preorder, ctr , is defined by p ctr q iff T (q) ⊆ T (p) and CT (q) ⊆ CT (p).

To adapt the notion of the completed trace preorder we need to take completed traces as those that can do no more non-time passing actions (since time can always pass, we'd otherwise have no completed traces). Hence we define: Definition 14 σ is a completed timed trace of a process p if ∃ q • p σ -→ q and q tr -→ implies tr ∈ {Op τ } * . CT t (p) denotes the set of completed timed traces of p. The completed timed trace preorder, t-ctr , is defined by p t-ctr q iff T t (q) ⊆ T t (p) and CT t (q) ⊆ CT t (p).

2

The basic relational embedding without time uses a global state that has been augmented with an additional element √ , which denotes that the given trace is complete (i.e., no operation is applicable). Thus it uses the finalisation:

Fin == {State • θState → * } ∪ {State | (∀ i : J • ¬ pre Op i ) • θState → √ }
We have to adapt in a similar fashion in the presence of time, in particular, amend the finalisation so that we correctly record our completed timed traces. We thus change the global state to R + × { * , √ } and set

Fin == {s : State • s → (s.t, * )} ∪{State | (∀ i : I ; τ : R + • ¬ pre(Op τ o 9 Op i )) • θState → (θState.t, √ )}
The effect on the downward simulation finalisation condition is that it becomes:

∀ AState; CState • R ∧ ∀ i : I ; l τ : R + • ¬ pre(COp τ o 9 COp i ) ⇒ ∀ i : I ; τ : R + • ¬ pre(AOp τ o 9 AOp i ) For an upward simulation, CFin ⊆ T o 9 AFin becomes ∀ CState • (∀ i : I ; τ : R + • ¬ pre(COp τ o 9 COp i )) ⇒ ∃ AState • T ∧ ∀ i : I ; tau : R + • ¬ pre(AOp τ o
9 AOp i ) Furthermore, if one makes the additional assumption of constancy of offers, then these reduce to the untimed conditions [START_REF] Derrick | Relational concurrent refinement: Automata[END_REF], namely:

Downward simulations: R o 9 CFin ⊆ AFin is equivalent to ∀ AState; CState • R ∧ ∀ i : J • ¬ pre COp i ⇒ ∀ i : J • ¬ pre AOp i Upward simulations: CFin ⊆ T o 9 AFin is equivalent to ∀ CState • ∀ i : J • ¬ pre COp i ⇒ ∃ AState • T ∧ ∀ i : J • ¬ pre AOp i
Those conditions, together with the above for non-time passing actions: R ∧ pre COp i ⇒ pre AOp i then give the required timed simulations for completed timed trace preorder.

Timed failure preorder Timed traces, as defined above, consist of traces where elements are either atomic or time passing actions. Our timed failures will be timed trace-refusals pairs, where refusals will be sets of actions which can be refused at the end of a trace. We thus use the following definition.

Definition 15 (σ, X ) ∈ (t-Act) * × P(Act) is a timed failure of a process p if there is a process q such that p σ -→ q, and next(q) ∩ X = ∅. F t (p) denotes the set of timed failures of p. The timed failures preorder, t-f , is defined by p t-f q iff F t (q) ⊆ F t (p).

Example 5. The timed automata corresponding to Q = (WAIT 2; a → stop) is a timed trace refinement, but not a timed failure refinement, of that corresponding to P = (a → stop). That is, P t-tr Q but P t-f Q.

The timed failures of P include ( d , ∅) for any time d , ( d 1 , a, d 2 , {a}) for any times d 1 , d 2 . Those of Q include ( 1 , {a}) and ( d 1 , a, d 2 , {a}) for any d 2 and any d 1 ≥ 2. Thus ( 1 , {a}) ∈ F t (Q) but this is not a failure of P . For the converse since we do not have timed trace refinement we cannot have timed failure refinement, for example, ( 0.5, a , ∅) ∈ F t (P ) but this is not a failure of Q.

2

Since we have no timelocks, we have defined the timed refusals to be a subset of P(Act). We can adapt the relational embedding in the obvious way, and extracting the simulations we get those of the timed trace preorder (see Section 4.2 above) plus those due to the finalisation conditions:

Downward simulations: R o 9 CFin ⊆ AFin is equivalent to ∀ i : I • ∀ AState; CState • R ∧ pre AOp i ⇒ pre COp i Upward simulations: CFin ⊆ T o 9 AFin is equivalent to ∀ CState • ∃ AState • ∀ i : I • T ∧ (pre AOp i ⇒ pre COp i )
However, note that the quantification over the state includes quantification over t, the variable representing time. Example 6. Figure 4 represents (the principle parts of) a retrieve relation between the states of two systems. With this retrieve relation it is easy to see that B is a timedfailure downward simulation of A.

Discussion

In this paper we have discussed how time might be modelled relationally, and thus derived simulations for relational embeddings of a number of refinement preorders found in timed process algebras. Following the basic methodology defined above one can define further embeddings and preorders. For example, we can define a timed failure trace preorder which considers refusal sets not only at the end of a timed trace, but also between each action in a timed trace, and adapting the appropriate definitions is straightforward.

The timed failure preorder defined above determines the refusals at the end of a trace, in a fashion similar to the definition of refusal sets for an untimed automata or the failures preorder in CSP. This is in contrast to a number of failures models given for timed CSP, where refusals are determined throughout the trace rather than simply at the end. Thus these models are closer to a timed failure trace semantics as opposed to a timed failure semantics. The need to do this arises largely due to the treatment of internal events and, specifically, their urgency due to maximal progress under hiding.

There are a number of variants of these models, perhaps reflecting the fact that the presence of time has some subtle interactions with the underlying process algebra. They include the infinite timed failures model discussed in [START_REF] Schneider | Concurrent and Real Time Systems: The CSP Approach[END_REF][START_REF] Mislove | Fixed points without completeness[END_REF], which as the name suggests includes infinite traces in its semantics, as well as the timed failures-stability model of Reed and Roscoe [START_REF] Reed | The timed failures-stability model for CSP[END_REF]. A number of different models are developed in [START_REF] Reed | A timed model for communicating sequential processes[END_REF][START_REF] Reed | A timed model for communicating sequential processes[END_REF][START_REF] Reed | The timed failures-stability model for CSP[END_REF], and a hierarchy described in [START_REF] Reed | A uniform mathematical theory for real-time distributed computing[END_REF].

The common aspect of these models is that refusals are recorded throughout the trace rather than just at the end. Thus, for example, considering P , Q and R defined by:

P = a → stop Q = b → stop R = c → stop
In untimed CSP we have

P (Q2R) = (P Q)2(P R)
Furthermore, in a timed setting using the timed failure preorder defined in Section 4.2 this equivalence still holds. For example, the timed failures of both sides of this equivalence include ( 1, b , {a, b, c}), reflecting an execution where 1 time unit passes followed by the occurrence of b, and afterwards all events are refused. However, if refusals are recorded throughout the trace, then these for the RHS include ( 1, b , [0, 1) × {c}), whereas those of the process on the LHS do not -this refusal representing an execution where c was refused over the time interval [0, 1) and b occurred at time 1.

Indeed, using the timed failure preorder defined in Section 4.2, the above law of untimed CSP still remains valid, but this does not hold in any of the timed failuresstability models nor the infinite timed failures model [START_REF] Schneider | Concurrent and Real Time Systems: The CSP Approach[END_REF][START_REF] Mislove | Fixed points without completeness[END_REF]. The infinite timed failures model of Schneider et al [START_REF] Schneider | Concurrent and Real Time Systems: The CSP Approach[END_REF][START_REF] Mislove | Fixed points without completeness[END_REF] differs in two respects from the model in Section 4.2, namely the inclusion of infinite traces and the refusal information throughout the trace. The inclusion of infinite traces means that a better treatment can be given to divergence. Specifically, in a timed analysis a more precise treatment of an infinite sequence of internal events can be given, since an such an infinite sequence of internal events can now be classified as either: a timed divergence if they all occur at one instant in time; a Zeno divergence if they approach some finite time; or as a well-timed sequence if they take for ever for the whole sequence to occur [START_REF] Schneider | Concurrent and Real Time Systems: The CSP Approach[END_REF]. Further, in timed CSP the first two possibilities are excluded from their notion of a well-timed process, thus nothing in timed CSP requires a treatment of divergence in the way that is necessary in untimed CSP.

The understanding of a failure (tr , X ) in the infinite timed failures model is that after the trace tr the execution will eventually reach a point after which all events can be refused for the remainder of the execution. Even without consideration of refusals throughout the trace, this differs slightly from the model in Section 4.2, because there our traces observed the passing of time, and we do not need to say that the execution will eventually reach a point . . ., since the quantification of 'eventually' is part of our timed traces. This model thus embeds the notion of constancy of offers since it requires that it will be possible to associate a timed refusal set of the form [t, ∞) × X with the execution. This restriction is not present in the model of Section 4.2 allowing time to change the events on offer.

It is argued in [START_REF] Schneider | Concurrent and Real Time Systems: The CSP Approach[END_REF] that the inclusion of infinite traces in a timed failures model provides a more uniform treatment of unstable processes in the context of relating untimed and timed models of CSP, and indeed it allows a refinement theory (called timewise refinement [START_REF] Schneider | Timewise refinement for communicating processes[END_REF][START_REF] Schneider | Timewise refinement for communicating processes[END_REF]) to formally link the two models.

The alternative approaches use stability values, which denote the time by which any internal activity (including time) following the end of a trace must have ceased. Thus, the timed failures-stability model of Reed and Roscoe consists of triples (tr , X , α), where α is the stability. The use of stability can be seen in the following three processes: → denotes a delay of 3 time units before control passing to the subsequent process, and wait 1 delays 1 time unit before terminating successfully. Then (see [START_REF] Schneider | Concurrent and Real Time Systems: The CSP Approach[END_REF]) these three processes have identical timed failures but can be distinguished by different stability values. For example, P has ( (1, a) , [0, 3) × {b}, 1) as a behaviour, whereas Q has ( (1, a) , [0, 3) × {b}, 4) and R ( (1, a) , [0, 3) × {b}, ∞). Further details of stability values and how they are calculated are given in [START_REF] Reed | The timed failures-stability model for CSP[END_REF].

P = a → stop Q = b
The need for refusals to be recorded during a trace in the above models arises from the urgency of internal events upon hiding in timed CSP. That arises ultimately from the consideration of the system/environment interface and the subsequent notion of maximal progress: that events occur when all participants are willing to engage in it. In the case of internal events, since the environment does not participate in them, they must occur when they become available. Now when an internal event occurs due to hiding, for example, as in the CSP process P = (a → stop) \ {a}, the maximal progress condition implies such an internal event is urgent, that is, it occurs at the instance it becomes enabled.

One consequence of this urgency is that it forces negative premises in the transition rules for the hiding operator in timed CSP, specifically, time can only pass in P \ A if no event from A is enabled in P .

This urgency also means we need more refusal information in order to maintain a compositional semantics. Reed and Roscoe give a number of examples of why hiding, urgency and a compositional semantics needs refusal information throughout the trace. One such example is the process ((a → stop) (wait 1; b → stop)) \ {a}. The urgency of the internal event upon hiding a means the non-deterministic choice is resolved in favour of a → stop and thus b cannot occur in a trace of this process. However, (1, b) is a trace of the process before hiding, meaning that more information is needed to regain compositionality. Further examples and discussion are given in [START_REF] Reed | The timed failures-stability model for CSP[END_REF].

However, in the context in which we began this discussion, namely a timed automata model, these issues are less relevant. Specifically, although a timed automata model can have internal events, a hiding operator is not defined, and therefore internal events do not have to be urgent. Furthermore, not all process algebraic models include urgency or maximal progress (see discussion in [START_REF] Nicollin | An overview and synthesis on timed process algebras[END_REF]). Additionally, one could argue that the urgency of internal events upon hiding is not entirely consistent with the informal semantics of untimed CSP. In particular, in untimed CSP the emphasis is on hidden events eventually occurring instantly: "a process exercises complete control over its internal events. ... [they] should not be delayed indefinitely once they are enabled" [START_REF] Schneider | Concurrent and Real Time Systems: The CSP Approach[END_REF].

Definition 8 (

 8 Labelled Transition Systems (LTSs)) A labelled transition system is a tuple L = (States, Act, T , Init) where States is a nonempty set of states, Init ⊆ States is the set of initial states, Act is a set of actions, and T ⊆ States × Act × States is a transition relation. The components of L are also accessed as states(L) = States and init(L) = Init. 2

1 →

 1 b → stop. A timeout can be modelled by allowing a state-change

Fig. 1 .

 1 Fig. 1. Simple timed specifications

Fig. 2 . 2 .

 22 Fig. 2. A timeout

Example 4 .

 4

Figure 3 augments

 3 Figure 1 by the representation of the retrieve relation between the states of the two systems. With this retrieve relation it is easy to see that B is a timed-trace downward simulation of A. However, the reverse implication would not hold since pre AOp i ⇒ pre BOp i fails to hold at the state right after a in B . In a similar fashion the timed automaton

Fig. 3 .

 3 Fig. 3. A retrieve relation between timed specifications

Fig. 4 .

 4 Fig. 4. A retrieve relation verifying a timed failure refinement

3 →

 3 stop R = c → loop where loop = wait1; loop

Here

3

 3

  Definition 3 (Data refinement)For data types A and C, C refines A, denoted A data C (dropping the subscript if the context is clear), iff for each program p over J , p C ⊆ p A .2

Definition 2 (Program) For a data type D = (State, Init, {Op i } i∈J , Fin) a program is a sequence over J. The meaning of a program p over D is denoted by p D , and defined as follows. If p = p 1 , ..., p n then p D = Init o 9 Op p1 o 9 ... o 9 Op pn o 9 Fin. 2