arXiv:1507.05597v2 [cs.LO] 28 Oct 2015  Marimba: A Tool for Verifying Properties of Hidden Markov Models ⋆  No ́ e Hern ́ andez 1 , Kerstin Eder 3 , 4 , Evgeni Magid 3 , 4 , Jes ́ us Savage 2 , and David A. Rosenblueth 1  1   Instituto de Investigaciones en Matem ́ aticas Aplicadas y en Sistemas  2   Facultad de Ingenier ́ ıa Universidad Nacional Aut ́ onoma de M ́ exico, D.F., M ́ exico  no   hernan@ciencias.unam.mx, drosenbl@unam.mx, savage@servidor.unam.mx  3   Department of Computer Science, University of Bristol, Bristol, BS8 1UB, UK  4   Bristol Robotics Laboratory, Bristol, BS16 1QY, UK  Kerstin.Eder@bristol.ac.uk, Evgeni.Magid@bristol.ac.uk  Abstract.   The formal verification of properties of Hidden Markov Mod- els (HMMs) is highly desirable for gaining confidence in the correctness of the model and the corresponding system. A significant step towards HMM verification was the development by Zhang et al. of a family of logics for verifying HMMs, called POCTL*, and its model checking algo- rithm. As far as we know, the verification tool we present here is the first one based on Zhang et al.’s approach. As an example of its effective appli- cation, we verify properties of a handover task in the context of human- robot interaction. Our tool was implemented in   Haskell , and the ex- perimental evaluation was performed using the humanoid robot   Bert2 .  1   Introduction  A Hidden Markov Model (HMM) is an extension of a Discrete Time Markov Chain (DTMC) where the states of the model are hidden but the observations are visible. Typically, an HMM is studied with respect to the three basic problems examined by Rabiner in [9]. However, to the best of our knowledge, no practical model checker exists for HMMs despite their broad range of applications, e.g., speech recognition, DNA sequence analysis, text recognition and robot control. We describe in this paper a tool for verifying HMM properties written in the Probabilistic Observation Computational Tree Logic* (POCTL* [11]), and use this tool for verifying properties of a robot-to-human handover interaction. POCTL* is a specification language for HMM properties. It is a probabilistic version of CTL* where a set of observations is attached to the   next   operator. Zhang et al. [11] sketched two model checking algorithms for POCTL*, an “au- tomaton based” approach, and a “direct” approach. We opted for the direct  ⋆   The   final   version   of   this   paper   was   accepted   in   the   13th   Interna- tional   Symposium   on   Automated   Technology   for   Verification   and   Anal- ysis   (ATVA   2015).   The   final   publication   is   available   at   Springer   via  http://dx.doi.org/10.1007/978-3-319-24953-7_14
2   N. Hern ́ andez, K. Eder, E. Magid, J. Savage, and D. A. Rosenblueth  approach for its lower time complexity. Noticeably, this approach produces a DTMC   D   and a Linear Temporal Logic (LTL) formula   φ , so the   PRISM   [6] model checker could be used to verify this property. Such a model checker fol- lows the automata based approach whose complexity is doubly exponential in  | φ |   and polynomial in   |D| , whereas we implemented the direct method by Cour- coubetis et al. [1] whose complexity is singly exponential in   | φ |   and polynomial in   |D| , which is also the final complexity of our tool. This direct method repeat- edly constructs a DTMC and rewrites an LTL formula, such that one temporal operator is removed each time while preserving the probability of satisfaction. We have named our model checker   Marimba . A marimba is a xylophone-like musical instrument that is popular in south-east Mexico and Central America.  Marimba   [5] was implemented in   Haskell   and compiled with GHCi. Our tool is available for download from   https://github.com/nohernan/Marimba .  2   Tool architecture and implementation  Haskell   was chosen to code this first version of   Marimba   since it allows us to work in a high-level abstract layer, by providing useful mechanisms like lazy evaluation and a pure functional paradigm. Furthermore,   Haskell   manages recursion efficiently; this is a valuable aspect because recursive calls are made continuously throughout the execution. As a future work, we consider coding  Marimba   in a language like   Java   and make it a symbolic model checker.  Marimba   features a command-line interface. Furthermore, instead of work- ing with a command window, a more user friendly and preferable execution is accomplished through the   Emacs   text editor extended with the   Haskell-mode .  2.1   Marimba’s input and modules  The first input is a   .poctl   file with the six elements of an HMM   H , namely a finite set of states   S , a state transition probability matrix   A , a finite set of observations   Θ , an observation probability matrix   B , a function   L   that maps states to sets of atomic propositions from a set   AP H , and an initial probability distribution   π   over   S . The second input is a POCTL* state formula   Φ   typed in the command window according to the syntactic rules:  Φ   ::=   true   |   false   |   a   |   ( ¬ Φ )   |   ( Φ   ∨   Φ )   |   ( Φ   ∧   Φ )   |   ( P ⊲⊳ p ( φ )) , φ   ::=   Φ   |   ( ¬ φ )   |   ( φ   ∨   φ )   |   ( φ   ∧   φ )   |   ( X o φ )   |   ( φ   U ≤ n φ )   |   ( φ   U φ ) ,  where   a   ∈   AP H ,   o   ∈   Θ ,   n   ∈   N ,   p   ∈   [0 ,   1], and   ⊲⊳   ∈ {≤ , <,   ≥ , > } . In addition, we define   X Ω   φ   as a shorthand for   ∨  o ∈ Ω   X o φ   provided   Ω   ⊆   Θ . We examine below the six   Haskell   modules that constitute   Marimba .  ModelChecker.hs   performs the initial computations of the model checker for POCTL*. It recursively finds a most nested state subformula of   Φ , not being a propositional variable, and the states of   H   that satisfy it. On the one hand, finding the states satisfying a propositional subformula is straightforward. On
Marimba: A Tool for Verifying Properties of Hidden Markov Models   3  the other hand, we invoke the module   DirectApproach.hs   to obtain the states satisfying a probabilistic state subformula. Next, this module extends the labels of such states with a new atomic proposition   a . In   Φ , the state subformula being addressed is replaced by   a . The base case occurs when we reach a propositional variable, so we return the states that have it in their label.  DirectApproach.hs   transforms the HMM   H   into a DTMC   D , and removes from the specification the observation set attached to the   next   operator   X   by generating a conjunction of the observation-free   X   with a new propositional variable. Thus, we obtain an LTL formula that is passed, together with   D , to the module   Courcoubetis.hs . The new propositional variables are drawn from the power set of observations. Remarkably, it is not necessary to compute such a power set since the label of a state in   D   is easily calculated.  Courcoubetis.hs   implements a modified version of the method by Courcou- betis et al. to find the probability that an LTL formula is satisfied in a DTMC. In this module, when dealing with the   U   and   U ≤ n   operators, we apply ideas from [10] for computing a partition of states of   D . Moreover, to handle the   U  operator we have to solve a linear equation system. To that end, we use the  linearEqSolver   library [3], which in turn executes the   Z3   theorem prover [2].  Lexer.hs   and   Parser.hs   are in charge of the syntactic analysis of the input. Finally,   Main.hs   is loaded to start   Marimba . This module manages the interaction with the user, and starts the computation by passing control to   ModelChecker.hs . In a typical execution,   Marimba   prompts the user to enter a   .poctl   file path. Next, our tool asks whether or not the user wants to take into account the initial distribution in the computation of the probability of satisfaction. This choice corresponds to opposite ideas presented in [1] and [11], i.e., the method by Courcoubetis et al. uses the initial distribution to define their probability measure, contrary to that defined by Zhang et al. Afterwards, a POCTL* formula has to be entered.   Marimba   returns the list of states satisfying this formula, and asks the user whether there are more formulas to be verified on the same model. The   .poctl   file is simply a text file where the elements of an HMM are de- fined, e.g., the set of states is defined by the reserved word   States , and if the model consists of five states, we write   States=5 . Likewise, POCTL* formulas have a natural writing, for example,   P < 0 . 1 ( X { o 1   } a ) is typed as   P[<0.1](X_{1}a) .  3   Verification of a human-robot interaction  We applied   Marimba   to a real-world example, namely the verification of the robot-to-human handover task [4] using the robot   Bert2   [7] at the Bristol Robotics Laboratory (BRL). The robot’s decision to release the object during the handover task is determined by an HMM [4]. Figure 1 presents the state diagram of the HMM corresponding to the basic handover interaction, where the label   L ( s ) is defined for each state. Next, we initialise   A ,   B   and   π   of the HMM as follows. The process starts at state   Robot not hold , so its initial distribution value   π 1   is almost one, while the
4   N. Hern ́ andez, K. Eder, E. Magid, J. Savage, and D. A. Rosenblueth  other states have initial distribution values close to zero. The initial matrix   A  must encourage the transitions shown in Figure 1. To initialise   B , we consider  Robot not hold  State 1  L (1)= { rnh }  Robot pick up  State 2  L (2)= { rpu }  User grab  State 4  L (4)= { ug }  Robot hold  State 3  L (3)= { rh }  Fig. 1.   The labelled states in- volved in the basic handover process.  as observations the ordered pairs whose first and second components are the index and middle fin- ger metacarpophalangeal joint motor current val- ues, respectively. By the Cartesian product of these values, we obtain 56,404 observations. Since these observations are merged with the states to generate the DTMC passed to   Courcoubetis.hs , and the size of a formula could grow considerably by associating the   next   operator with up to 56,404 observations,  Marimba ’s execution is not practical under these circumstances. Vector quantisation [8] was used to reduce the number of observations to just 13, which were taken to initialise matrix   B . Thus, the initial ordered pairs are grouped into 13 regions of the plane representing the observations. To make reliable estimates, we collected observations from 50 handover ex- periments on   Bert2 . These observations were used to train the initial HMM with the reestimation method found in the solution of Rabiner’s Problem 3 [9].  Liveness properties.   A liveness property requires that a   good thing   happens during the execution of a system. For example, we would like to know whether  the model generates the sequence of observations   O   =   o 1 , o 2 , o 3 , o 4   where   o 1 , o 2   ∈ { 3 ,   4 ,   6 }   and   o 3 , o 4   ∈   { 3 ,   4 ,   11 } , with probability greater than 0.88 ,   that is,  P > 0 . 88 ( X { 3 , 4 , 6 } ( X { 3 , 4 , 6 } ( X { 3 , 4 , 11 } ( X { 3 , 4 , 11 } true )))). Interestingly, this property is a generalisation of Rabiner’s Problem 1 [9].   Marimba ’s execution for this property is found in Figure 2. The inputs are the trained HMM, defined in  ModelBert2.poctl , and the previous formula. The output returned by   Marimba  is State 4. Hence, the model starting at state   User grab   is likely to generate   O .  Main>   main  Enter the file name where the HMM is located.  examples/ModelBert2.poctl  Would you like to consider each state as if it were the initial state, i.e., as if it had initial distribution value equal to 1? y/n:   y  Enter the POCTL* formula we are interested in.  P[>0.88] (X_ { 3,4,6 } (X_ { 3,4,6 } (X_ { 3,4,11 } (X_ { 3,4,11 } T))))  The states that satisfy it are: (Probability of satisfaction of each state:[4.998198505964186e-10, 4.08659792160621e-6,7.508994137303159e-3,0.8915357419467848]) [4] Do you want to continue checking more specifications? y/n:   n  Fig. 2.   Verifying a property with   Marimba .  A second liveness property states that   with probability at least 0.9,   Bert2  releases the object when the user grabs it.   The POCTL* formula for this property
Marimba: A Tool for Verifying Properties of Hidden Markov Models   5  is   P ≥ 0 . 9 ( rh   ∧   ( rh   U   ( ug   ∧   ug   U   rnh ))).   Marimba   outputs State 3, i.e., the speci- fication is satisfied when the starting state is   Robot hold . So, we expect   Bert2  to hold the object, and let it go when the user grabs it.  Safety properties.   A safety property establishes that a   bad thing   does not occur during the execution of a system. For instance,   with probability less than 0.05,   Bert2   abandons its serving position with the user not grabbing the object , that is,   P < 0 . 05 ( rh   ∧   X Θ   ( rnh   ∨   rpu )), where   Θ   is the set of observations. Our model checker returns   { 1 ,   2 ,   3 ,   4 }   as the set of states satisfying this property. We conclude that it is unlikely that the model, being at state   Robot hold , reaches a state other than   User grab , that is,   Robot not hold   or   Robot pick up . The satisfaction of the previous three specifications provides us with confi- dence that   Bert2   reliably performs the handover interaction specified above. On an Intel   R ©   Core TM   i3 1.70GHz computer with 4GB in memory,   Marimba  takes 28.55s to compute the states satisfying the first liveness formula. The time required for checking the other two properties studied here is around 0.06s. Further examples are given in the   examples   folder and   user’s manual   that come with   Marimba ’s source code.  4   Conclusions  Since the automatic verification of properties of HMMs seems to be an unat- tended problem, we present here   Marimba , a   Haskell   implementation of the model checking algorithm for POCTL* [11]. This model checking algorithm was slightly modified to carry out its computations in a real program.   Marimba ’s calculation is basically broken out in three stages that are coded in the modules  ModelChecker.hs ,   DirectApproach.hs   and   Courcoubetis.hs , such that the involved components, steps and transformations are well arranged throughout the im- plementation. Finally, we have successfully applied   Marimba   to verify relevant properties of a handover interaction from the robot   Bert2   to a human.  Acknowledgements.   We gratefully acknowledge support from grants PAPIIT IN113013 and Conacyt 221341, and especially thank the BRL staff for their assistance operating the robot   Bert2 . E. Magid and K. Eder have been sup- ported, in full and in part, respectively, by the UK EPSRC grant EP/K006320/1 ROBOSAFE: “Trustworthy Robotic Assistants”.  References  1. C. Courcoubetis and M. Yannakakis,   The complexity of probabilistic verification , J. ACM   42   (1995), no. 4, 857–907. 2. L. De Moura and N. Bjørner,   Z3: An efficient SMT solver , Proceedings of the Theory and Practice of Software (TACAS ’08), LNCS, Springer, 2008, pp. 337– 340. 3. L. Erkok,   linearEqSolver: a library to solve systems of linear equations, using SMT solvers. ,   https://github.com/LeventErkok/linearEqSolver .
6   N. Hern ́ andez, K. Eder, E. Magid, J. Savage, and D. A. Rosenblueth 4. E. C. Grigore, K. Eder, A. G. Pipe, C. Melhuish, and U. Leonards,   Joint action understanding improves robot-to-human object handover , IEEE/RSJ International Conference on Intelligent Robots and Systems, IEEE, 2013, pp. 4622–4629. 5. N.   Hern ́ andez,   Model   checking   based   on   the   hidden   Markov   model   and its   application   to   human-robot   interaction ,   Master’s   thesis,   Universi- dad   Nacional   Aut ́ onoma   de   M ́ exico,   M ́ exico,   2014,   Available   from  http://132.248.9.195/ptd2014/noviembre/303087692/Index.html . 6. M. Kwiatkowska, G. Norman, and D. Parker,   PRISM 4.0: Verification of proba- bilistic real-time systems , Proc. 23rd International Conference on Computer Aided Verification (CAV ’11), LNCS, vol. 6806, Springer, 2011, pp. 585–591. 7. A. Lenz, S. Skachek, K. Hamann, J. Steinwender, A. G. Pipe, and C. Melhuish,  The BERT2 infrastructure: An integrated system for the study of human-robot in- teraction , 10th IEEE-RAS International Conference on Humanoid Robots, IEEE, 2010, pp. 346–351. 8. Y. Linde, A. Buzo, and R. M. Gray,   An algorithm for vector quantizer design , IEEE Transactions on Communications   28   (1980), 84–95. 9. L. R. Rabiner,   A tutorial on hidden Markov models and selected applications in speech recognition , Proceedings of the IEEE   77   (1989), 257–286. 10. J. Rutten, M. Kwiatkowska, G. Norman, and D. Parker,   Mathematical techniques for analyzing concurrent and probabilistic systems , CRM Monograph Series, vol. 23, American Mathematical Society, 2004. 11. L. Zhang, H. Hermanns, and D. N. Jansen,   Logic and model checking for hid- den Markov models , Formal Techniques for Networked and Distributed Systems, FORTE 2005, LNCS, vol. 3731, Springer, 2005, pp. 98–112.
Marimba: A Tool for Verifying Properties of Hidden Markov Models   7  5   Appendix  Technical details and formal definitions concerning HMMs and the POCTL* formalism are presented next.  5.1   Hidden Markov Model  An HMM has two layers, one on top of the other. The stochastic process be- tween states on the underlying layer is hidden, and can be seen only through the stochastic process on the external layer that effectively produces a visible sequence of observations.  Definition 1.   A   labelled   Hidden   Markov   Model   [9]   consists   of   a   tuple  H   = ( S, A, Θ, B, L, π ) , where: –   S   =   { S 0 , S 1 , . . . , S n − 1 }   is a finite set of states; –   A   is a state transition probability matrix, such that:  A   =   { a ij   } , a ij   ≥   0   0   ≤   i, j   ≤   n   −   1 ,   ∑ n − 1  j =0   a ij   = 1   0   ≤   i   ≤   n   −   1;  –   Θ   =   { v 0 , v 1 , . . . , v m − 1 }   is a set of   m   observations; –   B   is the observation probability matrix,   B   =   { b j   ( k ) }   with  b j   ( k ) =   P   [ v k   |   S j   ] ,   0   ≤   j   ≤   n   −   1 ,   0   ≤   k   ≤   m   −   1;  –   L   :   S   →   2 AP H   maps states to sets of atomic propositions from a set   AP H ; –   π   is an initial probability distribution over   S , such that:  π i   =   P   [ q 0   =   S i ]   ≥   0   0   ≤   i   ≤   n   −   1 ,   ∑ n − 1  i =0   π i   = 1 .  An execution of the system which is being modelled by an HMM is repre- sented by a path.  Definition 2.   A path   [11]   is a sequence   ( s 0 , o 0 ) ,   ( s 1 , o 1 ) , . . . , where   s i   ∈   S ,   o i   ∈  Θ ,   a s i s i +1   >   0   and   b s i   ( o i )   >   0 ,   ∀ i   ≥   0 . A path can be finite ( ω fin ) or infinite ( ω ).  We denote the ( i   + 1)st state of   ω   by   ω s ( i ), and the ( i   + 1)st observation by  ω o ( i ). The suffix ( s i , o i ) ,   ( s i +1 , o i +1 ) , . . .   of   ω   is denoted by   ω [ i ]. We denote the sets of all finite and infinite paths in   H , starting with a pair whose state is   s , by  Path fin , H  s   and   Path H  s   , respectively. To quantify the probability that an HMM behaves in a certain way, we de- fine the measure Pr s   over the set   Path H  s   . The   basic cylinder set   induced by the cylinder   ω fin   = ( s 0 , o 0 ) ,   ( s 1 , o 1 ) , . . . ,   ( s k , o k ) is defined as   C ( ω fin ) =   { ω   ∈  Path H  s   | ∀ i   ∈ { 0 , . . . , k }   ( ω s ( i ) =   s i   ∧   ω o ( i ) =   o i ) } .   Let   Σ s   be the small- est   σ -algebra on   Path H  s   which contains all basic cylinder sets   C ( ω fin ), where  ω fin   = ( s, o 0 ) , . . . ,   ( s k , o k )   ∈   Path fin , H  s   . We define Pr s   on   Σ s   as, Pr s  (  C ( ( s, o 0 ) , . . . ,   ( s k , o k ) ))  =   π s b s ( o 0 )   ∏ k i =1   a s i − 1   s i   b s i   ( o i ) .
8   N. Hern ́ andez, K. Eder, E. Magid, J. Savage, and D. A. Rosenblueth  Let   Σ   be the smallest   σ -algebra on   Path H   containing all basic cylinder sets, such that   Path H   is the set of paths in   H   with no constraint on the state of the initial pair. In [5], the probability measure Pr H   on   Σ   is defined in terms of Pr s . We quantify the probability that an HMM behaves in a certain way by iden- tifying the set of paths that satisfy a formula, and then using Pr H   (or Pr s ).  5.2   POCTL*  The Probabilistic Observation Computational Tree Logic* (POCTL* [11]) has a   next   operator equipped with an observation constraint.  Definition 3 (Syntax).   Let   H   = ( S, A, Θ, B, L, π )   be an HMM defined over the set of atomic propositions   AP H . The syntax of POCTL* is defined as follows:  Φ   ::=   true   |   false   |   a   |   ( ¬ Φ )   |   ( Φ   ∨   Φ )   |   ( Φ   ∧   Φ )   |   ( P ⊲⊳ p ( φ )) , φ   ::=   Φ   |   ( ¬ φ )   |   ( φ   ∨   φ )   |   ( φ   ∧   φ )   |   ( X o φ )   |   ( φ   U ≤ n φ )   |   ( φ   U φ ) ,  where   a   ∈   AP H ,   o   ∈   Θ ,   n   ∈   N ,   p   ∈   [0 ,   1] , and   ⊲⊳   ∈ {≤ , <,   ≥ , > } . We distinguish between state formulas   Φ   and path formulas   φ .  Definition 4 (Semantics).   Let   H   = ( S, A, Θ, B, L, π )   be an HMM. For any state   s   ∈   S , the satisfaction relation   | =   is inductively defined as  s   | =   true   ∀ s   ∈   S, s   6   | =   false   ∀ s   ∈   S, s   | =   a   iff   a   ∈   L ( s ) , s   | =   ¬ Φ   iff   s   6   | =   Φ, s   | =   Φ 1   ∨   Φ 2   iff   s   | =   Φ 1   ∨   s   | =   Φ 2 , s   | =   Φ 1   ∧   Φ 2   iff   s   | =   Φ 1   ∧   s   | =   Φ 2 , s   | =   P ⊲⊳ p ( φ )   iff   Pr s { ω   ∈   Path H  s   |   ω   | =   φ }   ⊲⊳ p.  For any path   ω , the satisfaction relation is defined as  ω   | =   Φ   iff   ω s (0)   | =   Φ,   ω   | =   φ 1   ∨   φ 2   iff   ω   | =   φ 1   ∨   ω   | =   φ 2 , ω   | =   ¬ φ   iff   ω   6   | =   φ,   ω   | =   φ 1   ∧   φ 2   iff   ω   | =   φ 1   ∧   ω   | =   φ 2 , ω   | =   X o φ   iff   ω o (0) =   o   ∧   ω [1]   | =   φ, ω   | =   φ 1   U ≤ n φ 2   iff   ∃ j   ≤   n.   ( ω [ j ]   | =   φ 2   ∧ ∀ i < j. ω [ i ]   | =   φ 1 ) , ω   | =   φ 1   U φ 2   iff   ∃ j   ≥   0 .   ( ω [ j ]   | =   φ 2   ∧ ∀ i < j. ω [ i ]   | =   φ 1 ) .  Let   Ω   ⊆   Θ , we write   X Ω   φ   as a shorthand for   ∨  o ∈ Ω   X o φ . Therefore,  ω   | =   X Ω   φ   iff   ω o (0)   ∈   Ω   ∧   ω [1]   | =   φ .  6   Model checking algorithm  Let   H   = ( S, A, Θ, B, L, π ) be an HMM,   s   be a state in   S , and   Φ   be a POCTL* state formula. Next, we explain a method to know whether   s   | =   Φ   holds or not.
Marimba: A Tool for Verifying Properties of Hidden Markov Models   9  6.1   Stage One  According to [11], the model checking algorithm starts by taking a most deeply nested state subformula   Ψ   of   Φ , such that   Ψ   is not an atomic proposition. It is straightforward to find the states in   S   that satisfy   Ψ   when it is propositional. To obtain the states that satisfy   Ψ   when it is of the form   P ⊲⊳ p ( φ ), stage two of the model checker is invoked. Once we determine the states satisfying   Ψ   , their label is extended by a new atomic proposition   a Ψ   . Next,   Ψ   is replaced by   a Ψ   in  Φ . The algorithm proceeds recursively, unless   Φ   itself is replaced by   a Φ ; in such case the algorithm returns states   s , with   a Φ   ∈   L ( s ).  6.2   Stage Two  To identify the states that satisfy   P ⊲⊳ p ( φ ), we follow the direct approach that transforms the original   H   into a DTMC   D   = ( S D , A D   , L D , π D   ), where –   S D   =   S   ×   Θ , –   A D   (( s, o ) ,   ( s ′ , o ′ )) =   a ss ′   ·   b s ′   ( o ′ ), –   L D ( s, o ) =   L ( s )   ∪ { Ω   ⊆   Θ   |   o   ∈   Ω } , –   π D  ( s,o )   =   π s   ·   b s ( o ), that is defined over the set of atomic propositions   AP D   =   AP H   ∪ { Ω   |   Ω   ⊆   Θ } . The argument of   P , i.e.,   φ , is modified to obtain   φ ′   in a way that every occurrence of   X Ω   φ   is replaced by   Ω   ∧ X φ . Notice that   Ω   is a new atomic proposition defined in   AP D   .  6.3   Stage Three  As stated in [1,5], stage three recursively constructs a new DTMC   D ′   by applying the transformations   C X ,   C U   and   C U   ≤ n   , which are performed for each occurrence of   X ,   U   and   U ≤ n , respectively. To show how the transformations work, we focus here on   C X . It takes   X φ   as an innermost subexpression of   φ ′ . Then, it partitions the states of   D   into three disjoint subsets,   S D   =   S YES   ∪   S NO   ∪   S ? , where: –   S YES   consists of the states whose transitions are only into states satisfying   φ . –   S NO   consists of the states whose transitions are only into states satisfying   ¬ φ . –   S ?   consists of the states with transitions to both states satisfying   φ   and states satisfying   ¬ φ . Let   q u   denote the probability that   X φ   is satisfied starting from state   u   ∈   S D . We know that   q u   = 1 if   u   ∈   S YES , and   q u   = 0 if   u   ∈   S NO . Otherwise,   q u   = ∑  v   A D   ( u, v ), where the sum ranges over all successor states   v   of   u   satisfying formula   φ . Let   q u   = 1   −   q u . Moreover, the new DTMC   D ′   is defined over the set  AP D ′   =   AP D   ∪ { ξ } , where   ξ   is a new atomic proposition representing   X φ .  States of   D ′ .   For each   u   ∈   S YES   there is a new state ( u, ξ ) in   D ′ . For each   u   ∈  S NO   there is a new state ( u,   ¬ ξ ). And for each   u   ∈   S ? , there are two new states ( u, ξ ) and ( u,   ¬ ξ ). We define   L D ′  ( u, ξ ) =   L D ( u )   ∪ { ξ }   and   L D ′  ( u,   ¬ ξ ) =   L D ( u ).
10   N. Hern ́ andez, K. Eder, E. Magid, J. Savage, and D. A. Rosenblueth  Transitions of   D ′ .   The transition probability of ( u, ξ 1 )   →   ( v, ξ 2 ), with   ξ i   ∈ { ξ,   ¬ ξ }   and   i   ∈ { 1 ,   2 } , is defined as being equal to the probability that   D , being at state   u , transitions next to state   v , and starting from state   v   onward satisfies property   ξ 2 , conditioned on the event that in state   u   it satisfies property   ξ 1 .  Initial distribution of   D ′ .   If   u   ∈   S YES   ∪   S NO , then   π D ′  ( u,ξ 1   )   =   π D  u   . If   u   ∈   S ? , then there are two states in   D ′   for   u , namely ( u, ξ ) and ( u,   ¬ ξ ), with initial probabilities   π D  u   ·   q u   and   π D  u   ·   q u , respectively. Furthermore,   ψ   is obtained by replacing   X φ   by   ξ   in   φ ′ . If   φ ′   originally has   k   temporal operators, the algorithm applies   k   times the appropriate transformations   C X ,   C U   and   C U   ≤ n   , to finally get the DTMC   D k  and the propositional formula   ψ k . It is proved in [5] that   s   | =   P ⊲⊳p ( φ ) iff  ∑  o ∈ Θ  (   ∑  ξ i 1   ∈{ ξ 1 , ¬ ξ 1   }  . . .  ξ ik   ∈{ ξ k   , ¬ ξ k   }  Pr (( ... (( s,o ) ,ξ i 1   ) ,... ) ,ξ ik   )  ︸   ︷︷   ︸  σ 0  { σ   ∈   Path D k  σ 0   |   σ   | =   ψ k }  )  ⊲⊳ p.  Since   ψ k   is a propositional formula, Pr σ 0   { σ   ∈   Path D k  σ 0   |   σ   | =   ψ k }   is   π D k  σ 0   .