HASL: an expressive language for statistical verification of stochastic models. We introduce the Hybrid Automata Stochastic Logic (HASL), a new temporal logic formalism for the verification of discrete event stochastic processes (DESP). HASL employs Linear Hybrid Automata (LHA) as machineries to select prefixes of relevant execution paths of a DESP. The advantage with LHA is that rather elaborate information can be collected on-the-fly during path selection, providing the user with a powerful means to express sophisticated measures. A formula of HASL consists of an LHA and an expression Z referring to moments of path random variables. A simulation-based statistical engine is employed to obtain a confidence-interval estimate of the expected value of Z. In essence HASL provides a unifying verification framework where temporal reasoning is naturally blended with elaborate reward-based analysis. We illustrate the HASL approach by means of some examples and a discussion about its expressivity. We also provide empirical evidence obtained through Cosmos, a prototype software tool for HASL verification.

This software is also peer reviewed by journal TOMS.