MC4CSLTA: An Efficient Model Checking Tool for CSLTA

This demo presents MC4CSL^TA, an efficient Markov chain Model Checker for (four) the stochastic logic CSL^TA. In CSL^TA formulas are either steady state queries or path formulas, where accepting paths are specified through a Deterministic Timed Automata (DTA). MC4CSL^TA 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. MC4CSL^TA is written in C++, and is publicly available for the research community.