I n d on e s i an   Jo u r n al   o El e c t r i c al   En gi n e e r i n g   an d   C o m p u te r   S c i e n c e   V o l .   18 ,   N o .   1 A p r i l   20 20 ,   p p.   1571 ~ 157 7   IS S N :   2502 - 4752 ,   D O I :   10. 1 1591 / i j e e c s . v 1 8 .i 1 . pp 157 1 - 1577             1571       Jou r n al   h o m e pa ge ht t p: / / i j e e c s . i a e s c or e . c om   Im p r o v i n g   g r a p h - b a sed m e t h o d f o r   c o m p u t i n g   q u a l i t a t i v e   p r o p e r t i e o f   m a r k o v   d e c i s i o n   p r o c e sses       M o h amm ad s ad e gh   M o h agh e gh i 1 K h a yyam   S al e h i 2   1 D e pa r t m e n t   o f   C o m put e r   S c i e nc e ,   V a l i - e - A s r   U n i v e r s i t y   of   R a f s a n j a n ,   I r a n   2 D e pa r t m e n t   o f   C o m put e r   S c i e nc e ,   U n i v e r s i t y   o f   T a br i z ,   I r a n       A r ti c l e   I n fo     A B S TR A C T   Ar t i c l e   h i s t or y :   R e c e i v e A ug   1,   2019   R e v i s e S e p   2 1 ,   201 9   A c c e pt e O c t   1 1 ,   2 01 9       P r o ba bi l i s t i c   m o de l   c he c ki ng   i s   a   f o r m a l   v e r i f i c a t i o m e t ho d,   w h i c i s   us e t o   g ua r a nt e e   t he   c o r r e c t ne s s   o f   t he   c o m put e r   s y s t e m s   w i t s t o c ha s t i c   be ha v i o r s .   R e a c ha bi l i t y   pr o ba bi l i t i e s   a r e   t he   m a i c l a s s   o f   pr o pe r t i e s   t ha t   a r e   pr o po s e i n   pr o ba b i l i s t i c   m o de l   c he c ki ng .   S o m e   g r a ph - b a s e p r e - c om put a t i o c a de t e r m i ne   t ho s e   s t a t e s   f o r   w hi c t he   r e a c ha b i l i t y   p r o ba bi l i t y   i s   e xa c t l y   z e r o   o r   o ne .   I t e r a t i v e   n um e r i c a l   m e t ho ds   a r e   us e t o   c o m put e   t h e   r e a c ha b i l i t y   pr o ba bi l i t i e s   f o r   t h e   r e m a i n i ng   s t a t e s .   I t h i s   p a pe r ,   w e   f o c us   o n   t he   g r a p h - ba s e pr e - c o m put a t i o ns   a n pr o po s e   a   he u r i s t i c   t o   i m pr o v e   t he   pe r f o r m a nc e   o f   t he s e   pr e - c o m put a t i o ns .   T h e   pr o po s e he u r i s t i c   a pp r o xi m a t e s   t he   s e t   o f   s t a t e s   t h a t   a r e   c o m put e i t he   s t a n da r p r e - c o m put a t i o m e t ho ds .   T he   e xpe r i m e n t s   s ho w   t ha t   t he   p r o po s e he ur i s t i c   c a n   c o m put e   a   m a i n   pa r t   o f   t he   e xpe c t e s t a t e s ,   w h i l e   r e duc e s   t he   r un ni ng   t i m e   by   s e v e r a l   o r de r s   o f   m a g ni t ud e .   Ke y w or ds :   G ra p h - b a s e p r e - c o m put a t i o n   M a r ko v   de c i s i o n   p r o c e s s e s   P r o b a b i l i s t i c   m o de l   c h e c ki n g   Q ua l i t a t i v e   r e a c ha b i l i t y   pr o b a b i l i t i e s   C opy r i gh t   ©   2020   I n s t i t ut e   o f   A dv anc e E ng i ne e r i ng   and   S c i e nc e .     A l l   r i gh t s   r e s e r v e d .   Cor r e s pon di n g   Au t h or :   M o h a m m a ds a de g M o h a g h e g h i ,   D e pa rt m e n t   o f   Co m put e s c i e n c e ,   V a l i - e - A s r   U n i v e r s i t y   of   R a f s a n j a n,   I r a n.   E m a i l :   m o ha g h e g hi @ v r u. a c . i r       1.   I N TR O D U C TI O N     F o r m a l   m e t h o ds   a r e   m a t h e m a t i c a l - b a s e a pp r o a c h e s   t ha t   a r e   us e i n   s of t w a r e   e n gi n e e r i n a nd  ha r dw a r e   de s i gn.   T h e   go a l   o f   t h e s e   m e t h o ds   i s   t o   gua ra n t e e   t h e   c o r r e c t n e s s   of   t h e   qu a l i t a t i v e   o r   qua nt i t a t i v e   pr o pe rt i e s   o f   t h e   de s i r e s y s t e m s   [1,   2].   M o de l   c h e c ki ng  i s   a n   a ut o m a t e f o r m a l   m e t h o t ha t   us e s   g r a p h - b a s e s t r uc t u r e s   f o r   m o de l l i n t h e   u n de rl y i n s y s t e m s   a n d   l o gi c - b a s e pr o po s i t i o n s   t o   s pe c i fy   t h e   s y s t e m   pr o pe rt i e s   [1,   3] .   A   m o de l   c h e c ke r   i s   a   s of t w a r e   t o o l   t h a t   de c i de s   t h e   s a t i s f i a b i l i t y   of   t h e   s pe c i f i e pr o pe r t i e a ga i n s t   t h e   p r o po s e m o de l   [1,   4] .   B e c a us e   of   t h e   s t oc h a s t i c   b e h a v i o r s   of  m a n y   c o m put e r   s y s t e m s ,   p r o b a b i l i s t i c   s t r uc t u r e s   a r e   m o r e   us e f ul   fo r   m o de l i ng  s uc s y s t e m s   [4 - 6].   M a r ko v   c h a i n s   a nd  M a r ko v   de c i s i o n   pr o c e s s e s   (M D P s a r e   w e l l - kn o w n   s t r uc t u r e s   fo r   m o de l l i n s t o c h a s t i c   s y s t e m s   a n a r e   w i de l y   us e i n   a rt i f i c i a l   i n t e l l i ge n c e ,   e c o n o m y ,   o pe r a t i o n s   r e s e a r c h   a n s o f t w a r e   e n g i n e e r i ng  [7 - 9] .   S e v e r a l   e xa m p l e s   of   t h e   s t o c h a s t i c   s y s t e m s   a n t h e i m o de l l i n a r e   a v a i l a b l e   i n   [3 ,   4 ,   7] .   F o r   t hi s   c l a s s   o f   s ys t e m s ,   p r o b a b i l i s t i c   m o de l   c h e c ki n i s   a   go o d   t e c hn i q ue   t o   v e r i fy   t h e   qua nt i t a t i v e   o r   qua l i t a t i v e   pr o pe rt i e s   o f   t h e   s y s t e m s .   P R S IM   [10],   S T O R M   [11]  a n d   Is c a s M [12]   a r e   s t a t e   o f   t h e   a r t   p r o b a b i l i s t i c   m o de l   c h e c ke rs .   T h e   m a i n   c l a s s e s   of  pr o pe r t i e s   t ha t   a r e   us e i n   p r o b a b i l i s t i c   m o de l   c h e c ki n c o n t a i n   r e a c ha b i l i t y   pr o b a b i l i t i e s ,   i . e .   t h e   m a xi m a l   o r   m i ni m a l   p r o b a b i l i t y   of   r e a c hi n a   s e t   of   g o a l   s t a t e s   i n   t h e   M D P   m o de l .     A   s t a n d a r a pp r o a c f o r   c o m put i n r e a c ha b i l i t y   pr o b a b i l i t i e s   i s   t o   us e   i t e r a t i v e   gra p h - b a s e a nd  n u m e ri c a l   m e t h o ds   [13].   G ra p h - b a s e m e t h o ds   (a l s o   c a l l e pr e - c o m put a t i o n c o m put e   t h e   s e t   of   s t a t e s   fo r   w h i c h   t h e   pr o b a b i l i t y   of   r e a c h i n a   go a l   s t a t e   i s   e xa c t l y   z e r o   o r   o n e   [ 4].   A n   i t e r a t i v e   n um e r i c a l   m e t h o s t a r t s   f r o m   a n   i n i t i a l   v e c t o r   o f   v a l ue s   a n i t e r a t i v e l y   upda t e s   t h e   v a l ue s   u nt i l   s a t i s fy i n g   t h e   s t o ppi ng  c r i t e ri o [1] .   Evaluation Warning : The document was created with Spire.PDF for Python.
                                IS S N :   2502 - 4752   In do n e s i a J   E l e c   E ng  &   Co m S c i ,   V o l .   18 ,   N o .   1 A p r i l   20 20  :     1571   -   1577   1572   T h e   m a i n   c h a l l e n ge   of   m o d e l   c h e c ki n i n   a l l   v a r i a n t s   i s   t h e   s t a t e   e xpl o s i o n   pr o b l e m ,   i . e .   t h e   n u m b e r   of   t h e   s t a t e s   o f   t h e   m o de l   g r o w s   e xp o n e n t i a l l y   i n   t h e   n u m b e r   o f   i t s   c o m po n e n t s .   S e v e r a l   t e c hn i q ue s   a r e   pr o po s e t o   c o pe   w i t h   t hi s   p r o b l e m   [1,   1 4 - 17] .   I t h e   c a s e   of   pr o b a b i l i s t i c   m o de l   c h e c ki n t h e   r u nn i ng  t i m e   of   i t e r a t i v e   m e t h o ds   i s   t h e   m a i n   p r o b l e m   t h a t   l i m i t s   t h e   s c a l a b i l i t y   of   t h e   m e t h o [3,   1 8,   1 9].   S e v e r a l   t e c hn i q ue s   ha v e   b e e n   pr o po s e t o   i m pr o v e   t h e   pe r f o r m a n c e   of   t h e   s t a n d a r p r o b a b i l i s t i c   m o de l   c h e c ki n g   m e t h o ds .   T h e s e   t e c hn i qu e s   a r e   us e t o   r e duc e   t h e   r u nni ng   t i m e   o f   t h e   g ra p h - b a s e [20 21]   o r   num e r i c a l   c o m put a t i o n s   [22 - 24]  o r   b o t h   m e t h o ds   [16 25].   A l t h o ug h   t h e   p r o po s e m e t h o ds   s h ow   pr o m i s i n r e s ul t s   i t h e   ru nn i ng  t i m e   o f   pr o b a b i l i s t i c   m o de l   c h e c ki n g,   e xpe ri m e nt a l   r e s ul t s   s h o w   m o r e   i m p r o v e m e n t   i s   n e e de f o r   i t e ra t i v e   gra p h - b a s e o f   n u m e ri c a l   m e t h o ds   [26] .   I n   t h i s   pa p e r ,   w e   c o n s i de t h e   r u nni n t i m e   o f   gr a p h - b a s e m e t h o ds   a s   a n   i m po r t a n t   p r o b l e m   i n   p r o b a b i l i s t i c   m o de l   c h e c ki n a n p r o po s e   a   n e w   a ppr o a c h   t o   r e duc e   t h i s   r u nni n g   t i m e .   T h e   fo r w a r a n b a c kw a r a pp r o a c h e s   a r e   t w o   a l t e rn a t i v e s   f o r   gr a p h - b a s e c o m put a t i o n s   i n   t h e   pr o b a b i l i s t i c   m o de l   c h e c ki ng  o f   M D P s   [1].   T h e   f o r w a r a pp r o a c i s   n o rm a l l y   f a s t e r   t ha n   t h e   b a c kw a r d   a pp r o a c h,   b ut   i t s   m a i n   d ra w b a c i s   t h e   m e m o r y   ov e r h e a d ,   w h i c h   l i m i t s   i t s   s c a l a b i l i t y   t o   r e l a t i v e l y   s m a l l   m o de l s   [1,   20] .   A s   a   r e s ul t ,   m o s t   p r o m i n e n t   m o de l   c h e c ke r s   (s uc h   a s   P R IS M   a n Is c a s M C)  us e   t h e   f o r w a r a pp r o a c f o r   t h e   p r e - c o m put a t i o n s   t o   a v o i m e m o r y   ov e r h e a d ,   w hi c i s   e s s e n t i a l   t o   o ve r c o m e   t h e   s t a t e   e xpl o s i o n   pr o b l e m   [15,   27].   T h e   m o t i v a t i o n   of   t h i s   pa pe r   i s   t o   i m pr o v e   t h e   pe r f o r m a n c e   of   t h e   gr a p h - b a s e d   pr e - c o m put a t i o n   m e t h o ds .   T o   a vo i m e m o r y   ov e r h e a d ,   w e   fo c us   o n   t h e   fo r w a r a pp r o a c h   fo r   pr e - c o m put a t i o n .   A s   t h e   m a i n   c o n t ri b ut i o n   o f   t h e   p a pe r,   w e   pr o po s e   a   h e u r i s t i c   t o   r e duc e   t h e   r u nni n t i m e   o f   pr e - c o m put a t i o n   i n   t h e   f o r w a r a pp r o a c h.   T hi s   h e uri s t i c   r e duc e s   t h e   n u m b e r   o f   i t e r a t i o n s   by   a ppr o xi m a t i n t h e   s e t   of   e xp e c t e s t a t e s   i n   a i m p r o v e o r de r.   A l t h o ug h   t h i s   h e uri s t i c   do e s   n o t   gua ra n t e e   t o   de t e c t   a l l   s t a t e s   t h a t   t h e   s t a n d a r p r e - c o m put a t i o n   a l go ri t hm s   do ,   t h e   e xpe r i m e nt s   s h o w   t h a t   i t   c a n   r e duc e   t h e   ov e r a l l   r u n - t i m e   i n   m o s t   c a s e s   a n d   i m p r o v e s   t h e   pe r f o r m a n c e   o f   pr o b a b i l i s t i c   m o de l   c h e c ki n g   o f   M D P s .       2.   F O R M A P R O B LE M   D EF I N A TI O N   A N D   B A C K G R O U N D   In   t h i s   s e c t i o n,   w e   pr o po s e   a   b r i e f   r e v i e w   of   t h e   m a i n   c o n c e pt s   o f   pr ob a b i l i s t i c   m o de l   c h e c ki n t ha t   a r e   us e i n   t h i s   p a pe r.   M o r e   de t a i l s   a b o ut   pr o b a b i l i s t i c   m o de l   c h e c ki ng  a n t h e i r   m e t h o ds   a r e   a v a i l a b l e     i n   [1 ,   3,   4] .     2. 1 .       P r o b ab i l i s ti c   M o d e l s   an d   R e a c h ab i l i ty   P r o b ab i l i ti e s   M a r ko v   d e c i s i o n   pr o c e s s e s   a r e   us e i n   p r o b a b i l i s t i c   m o de l   c h e c ki n t o   m o de l   b o t h   n o n de t e rm i ni s t i c   a n p r o b a b i l i s t i c   a s pe c t s   o f   a   s y s t e m   [7].   D e f i n i t i o n   1.   (M a r ko v   D e c i s i o n   P r o c e s s A   M a r ko v   D e c i s i o n   P r o c e s s   (M D P )   i s   de f i n e a s   a   t u pl e     w h e r e     i s   a   f i ni t e   s e t   o f   s t a t e s ,     i s   t h e   i n i t i a l   s t a t e ,     i s   a   f i n i t e   s e t   o f   a c t i o n s .   F o r   e ve r y   s t a t e     t h e   s e t   of   e n a b l e a c t i o n s   o f     i s   de n o t e by   .   W e   us e     a s   t h e   s i z e   of   t h i s   s e t   a n   i s   a   p r o b a b i l i s t i c   t r a n s i t i o n   f u n c t i o n   a n i s   de f i n e a s   a   s ub s e t   of   .   F o r   e a c h   s t a t e     a n e n a b l e a c t i o n   ,   e xa c t l y   o n e   t r a n s i t i o n     e xi s t s .   T h e   no t a t i o n     m e a n s   t ha t     i s   a n   e l e m e nt   o f   .   W e   us e     t o   de n o t e   t h e   p r o b a b i l i t y   of   r e a c hi n f r o m     t o   .   By   t h e   a c t i o   i s   t h e   s e t   o f   go a l   s t a t e s .   M D P s   a r e   w i de l y   us e t o   m o de l   d e c i s i o n   m a ki ng  p r o b l e m s   i n   s t o c h a s t i c   e n v i r o nm e nt s .   T ra n s i t i o n s   o a n   M D P   M   s h ow   t h e   b e h a v i o r   of   t h e   r e l a t e s y s t e m   [1].   F o r   a   s t a t e   ,   a   t ra n s i t i o n   i s   pe r f o r m e i n   t w o   s t e ps :   F i r s t ,   a n   a c t i o n     i s   s e l e c t e n o n - de t e r m i ni s t i c a l l y .   Ne xt ,   t h e   de s t i n a t i o n   s t a t e     i s   s e l e c t e r a n do m l y   w i t h   p r o b a b i l i t y   .   W e   us e     f o r   t h e   s e t   o f   s uc c e s s o r   a n d   p r e de c e s s o r   a nd  - s uc c e s s o r   s t a t e s   o f   :       (1)         (2)         (3)     W e   us e     f o r   t h e   s i z e   o f     a n de f i n e   i t   a s   t h e   n u m b e r   o f   s t a t e s   a n t r a n s i t i o n s   o f   M .   A   f i ni t e   p a t of     i s   a   po s s i b l e   s e que n c e   of   a c t i o n s   a n t r a n s i t i o n s   o f     a n i s   de f i n e a s     w h e r e     a nd    f o r   a l l   .   W e   us e     f o r   t h e   l a s t   s t a t e   o f     R e a c h a b i l i t y   pr o b a b i l i t i e s   a r e   o n e   of  t h e   m a i n   p r o pe r t i e s   of  pr o b a b i l i s t i c   m o de l s   t ha t   a r e   c o m put e i n   p r o b a b i l i s t i c   m o de l   c h e c ki n [ 3,   4] .   A   r e a c ha b i l i t y   pr o b a b i l i t y   i s   de f i n e a s   t h e   p r o b a b i l i t y   o f   r e a c h i n g   a   go a l   s t a t e   f r o m   t h e   i ni t i a l   s t a t e   o f   t h e   m o de l .   I n   t h e   c a s e   o f   M D P s ,   r e a c ha b i l i t y   pr o b a b i l i t i e s   a r e   de f i n e a s   t h e   o pt i m a l   (m i n i m a l   o r   m a xi m a l p r o b a b i l i t y   of   r e a c h i ng  o n e   of   t h e   go a l   s t a t e s   f r o m   t h e   i n i t i a l   s t a t e   .   W e   us e   Evaluation Warning : The document was created with Spire.PDF for Python.
In do n e s i a J   E l e c   E ng  &   Co m S c i     IS S N :   2502 - 4752       Im pr ov i ng   gr aph - bas e d   m e t hods   f or   c om p ut i ng  qual i t a t i v e   p r ope r t i e s   o f   ( Moham m ads a de gh   Mo hagh e ghi )   1573     a n   fo r   m i n i m a l   a n m a xi m a l   r e a c h a b i l i t y   pr o b a b i l i t i e s   o M .   It e ra t i v e   n u m e r i c a l   a pp r o a c h e s   (s uc h   a s   v a l ue   i t e r a t i o n   [18]  a n po l i c y   i t e r a t i o n   [4] c a n   b e   us e t o   a ppr o xi m a t e   t h e   r e a c h a b i l i t y   pr o b a b i l i t i e s .     2. 2 .      Q u al i tat i v e   R e a c h ab i l i ty   S o m e   gr a p h - b a s e c o m put a t i o n s   c a n   de t e rm i n e   t h e   s e t   o f   s t a t e s   f o r   w h i c t h e   e xt r e m a l   r e a c h a b i l i t y   pr o b a b i l i t i e s   a r e   e xa c t l y   o r   1.   I n   t h e   c a s e   of   m a xi m u m   r e a c ha b i l i t y   pr ob a b i l i t y ,   t h e s e   s e t s   a r e   de n o t e b y     a n d     a n d   a r e   de f i n e a s :         (4)         (5)     W e   de f i n e     f o r   t h e   r e m a i n i ng  s t a t e s .   F o r   t h e   c a s e   o f   m i ni m u m   r e a c h a b i l i t y   pr o b a b i l i t i e s ,   w e   us e     a n   a n de f i n e   t h e m   i n   a n   a n a l o go us   w a y   [4].   T h e   c o m put a t i o n s   of  t h e s e   s e t s   a r e   c a l l e qu a l i t a t i v e   r e a c ha b i l i t y   a na l y s i s   a n a re   us e a s   pr e - c o m put a t i o n   i n   p r o b a b i l i s t i c   m o de   c h e c ki ng.   T h e   m a i n   a i m s   o f   pr e - c o m put a t i o n s   a r e   t o   s i m pl i f y   t h e   i t e r a t i v e   c o m put a t i o n s   by   foc us i n o n     a n t o   i n c r e a s e   t h e   p r e c i s i o n   o f   c o m put a t i o n s   [4 ,   18 ,   20 ,   25] .   A l go r i t hm   a n A l go r i t hm   s h o w   t h e   s t a nda rd  pr e - c o m put a t i o n   m e t h o ds   f o r   t h e     a nd    s e t s   [4] .               A l go r i t h m   i t e ra t i v e l y   c o m put e s   t h e   s e t     o f   s t a t e s   t ha t   c a r e a c h   t o   o n e   o f   t h e   go a l   s t a t e s   .   I n   e a c h   i t e r a t i o n,   t h e   a l go ri t hm   a dds   a   s t a t e     t o     i f   a t   l e a s t   o n e   s t a t e     h a s   b e e n   a dde t o     i n   t h e   p r e v i o us   i t e ra t i o n .   F o r   a n y   s t a t e   ,   w e   h a v e   .   T h e   r e m a i n i ng   s t a t e s   c a nn o t   r e a c t o   a n y   of   t h e   go a l   s t a t e s   a n a r e   r e t u rn e d   a s   t h e   s e t .     A l go r i t h m   2   us e s   a   n e s t e w hi l e   l o o t o   c o m pu t e   t h e     s e t .   T h e   o ut e r   l o o s t a rt s   f r o m     a nd  s uc c e s s i ve l y   r e m ov e s   t h o s e   s t a t e s     fo r   w h i c h   w e   a r e   s u r e   .   It   i n duc e s   a   s e que n c e   of     s e t s ,   w h e r e   .   T o   c o m put e   t h e     s e t s ,   t h e   i nn e r   l o o s t a r t s   f ro m   G   (l i n e   o f   A l go r i t h m   2)  a n i t e ra t i v e l y   a dds   e a c h   s t a t e     t o     i f     c a n   r e a c h   t o   o n e   o t h e   go a l   s t a t e s   w i t h   pr o b a b i l i t y   o n e   v i a   t h e   s t a t e s   of     F o r   t h e   r e m a i n i ng  s t a t e s   (t h e   s t a t e s   i n   ) ,   w e   a r e   s ur e   t h a t   t h e y   d n o t   b e l o n g   t o   .   T h e   p r o of   of   c o r r e c t n e s s   o f   t h e s e   a l go ri t hm s   i s   a v a i l a b l e   i [18] .       3.   R ES EA R C H   M ET H O D   T h e   t i m e   c o m pl e xi t y   o A l go r i t hm   i s   i n     a nd  t h e   t i m e   c o m pl e xi t y   of   A l go r i t h m   i s   i n   .   I n   t h e s e   c a s e s ,   w e   s upp o s e   t h a t   f o r   e a c h   s t a t e   ,   t h e   a l go ri t h m s   c a n   de t e rm i n e   a n y   s t a t e s   of  Evaluation Warning : The document was created with Spire.PDF for Python.
                                IS S N :   2502 - 4752   In do n e s i a J   E l e c   E ng  &   Co m S c i ,   V o l .   18 ,   N o .   1 A p r i l   20 20  :     1571   -   1577   1574     i   [1].   F o r   t h i s   pu r po s e ,   t h e   m e t h o s h o ul r e s t o r e   t he   i n f o r m a t i o o f   t h e   m o de l   i t h e   b a c k w a r a pp r o a c h,   i . e .   f o r   e a c h   s t a t e   ,   t h e   l i s t   o f   s t a t e s   i n     s h o ul b e   r e s t o r e d.   T h e   m a i dra w b a c o f   r e s t o r i n t h e   i n f o r m a t i o n   o f   a   m o de l   i s   i t s   m e m o r y   o ve r h e a w h i c h   i s   a   m a i n   c ha l l e n ge   i t h e   s t a t e   e xpl o s i o n   p r o b l e m .   O n   t h e   o t h e r   ha n d ,   t h e   f o r w a r i m pl e m e n t a t i o n   o f   t h e s e   a l go r i t hm s   (a s   i s   us e i P R IS M   [10])  n e e n o t   a n y   a ddi t i o na l   m e m o r y ,   b ut   m a y   i n c r e a s e   t h e   r u nni ng  t i m e   o f   t h e   c o m put a t i o n s .     T o   i m p r o v e   t h e   pe r f o r m a n c e   o f   t h e   p r e - c o m put a t i o n s   i t h e   f o r w a r m a nn e r,   w e   pr o po s e   a   h e uri s t i c   t o   r e duc e   t h e i r   r u nni n t i m e .   A s   t h e   f i r s t   pa rt   o f   t h e   h e u r i s t i c ,   w e   m o d i fy   A l g o r i t hm   f o r   t h e   c o m put a t i o n   o f   t h e     s e t .   A s   t h e   s e c o n pa r t   ( t h e   m a i n   c o n t r i b ut i o n   o f   t h e   w o r k),   w e   pr o po s e   a   n e w   a ppr o a c h   t o   a pp r o xi m a t e   t h e     s e t .       3. 1 .      I m p r o v i n M e th o d   fo r   C o m p u ti n   T h e   i de a   o f   A l go r i t h m   (w hi c h   i s   us e i n   P R IS M   a n Is c a s M C)  i s   t o   a dd  a   s t a t e     t o     i f   a t   l e a s t   o n e   s t a t e s   i n     h a s   b e e n   a dde i n   t h e   pr e v i o us   i t e r a t i o n.   T o   r e duc e   t h e   n u m b e r   of   i t e r a t i o n s   o t h i s   a l go ri t hm   i n   t h e   f o r w a r d   a pp r o a c h,   i t   c a us e   o nl y   o n e   s e t   ( t o   s t o r e   t h e   s e t   o f   s t a t e s   t ha t   c a r e a c h   t o     In  e a c i t e ra t i o n   ,   a   s t a t e     i s   a dde t o     i f   a t   l e a s t   o n e   s t a t e   i n     ha s   b e e n   a dde t o     i n   t h e   i t e ra t i o n     o r   .   N o t e   t h a t   i n   A l go ri t hm   1,     i s   a dde t   o n l y   i f   o n e   s t a t e   i n     h a s   b e e n   a dde t   i t h e   p r e v i o us   i t e ra t i o n   a n d   n o t   i n   t h e   c u rr e n t   o n e .       3. 2    I m p r o v i n M e th o d   fo r   A p p r o x i m ati n   In   t h i s   s e c t i o n   w e   pr o pos e   o ur   h e u r i s t i c   t o   c o m put e   a   s e t   a s   a n   a pp r o xi m a t i o n   o t h e     s e t .   T h i s   h e u r i s t i c   s t a r t s   f r o m     a nd  i t e r a t i v e l y   c o m put e   t h e   s e t s     w h e r e     i s   t h e   f i xe po i n t   s e t   of   t h e   c o m put a t i o n s .   F o r   e a c h   i t e ra t i o n     of   t h e   h e u r i s t i c ,   a   s t a t e     s h o ul d   b e   a dde t o     i f   t h e r e   e xi s t s   a a c t i o n     fo r   w h i c h   .   I n   t hi s   c a s e ,   a l l   - s uc c e s s o r   s t a t e s   o f     a r e   i n   ,   w h i c h   m e a n s   f o r   a l l   o f   t h e s e   s t a t e s ,   w e   a r e   s ur e   t ha t   t h e i r   m a xi m u m   r e a c ha b i l i t y   pr o b a b i l i t y   i s   o n e .   T hi s   h e u ri s t i c   i s   e xpl a i n e d   i A l go r i t h m   3 .         T h e   r u nni n t i m e   o f   A l go r i t hm   3   i s     w h e r e     t h e   n um b e o f   i t e ra t i o n s   o f   t h e   a l go r i t hm   i s   a n   i s   t h e   s i z e   of   t h e   m o de l .   I n   w o r s t   c a s e ,     a n t h e   w o r s t   c a s e   t i m e   c o m pl e xi t y   of   t h e   a l go ri t hm   i s   i n   .   H ow e v e r ,   i n   m o s t   c a s e s ,   t h e   a l go ri t hm   t e r m i n a t e s   a f t e r   a   f e w   n um b e r s   o f   i t e r a t i o n s .   N o t e   t h a t   t h e   p r o po s e h e u r i s t i c s   i t hi s   s e c t i o ( S ub s e c t i o n s   3. 1   a n d   3 . 2)   do   n o t   n e e a n y   a ddi t i o n a l   m e m o r y .       4.   R ES U LTS   A N D   A N A L Y S I S   T o   c o m pa r e   t h e   r u nn i ng  t i m e   of   o ur   h e u ri s t i c   f o r   pr e - c o m put a t i o n   w i t h   t h e   s t a n d a r m e t h o d,     w e   h a v e   i m pl e m e nt e t h e m   i n   P R IS M .   W e   us e   c l a s s e s   of  s t a nda r c a s e   s t udi e s   w h i c h   a r e   us e i n   s e ve r a l   pr e v i o us   w o r ks   [4,   15 ,   19 ,   20 ,   26,   28 ].   F o r   e a c h   c l a s s ,   w e   c o n s i de r   m o de l s .   M o r e   d e t a i l s   a b o ut   t h e s e   c a s e   s t udi e s   a r e   a v a i l a b l e   i [10] .   I T a b l e   w e   pr o po s e   t h e   na m e ,   pa ra m e t e r   v a l ue s ,   t h e   n u m b e r   o f   s t a t e s   o f   e a c h   m o de l   a n t h e   e xpe ri m e n t a l   r e s ul t s .   W e   us e   t h e   s pa r s e   e n g i n e   of   P R IS M   fo r   r u nni n t h e   s t a nda rd  a n d   i m p r o v e pr e - c o m put a t i o n   m e t h o ds .   W e   pr o pos e   t h e   n u m b e r   of   s t a t e s   i n   t h e     a n   s e t s   a n t h e   a pp r o xi m a t i o n   o f     (c o l um n s     a n   i n   T a b l e   1 .   W e   a l s o   pr o po s e   t h e   r u nni n t i m e s   o s t a n d a r p r e - c o m put a t i o n s   a n d   o ur  p r o po s e m e t h o ds .   A l l   t i m e s   a r e   i n   s e c o n ds .   F o r   m o s t   c a s e s   (e xc e pt   t h e   c o i n   o n e s o ur   h e u ri s t i c   f i n ds   a l l   s t a t e s   o f   t h e     s e t .   O n   t h e   o t h e r   ha n d ,   o ur   h e u r i s t i c   r e duc e s   t h e   r u nn i ng  t i m e   o pr e - c o m put a t i o n s   f o r   a l l   c a s e s .   T h e   b e s t   r e s ul t   i s   f o r   CS M A   (n = 3 , k= 6 w h i c h   t h e   r u nn i ng  t i m e   of   t h e   s t a n d a r p r e - c om put a t i o n   m e t h o i s   m o r e   t ha n   h o u r s   (24603   s e c o n ds ),   w h i l e   t h e   ru nn i ng  t i m e   of   o ur   i m p r o v e m e t h o i s   l e s s   t h a n   30  s e c o n ds .   F o r   o t h e r   c a s e s   of   CS M A   a n m o s t   c a s e s   of   z e r o c o n f ,   w l a n   a n w l a c o l l i de   o ur   m e t ho ds   r e duc e   t h e   ru nn i ng  t i m e s   o f   pr e - c o m put a t i o by   t w o   o r de r s   o f   m a g n i t ude .   T h e s e   r e s ul t s   s h o w   t h a t   o u r   h e uri s t i c   p r e s e nt s   a   s i g ni f i c a n t   i m p r o v e m e n t   i n   t h e   pe r f o r m a n c e   o f   gra p h - b a s e i t e ra t i v e   m e t h o ds   i p r o b a b i l i s t i c   m o de l   c h e c ki n g .   Evaluation Warning : The document was created with Spire.PDF for Python.
In do n e s i a J   E l e c   E ng  &   Co m S c i     IS S N :   2502 - 4752       Im pr ov i ng   gr aph - bas e d   m e t hods   f or   c om p ut i ng  qual i t a t i v e   p r ope r t i e s   o f   ( Moham m ads a de gh   Mo hagh e ghi )   1575   T a b l e   1 .   R u nn i ng  T i m e   of  P r e - Co m put a t i o n   M e t h o ds   f o r   M D P   M o de l s   M o d e l   P a ra m e t e r( s )         T i m e     T i m e   Co i n   n = 2 , K = 4 5   5 , 7 7 6   12   30   3 . 2 4   12   0 . 0 1   n = 4 , K = 1 2   3 2 , 0 5 6   6 , 1 5 6   294   1 0 . 9 6   324   0 . 0 3   n = 4 , K = 2 0   5 3 , 0 4 8   9 , 9 9 6   294   2 9 . 2   324   0 . 0 8   n = 6 , K = 9   6 8 , 9 1 4   1 8 , 2 0 2   694   2 8 . 4 8   988   0 . 0 7   Z e r o c o n f   K = 8   1 , 8 7 0 , 3 3 8   1 7 1 , 7 4 9   6 1 1 , 3 3 0   7 7 . 7 5   1 7 1 , 7 4 9   0 . 6 6   K = 1 0   3 , 0 0 1 , 9 1 1     1 9 7 , 0 0 4   9 5 7 , 8 0 7   9 4 . 6   1 9 7 , 0 0 4   1 . 1 6   K = 1 2   3 , 7 5 4 , 3 8 6   1 8 9 , 3 7 2   1 , 0 8 2 , 1 4 5   1 1 3 . 5   1 8 9 , 3 7 2   1 . 4 6   K = 1 4   4 , 4 2 7 , 1 5 9   1 7 1 , 8 5 1   1 , 1 6 0 , 9 6 4   1 4 1 . 1   1 7 1 , 8 5 1   1 . 8   CS M A   n = 3 , k = 4   2 4 9 , 6 7 8   1 1 8 , 5 4 4   7 , 7 2 6   2 2 . 7 2   1 1 8 , 5 4 4   0 . 2 4   n = 3 , k = 6   1 4 , 2 2 2 , 5 2 9   1 0 , 1 2 0 , 3 7 9   1 6 9 , 2 0 6   2 4 6 0 3   1 0 , 1 2 0 , 3 7 9   2 5 . 2 6   n = 4 , k = 2   3 9 , 4 8 1   6 , 3 1 2   1 , 9 7 2   5 . 7   6 , 3 1 2   0 . 0 5   n = 4 , k = 4   5 , 8 7 4 , 8 5 3   5 1 4 , 4 5 7   1 7 1 , 9 6 0   1 3 2 4 . 9   5 1 4 , 4 5 7   2 2 . 1 2   W l a n   T T M = 1 5 0 0 , n = 5   3 , 6 3 4 , 5 1 8   2 , 7 3 4 , 1 6 4   8 4 7 , 9 6 7   6 0 . 9 8   2 , 7 3 4 , 1 6 4   1 . 5 1   T T M = 3 0 0 0 , n = 5   5 , 9 8 9 , 5 1 8   4 , 3 0 0 , 1 6 4   1 , 5 9 4 , 9 6 7   1 2 5 . 8 1   4 , 3 0 0 , 1 6 4   2 . 6 3   T T M = 2 5 0 , n = 6   5 , 7 5 5 , 6 2 8   5 , 0 8 3 , 4 3 6   6 4 1 , 5 8 1   4 5 . 7   5 , 0 8 3 , 4 3 6   3 . 5 6   T T M = 4 5 0 , n = 6   6 , 3 7 9 , 0 2 8   5 , 4 9 7 , 0 3 6   8 4 4 , 3 8 1   6 0 . 6 2   5 , 4 9 7 , 0 3 6   4 . 1 3   W l a n _ c o l l i d e   T T M = 1 0 0 0 , n = 5   2 , 8 5 1 , 6 1 9   2 , 2 1 2 , 1 6 5   6 0 1 , 0 6 7   6 5 . 9 5   2 , 2 1 2 , 1 6 5   1 . 0 4   T T M = 2 5 0 0 , n = 5   5 , 2 0 9 , 6 1 9   3 , 7 7 8 , 1 6 5   1 , 3 5 1 , 0 6 7   1 4 0 . 3 6   3 , 7 7 8 , 1 6 5   2 . 5   T T M = 2 0 0 , n = 6   5 , 6 0 0 , 2 8 0   4 , 9 8 0 , 0 3 7   5 9 1 , 3 8 2   5 4 . 8 5   4 , 9 8 0 , 0 3 7   3 . 2 6   T T M = 4 0 0 , n = 6   6 , 2 2 4 , 0 8 0   5 , 3 9 3 , 6 3 7   7 9 4 , 5 8 2   8 4 . 9 9   5 , 3 9 3 , 6 3 7   3 . 8 9       T o   c o m pa r e   t h e   o v e r a l l   ru nn i ng  t i m e   o f   pr o b a b i l i s t i c   m o de l   c h e c ki n g ,   w e   c o n s i de r   t h e   r u nni n t i m e s   of   gr a p h - b a s e c o m put a t i o n s   o f   t h e     a n   s e t s   a n t h e   ru nni n t i m e   of   t h e   i t e ra t i v e   n u m e r i c a l   m e t h o ds .   W e   s e l e c t   o n e   s a m p l e   m o de l   f r o m   e a c h   c l a s s   o f   c a s e   s t udi e s   a n p r o po s e   t h e   r e s ul t s   i F i g u r e s   t o   3.   E a c h   f i gu r e   p r e s e nt s   t h e   r u nni ng  t i m e   o f   t h e   s t a n d a r a n d   i m p r o ve m e t h o ds   fo r   c o m put i ng  t h e     a nd    s e t s .   W e   a l s o   us e   t h e   S CC - b a s e t o po l o gi c a l   a n d   t h e   l e a rn i ng - b a s e m e t h o ds   a s   t w o   w e l l - kn o w n   i m p r o v e i t e ra t i v e   g r a p h - b a s e a n n u m e r i c a l   m e t h o ds   [16 ,   19,   2 0,   23,   25] .   T h e s e   m e t h o ds   a r e   n o w   a v a i l a b l e   i n   t h e   e xpl i c i t   e n gi n e   o f   P R IS M .   F o r   t h e   Co i n   c l a s s ,   w e   s e l e c t   t w o   s a m pl e   m o de l s   t o   s t udy   t h e   i m p a c t   o f   o ur   h e u r i s t i c   o t h e   o v e r a l l   r u nni n t i m e   o f   t h e   p r o b a b i l i s t i c   m o de l   c h e c ki n g .   T h e   r e s ul t s   o f   t h e s e   f i gu r e s   s h o w   t h a t   f o r   a l l   c a s e s ,   t h e   ru nn i ng  t i m e   o f   pr o b a b i l i s t i c   m o de l   c he c ki n w i t h   o u r   h e u r i s t i c   i s   l e s s   t h a n   t h e   r u nni n g   t i m e   o t h e   o t h e r   m e t h o ds .   T h e   r e s ul t s   s h o w   t h a t   t h e   r u nni ng  t i m e s   a r e   r e duc e fo r   t h e   c o m put a t i o n s   o b o t h     a n   s e t s .   In   m o s t   c a s e s ,   t h e   t o t a l   r u nni n t i m e   o f   pr ob a b i l i s t i c   m o de l   c h e c ki ng  i s   r e duc e t o   l e s s   t h a n   50%  o f   t h e   r u nni ng  t i m e   o f   t h e   b e s t   pr e v i o us   m e t h o d,   w h i c s h o w s   a   s i g n i f i c a nt   i m p r o v e m e n t   i o ur  pr o po s e h e uri s t i c .   F o r   CS M A ( n = 3 , k = 6)  a nd  CS M A ( n = 4, k = 4),   w h i c h   i s   n o t   p r e s e nt e h e r e ,   t h e   t o t a l   r u nni ng  t i m e   i s   r e duc e t o   l e s s   t h a 1 o f   t h e   r u nni n g   t i m e   o f   t h e   b e s t   p r e v i o us   m e t h o d.           F i gu r e   1 .   R u nn i ng  t i m e s   o f   pr o b a b i l i s t i c   m o de l   c h e c ki ng  f o r   Co i s a m pl e   m o de l s       F i gu r e   2 .   R u nn i ng  t i m e s   o f   pr o b a b i l i s t i c   m o de l   c h e c ki ng  f o r   Z e r oc on f   a n d   CSM A   s a m pl e   m o de l s       Evaluation Warning : The document was created with Spire.PDF for Python.
                                IS S N :   2502 - 4752   In do n e s i a J   E l e c   E ng  &   Co m S c i ,   V o l .   18 ,   N o .   1 A p r i l   20 20  :     1571   -   1577   1576       F i gu r e   3 .   R u nn i ng  t i m e s   o f   pr o b a b i l i s t i c   m o de l   c h e c ki n f o r   w l a a n d   w l a n _c o l   m o de l s       5.   C O N C LU S I O N   T h e   pa pe r   p r o po s e a   h e uri s t i c   t o   r e duc e   t h e   r u nni n t i m e   of   pr e - c o m put a t i o n   f o r   p r o b a b i l i s t i c   m o de l   c h e c ki n o f   M D P s .   T h e   i de a   o f   t h e   p r o po s e m e t ho ds   i s ub s e c t i o n   3. 1   a n d   3 . i s   t o   r e duc e   t h e   n u m b e r   o f   i t e ra t i o n s   o f   t h e   g r a p h - b a s e p r e - c o m put a t i o n s .   E xpe r i m e nt a l   r e s ul t s   s h o w   t h a t   t h e   p r o po s e d   h e u r i s t i c   r e duc e s   t h e   r u nn i ng  t i m e s   by   s e v e r a l   o r de r s   of  m a g ni t ude   a n o ut pe r f o r m s   t h e   s t a n da rd  a n d   pr e v i o us   i m p r o v e m e t h o ds   f o r   p r o b a b i l i s t i c   m o de l   c h e c ki ng.   F o f ut u r e   w o r ks ,   o t h e p r o b a b i l i s t i c   s t r uc t u r e s   (s uc h   a s   p r o b a b i l i s t i c   t i m e a ut o m a t a   o r   s t o c h a s t i c   h y b r i a u t o m a t a c a n   b e   c o n s i de r e a n o n e   c a n   s t udy   t h e   i m p a c t   o f   t h e   p r o po s e h e u r i s t i c   o t h e   pe r f o r m a n c e   o f   m o de l   c h e c ki ng  m e t h o ds   f o r   t h e s e   s t r uc t u r e s .         R EF ER EN C ES   [ 1]   C hr i s t e l   B a i e r   a nd   J o o s t - P i e t e r   K a t o e n .   P r i nc i p l e s   o f   m o de l   c he c ki ng .   M I T   p r e s s ,   2008 .     [ 2]   M ung ka s i ,   S ud i .   F o r m a l   e xpa n s i o m e t ho f o r   s o l v i ng   a e l e c t r i c a l   c i r c ui t   m o de l .   T E L K O M N I K A   ( T e l e c om m uni c a t i on,   C om p ut i ng ,   E l e c t r o ni c s   and   C on t r ol ) ,   v o l .   17( 3) .   p p.   13 38 - 1343 ,   201 9.     [ 3]   C hr i s t e l   B a i e r ,   e t   a l . ,” P r o ba bi l i s t i c   M o de l   C he c k i ng .   D e pe ndabl e   Sof t w ar e   Sy s t e m s   E ng i ne e r i ng .   2016 ,     v o l .   45,   p p :   1 - 23.   [ 4]   V .   F o r e j t   e t   a l . ,” A ut o m a t e V e r i f i c a t i o T e c hn i qu e s   f o r   P r o ba b i l i s t i c   S y s t e m s .   I SF M   201 1,   V o l .   1 1,   pp .   53 - 113 .   [ 5]   A l o s t a d,   J a s e m   M .” I m pr o v e pr o ba bi l i s t i c   di s t a nc e   ba s e l o c a l i t y   pr e s e r v i ng   pr o j e c t i o ns   m e t ho t o   r e d uc e   di m e n s i o na l i t y   i l a r g e   da t a s e t s .   I n t e r nat i o nal   J o ur n al   of   E l e c t r i c a l   a nd  C om pu t e r   E ng i ne e r i ng   ( I J E C E ) ,   v o l .   9( 1 ) ,   pp.   59 3 - 599,   2 019 .     [ 6]   E z a t ul A km a   A bdul l a h,   S i t i M e r i a m Z a h a r i ,   S . S a r i f a hR a d i a hS ha r i f f ,   M uha m m a A s m ui   A bdul   R a hi m .   " M o de l l i ng   v o l a t i l i t y   of   K ua l a   L um pur   c om po s i t e   i n de ( K L C I )   us i ng   S V   a nd  g a r c m o de l s .   I ndone s i an  J our nal   o f   E l e c t r i c a l   E ngi ne e r i n and   C om pu t e r   Sc i e nc e   ( I J E E C S) .   V o l .   1 3( 3 ) ,   2 019 .     [ 7]   M L .   P u t e r m a n” M a r ko v   de c i s i o p r o c e s s e s :   di s c r e t e   s t o c ha s t i c   dy na m i c   pr o g r a m m i ng ,   J o hn  W i l e y   &   So ns   2014   A ug   28.   [ 8]   L a l a o ui ,   M o ha m e d ,   A bde l l a t i f   E l   A f i a ,   a nd  R a d do ua ne C h i h e b .   A   s e l f - t u ne s i m u l a t e a nn e a l i ng   a l g o r i t hm   us i ng   hi dd e m a r ko v   m o de l .   I nt e r n at i ona l   J ou r na l   o f   E l e c t r i c a l   an C om pu t e r   E n gi ne e r i ng  ( I J E C E ) ,   v o l .   8( 1 ) ,     pp.   29 1 - 298,   2 018 .   [ 9]   M a r bun ,   M u s a   P a r t a h i ,   N g a pu l i I r m e a S i ni s uk a ,   a n N a na ng H a r i y a nt o .   T he   us e   o f   M a r ko v   C ha i m e t ho t o   de t e r m i ne   s pa r e   t r a n s f o r m e r   n um be r   a n l o c a t i o n .” I n t e r nat i on al   J our na l   of   E l e c t r i c a l   an C om p ut e r   E ng i ne e r i ng   ( I J E C E ) ,   v o l .   9( 1) ,   pp .   1 - 8 ,   201 9.     [ 10]   K w i a t ko w s ka   M ,   N o r m a G ,   a n P a r ke r   D .   P R I S M   4 . 0 :   V e r i f i c at i on   of   pr obab i l i s t i c   r e al - t i m e   s y s t e m s .   I n I nt e r na t i o na l   c o nf e r e nc e   o c o m put e r   a i d e d   v e r i f i c a t i o 2011   J ul   14  ( pp .   585 - 591 ) .   S pr i ng e r ,   B e r l i n,   H e i de l b e r g .     [ 11]   D e hne r t   C ,   e t   a l . ,   A   s t or m   i s   c om i ng :   A   m ode r pr o bab i l i s t i c   m ode l   c he c k e r .   I n I nt e r n a t i o na l   C o nf e r e nc e   o n   C o m put e r   A i de d   V e r i f i c a t i o 2 017   J u l   24   ( pp.   5 92 - 600 ) .   S p r i ng e r ,   C ha m .     [ 12]   H a hn,   E r n s t   M o r i t z ,   Y i   L i ,   S v e S c he w e ,   A ndr e a   T u r r i n i ,   a nd  L i j un   Z ha ng .   I S C A S M C :   A   W e bba s e P r o ba b i l i s t i c   M o de l   C he c ke r .   I n   I nt e r na t i ona l   Sy m p os i um   on   F or m al   M e t hod s ,   pp.   31 2 - 317.   S p r i ng e r ,   C h a m ,   20 14 .     [ 13]   G .   N o r m a a nd   D .   P a r ke r .   Q ua n t i t a t i v e   v e r i f i c a t i o n :” F o r m a l   g ua r a n t e e s   f o r   t i m e l i n e s s ,   r e l i a b i l i t y   a nd  pe r f o r m a nc e .   T e c h ni c al   r e po r t ,   T he   L o ndon   M at he m at i c a l   Soc i e t y   and  t he   Sm i t I n s t i t ut e ,   20 14.     [ 14]   H a r t m a nns .   O n   t he   a n a l y s i s   o f   s t o c ha s t i c   t i m e d   s y s t e m s .   P hD   t he s i s ,   S a a r l a nd   U n i v e r s i t y ,   2015 .     [ 15]   J o a c hi m   K l e i n ,   e t   a l . ,” A dv a nc e s   i p r o ba b i l i s t i c   m o de l   c he c ki ng   w i t h   P R I S M :   v a r i a bl e   r e o r de r i ng ,   qu a n t i l e s   a nd   w e a de t e r m i n i s t i c   B c hi   a ut o m a t a .   I nt e r n at i ona l   J o ur n al   on  S of t w ar e   T ool s   f or   T e c h nol ogy   T r ans f e r ,   v o l .   20 ( 2) ,   pa g e s   179 - 194 .   201 8.     [ 16]   M a t e u s z   U j m a .   O V e r i f i c a t i o a n C o nt r o l l e r   S y nt he s i s   f o r   P r o ba bi l i s t i c   S y s t e m s   a t   R unt i m e   P hD   t he s i s ,   U ni v e r s i t y   o f   O xf o r d,   201 5.     [ 17]   G ul ds t r a nd  L a r s e n .   S t a t i s t i c a l   M o de l   C he c ki ng   t he   20 18  E d i t i o n!   I n :   M a r g a r i a   T . ,   S t e f f e B .   ( E ds )   L e v e r a g i ng   A ppl i c a t i o ns   o f   F o r m a l   M e t ho ds ,   V e r i f i c a t i o a nd  V a l i da t i o n.   V e r i f i c a t i o n.   I S oL A   2018.   L e c t ur e   N o t e s   i n   C o m put e r   S c i e nc e ,   v o l   1 1245 .   Spr i n ge r ,   C ha m .     Evaluation Warning : The document was created with Spire.PDF for Python.
In do n e s i a J   E l e c   E ng  &   Co m S c i     IS S N :   2502 - 4752       Im pr ov i ng   gr aph - bas e d   m e t hods   f or   c om p ut i ng  qual i t a t i v e   p r ope r t i e s   o f   ( Moham m ads a de gh   Mo hagh e ghi )   1577   [ 18]   L uc a   D e   A l f a r o .   F o r m a l   v e r i f i c a t i o o f   p r o ba bi l i s t i c   s y s t e m s .   P h D   t h e s i s ,   S t a nf o r U n i v e r s i t y ,   19 97 .     [ 19]   C hr i s t e l   B a i e r ,   e t   a l . ,” E ns u r i n t he   r e l i ab i l i t y   o f   y o ur   m o de l   c h e c k e r :   I n t e r v a l   i t e r at i o f o r   M ar k ov   D e c i s i on   P r oc e s s e s .   I I nt e r na t i o na l   C o nf e r e nc e   o C o m put e r   A i de d   V e r i f i c a t i o n,   pp.   1 60 - 180 .   S pr i ng e r ,   C ha m ,   2 017 .     [ 20]   M ,   K w i a t ko w s k a   e t   a l . ,” I nc r e m e nt al   qua nt i t at i v e   v e r i f i c a t i on  f o r   M ar k ov   de c i s i on  pr o c e s s e s .   I n   D e pe nda bl e   S y s t e m s   &   N e t w o r ks   ( D S N ) ,   2 011   I E E E / I F I P   41s t   I nt e r na t i o na l   C o nf e r e nc e   o 201 J un   27   ( pp .   359 - 370 ) .   I E E E .     [ 21]   C ha t t e r j e e   K ,   L a c ki   J .   F as t e r   al g or i t hm s   f or   M ar k ov   de c i s i on  pr oc e s s e s   w i t l ow   t r e e w i dt h .   I I nt e r na t i o na l   C o nf e r e nc e   o C o m put e r   A i de d   V e r i f i c a t i o 2 013   J u l   13   ( pp.   5 43 - 5 58) .   S pr i ng e r ,   B e r l i n ,   H e i de l b e r g   [ 22]   H a dda d ,   S e r g e ,   a nd  B e n j a m i M o nm e g e .   I nt e r v a l   i t e r a t i o a l g o r i t hm   f o r   M D P s   a nd  I M D P s .   T h e o r e t i c a l   C om put e r   Sc i e nc e ,   735   ( 2018 ) :   111 - 131 .     [ 23]   K l e i n,   J o a c hi m ,   C hr i s t e l B a i e r ,   P h i l i pp   C hr s z o n,   M a r c us   D a um ,   C l e m e ns   D ubs l a f f ,   S a s c ha K l pp e l ho l z ,   S t e f f e n   M R c ke r ,   a nd  D a v i M l l e r .   A dv a nc e s   i pr o ba b i l i s t i c   m o de l   c he c ki ng   w i t P R I S M :   v a r i a bl e   r e o r de r i ng ,   q ua n t i l e s   a nd  w e a de t e r m i n i s t i c   B c hi   a ut o m a t a .   I n t e r na t i ona l   J ou r na l   on   Sof t w ar e   T ool s   f or   T e c hno l ogy   T r an s f e r ,   v o l .   20( 2 ) ,   p p.   17 9 - 194,   2 018 .     [ 24]   M a t e e s c u,   R a du ,   a n J o s   I g na c i R e que no .   O n - t h e - fl y   m o de l   c he c ki ng   f o r   e xt e nde a c t i o nba s e p r o ba bi l i s t i c   o pe r a t o r s .   I nt e r n at i on al   J o ur n al   on   So f t w ar e   T oo l s   f o r   T e c hno l og y   T r a ns f e r V o l   2 0( 5 ) ,   p p.   56 3 - 587 ,   2 018 .     [ 25]   W a ng ,   J i ng y i ,   J un  S un,   Q i xi a   Y ua n ,   a nd  J u P a ng .   L e a r ni ng   pr o ba bi l i s t i c   m o de l s   f o r   m o de l   c h e c ki ng:     a e v o l ut i o na r y   a ppr o a c a nd  a e m p i r i c a l   s t udy .   I n t e r na t i on al   J ou r na l   o S of t w ar e   T ool s   f o r   T e c hn ol ogy   T r ans f e r V o l   20( 6) ,   pp .   689 - 704 ,   201 8.     [ 26]   E r ns t   M o r i t z ,   e t .   a l .” T he   201 c o m pa r i s o o f   t oo l s   f o r   t he   a na l y s i s   o f   qua nt i t a t i v e   f o r m a l   m o de l s .   I I nt e r nat i ona l   C onf e r e nc e   on  T oo l s   and  A l g or i t hm s   f or   t he   C ons t r u c t i on   an A na l y s i s   o f   S y s t e m s ,   pp.   69 - 92 .   S pr i ng e r ,     C ha m ,   201 9.     [ 27]   V o E s s e n ,   C hr i s t i a n ,   B a r b a r a   J o bs t m a n n,   D a v i P a r ke r ,   a n R a hu l   V a r s hne y a .   S y nt he s i z i ng   e f f i c i e n t   s y s t e m s   i n   pr o ba bi l i s t i c   e nv i r o nm e n t s .   A c t a I nf or m a t i c a ,   v o l   53 ( 4 ) ,   pp .   425 - 4 5 7,   201 6.     [ 28]   M o ha m m a ds a de g M o ha g he g hi ,   J a be r   K a r i m po ur ,   A y a z   I s a z a de h,   P r i o r i t i z i ng   M e t ho ds   t o   A c c e l e r a t e   P r o ba bi l i s t i c   M o de l   C he c k i ng   o f   D i s c r e t e - T i m e   M a r ko v   M o de l s ,   T he   C om put e r   J our nal ,   201 9.         B I O G R A P H I ES   O F   A U T H O R S       M o ha m m a ds a de g M o ha g he g hi   r e c e i v e d   h i s   P h. D   i c o m put e r   s c i e nc e   f r o m   U n i v e r s i t y   o f   T a br i z   i 2 019 ,   M s   i c o m put e r   s c i e nc e   f r o m   S ha r i f   uni v e r s i t y   of   t e c hno l ogy   i 2008  a nd  B s   i s o f t w a r e   e ng i ne e r i ng   f r o m   S ha hi dbe h e s h t y   uni v e r s i t y   i 2006 .   H e   i s   c uur e nt l y   a   f a c ul t y   m e m be r   o f   c o m put e r   s c i e nc e   i V a l i - e - a s r   un i v e r s i t y   o f   R a f s a nj a n ,   I r a n.   H i s   m a i r e s e a r c h   i nt e r e s t s   i nc l ude   f o r m a l   v e r i f i c a t i o o f   s t oc ha s t i c   a nd  r e a l - t i m e   s y s t e m s ,   pr o ba b i l i s t i c   m o de l   c he c ki ng   a nd   m a c hi n e   l e a r n i ng .         K ha y y a m   S a l e h i   r e c e i v e h i s   M . S c .   de g r e e   i C o m put e r   S c i e nc e   f r o m   S ha r i f   U n i v e r s i t y   o f   T e c hno l o gy   i 2010  a n hi s   P h . D .   i C o m put e r   S c i e nc e   a t   U ni v e r s i t y   of   T a br i z   i 2019 .     H i s   r e s e a r c i nt e r e s t s   i nc l ud e   qu a n t i f i c a t i o o f   i nf o r m a t i o l e a ka g e ,   f o r m a l   m e t ho ds ,   a n A I   i c o m put e r   s e c ur i t y .       Evaluation Warning : The document was created with Spire.PDF for Python.