{'fraction_non_alphanumeric': 0.03743683282002213, 'fraction_numerical': 0.009269503334031037, 'mean_word_length': 4.373393316195373, 'pattern_counts': {'":': 0, '<': 1, '<?xml version=': 0, '>': 3, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 9, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
Symblicit Exploration and Elimination for Probabilistic Model Checking

Binary decision diagrams can compactly represent vast sets of states, mitigating the state space explosion problem in model checking. Probabilistic systems, however, require multi-terminal diagrams storing rational numbers. They are inefficient for models with many distinct probabilities and for iterative numeric algorithms like value iteration. In this paper, we present a new"symblicit"approach to checking Markov chains and related probabilistic models: We first generate a decision diagram that symbolically collects all reachable states and their predecessors. We then concretise states one-by-one into an explicit partial state space representation. Whenever all predecessors of a state have been concretised, we eliminate it from the explicit state space in a way that preserves all relevant probabilities and rewards. We thus keep few explicit states in memory at any time. Experiments show that very large models can be model-checked in this way with very low memory consumption.

standard approach is to proceed in two phases: First, explore the state space, building a representation of the set of reachable states and the transitions connecting them. Transitions are annotated with rational values for probabilities and rewards, which are usually represented as floating-point numbers. Second, use an iterative numeric algorithm such as value iteration [35] or one of its sound variants [5,21,29,36] to compute the quantity of interest. These algorithms in fact compute a value for every state that approximates the quantity starting from that state up to a prescribed error ǫ. In contrast to classic functional model checking, which admits on-the-fly algorithms for e.g. reachability or LTL properties, probabilistic model checking is thus doubly affected by the state space explosion problem: First, the entire state space must be stored in memory, including many numeric values. Second, the numeric computation requires multiple vectors of values to be stored, and updates to be performed on them, for all states.
Current approaches to mitigate the state space explosion problem in probabilistic model checking include the use of partial exploration and learning algorithms, bisimulation minimisation, and compact representations of the state space or value vectors by binary decision diagrams (BDDs). They exploit different structural properties that only sometimes overlap. The learning-based approaches [1,8] for reachability probabilities work well for models where a small initial subset of the state space determines most of the probability mass. In such cases, which are not abundant among existing case studies [23], they complete in a few seconds while exhaustive approaches run out of time or memory [11,Table 1]. Bisimulation minimisation reduces the state space to a quotient according to a probabilistic bisimulation relation; see [3,Sect. 5.1] for an overview. It has been implemented in Storm [15] and allows certain very large models to be checked efficiently; in general, its impact depends on the amount of bisimilar states in the given system. Finally, BDDs [9,33] have a long history of use in (discrete-state) model checking [12] to compactly represent state spaces, in good cases reducing memory usage by orders of magnitude. They work well when the state space is structured and exhibits symmetry, which is often the case for reallife case studies modelled by humans (as opposed to randomly generated examples). In probabilistic model checking, however, numeric values from continuous domains are part of state spaces and must be encoded in the decision diagrams. A binary encoding of their floating-point representation does not usually result in compact diagrams; instead, multi-terminal BDDs (MTBDDs), where each of the (unbounded number of) leaves represents one number, have been applied with some success, notably in the probabilistic model checker Prism [32]. They however do not provide much compaction for models with many distinct probabilities or reward values due to the large number of leaves. They also do not work well to represent the large vectors of values used in iterative numeric algorithms such as value iteration, which progress through many very different intermediate values for each state before converging to, but often not reaching, a fixpoint. For this reason, Prism defaults to its hybrid engine, which uses MTBDDs for the state space but arrays of double-precision values for iteration. Its fully symbolic mtbdd engine only solves specific large structured models in reasonable runtime.
Our contribution is a new approach that combines (MT)BDDs, explicit state representations, and state elimination to tackle the problem of model-checking large probabilistic specifications. Its novelty lies in (1) using BDDs precisely for those tasks that they work well for, and (2) using state elimination instead of the standard iterative algorithms in the computation phase. We work with discrete-state probabilistic systems; in this paper, we use DTMC to explain our approach, but the same techniques apply directly to CTMC, Markov decision processes (MDP) [35], and Markov automata (MA) [16], too.
Our state space exploration performs a standard explicit-state breadth-first search, but we use a decision diagram instead of the standard hashset to store the set of visited states. We do not store transitions, thus no continuous numeric values blow the diagram up. However, we do count the number of predecessors of each state-thus we use an MTBDD. Since this number is a discrete quantity with low variation in most models, the diagrams usually remain compact. For the computation phase, we explore the state space again, this time creating a representation that includes transitions, but that is explicit. During this exploration, we keep track of the number of explored predecessors of each state. Whenever, for some fully-explored state s, this number reaches the predecessor count given by the MTBDD, we apply state elimination: we remove s from the (yet incomplete) explicit state space representation, and replace all of its incoming and outgoing transitions by direct transitions between the predecessors and successors of s. By redistributing the original transitions' probabilities and rewards in the right way, the quantity of interest remains unaffected. This method of computation simultaneously avoids the iterative algorithms' convergence and precision issues [20] and keeps memory usage due to the explicit representation low: on most models, most states are eliminated soon after they have been fully explored, thus only few need to be kept in memory at any time. Upon termination, only the initial state and goal state(s) remain, and the value for the quantity of interest can be read off the transitions connecting them.
Two technical insights make our computation phase work well: First, we use an explicit representation not only to avoid storing (continuous) probabilities and rewards in an MTBDD, but also because state elimination tends to create unstructured intermediate state spaces that would blow up any BDD representation. Second, the precomputed predecessor count allows us to eliminate a state at precisely the moment after which we will not encounter it again in our search, avoiding costly re-explorations and re-eliminations.
Related work. State elimination stems from the classic reduction algorithm to convert a finite automaton into a regular expression [10]. It was introduced to probabilistic model checking to solve parametric Markov chains [13] and forms the core of the Param [25] and Prophesy [14] tools. For non-parametric models, it enables efficient computation of reward-bounded reachability probabilities [22]. In this paper, we use it for non-parametric Markov chains and unbounded (infinite-horizon) properties. In all of these settings, its effectiveness crucially depends on the order in which states are eliminated, which is determined by (configurable) heuristics. Symblicit techniques have previously been used for long-run average properties [38], based on bisimulation minimisation, and later expanded in related settings [7]. A different form of elimination on strongly-connected components was used by Gui et al. [19] to accelerate the (explicit-state) computation of reachability probabilities via value iteration.

Background
Mathematical notions. R + 0 is the set of all non-negative, and R + the set of all positive, real numbers. A (discrete) probability distribution over S is a function is the set of all probability distributions over S. We also write a transition as s p − → s ′ if p = P (s)(s ′ ) > 0. A transition is uniquely identified by the two states it connects. When in state s of a DTMC, we delay for one time unit before jumping to the next state. Continuous-time Markov chains (CTMC) extend DTMC by additionally assigning a rate Q(s) ∈ R + to every state. Then the probability to delay for at most t time units is 1 − e −Q(s)·t , i.e. the residence time follows the exponential distribution with rate Q(s). In both models, the probability to then move to state s ′ is given by P (s). When staying for t time units in state s, we incur a reward of R(s) · t. To simplify the presentation, we use DTMC throughout this paper, but mention the changes needed in definitions or algorithms to use CTMC, where appropriate. Example 1. As a running example, we use a very abstract model of the Zeroconf protocol [6], shown as DTMC M z in Fig. 1 (adapted from [18]). We draw transitions as arrows labelled with their probability. Non-zero rewards are given next to the states. M z has 7 states and 12 transitions. The protocol is used by hosts joining a network to auto-configure a unique IP address. A new host joining the network of h = 32 host starts in state i. It selects an address uniformly at random from the space of a = 2 8 addresses. The probability that the address is already in use is h a = 1 8 . The host checks n = 4 times whether its address is already in use. If it is not, all checks will succeed, modelled by state ok, to which we moved with probability 1 − h a . If it is, then states n down to 1 model the checks. Each check can fail to give the correct negative result due to message loss with probability p = 0.2. If all tests do so, then the host incorrectly believes that it has a unique address, in state ⊥. Otherwise, it retries with a newly chosen address from state i. We incur a reward of 1 in state i, i.e. for every IP address we try. The size of the DTMC can be blown up arbitrarily via parameter n.
In practice, higher-level modelling languages like Modest [24] or the Prism language [32] are used to specify larger DTMC. The semantics of a DTMC is formally captured by its paths: Definition 2. Given a DTMC M as above, a finite path is a sequence π fin = s 0 t 0 s 1 t 1 . . . s n of states s i ∈ S and delays . Π fin is the set of all finite paths starting in s I . A path is an analogous infinite sequence π, and Π are all paths starting in s I . We define s ∈ π ⇔ ∃ i : s = s i . Let π →m for m ∈ N be the prefix of π of length m, i.e. |π →m | = m, and let π →G be the shortest prefix of π that contains a state in G ⊆ S, or ⊥ if π contains no such state. Let rew(⊥) def = ∞.
In CTMC, the t i can be arbitrary numbers in R + 0 . For M as above, following the rules described below Definition 1 and the standard cylinder set construction [4], we obtain a probability measure P M on measurable sets of paths starting in s I . Definition 3. Given a set of goal states G ⊆ S, the reachability probability w.r.t. g is P(⋄ G) def = P M (π ∈ Π | ∃ g ∈ G : g ∈ π). Let r G : Π → R + 0 be the random variable defined by r G (π) = rew(π →G ). Then the expected reward to reach G is the expected value of r G under P M , written as E( G). Let r lra : Π → R + 0 be defined by r lra (π) = lim i→∞ rew(π →i )/dur(π →i ). Then the long-run average reward is the expected value of r lra under P M , written as L.
The steady-state probability S(S ′ ) of residing in a state in S ′ ⊆ S is a special case of the long-run average reward where R(s) = 1 if s ∈ S ′ and 0 otherwise. Whenever we consider a DTMC with a set of goal states G, we assume that they have been made absorbing, i.e. that for all g ∈ G we have P (g)(g) = 1. Given a CTMC, reachability probabilities and expected rewards can be computed on its embedded DTMC, obtained by dividing all rewards by Q(s); only for long-run averages do we need a dedicated treatment of the rates resp. residence times.
Example 2. For our Zeroconf example DTMC M z from Fig. 1, we may want to compute the probability to eventually pick a unique address P(⋄ { ok }), which will be just below 1, and the expected number of addresses that we ever try is ∞ by definition since the set of paths that never reach state ok has positive probability.

Binary Decision Diagrams
Binary decision diagrams (BDDs) [9,33] represent Boolean functions as rooted directed acyclic graphs. They have two leaf nodes, true and false. Every inner node is associated to one input bit, and has two children: the high (solid line) and low (dotted line) child. On a path from the root to a leaf, every bit must occur at most one. Such a path corresponds to the inputs in which bit b i is assigned to true (false) if we go from a node for b i to its high (low) child. We typically order the bits on all paths, merge isomorphic subgraphs, and remove redundant nodes. Then a BDD can represent many functions with few nodes.
In model checking, BDDs are used to represent sets of states (by assigning true to the binary encoding of a state iff it is in the set) as well as the transition relation (by assigning true to the binary encoding of a pair of states if they are connected by a transition). In probabilistic model checking, however, we need to encode functions that map to rational numbers to encode transition probabilities, rewards, and the value vectors in value iteration. Most tools represent them as 64-bit floating-point values, but the corresponding binary representation does not typically allow good compression with BDDs. Symbolic probabilistic model checkers such as Prism [32] this use multi-terminal BDDs (MTBDDs) with one leaf node per number. Since a finite model only contains finitely many probabilities, or values for states, this approach is effective, but often not efficient: for example, when performing value iteration on our example DTMC M z for P(⋄ { ok }), we have to encode the following function after 5 iterations: { i → 0.99225, 4 → 0.9716, 3 → 0.966, 2 → 0.938, 1 → 0.784, ok → 1, ⊥ → 0 } Observe that every state has a distinct value, thus the MTBDD offers no compression. In practice, they only work well for very specific models with few distinct transition probabilities and rewards, and where the iterative numeric algorithms assign the same (intermediate) values to many states.
Example 3. Fig. 2 shows an MTBDD mapping every state of M z to its number of predecessor states. We have 7 states, thus use 3 bits for their encoding. States 1 through 4 are encoded as that number, i is 5 (101 2 ), ok is 6 ((110 2 ), and ⊥ is 7 (111 2 ). There is no (reachable) state encoded as 0, thus we map 0 to the extra ⊥ leaf node-in this way, such an MTBDD can indicate that certain states are unreachable, or have not been explored yet. Observe that the MTBDD representation achieves some compression by excluding two redundant nodes for bit 2. If we scale the model up by increasing n, the compression would increase.

State Elimination
State elimination is a process by which a state of a DTMC is removed, i.e. transitions are modified such that it is no longer reachable from the initial state and it is removed from the state set S, in a way that preserves the values of all properties of interest. We show the schematic of state elimination in Fig. 3: we eliminate a state t by redistributing the probability to enter a self-loop onto its other outgoing transitions, then combine its incoming and outgoing transitions.
It is easy to see that this preserves the probabilities of all measurable sets of paths that pass through t when projecting t out from every path. In particular, the paths that forever take the self-loop have probability mass zero, which is why we could eliminate the loop. For rewards, the transformation only preserves the expected reward values of sets of paths: 1. In t, the expected number of times we take the self-loop is pc 1−pc , thus the expected reward from passing through t is rt·pc 1−pc (for the loop) plus r t (for taking one of the other outgoing transitions. 2. Out of s, the probability to enter t next is p a , thus we multiply the expected reward of passing through t by p a and add this to the reward of s. Alg. 1 shows the pseudocode to perform state elimination on a DTMC stored in explicit data structures (i.e. hash sets for states, lists of transitions, etc.).

Symblicit Exploration and Elimination
As we explained in Sect. 1 and illustrated in Sect. 2.2, many probabilistic models do not give rise to a compact BDD-based representation if the numeric valuesprobabilities, rewards, rates for CTMC-are included. Furthermore, the standard iterative numeric algorithms like value iteration usually produce data that is hardly BDD-compressible. In this section, we present a combined symbolicexplicit approach that uses MTBDDs in a way that usually avoids such problems, and that uses state elimination to calculate P, E, and L values without having to keep (values for all states of) the entire state space in memory.
The pseudocode of our approach is shown as function ExploreEliminate in Alg. 2. It uses functions Explore of Alg. 3 and Eliminate of Alg. 1. We typeset values that represent executable code in monospace font: compact specifications in high-level modelling languages are typically compiled to or interpreted as functions that, given an explicit (bit string) representation of a state, enumerate its transitions (P), compute its reward (R), and return true iff it is a goal state Our first step, in line 2, is to symbolically explore the set of reachable states by calling function Explore. This function performs a standard breadth-first search, using a BDD for the set of visited states, and additionally constructs an MTBDD that counts the number of predecessors of each state like the one shown in Fig. 2 for M z . In our implementation, seen and pre are actually managed in a single MTBDD as explained in Example 3.
We then, starting from line 3, perform another exploration of the state space. This time, however, we use explicit data structures, and we track the number of fully explored predecessors for every state in hash table pre ′ . A state is fully explored if its reward, all of its transitions, and all successor states, have been added to the explicit representations for S, R, and P . We track the set of fully explored states in hash set done. Whenever we are done visiting a state s in this second exploration (i.e. in line 13 and below), it has just become fully explored, and the fully-explored-predecessor count of its successors has changed. We then check which of these changed states fulfils the criteria for being eliminated: It must be fully explored (which only s is for certain), and all of its predecessors must be fully explored (which we determine by comparing pre ′ andp re). We call Eliminate on these states in line 17. In this way, if we indeed manage to eliminate most states soon after they have been explored, the explicit data structures-S, P , R, pre ′ , done, etc.-only track few states at any time and thus consume little memory. The predecessor count inp re is crucial for being able to perform efficient elimination; without it, we would have to apply heuristics that could lead to states being eliminated that would later be explored as successors of other states again, leading to costly re-exploration and re-eliminations. 1 function ExploreEliminate(sI , P, R, G) // explicit sI , executable P, R, G 2p re := Explore(sI , P) // get predecessor count MTBDD for all states if we compute a reachability probability then return g∈G P (sI)(g) 21 else if we compute an expected reward then 22 if spt (P (sI)) \ G = ∅ then return ∞ // we have P(⋄ G) < 1 23 else return R(si) + g∈G P (sI )(g) · R(g)

Alg. 2: Symblicit exploration-elimination for probabilities and expected rewards
In Eliminate, if a state is part of the set S keep , we still modify and "redirect" the transitions of its predecessors to go around this state, but we do not remove it from the state space. We use this to avoid eliminating the initial state s I . We also do not eliminate states whose only transition is a self-loop: they do not have successors to which transitions could be redirected. Elimination will thus eventually reduce each bottom strongly connected component (BSCC) of the DTMC to one such self-loop state. Since we assume all goal states to only have a self-loop, each of them is a BSCC. Once the outer loop of line 5 in ExploreEliminate finishes, Eliminate has been called for all states. Every surviving state at this point is thus the result of eliminating a number of transient states plus a nongoal BSCC or a goal state, and has become a direct successor of the initial state.  Sincep re tells us that i still has unexplored predecessors, we cannot eliminate, and next explore ok in step (2). We then eliminate ok-its only predecessor i is fully explored-but since ok has just a single self-loop, the elimination has no effect. In step (3), we have just explored state 4, which can now be eliminated. The result is shown as step (4). We proceed in the same pattern in steps (5) through (8). Then, in step (9), we fully explore state 1. Now all predecessors of i are fully explored, and we can eliminate both 1 and i. For the sake of illustration, let us pick the more complicated ordering and eliminate i first. The result is shown as step (10).
Since i is the initial state, we keep it, but redirect all incoming transitions. We also merge its rewards, which is why 1 now has a non-zero reward. Note that we show rationals in Fig. 4, but our implementation uses floating-point numbers. Remember that, withoutp re, we might have eliminated i too early; after any subsequent exploration of a state in { 1, . . . , n }, we would then have to re-eliminate i. We finally eliminate 1 in step (11) and explore state ⊥ in step (12). At this point, the outer loop terminates; we read P(⋄ { ok }) = 4375 4376 ≈ 0.999771 and E( { ok, ⊥ }) = 1 + 119918 119793 ≈ 2.001043. Observe that, at any time, we kept at most 4 explicit states in memory. We can arbitrarily increase the size of this model by increasing n, but will only ever need at most 4 states in memory.  Long-run average rewards. The algorithm we presented so far computed reachability probabilities and expected rewards. For long-run average reward properties, there are no goal states. In such a case, our state elimination procedure computes the recurrence reward for each BSCC [17].

Fig. 4. Example for exploration with interleaved elimination on Mz
To obtain the long-run average reward, we need to divide the recurrence reward for the rewards as given in the DTMC by the recurrence reward that we would obtain if all states had reward 1. We can do so by straightforwardly extending Algs. 1 and 2 to work on two reward structures r u and r l in parallel. Upon termination of the outer loop in ExploreEliminate, we then have one of the two situations described at the end of Sect. 4 in [17], and can again directly read off the value for our (L-)property. Consider Fig. 5: In the simpler case, the remaining model consists of the initial state s with a self-loop with probability one and r u = u s , r l = l s . In this case, the average value is u s ls . In the other case, the remaining model consists of the initial state s which has a probability of p i to move to one of the other n remaining states s i , i = 1, . . . , n, which all have a self-loop with probability one and r u (s i ) = u i , r l (s i ) = l i . In this case, the average value is i=1,...,n p i ui li . When computing long-run average rewards, the final value for L may be small, but the two recurrence rewards that we need to divide are often extremely large numbers beyond what can usefully be represented as 64-bit (i.e. doubleprecision) floating point numbers. We thus implemented a variant of our algorithm that uses the GNU MPFR library (see mpfr.org) for arbitrary-precision floating-point arithmetic, allowing us to use more than 64 bits. We did not find this to significantly affect the performance of the overall approach.
Alternatives and optimisations. So far, we have assumed that we compute successors for each state explicitly and individually. For the state elimination phase, doing so is indeed necessary. However, for just exploring the states we could also compute the transition relation as a BDD, and then use the transition relation to symbolically explore the set of reachable states. This is the standard approach in model checkers such as PRISM [32] and potentially faster than the semi-symbolic approach we have discussed. Also, using the transition relation and according MTBDD operations (in particular sum-abstraction), the number of predecessors of each state can also be computed symbolically.
We have so far assumed that the reachable states and the number of predecessors are stored as (MT)BDDs. An alternative to this approach is to store these numbers on secondary storage (e.g. hard disk) in a similar way as e.g. in [28]. This approach would be useful for models the state space of which is not suitable to be stored as a BDD. This might be the case because of lack of implicit symmetries or because the size of the representation of each state is not constant.

Experimental Evaluation
We have implemented a preliminary version of our method which we integrated as a plugin for the probabilistic model checker ePMC [26]. For the analysis, we transform the model and property into C++ code so as to have a means to quickly compute successors of states, similar to the approach used in SPIN [31]. This C++ file is then appended with code so as to achieve the following: In the first phase, we then explore the state space in a breadth-first manner where we explore each state explicitly but store sets of states as BDDs, using the BDD package CUDD [2]. In the second phase, we generate an MTBDD mapping all states to value 0. Then, we iterate over all reachable states, recompute their successors, and increment the value of these successors in the MTBDD by 1 each time. In the third phase, we execute the state elimination algorithm as discussed. This C++ code is then compiled and run in a process separate from ePMC, such that we can measure the memory usage exactly (the memory usage of ePMC itself is not of much interest, because it is rather small and about the same for any analysis).
In the following, we apply our tool on several case studies from the website of the probabilistic model checker PRISM. All experiments were performed on a MacBook Pro with a 2.7 GHz Quad-Core Intel Core i7 processor and 16 GB 2133 MHz LPDDR3 RAM. In the following tables, "model states" is the total number of states the model has for the given parameters, "result", is the value of the property computed, "time" is the total time of the analysis in seconds, "exp. states" ("exp. transitions") are maximal number of states (transitions) being stored explicitly at the same time. By "peak mem" we denote the maximal memory usage in MB of the analysis process.

Simple Molecular
Reactions: Na + Cl ↔ Na + + Cl − This case study 3 is a CTMC modelling the chemical reaction Na + Cl ↔ Na + + Cl − . The parameters of this case study are N1 , the initial number of Na molecules and N2 , the initial number of Cl molecules. In Table 1, we consider the performance figures for the analysis of R=?[S] which describes the expected long-run average number of Na molecules. Here, we consider a starting configuration in which initially the number of Na and Cl is the same, that is, As we see, the model scales well for large numbers of molecules and accordingly large state spaces. The memory usage grows only slowly with increasing model parameters, and the number of states and transitions required to be stored explicitly is constant.

Bounded Retransmission Protocol
The Bounded Retransmission Protocol [30] 4 is a file transmission protocol. Files are divided into N packages, each of which is transferred individually. Data and confirmation packages are sent over unreliable channels, such that they might get lost. Packages can only be resent a number of MAX times. In Table 2, we provide performance figures for the analysis of the property P=?[ F s=5 ], that is the probability that the sender does not eventually report a successful transmission. "N " and "MAX " are as discussed above, the other numbers are as in the previous case study.
Compared to the instances of the PRISM website, we have analysed instances with higher parameter numbers N and MAX because our focus was in the scalability of our method. For comparison, for the first table entry we used the same parameters as the last table entry on the PRISM website.
As we see, we are able to handle instances with several million states with a low memory usage. Even for higher parameter values for which the number of total states the model consists of is in the millions, we never use more than a few thousand explicit states and transitions and less than 100MB.

Wireless Communication Cell
This case study is a performance model of wireless communication cells [27] 5 . The parameter N describes the number of channels in a cell. We analyse the property R{"calls"}=? [ S ] which describes the average number of calls in the cell on the long run. We provide performance figures in Table 3.  Also for this case study, the approach works fine in that the number of states and transitions to be stored is small as is the peak memory usage.

Crowds Protocol
The Crowds protocol [37] 6 is a means to allow anonymous web browsing. To do so, messages are not directly sent, but forwarded to other users, who might either forward them again or send them to the destination. By doing so, it is hard for attackers to decide whether the sender of a message is the original sender or is just forwarding the message. The model version we consider has two parameters: TotalRuns is the number of routing paths of the model instance, and CrowdSize is the number of honest participants of the protocol. We consider the property Pmax=?[true U (new & runCount=0 & observe0 > observe1 & ... & observe0 > observe19)] which means that an attacker is eventually able to observe the true sender of a message more often than participants just forwarding the message and is thus able to guess the original sender. In Table 4 As we see, for this model the current implementation does not perform very well. The reason is that too many states and transitions have to be stored explicitly at the same time, leading to a large memory overhead.

Embedded Control System
This case study [34] 7 is an embedded control system which features a cyclic polling process. If a certain component detects that more than a given number MAX _COUNT of cycles have been skipped due to issues,then the system is shut down for safety reasons. We consider the property R{"danger"}=? [ F "down" ], which expresses the expected time the system is in an endangered state before it eventually has to be shut down. We provide performance figures in Table 5. Again, the analysis method works fine, as the number of states and transitions stored explicitly is limited.

Conclusion and Future Work
In this paper, we have discussed a new memory-efficient analysis method for properties of stochastic models. Our method is widely applicable to a large variety of stochastic models and properties, though, for conciseness of presentation we have concentrated on DTMCs (with some of the case studies being CTMCs). Experimental evidence has shown that our approach has the potential to analyse models with millions of states with just a few megabytes. One advantage of our method is that we directly obtain a precise result: Our current implementation is based on (variable-precision) floating-point numbers, and computation precision is limited by the properties of this representation. We could however as well use exact (rational) arithmetic and would obtain exact values without any change in the core algorithms, since all intermediate and final values are rational, though at the cost of increased computation time and memory usage. Alternatively, we could use interval arithmetic so as to obtain precise upper and lower bounds of the values computed, again, without any change in the algorithm, and with only moderate overhead. This is in contrast to methods based on value iteration or state-space abstraction, for which special precaution is required to ensure this. Our current implementation explores and eliminates states in a strict breadthfirst search order. Motivated by the problematic performance of the Crowds protocol case study, we also want to consider different search orders so as to improve the behaviour for models for which the strict breadth-first search order does not perform well.