Symbolic state-space exploration and numerical analysis of state-sharing composed models

作     者：Derisavi, S Kemper, P Sanders, WH 

作者机构：Univ Illinois Coordinated Sci Lab Elect & Comp Engn Dept Urbana IL 61801 USA Univ Illinois Comp Sci Dept Urbana IL 61801 USA Univ Dortmund D-44221 Dortmund Germany 

出 版 物：《LINEAR ALGEBRA AND ITS APPLICATIONS》 (线性代数及其应用)

年 卷 期：2004年第386卷第0期

页      面：137-166页

核心收录：

学科分类：07[理学] 0701[理学-数学] 070101[理学-基础数学] 

主　　题：multi-valued decision diagrams Matrix diagrams numerical analysis symbolic state-space exploration 

摘      要：The complexity of stochastic models of real-world systems is usually managed by abstracting details and structuring models in a hierarchical manner. Systems are often built by replicating and joining subsystems, making possible the creation of a model structure that yields lumpable state spaces. This fact has been exploited to facilitate model-based numerical analysis. Likewise, recent results on model construction suggest that decision diagrams can be used to compactly represent large continuous time Markov chains (CTMCs). In this paper, we present an approach that combines and extends these two approaches. In particular, we propose methods that apply to hierarchically structured models with hierarchies based on sharing state variables. The hierarchy is constructed in a way that exposes structural symmetries in the constructed model, thus facilitating lumping. In addition, the methods allow one to derive a symbolic representation of the associated CTMC directly from the given model without the need to compute and store the overall state space or CTMC explicitly. The resulting representation of a generator matrix allows the analysis of large CTMCs in lumped form. The efficiency of the approach is demonstrated with the help of two example models. (C) 2004 Published by Elsevier Inc.