IDD-MC is a symbolic analysis tool for bounded stochastic Petri nets with extended arcs. Its engine is based on Interval Decision Diagrams and facilitate the validation of standard Petri net properties, model checking the Computation Tree Logic (CTL) and the Stochastic Continuous Logic (CSL). In this paper we give an informal overview of the currently implemented analysis techniques and report on the most recent extension: the evaluation of rewards. We present some experimental results which show the e ciency of our implementation.
Stochastic Petri Nets (SPN) are an established formalism for the modeling and analysis of systems, among them biological networks [GHL07,HGD08,HDG09]. Assuming bounded Petri nets, interesting qualitative properties as reversibility and liveness can be determined by applying graph theoretic methods to the reachability graph. Although the complexity of these methods is linear in the size of the reachability graph, its size can grow over exponentially [PW03]. This calls for dedicated techniques as partial order reduction or symbolic state space representation. Here we consider techniques based on an e cient state space encoding using Interval Decision Diagrams (IDD), a generalization of Binary Decision Diagrams (BDD).
In a biological setting tokens often represent molecules or concentration levels. Thus the state space explosion is caused both by concurrency and by a high boundedness degree. The use of IDDs addresses especially the latter issue.
The quantitative semantics of a stochastic Petri net is described by a Continuous time Markov Chain (CTMC). Assuming a net without parallel transitions, the associated CTMC is a graph isomorphic to the reachability graph, but arcs are labeled by ring rates, given by the possibly state-dependent rate functions of the Petri net transitions. In general the rates are given by a sparse matrix indexed by the reachable states. CTMC theory o ers a variety of numerical methods for an exhaustive analysis [Ste94]. But in practice either an in nite or a hugh state space of the investigated models are often a very strict limitation. In these cases simulative or approximative methods represent possible alternatives [HRSS10]. However, certain properties or the demand for a high accuracy of the results require an exhaustive exploration, which in turn calls for an e cient representation of the CTMC and the adaption of the established algorithms. So did we by implementing our SPN analysis engine in IDD-MC which we will present in the next sections. 2
There are several tools which o er similar functionality as IDD-MC as for instance the probabilistic model checker PRISM [HKNP06], the SMART tool [CJMS06], Mobius [GKL+09] or GreatSPN [BBC+09] . The most similarities exist regarding to PRISM. Its symbolic engine is based on Multi Terminal Binary Decision Diagrams (MTBDD) which turn out to be not the best solution when dealing with biological networks [SH09] and thus inspired the implementation of IDD-MC's stochastic analysis features. 3
IDD-MC IDD-MC is a tool for symbolic state space based analysis; rst for bounded Petri nets with extended arcs, recently also for bounded stochastic Petri nets. The symbolic engine is based on Reduced Ordered Interval Decision Diagrams (ROIDDs), IDDs for short, which represent a canonical representation for interval logic functions used to encode sets of states (markings) of bounded Petri nets; see [Tov08] for a detailed discussion. It o ers a very e cient implementation of IDDs and related operations, among them dedicated operations for the ring of Petri net transitions. 3.1
Upon this IDD engine the following qualitative analysis features have been realized:
E cient state space generation. Three state space generation algorithms have been implemented; common breath- rst-search, transition-chaining and saturation. The latter algorithm is highly e cient concerning runtime and memory consumption by exploiting the locality of transition ring.
Basic Petri net properties. The tool allows to check for reversibility and liveness of transitions. Therefor e cient decomposition of the strongly connected components has been implemented.
CTL model checking. Given a bounded Petri net N and a Computation Tree Logic (CTL) formula ' (see [CGP01] for an introduction), the model checking problem is to decide whether ' holds in the initial state of N . The classical CTL model checking algorithm [CES86] can be adapted to solve the problem using a symbolic representation of the reachable states of N . It determines for each subformula of ' the set of states ful lling starting from the innermost formulas. Then it proceeds such that when processing a formula, the set of fullling states have been determined for all its subformulas. A CTL subformula can either be a state formula or a path formula containing a temporal operator. While a state formula can be evaluated locally in a state, a path formula requires to evaluate the paths starting in a state. In a symbolic setting this can be solved by xpoint computations. The top-formula ' is true if the initial state is contained in its associated set.
In addition to qualitative analysis of bounded Petri nets IDD-MC o ers the following quantitative analysis techniques for bounded stochastic Petri nets:
Transient analysis. Transient analysis is the computation of the probability distribution at a certain time point starting with a certain initial probability distribution. One of the standard techniques is uniformization. The basic idea is to embed a special discretization of the CTMC into a Poisson process which has the same probability distribution at time . Its computation reduces to truncate an in nite sum of matrix-vector multiplications. For a detailed description and further techniques see [Ste94]. IDD-MC realizes transient analysis by applying an on-the- y multiplication algorithm, which does not require an explicit encoding of the CTMC's rate matrix.
Steady State analysis. Continuous time Markov Chains often reach nally a stable probability distribution, which is called the steady state. It can be interpreted as the transient probability distribution for in nite time. Computing the steady state probabilities means to solve a linear system of equations. Iterative methods as Jacobi and Gauss-Seidel are the favored techniques. IDD-MC o ers Jacobi, Gauss-Seidel and Pseudo-Gauss-Seidel [Par02] solver based on our on-the- y multiplication.
CSL model checking. The qualitative analysis techniques, transient and steady state analysis are the needed ingredients to realize model checking of the Continuous Stochastic Logic (CSL) introduced in [ASSB00]. Beeing an stochastic adaption of CTL, the basic model checking procedure is similar. The evaluation of path formulas with time-bounded temporal operators can be achieved by applying transient analysis as proposed in [BHHK00] and implemented in our tool. In [BHHK00], CSL has been extended by a special steady state operator and temporal operators without time bounds. Untimed operators require to solve a linear system of equations based on the Embedded Markov Chain of the original CTMC applying one of the iterative methods. 3.2
E
ciency issues There are several aspects which are signi cant for the e cient implementation of the mentioned analysis techniques.
Variable order. It is well known that the variable order a ects the size of the decision diagram (DD) and thus has a signi cant impact on the runtime and memory consumption of the DD implementation. What this means in practice can be seen in [SH09]. IDD-MC uses heuristics [Noa99] based on the Petri net structure to compute static variable orders which produce small-sized DDs in most cases. Furthermore, the tool makes use of so-called Shared IDDs which means that several IDD-instances reference to the same set of IDD nodes. This allows, for instance, to check for equality in constant time.
CTMC representation. One of the most challenging problems with quantitative analysis of an SPN is the representation of the rate matrix of its induced CTMC. There are established symbolic techniques as MTBDDs or Kronecker products implemented in existing tools [MP04]. But these techniques may fail under special conditions. For instance, a MTBDD representation su ers from an high amount of distinct non-zero values in the matrix and from a high number of BDD variables caused by an high boundedness degree of the model [SH09].
IDD-MC's numerical engine is based on an on-the- y approach, which has also been considered for an explicit state space representation in [DSS97] and symbolically in [Sch08,SH09]. In our case the CTMC is represented by the Petri net structure, the reachable states encoded as an IDD, and the rate functions of the transitions. A multiplication of the matrix and a vector is realized by traversing the IDD for all transitions of the net. The traversation simulates the ring of all enabled transitions for all states. Therefor we consider the pre- and post conditions to compute the index of the source and target state and to collect the arguments for the possibly state-dependent rate functions. To achieve this, the IDD has been augmented with certain index informations; see [ST10] for more information. To prevent from unnecessary recomputations, we use the caching strategy from [Par02] adapted to our special settings. The multiplication operation multiply(StateSet S, TransitionSet T, Vector argument, Vector result) is implemented con gurable concerning the set of considered states S and transitions T . This allows, for instance, to parallelize a single multiplication given a suitable state space partition. In [HRSS10] we present results were we achieved a speedup close to the number of physical cores of current multi-core work stations. Recently we extended our tool by reward structures. In the next section we brie y sketch how to incorporate rewards and their analysis. 4
Rewards (also interpretable as costs) de ne additional measures for probabilistic models and can be associated to states and transitions. They are speci ed by possibly state-dependent reward functions. A reward for a state will be accumulated and weighted with the time the system remains in it. A transition reward is acquired each time a transition res.
Conform to the probabilistic model checker PRISM rewards can be added to a model by specifying a reward structure, a collection of state and transition reward items.
A state reward item consists of a guard de ning a set of states and the reward function. A transition reward item de nes for a certain Petri net transition a reward function. Additionally a guard may restrict the set of enabling states of the transition for which the reward should be considered.
Each state reward item de nes a vector which assignes to all states satisfying the associated guard the reward value computed using the reward function. Each transition reward item de nes a matrix where all entries representing a state transition caused be the associated Petri net transition and starting in states satisfying the guard. Each reward structure thus de nes a vector representing the sum of all reward vectors de ned by the state reward items and a transition reward matrix representing the sum of the reward matrices de ned by the transition reward items of the structure. These vectors and matrices are in the dimension of the reachable states and introduce the same problem as the representation of the CTMC. In PRISM reward structures are encoded by MTBDDs.
Since IDD-MC follows a matrix free strategy, we use our on-the- y multiplication to compute the rewards when needed. A reward item is represented by a set of states and an additional implicit Petri net transition. When adding a reward structure to a stochastic Petri net, the tool adds a new transition for each de ned reward item. For a state reward, the rate function of the new implicit transition is the reward function itself. For a transition reward the reward function multiplied by the rate function of the referenced Petri net transition becomes the rate function of the new implicit transition. This enables the computation of an entry-wise matrix product which is required by the analysis of transition rewards [KNP07].
For a state reward, the assigned set of states is the subset of the reachable states satisfying the speci ed guard. For a transition reward, the assigned set of states are the reachable enabling states of the referenced Petri net transition satisfying the speci ed guard. Pre- and post conditions of these new transitions are con gured in that way that the transition is enabled in every reachable state and its ring does not change the system state but allows to compute the reward.
For the analysis of a reward-augmented model we extend (again conform to PRISM) CSL by the special reward operator R and four new state formulas. Given a reward structure r, a real valued reward bound b and an operator ./2 f>; ; <; g we de ne the following formulas: 1. Rf\r"g./b[C t] The expected cumulative reward within the rst t time units is ./ than b. 2. Rf\r"g./b[I=t] The expected state reward at time t is ./ than b. 3. Rf\r"g./b[F ] The expected cumulated reward until the rst time a state is reached satisfying the state property is ./ than b. 4. Rf\r"g./b[S] The expected long-run average reward is ./ than b.
Because of the given space limitations we can not discuss the evaluation of all these formulas and refer to [KNP07]. However the basic step is to compute initially a single vector of reward values in the size of the state space. In the case of the cumulative operator C t, for instance, the vector represents the sum of the state reward vector and a vector containing the row sums of a matrix achieved by an entry-wise multiplication of the CTMC rate matrix and the matrix representing the transition rewards. This pre-computation step can be simply realized using our transition-based reward representation and our multiply operation.
To compute the state reward vector of a reward structure we apply the multiplication successively to all implicit transitions representing state reward items. The argument vector is initialized with 1 in every entry. Since transitions do not change the state by ring, this means to extract the elements of the diagonal of the matrix, belonging to rows de ned by a state set satisfying the guard. The computed rate of these implicit state transitions are the actual state rewards and are added to the result vector. Actually we are computing the row sums of a matrix where only one element per row is non-zero and add these sums to our result vector.
Obviuosly, we will not set the result vector to zero after a multiplication. We similarely compute the entries of transitions reward matrix just considering the transitions representing transition reward items.
For the mentioned case of the cumulative operator, we start o with a zero result vector and apply the multiplication sequentially for all implicit transitions de ned by the reward structure, state rewards as well transition rewards. 4.1
To demonstrate the e ciency of our tool we present some experimental results. We run IDD-MC and PRISM 3:3:1 on a 8 2:26 GHz MAC Pro with 32 GB RAM with eight physical cores (with hyper-threading 16 logical cores). We consider a stochastic Petri net model of the Mitogen activated protein kinase cascade (MAPK) [HF96]. The Petri net model has been created with our tool Snoopy [RMH10]. The PRISM model and the reward structure were taken from the PRISM case study suite. Snoopy implements an export mechanism to create PRISM models including the computation of the same static variable orders as IDD-MC. Thus we used for our experiments Snoopy also to create another model description in the PRISM language. The used CSL formula Rf\time"g=?[F(kpp = N )]1 was taken from [KNP08]. This formula requires the generation of the Embedded Markov Chain. To solve the linear system of equations we used the Jacobi method, the default in both tools. In our experiments we varied the number of tokens on certain places using parameter N of the scalable model, which comprises 22 places and 30 transitions. The number of reachable states represents the dimension of the rate matrix, the number of transitions represents the number of non-zero matrix entries. We used IDD-MC with one and with 16 threads.
The gures in Table 1 show that a good variable order reduces the analysis time signi cantly. Using all logical cores of our test system allows a speed up about factor seven. Except the very small state space for N = 2 and N = 4 IDD-MC outperforms PRISM for the given model and formula also without multi-threading, and using the same variable order. 5
We have presented IDD-MC, a symbolic tool for qualitative and quantitative analysis of bounded stochastic Petri nets. We summarized its main features, especially the analysis of reward structures. Experiments show that the tool 1 To use '=?' means to compute the reward for the initial state 2 4 6 8 10 states transitions
IDD-MC1 IDD-MC16
PRISMorg
PRISMgo 2,172 99,535 1,373,026 10,276,461 52,820,416 outperforms the PRISM model checker for the considered case study. We intend to support Generalized stochastic Petri nets (GSPN) and to realize out-of-core techniques. Furthermore there are several aspects for performance optimization as improving variable ordering and parallelization.