View article

Modelling and verification of software systems is an effective phase of system development, as it can uncover failures in design early in the development process. There is an increasing need for languages and processes that allow for the specification of uncertainty that allow, for example, the modelling of the unknown behaviour of a user, or the stochastic failure rate of hardware components. In this paper we introduce a formal semantics on Stochastic Regular Expressions (SREs) over probabilistic action logics for quantitative verification. We provide the recursive calculation of the language generated by an SRE, enhanced to reuse local results for global verification of system specifications. Furthermore, we demonstrate how to model systems with SREs and how to perform reachability analysis with Probabilistic Action-based Computational Tree Logic (PACTL*).