Improving and Assessing the Efficiency of the MC4CSLTA Model Checker

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).