Modelling and veri cation of software systems is an e ective 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 speci cation 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 veri cation. We provide the recursive calculation of the language generated by an SRE, enhanced to reuse local results for global veri cation of system speci cations. Furthermore, we demonstrate how to model systems with SREs and how to perform reachability analysis with Probabilistic Action-based Computational Tree Logic (PACTL*).
The analysis of systems with a probabilistic behaviour plays an important role in several applications, such as software engineering, speech recognition, digital communications and computational biology among others. On the other hand, regular expressions have spread through all of theoretical computer science and enjoy plentiful applications in the eld of natural language processing, including parsing, deep language models, model inference and machine translation.
Several studies have been conducted in probabilistic version of regular
expressions that is studied as probabilistic concurrent Kleene algebra in [
Kartzow and Weidner [
In this paper, we de ne a semantics of stochastic regular expressions in the
context of probabilistic model checking, employing a probabilistic extension of
Action-based Computation Tree Logic (ACTL*) to reason about temporal
properties quantitatively. Probabilistic model checking [
Stochastic Regular Expressions (SRE)
In this section, we brie y recall SRE [
The syntax of a Stochastic Regular Expression (SRE) E over an alphabet de ned recursively as follows:
E :=
X Ei[ni] i
E1 : E2
E f with 2 [ f"g, ni 2 N0, f 2 [0; 1]
R and every term Ei is a SRE, such that: 1. Atomic Action : is an atomic action that belongs to the alphabet . 2. Choice Pi Ei[ni]: One of the provided terms Ei[ni] is probabilistically chosen according to calculated probabilities from occurence values. ni denotes the occurrence value or choice rate for each term, such that the i-th term is chosen with probability Pnjinj . Occurrence value or choice rate is de ned as the number of cases that the node is chosen statistically. 3. Concatenation E1 : E2: The terms E1 and E2 are successively interpreted. 4. Kleene Closure E f : The term E is repeated for an inde nite number of times, subject to a binomial distribution. Each iteration occurs with a probability of f . The termination probability is 1 f . 5. Plus Closure E+f : The +Closure is a syntactic sugar that is omitted here, but can be easily emulated with E : E f .
Without loss of generality, the empty string " is not included in the alphabet. However we include the empty string as an atomic action. On the other hand, can be derived from an expression like 0:0; 2 .
A derivation of a conventional regular expression E is the set of sentences, or strings over the alphabet, derivable from it. This de nes the language L(E) of E. This notion of language derivation is similarly applicable to SRE, except that each string has a probability value associated with it, and hence the language itself is associated with a probability distribution of its members as explained in the following within its denotational semantics. 2.2
Intuitively SREs can be understood as an expression that de nes a speci c
probability function over its language strings such that JEK : s 2 ! [0; 1]. Such
probabilistic language (p-language) is previously described for discrete events
systems in [
The semantics of SREs are described by the p-language [
Example 1. Let L be a probabilistic language [
In the following we formally de ne some additional notions which will be referred to throughout this paper.
De nition 1 (Words of a SRE). W ords(E) = fw j w 2 L(E)g De nition 2 (Word length). A length of a word w = w0w1:::wn is the number of included characters and denoted as jwj= n through the paper. De nition 3 (Probability of a word in the language). The probability function JEKs for every possible SRE term E ( j P Ei(ni) j E1 : E2 j E f j E+f ) is calculated recursively, where s = 1; :: n 2 : { Atomic actions: { Choice
J Ks = 1; if J Ks = 0; if 6= s
= s r X Einizs = X k
nk P ni
JEkKs (2) (3) Since every term might recognize s, the overall probability for a choice expression is the sum of all the term probabilities with respect to s. { Concatenation:
JE1 : E2Ks = n In the summation, s is decomposed into two (possibly empty) substrings, each of which may be consumed by a concatenated expression. Even though one term may recognize its substring argument, if the other term does not recognize its respective substring, then that term returns a probability of 0, and the overall probability for that instance of decomposition is 0. { Kleene closure:
J E f s =
K n X (f i=1
JEK 1:: i JE f K i+1:: n)
(4) J E f K" = 1
f +f JEKs J
E f "
K The rst formula accounts for empty strings, as the only way an iterated expression should recognize an empty string is by not iterating; in other words terminating without executing (The termination probability is therefore 1-f ). The other formula recursively de nes the general case. Here, one iteration of E will consume some portion of s, and the rest of s is consumed by further iterations. It is assumed that an iteration of a loop always consumes some non-empty string. Otherwise, the semantic model would have to account for Kleene closure iterating inde nitely on an argument, which is not an useful behaviour.
All SRE probability functions presented above are well formed probabilitity
functions. Interested readers can nd the details of probability functions and the
proof of well formness in [
Action based Computation Tree Logic (ACTL*)
ACTL* is introduced in [
We bie y recall the de nitions required for the ACTL* semantics.
De nition 4 (Labelled transition systems ). A labelled transition system is a tuple (S; Act; !) where: . S is a nite set of states . Act is a nite, non-empty set of actions . ! is the transition relation denoted in of ! is called a transition.
S (Act [ )
S and any element De nition 5. A sequence (s0; 0; s1)(s1; 1; s2):: 2 s0. A run = (s; ) is a pair from s 2 S, where of is s (f irst( ) = s) and path( ) = . If a run we denote as . ! 1 is called a path from is a path from s, rst state is a su x for run , then The semantics is given by satisfaction relations based on the de nitions above: j= T rue always j= :' i j= ' ^ '0 i 6j= '
j= ' and i there exists a run j= 9 j= U 0 i there exists a j= X ' i there exists s, , s0, j= Xa' i there exists s, s0, j= '0
such that 2 run(f irst( )) such that with such that
j= j= 0 and for all = (s; (s; ; s0)) and
j= ' such that = (s; (s; a; s0)) and j= ' (6) : j= 0 3
Semantics of Stochastic Regular Expression Trees with
Probabilistic Action based Computation Tree Logic
Our goal is to reason about temporal properties on SRE models probabilistically.
A very common logic Probabilistic computation tree logic (PCTL*) [
The extended syntax of a Probabilistic ACTL* (PACTL*) is de ned as follows where ' is a word and is a SRE formula.
De nition 6 (Syntax of PACTL*).
= : j ^ 0 j PP (') ' = true j Xa' j X ' j ' U '0 (7) (8) where P Every SRE term E is de ned as a node that speci es operation type (choice, concatenation, kleene closure or action), choice rate, kleene probability and subnode(s).
Formally E is an action or a tuple based on its type: (N ; R), (N ), (N ; k) if the opetaion types are choice, concatenation, kleene closure (T = + j:j or action a 2 ,) respectively. where N = fE1; E2; :::; Eng is the nite set of subnodes in the operating order (E1 : E2 6= E2 : E1), R = fr1; r2; ::rng is the set of corresponding choice rates (r 2 N) and k 2 [0; 1] is a kleene probability.
We construct every SRE node in a bottom up fashion by parsing the given string by using operator presedence. Hence, we avoid the ambiguity of the parsed trees and remain them unique. (The order of operator predence is ; :; +). We also restrict one operation type per SRE node which allows unambiguity.
The semantics is de ned a satisfaction relation for a word w and a SRE term E as follows:
E j= : E j=
i E 6j=
^ 0 i E j= ^ E j= 0
E j= PP (') i P rfw j= ' j w 2 W ords(E)g 2 P
w j= true always
w j= Xa' i w[0] = a and w[
jwj, w[i] j= '0 and w[j] j= ', 8j < i: The set of words for an SRE can be calculated recursively on SRE node E: 8 a ; >f g >>>> S W ords(Ei); W ords(E) = ><Ei2N >(W ords(E0) W ords(E1))::: W ords(En); 8Ei 2 N >>>>>S1 W ords(Esub)k; where Esub 2 N and E = (Esub) : k (9) (10) (11) (12) (13) (14) (15) if T = a if T = + if T =: if T = (16) A system is speci ed as an SRE tree that includes a root node and nite set of nodes. An SRE tree is formally de ned as; TE = (Eroot; E ; ), where Eroot is the root node, E is the nite set of all nodes and is the alphabet. Hence, verifying the the root node Eroot will result in verifying the system. 4
Example: System Speci cation with SRE Tree We provide an example automata and a corresponding SRE system speci cation in the following paragraphs. Let us assume that we have a system that is composed of some web services aiming to achieve a message protocol. The subcomponents Service 1(S1) and Service 2(S2) are executing the login of sytem and message sending and logging out from the system respectively. The system can be de ned as a stochastic regular expression tree as follows:
TE = (Eroot; E ; ) Eroot = S E = fS; S1; S2; E1; E2; E3; E4; E5; E6g
= fstart; login; authenticationF ail; logout; sendM sg;
msgF ail; terminate; success; retryg
S = S1 : S2
S1 = start : login
S2 = authenticationF ail[
E6 = success : retry
Let a PACTL* formula P[0:3;0:4] true U (XmsgFail)true for the analysis on TE . The formula indicates the reachability analysis of the action \msgFail" on the root node Eroot = S. The words reaching the \msgFail' from S are then recursively calculated: W ords(S)[reaching\msgFail"] W ords(S) = fstart:login:sendM sg:msgF ail (0:0325); start:login:sendM sg:succes:retry:msgF ail (0:008125); start:login:sendM sg:succes:retry:succes:retry:msgF ail (0:00203125); ::::g The union is then 0:0325 1 Y(0:25)i = 0:0325 2 [0:3; 0:4] i=0 S j= P[0:3;0:4] true U (XmsgFail)true (17) (18)
Visually, we provide the corresponding probabilistic automata in Figure 1.
The proof of equivalence between probabilistic Rabin automata [
SREs are calculated in a bottom up way by remaining the probabilistic calculations of strings. Such techique enables to reach every calculation on each node locally. The idea is to calculate all information on every SRE term and compose the solutions based on the operations.
Service1 1 5
Service2 We described a formal semantics for model checking of SREs that enjoys various applications in computer science. We studied the stochastic regular expressions with action based probabilistic logic in the model checking context and used stochastic regular expressions as an input model. Our initial attempt to reachability analysis with strings is also presented which is promising and convenient for parallel and incremental computation especially in the domain of component based systems or modular systems. The further investigation is to extend the reachibility analysis for the application of full PACTL* on SRE trees and evaluate our approach with set of models. Furthermore, we are planning to use SRE model checking for the incremental computation of local changes that can occur in the model.