This demo paper presents MC4CSLTA, an efficient Markov chain Model Checker for (four) the stochastic logic CSLTA. In CSLTA formulas are either steady state queries or path formulas, where accepting paths are specified through a Deterministic Timed Automata (DTA). MC4CSLTA takes as input a labeled CTMC, a query, one or more DTA involved in the query (possibly expressed in parametric form), and computes the needed probability to assess the truth value of the formula. MC4CSLTA is written in C++, and is publicly available for the research community.
MC4CSLTA: An Efficient Model Checking Tool for CSLTA
AMPARORE, ELVIO GILBERTO;DONATELLI, Susanna
2010-01-01
Abstract
This demo paper presents MC4CSLTA, an efficient Markov chain Model Checker for (four) the stochastic logic CSLTA. In CSLTA formulas are either steady state queries or path formulas, where accepting paths are specified through a Deterministic Timed Automata (DTA). MC4CSLTA takes as input a labeled CTMC, a query, one or more DTA involved in the query (possibly expressed in parametric form), and computes the needed probability to assess the truth value of the formula. MC4CSLTA is written in C++, and is publicly available for the research community.
File in questo prodotto:
Non ci sono file associati a questo prodotto.
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
