HASL: An Expressive Language for Statistical Verification of Stochastic Models
The authors 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.