（计算机应用技术专业论文）框架时序逻辑程序语言msvl的形式语义.pdf

摘要 摘要 形式语义是对软件系统进行形式化验证和分析的重要理论基础。程序语言的语 义可以帮助人们更好的理解、执行、分析软件系统。操作语义有助于语言的实现，公 理语义有利于程序的验证，指称语义在强大的数学理论支持下为程序的含义提供了精 确的数学描述。 时序逻辑程序设计是一种新型的程序设计范式，程序的具体执行和性质的描述可 以在同一逻辑框架内表示，适用于并发系统的建模、模拟和验证。尽管研究人员开发 了相关的解释器来执行各类时序逻辑程序语言，时序逻辑及其可执行子集被广泛地应 用于系统的规范和验证中，但是到目前为止，至少在区间时序逻辑程序语言中，还没 有一套系统而完整的形式语义。本文以区间时序逻辑程序语言m s v l 为研究对象，分 别从模型语义、操作语义、公理语义三条主线来研究区间时序逻辑程序的形式语义， 并对三种语义之间的一致性、互补性进行分析和证明。 本文研究了m s v l 语言的极小模型语义。由于m s v l 语言中的框架技术破坏了逻辑 的单调性，传统的规范模型已不再适用于捕获该语言的模型语义。因此，我们提出了 极小模型理论并证明了极小模型的存在性定理。 为了正确理解程序语言的执行过程，本文研究了m s v l 语言的结构化操作语义。 首先定义了一种新的适用于描述区间时序逻辑程序语言语义的表达式格局和命令格 局。其次给出了带有时态操作符的算术表达式和布尔表达式的求值规则，以及程序的 状态迁移系统和区间迁移系统。状态迁移系统包括将一个程序化简为与其等价的正则 形的语义等价规则和状态上的迁移规则。区间迁移系统给出了将程序从一个状态迁移 到下一个状态的区间迁移规则。进一步，我们研究了两类迁移系统的性质，并证明了 操作语义和基于模型理论的极小模型语义之间的一致性。最后基于本文提出的操作语 义，开发了具有对软硬件系统进行建模、模拟和验证功能的m s v l 语言的解释器。 为了实现在同一逻辑框架内对并发系统进行建模和验证的目的，本文研究 了m s v l 语言的公理语义。在该方法中，m s v l 语言作为程序设计语言来描述系统行为 ( 系统建模) ，命题投影时序逻辑作为断言语言描述系统性质。这样，系统的模型和 性质的规范可以用同一逻辑记号表示，简化了验证在不同形式化记号之间转换的复杂 过程。进一步，我们给出将程序推演为正则形的状态公理和状态推演规则以及程序在 区间上的公理和推演规则，这些规则在将程序从一种状态转换到另一种状态的同时实 现程序性质的验证。另外，基于m s v l 语言的操作语义，我们证明了该公理系统的可 靠性和相对完备性。最后，使用该语言的公理语义对一个应用实例的完全正则性质进 行了形式化验证。 关键词：时序逻辑程序设计框架极小模型操作语义公理语义 a b s t r a c t f o rv e r i f i c a t i o na n d a n a l y s i so fs o f t w a r e i sa ni m p o r t a n tt h e o r e t i c a lf o u n d a t i o n sa n d s y s t e m si nar i g o r o u sw a y , f o r m a ls e m a n t i c s a l le s s e n t i a lp r e r e q u i s i t e t h es e m a n t i c so f p r o g r a m m i n gl a n g u a g e se n a b l eu st ou n d e r s t a n d ，e x e c u t ea n da n a l y z eas o f t w a r es y s - t e m o p e r a t i o n a ls e m a n t i c sc a nh e l pu st oi n t e r p r e ta n de x e c u t ea l a n g u a g e ，a x i o m a t i c s e m a n t i c sh a sg r e a tf a c i l i t yi nv e r i f i c a t i o n ， f o r m a l i s mf o rs e m a n t i cs p e c i f i c a t i o n s a n dd e n o t a t i o n a ls e m a n t i c so f f e r sap o w e r f u l 上m p o r a ll o g i cp r o g r a m m i n gi san e wp a r a d i g mf o rd e s c r i b i n gc o n c u r r e n ts y s t e m s i nw h i c ht h ei m p l e m e n t a t i o no fs y s t e m sa n d p r o p e r t yo fs y s t e m sc a nb es p e c i f i e di no n e l o g i c t h o u g hr e s e a r c h e r sd e v e l o p e di n t e r p r e t e r st oe x e c u t et e m p o r a ll o g i cp r o g r a 加【s ， a n dt e m p o r a ll o g i ca n di t se x e c u t e ds u b s e t sa r ew i d e l ya p p l i e d t ot h ea r e a so fc o n c u r r e i l t p r o g r a m sv e r i f i c a t i o n ，h o w e v e r ，t h e r eh a sn o tf o r m a l i z e da ni n t e g r a t e df o r m a ls e m a n t i c s f o rt e m p o r a ll o g i cp r o g r a m s ，a tl e a s tf o ri n t e r v a lt e m p o r a l l o g i cp r o g r a m m i n g1 a n g u a g e s l 。h e r e i b r e ，w ea r em o t i v a t e dt oi n v e s t i g a t et h ef o r m a ls e m a n t i c so fi n t e r v a lt e m p o r a ll o g i c p r o g r a m m i n gl a n g u a g em s v l ，i n c l u d i n gi t sm i n i m a lm o d e l ，o p e r a t i o n a la n d ( i o m a t i c s e m a n t i c s t h i st h e s i sf i r s ti n v e s t i g a t e st h em i n i m a lm o d e ls e m a n t i c so fm s v l s i n c e f r a 】一 1 n gd e s t r o y sm o n o t o n i c i t y ，c a n o n i c a lm o d e l su s e dt od e f i n et h es e m a n t i c so fn o n 仔剐 n e d p m g r a m sa r en ol o n g e ra p p r o p r i a t e t od e a lw i t ht h i s am i n i m a lm o d e lt h e o r yi sd e v e l - o p e d b yw h i c ht h et e m p o r a ls e m a n t i c so fm s v lp r o g r a m si sc a p t u r e d t h ee 1 ) d s t e n c e o fam i n i m a lm o d e lf o rag i v e nf r a m e dp r o g r a m i sp r o v e d t h i st h e s i st h e ni n v e s t i g a t e st h eo p e r a t i o n a ls e m a n t i c so fm s v l an e wc o n 6 毋l - r a t i o nw i t hi n t e r v a l sf o rm s v lp r o g r a m si sd e f i n e d t h ee v a l u a t i o nr u l e sf o rb o t ht h e a r i t h m e t i ca n db o o l e a ne x p r e s s i o n sw i t ht e m p o r a lo p e r a t o r sa r ed e f i n e d t h es e m a n t i c e q u i v a l e n c er u l e sf o rt h er e d u c t i o no fap r o g r a mw i t h i nas t a t ei sf o 咖a l i z e d n l r t h e 卜 m o r e ，t n et r a n s i t i o nr u l e sw i t h i nas t a t ea n dt r a n s i t i o nr u l e so v e ra ni n t e r v a lb e t w e e n c o n f i g u r a t i o n sa r ea l s os p e c i f i e d t h u s ，t h ee x e c u t a b l eb e h a v i o ro ff r a m e dp r o g r a 脚c a i l b ec a p t u r e di na no p e r a t i o n a lw a y i n a d d i t i o n ，t h ec o n s i s t e n c yb e t w e e nt h eo p e r a t i o n a l l s e m a n t i c sa n dt h em i n i m a lm o d e ls e m a n t i c sb a s e do nm o d e l t h e o r yi sp r o v e di nd e t a i l b a s e do nt h eo p e r a t i o n a ls e m a n t i c sp r o p o s e di nt h i st h e s i s ，a ni n t e r p r e t e rf o r m o d e l i n g ， s i m u l a t i n ga n dv e r i f y i n gc o n c u r r e n ts y s t e m s ，h a sb e e nd e v e l o p e d t h i r d l y , f o rt h ep u r p o s eo fv e r i f y i n gt h ep r o p e r t i e so fc o n c u r r e n td r o g r a n l si na u n i f i e dn o t a t i o n ，t h i st h e s i si n v e s t i g a t e st h ea x i o m a t i c8 e m a n t i c so fm s v l w i t ht h i s m e t h o d ，as y s t e mi sf i r s tm o d e l e du s i n gm s v l l a n g u a g e f u r t h e r ，ap r o p e r t yo ft h es y s - i v f o r m a ls e m a n t i c so ff r a m e d t e m p o r a l l o g i c p r o g r a m m i n gl a n g u a g em s v l t e mi ss p e c i f i e db yp r o p o s i t i o n a lp r o j e c t i o nt e m p o r a ll o g i c ( p p t l ) t h u s ，t h em o d e l a n dp r o p e r t yo fas y s t e ma r ew r i t t e ni nt h es a m el o g i cp r o j e c t i o nt e m p o r a ll o g i c ( p t l ) m o r e o 、，e r as e to fs t a t ea 对o l sa n ds t a t ei n f e r e n c er u l e si sg i v e nt od e d u c eap r o g r a m i n t oi t sn o r m a lf o r m ，a n da s e to fa x i o m sa n di n f e r e n c er u l e so v e ri n t e r v a l si sf o r m a l i z e d t ot r a i l s f 0 珊ap r o g r a mf r o mo n es t a t et oa n o t h e r i na d d i t i o n ，af o r m a lp r o o fo f t h e s o u n d n e s sa n dr e l a t i v ec o m p l e t e n e s so ft h es y s t e mw i t hr e s p e c tt oa l lo p e r a t i o n a l m o d e i o fm s v li sg i v e n f i n a l l y , a ne x a m p l ei sg i v e nt oi l l u s t r a t eh o wt ou s et h ea x i o m a t l c s y s t e mt op r o v ea f u l lr e g u l a rp r o p e r t yo fp r o g r a m s k e y w o r d ：t e m p o r a ll o g i cp r o g r a m m i n g f r a m i n g m i n i m a lm o d e lo p e r _ a t i o n a ls e m a n t i c s a x i o m a t i cs e m a n t i c s l i s to ff i g u r e si x f i g 1 1 f i g 1 2 f i g 2 1 f i g 2 2 f i g 2 3 f i g 2 4 f i g 2 5 f i g 3 1 f i g 4 1 f i g 5 1 f i g 5 2 f i g 5 3 f i g 5 4 f i g 5 5 f i g 6 1 f i g 6 2 f i g 6 3 l i s to ff i g u r e s af l o w c h a r tf o rt h es e q u e n t i a ls t a t e m e n t t e m p o r a ll o g i cp r o g r a m m i n gl a n g u a g e s ap r o j e c t e di n t e r v a l i n t e r p r e t a t i o no fp p t lf o r m u l a s i n t e r p r e t a t i o no fp t l t e r m s i n t e r p r e t a t i o no fp t l f o r m u l a s d e r i v e dp t lf o r m u l a s p o s s i b l ee x e c u t i o n so fp l ，p 2 ，p 3 ) p r jq n f gf o rm s v lp r o g r a m s 。 t h er e l a t i o n s h i pb e t w e e n 盯a n d 鼠 i n t e r f a c eo fm s v li n t e r p r e t e r t h r e em o d e si nm s v li n t e r p r e t e r s i m u l a t i o no fp r o gv ii m o d e l i n go fp r o gv i i d e d u c t i o nt r e eo fp r o g r a mp p s e u d oc o d ef o rt w op r o c e s s e saa n dbc o m p e t i n gf o r as h a r e dr e s o u r c e ak r i p k es t r u c t u r ef o rt w op r o c e s s e st h a tp r e s e r v e m u t u a le x c l u s i o n p 3 p 9 p 1 6 p 1 7 p 1 8 p 1 9 p 2 1 p 3 1 p 5 0 p 5 8 p 8 4 p 8 4 p 8 5 p 8 5 p 1 0 6 p 1 0 9 p 1 0 9 l i s to ft a b l e s x i t a b l e2 1 t a b l e2 2 t a b l e3 1 t a b l e4 1 t a b l e5 1 t a b l e5 2 t l a b l e5 3 t a b l e5 4 t a b l e5 5 t a b l e5 6 t a b l e6 1 t a b l e6 2 t a b l e6 3 t a b l e6 4 t l a b l e6 5 t i a b l e6 6 t a b l e6 7 l i s to ft a b l e s p t ll a w si p t ll a w si i 纾仍i l el a w s 。 f r a m i n gl a w s e v a l u a t i o nr u l e so fa r i t h m e t i ce x p r e s s i o n s e v a l u a t i o nr u l e so fb o o l e a ne x p r e s s i o n s s e m a n t i ce q u i v a l e n c er u l e so ff l a m e dp r o g r a m s s e m a n t i ce q u i v a l e n c er u l e so ft r u t hv a l u e s t r a n s i t i o nr u l e sw i t h i nas t a t e i n t e r v a lt r a n s i t i o nr u l e s s t a t ea x i o m s s t a t ei n f e r e n c er u l e s a x i o m so v e ri n t e r v a l s a ni n t e r v a ls u b s t i t u t i o nr u l e a s s i g n m e n ts t a t e m e n t sr u l e s t e m p o r a l n e x t a n d e m p t y r u l e s s e l e c t i o ns t a t e m e n ta n de x i s t e n t i a lq u a n t i f i c a t i o nr u l e s p 2 3 p 2 4 p 3 2 p 3 9 p 5 9 p 6 0 p 6 1 p 6 2 p 6 3 p 7 1 p 8 8 p 8 9 p 9 9 p 9 9 p 1 0 0 p 1 0 1 p 1 0 2 西安电子科技大学 学位论文独创性( 或创新性) 声明 秉承学校严谨的学风和优良的科学道德，本人声明所呈交的论文是我个人在 导师指导下进行的研究工作及取得的研究成果。尽我所知，除了文中特别加以标 注和致谢中所罗列的内容以外，论文中不包含其他人已经发表或撰写过的研究成 果；也不包含为获得西安电子科技大学或其它教育机构的学位或证书而使用过的 材料。与我一同工作的同志对本研究所做的任何贡献均已在论文中做了明确的说 明并表示了谢意。 申请学位论文与资料若有不实之处，本人承担一切的法律责任。 本人签名：互蝴 日期兰! ! 乏堑：f 西安电子科技大学 关于论文使用授权的说明 本人完全了解西安电子科技大学有关保留和使用学位论文的规定，即：研究 生在校攻读学位期间论文工作的知识产权单位属西安电子科技大学。学校有权保 留送交论文的复印件，允许查阅和借阅论文；学校可以公布论文的全部或部分内 容，可以允许采用影印、缩印或其它复制手段保存论文。同时本人保证，毕业后 结合学位论文研究课题再攥写的文章一律署名单位为西安电子科技大学。 ( 保密的论文在解密后遵守此规定) 本学位论文属于保密，在一年解密后适用本授权书 本人签名盈互竭涌 导师签名： 歹一 业学差 c h a p t e r1 i n t r o d u c t i o n t h ec o r r e c t n e s so fs o f t w a r eh a sl o n gb e e nag r a n dc h a l l e n g ei nc o m p u t e rs c i e n c ef s 4 i np r a c t i c e ，s i m u l a t i o na n dt e s t i n ga r e w i d e l ya p p l i e dt oe v a l u a t et h eq u a l i t yo fs o f t w a r e ， b u tt h e ya r eq u i t ei n a d e q u a t et oe n s u r et h ec o r r e c t n e s s m a n yr e s e a r c h e r sb e l i e v et h a t i n t r o d u c i n gm o r em a t h e m a t i c a la p p r o a c hc a ni m p r o v et h es o f t w a r ed e v e l o p m e n tp r o c e s s a n dt h e r e b yy i e l ds o f t w a r ew i t hb e t t e rs t r u c t u r e ，g r e a t e r m a i n t a i n a b i l i t ya n df e w e re r r o r s 【8 5 】i nc o m p u t e rs c i e n c ea n ds o f t w a r ee n g i n e e r i n g ，m a t h e m a t i c a l l y - b a s e dt e c h n i q u e sf o r d e v e l o p i n gs o f t w a r es y s t e m sa r ec a l l e df o r m a lm e t h o d s f o r m a lm e t h o d se m b r a c et w ot e c h n i q u e sf 2 1 - 2 6 ，o n ei sf o r m a ls p e c i f i c a t i o na n dt h e o t h e ri sf o r m a lv e r i l z c a t i o n b o t ha r ee s t a b l i s h e do ne l e m e n t a r ym a t h e m a t i c s ，s u c ha ss e t t h e o r y , l o g i ca n da l g e b r a i ct h e o r y f o r m a ls p e c i f i c a t i o nd e s c r i b e sw h a tas y s t e ms h o u l d d o ，o f t e nw r i t t e ni nal a n g u a g ew i t hf o r m a ls y n t a xa n ds e m a n t i c s f o r m a lv e r i f i c a t i o n i sa na p p r o a c ht op r o v et h a ta s y s t e mo p e r a t e sc o r r e c t l y 2 6 ，2 7 ，3 1 t h eb a s i ci d e a i nf o r m a lv e r i f i c a t i o ni st oc o n s t r u c taf o r m a lm o d e lt od e s c r i b et h ep o s s i b l eb e h a v i o r o fas y s t e m b e s i d e s ，t h ed e s i r a b l eb e h a v i o ro ft h es y s t e mi sr e p r e s e n t e di naf o r m a l s p e c i f i c a t i o n b a s e do nt h e s et w of o r m a l i s m so n ec a nc h e c kb yf o r m a lp r o o fw h e t h e r t h ep o s s i b l eb e h a v i o rs a t i s f i e st h ed e s i r e dr e q u i r e m e n t s n o w a d a y s ，t h em o s tc o m m o n l y u s e df o r m a lv e r i f i c a t i o nm e t h o d sa r em o d e lc h e c k i n ga n dt h e o r e mp r o v i n g 【1 4 5 ，1 4 6 h o w e v e r ，f o rc a r r y i n go u tt h ev e r i f i c a t i o na n da n a l y s i so fs o f t w a r es y s t e m si na r i g o r o u sw a y , f o r m a ls e m a n t i c so fp r o g r a m m i n gl a n g u a g e si sa ni m p o r t a n tt h e o r e t i c a l f o u n d a t i o na n da ne s s e n t i a lp r e r e q u i s i t e 1 1f o r m a ls e m a n t i c sm e t h o d o l o g i e s t h es t u d yo fl a n g u a g e sc a nb ep a r t i t i o n e di n t os y n t a xa n ds e m a n t i c s ；h e i n zz e - m a n e ka p p l i e dt h e s et e r m i n o l o g i e st op r o g r a m m i n gl a n g u a g e si n 【3 9 t h es y n t a xi s c o n c e r n e dw i t ht h eg r a m m a t i c a ls t r u c t u r eo fp r o g r a m s ，w h i c hi st h ea l p h a b e to fs y m - b o l sa n daf o r m a ld e s c r i p t i o no ft h ew e l l - f o r m e de x p r e s s i o n sa n d p r o g r a m s b a c k u s - n a u r f o r m ( b n f ) w a st h ef i r s tm a t h e m a t i c a lt o o lf o rp r e c i s e l ys p e c i f y i n gt h es y n t a xo fp r o - g r a m m i n gl a n g u a g e s ，w h i c hw a si n t r o d u c e db yj o h nb a c k u si n1 9 5 9t od e s c r i b et h e a l g o l5 8l a n g u a g e ，a n de n h a n c e db yp e t e rn a u ra n du s e dt od e f i n ea l g o l 6 0 3 8 1 e v e nt o d a yi t i ss t i l lt h em o s tp o p u l a rn o t a t i o nu s e dt od e f i n et h el a n g u a g es y n t a x o t h e rf o r m a ln o t a t i o n st od e f i n et h es y n t a xs u c ha sr e g u l a re x p r e s s i o n s ，c o n t e x tf r e e g r a m m a r s 4 9 ，5 0 】a r ew i d e l ya p p l i e da sw e l l b yc o n t r a s t ，t h es e m a n t i c so fap r o g r a m m i n gl a n g u a g e ，w h i c hi st h em e a n i n go f t h a tl a n g u a g e ，w a ss p e c i f i e di n f o r m a l l yf o rm a n yy e a r s b e c a u s ee f f e c t i v et e c h n i q u ef o r p r e c i s e l ys p e c i f y i n gt h er u n - t i m eb e h a v i o ro fp r o g r a m sh a v eb e e np r o v e dm u c hh a r d e r t od e v e l o p 【3 7 i ti sf o rt h i sr e a s o nt h a tap r o g r a m m i n gl a n g u a g e sd o c u m e n t a t i o n v e r yo f t e ng i v e so n l yi n f o r m a ld e f i n i t i o n so ft h em e a n i n go ft h ev a r i o u sc o n s t r u c t s ， s u p p o r t e db yd i f f e r e n tn o t a t i o n s ，p s e u d oc o d ef r a g m e n t s ，a n de v e nn a t u r a ll a n g u a g e s t h i ss i t u a t i o nc a u s e dp r o b l e m sf o rt h el a n g u a g eu s e r sa n dl a n g u a g ec o m p i l e rd e v e l o p e r s b e c a u s eo ft h ea m b i g u i t i e sa n di n c o n s i s t e n c i e s t h e r e f o r e ，i ti sn e c e s s a r yt og of u r t h e r a n dg i v eaf u l lf o r m a l ，m a t h e m a t i c a ld e f i n i t i o no fal a n g u a g e ss e m a n t i c s s o m eo ft h e r e a s o 璐f o rt h ef o r m a ls e m a n t i c sa r es u m m a r i z e da sf o l l o w s i tc a nr e v e a la m b i g u i t i e sa n ds u b t l ec o m p l e x i t i e si np r o g r a m m i n gl a n g u a g ec o n - s t r u c t s i tc a nf o r mt h eb a s i sf o ri m p l e m e n t a t i o n ，a n a l y s i sa n dv e r i f i c a t i o n i tc a np r o v i d eau s e f u lu s e rd o c u m e n t a t i o n at r a i n e dp r o g r a m m e rc a nr e a da f 6 r m a ls e m a n t i c sd e f i n i t i o na n du s ei ta sar e f e r e n c et oa n s w e rq u e s t i o n sa b o u tt h e l a n g u a g e i tc a ns u g g e s tu s e f u ln e wp r o g r a m m i n gs t y l e s ，e g ，c h u r c h sl a m b d ac a l c u l u so n f u n c t i o n a lp r o g r a m m i n g i nt h e o r e t i c a lc o m p u t e rs c i e n c e ，f o r m a ls e m a n t i c si saf o r m a lw a yo rm e t h o dt o d e f i n et h em e a n i n go fap r o g r a m m i n gl a n g u a g e t h e r ea r em a n ya p p r o a c h e st of o r m a l s e m a n t i c s ，w h i c hb e l o n gt ot h r e em a j o rc l a s s e sd i s c u s s e db e l o w 1 1 1 o p e r a t i o n a ls e m a n t i c s i na no p e r a t i o n a ls e m a n t i c s ，w ea r ec o n c e r n e dw i t hh o wt oe x e c u t ep r o g r a m s m o r e p r e c i s e l y w e 甜ei n t e r e s t e di nh o wt h es t a t e sa r em o d i f i e dd u r i n gt h ee x e c u t i o no ft h e s t a t e m e n t s t h ef i r s tr i g o r o u sa n ds y s t e m i cr e p r e s e n t a t i o no ft h i si d e ai sp r o p o s e db yp e t e r l a n d i n 8 7 - 9 0 ，w h e r ea na b s t r a c tm a c h i n e ( c a l l e ds e c d ) a n das e to fo p e r a t i o n so n t h i sm a c h i n ea r ed e f i n e d i nt h e1 9 6 0 s ，t h ei b mv i e n n al a b o r a t o r y 【9 2 】d e f i n e da n a b s t r a c ti n t e r p r e t i n gm a c h i n ef o rp l il a n g u a g eu s i n gv d l ，a sw e l lk n o w nv i e n n a d e f i n i t i o nl a n g u a g e 【9 1 a r o u n dt h ey e a ro f1 9 8 0 ，am o r ee f f e c t i v ea p p r o a c ht od e f i n e t h eo p e r a t i o n a ls e m a n t i c sc a m ei n t ob e i n g ，n a m e ds t r u c t u r a lo p e r a t i o n a ls e m a n t i c s ( s o s ) ，p i o n e e r e db yg o r d o np l o t k i n 【9 3 ，1 0 6 t h a n k st o i t si n t u i t i v ea n dc o n c i s e l o o k s o sh a sg a i n e dg r e a tp o p u l a r i t ya n dh a sb e c o m ead ef a c t os t a n d a r di nd e f i n i n g o p e r a t i o n a ls e m a n t i c s t h eb a s i ci d e ai ns o si st od e f i n et h eb e h a v i o ro fap r o g r a mi nas t r u c t u r a lw a y , w h i c hm e a r l i st h a tt h eb e h a v i o ro fap r o g r a mi sb u i l tu pi n d u c t i v e l yi nt e r m so ft h e b e h a v i o ro fi t sp a r t s t h es o sd e f i n e st h eb e h a v i o ro fap r o g r a mb a s e do nt r a n s i t i o n s y s t e m s at r a n s i t i o ns y s t e mi ss p e c i f i e db yas e to fc o n f i g u r a t i o n sca n dab i n a r y r e l a t i o n _ sc c t h e r ea r et w ot y p e so fc o n f i g u r a t i o n s ： 1 ( s ，s ) r e p r e s e n