CSLTA is a stochastic logic which is able to express properties on the behavior of a CTMC, in particular in terms of the possible executions of the CTMC (like the probability that the set of paths that exhibits a certain behavior is above/below a certain threshold). This paper presents the new version of the the stochastic model checker MC4CSLTA, which verifies CSLTA formulas against a Continuous Time Markov Chain, possibly expressed as a Generalized Stochastic Petri Net. With respect to the first version of the model checker presented in, version 2 features a totally new solution algorithm, which is able to verify complex, nested formulas based on the timed automaton, while, at the same time, is capable of reaching a time and space complexity similar to that of the CSL model checkers when the automaton specifies a neXt or an Until formulas. In particular, the goal of this paper is to present a new way of generating the MRP, which, together with the new MRP solution method presented in provides the two cornerstone results which are at the basis of the current version. The model checker has been evaluated and validated against PRISM (for whose CSLTA formulas which can be expressed in CSL) and against the statistical model checker Cosmos (for all types of formulas).
Improving and Assessing the Efficiency of the MC4CSLTA Model Checker
AMPARORE, ELVIO GILBERTO;Donatelli, Susanna
2013-01-01
Abstract
CSLTA is a stochastic logic which is able to express properties on the behavior of a CTMC, in particular in terms of the possible executions of the CTMC (like the probability that the set of paths that exhibits a certain behavior is above/below a certain threshold). This paper presents the new version of the the stochastic model checker MC4CSLTA, which verifies CSLTA formulas against a Continuous Time Markov Chain, possibly expressed as a Generalized Stochastic Petri Net. With respect to the first version of the model checker presented in, version 2 features a totally new solution algorithm, which is able to verify complex, nested formulas based on the timed automaton, while, at the same time, is capable of reaching a time and space complexity similar to that of the CSL model checkers when the automaton specifies a neXt or an Until formulas. In particular, the goal of this paper is to present a new way of generating the MRP, which, together with the new MRP solution method presented in provides the two cornerstone results which are at the basis of the current version. The model checker has been evaluated and validated against PRISM (for whose CSLTA formulas which can be expressed in CSL) and against the statistical model checker Cosmos (for all types of formulas).File | Dimensione | Formato | |
---|---|---|---|
Amparore-Donatelli-EPEW2013.pdf
Accesso aperto
Descrizione: Articolo principale
Tipo di file:
POSTPRINT (VERSIONE FINALE DELL’AUTORE)
Dimensione
1.58 MB
Formato
Adobe PDF
|
1.58 MB | Adobe PDF | Visualizza/Apri |
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.