|
Abstract : |
We present a new approach to the compact symbolic representation of stochastic transition systems, based on Decision Node BDDs, a novel stochastic extension of BDDs. Parallel composition of components can be performed on the basis of this new data structure. We also discuss symbolic state space reduction by Markovian bisimulation. In many areas of system design and analysis, there is the problem of generating, manipulating and analysing very large state spaces. We focus on stochastic labelled transition systems (SLTS) where each transition is labelled by an action name and an exponential delay. Such SLTSs (which originate, e.g., from Stochastic Process Algebra specifications [3]) can be interpreted as Markov chains and used for performability analysis. We propose a novel approach to SLTS representation and manipulation which is based on symbolic techniques. This is motivated by the fact that, in recent years, the problem of representing and analysing large state spaces has been very successfully approached by using Binary Decision Diagrams (BDD) [1]. This work took place in the context of formal verification and model checking, i.e. dealing exclusively with functional behaviour, disregarding temporal aspects. The success of symbolic techniques for functional analysis induced us to experiment with BDD-based representations of stochastic LTS. We introduce a novel data structure, Decision Node BDDs (DNBDD), which can capture not only functional, but also temporal (stochastic) information [4]. The idea is to employ binary encodings of states and transitions and store them in a canonical, graph-based format, a BDD. The information about transition rates is attached to a subset of the BDD nodes (the decision nodes) without modifying the basic structure of the BDD. Complex systems can be most conveniently specified as a number of interacting components. Using traditional representations, parallel composition of components leads to an exponential growth of the state space, since all possible in-, |
