Cosmos: a Statistical Model Checker for the Hybrid Automata Stochastic Logic

Cosmos is a statistical model checker for Hybrid Automata Stochastic Logic (HASL). HASL uses Linear Hybrid Automata (LHA), a generalization of Deterministic Timed Automata (DTA), to describe accepting execution paths of a Discrete Event Stochastic Process (DESP), a class of stochastic models which includes, but is not limited to, Markov chains. As a result, HASL verification turns out to be a unifying framework where sophisticated temporal reasoning is naturally blended with elaborate reward-based analysis. Cosmos takes as input a DESP (described in terms of a Generalized Stochastic Petri Net), a LHA and an expression Z representing the quantity to be estimated. It returns a confidence interval estimation of Z. Cosmos is written in C++ and is freely available to the research community. It is jointly developed by searchers of Inria, at LSV and LACL.