期刊名称：International Journal of Computer Science and Network Security
印刷版ISSN：1738-7906
出版年度：2013
卷号：13
期号：7
页码：79-86
出版社：International Journal of Computer Science and Network Security
摘要：The main disadvantage of Model Checking is the state-explosion problem, which can occur if the system under verification has many processes or complex data structures. Although the state-explosion problem is inevitable in worst case, over the past 2 decades considerable progress has been made on the problem for certain classes of state-transition systems that occur often in practice. Using of Decision Diagrams to hold and manipulate the state space is an approach for this problem. In this approach the state space of the model is preserved in symbolic way instead of set. An algorithm is proposed in this paper for symbolic state space generation on SDES description models. Using SDES which is a multi-formalism description makes it possible to transform other stochastic discrete event system formalisms like Petri nets, stochastic activity networks, etc. to SDES formalism and then generate symbolic state space for them. Using symbolic state space generation by reduced ordered decision diagrams makes it possible to produce larger state spaces; which is used to producing state space of models in PDETool in order to alleviate its state space explosion problems.
关键词：Symbolic state space generation; reduced ordered binary decision diagrams; state space explosion; SDES description; stochastic discrete event systems.
