Reachable state space generation for structured models which use functional transitions

Afonso Sales 1 Brigitte Plateau 1
1 MESCAL - Middleware efficiently scalable
Inria Grenoble - Rhône-Alpes, LIG - Laboratoire d'Informatique de Grenoble
Abstract : This paper presents a new approach to obtain the reachable state space (RSS) of a structured model which uses functional transitions. We use multi-valued decision diagrams (MDD) to store sets of reachable spaces and stochastic automata networks (SAN) formalism to describe structured models. We focus our contribution in the proposal of a method to generate a compact MDD description taking advantage of the modular structure of SAN formalism, which also allows to represent the transition rate matrix of a continuous-time Markov chain by means of a sum of generalized Kronecker products. The method is tested on some models and the conclusion presents future work.
Document type :
Conference papers
Complete list of metadatas
https://hal.inria.fr/hal-00788913
Contributor : Arnaud Legrand <>
Submitted on : Friday, February 15, 2013 - 1:46:20 PM
Last modification on : Thursday, October 11, 2018 - 8:48:02 AM

Identifiers

Collections

INRIA | UGA | TDS-MACS | LIG | LIG_SRCPR

Citation

Afonso Sales, Brigitte Plateau. Reachable state space generation for structured models which use functional transitions. Proceedings of the 6th International Conference on the Quantitative Evaluation of Systems (QEST'09), 2009, Budapest, Hungary. pp.269-278, ⟨10.1109/QEST.2009.29⟩. ⟨hal-00788913⟩

Export

BibTeX TEI DC DCterms EndNote

Share

Metrics

Record views

188

Contact


archive-ouverte@inria.fr