HASL: an Expressive Language for Statistical Verification of Stochastic Models

Abstract

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