Compositional Representation and Reduction of Stochastic Labelled Transition Systems based on Decision Node BDDs.
Markus Siegle · 1999
Compact symbolic representations of large labelled transition systems, based on binary decision diagrams (BDD), are discussed. Extensions of BDDs are considered, in order to represent stochastic transition systems for performability analysis. We introduce Decision Node BDDs, a novel stochastic extension of BDDs which preserves the structure and properties of purely functional BDDs. It is shown how parallel composition of components can be performed in this context, without leading to state space explosion. Furthermore, we discuss state space reduction by Markovian bisimulation, also entirely based on symbolic techniques. Together, parallel composition and state space reduction enable a compositional approach to the stochastic modelling of concurrent systems. 1 Introduction In many areas of system design and analysis, there is the problem of generating, manipulating and analysing large state spaces, usually represented in the form of labelled transition systems (LTS). Such transition ...