To search, Click below search items. |
| All Published Papers Search Service |
|
|
|
Title |
Implementation of Symbolic State Space Generator using Reduced Ordered Binary Decision Diagram based on SDES Description in PDETOOL Framework |
|
Author |
Reza Fathi, Mohammad Abdollahi Azgomi |
| Citation |
Vol. 13 No. 7 pp. 79-86 |
|
Abstract |
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. |
|
Keywords |
Symbolic state space generation; reduced ordered binary decision diagrams, state space explosion; SDES description; stochastic discrete event systems. |
|
URL |
