Activity-Local Symbolic State Graph Generation for High-Level Stochastic Models

摘要

We introduce a new, efficient method for constructing compact symbolic representations of very large stochastic labelled transition systems. Contrary to known symbolic state space generation techniques, our technique is applicable to general high-level models which do not have to possess any particular structure. The method is based on zero-suppressed binary decision diagrams which we extended to the multi- terminal case. The symbolic representation is obtained by evaluating the semantics of the high-level model. During this step of explicit state graph exploration one constructs a separate symbolic representation of all transition induced by the same activity in an on- the-fly fashion. The obtained "activity-local" structures are finally composed in order to obtain a compact symbolic representation of the state graph of the overall system. For the then required step of symbolic reachability analysis we propose a new, sequential and activity oriented scheme which leads to better run-times than conventional symbolic reachability computation. Comparing our new method to previously published schemes, the paper demonstrates the following advantages: (a) The approach is applicable to a general class of high-level stochastic models. (b) In partial-order style we avoid the explicit generation of shuffled sequences of independent activities, which results in much higher generation speed. (c)The composition scheme, as well as the new data structure, results in extremely compact symbolic representations. Furthermore, the composition scheme does not require any product-form of the models subunits to be composed, as in case of the Kronecker- based approaches. (d) The proposed variant of symbolic reachability analysis significantly reduces runtime, where other symbolic SG representation methods, e.g. like the ones implemented in the tools CASPA and PRSIM, may benefit from.