（计算机软件与理论专业论文）公式时钟自动机——一种新的形式化验证工具.pdf

公式时钟自动机一种新的形式化验证工具 摘要 在计算机科学领域内，自动机是分析模拟许多现象的有力工具，特别是在 并行有限状态系统中，自动机理论有着较重要的地位。但它只能描述系统的事 件发生的先后次序关系，而不能精确表达事件发生之间的时间延迟及实时需求。 为了捕捉实时系统的行为的实时需求，人们提出了时问自动机。时间自动机是 在自动机中加入时间信息，它常用来模拟实时系统的行为。对实时系统进行验 证就是检验系统的实现是否满足其属性需求。假设系统的实现用时间自动机a i 建模，其属性需求用时问自动机a s 建模。为了进行验证我们只需判断a l 所识 别的语言是否包含在氏所识别的语言中。若a s 是确定的时间自动机，此问题 是p s p a c e 完全的，然而，若a s 是非确定的，则此问题是不可判定的。 本文在对时间自动机进行深入研究的基础上，提出了公式时钟自动机。在 公式时钟自动机中，每一个事件对应一个命题、并且针对给定命题集上的每个 线性命题时态逻辑公式，我们定义两个时钟：公式记录时钟与公式预测时钟。 前者记录公式最近一次被满足时距目前的时间，后者预测下一次公式将被满足 时距目前的时间。然后讨论了公式时钟自动机的确定性和非确定性，公式时钟 自动机识别的语言类在并、交、补运算下的封闭性；并证明了确定的公式时钟 自动机和非确定的公式时钟自动机表达能力的等价性，这意味这每一个非确定 的公式时钟自动机都能转换为一个与之识别相同时间语言的确定的公式时钟自 动机；我们将时间字扩展为无穷的，从而定义了公式时钟b q c h i 自动机与公式 时钟m u l l e r 自动机；最后给出了用它进行实时系统的形式化验证方面及对实时 系统建模的应用。 关键字：公式记录时钟公式预测时钟时态算子时间字 公式时钟自动机一种新的形式化验证工具 a b s t r a c t f i n i t ea u t o m a t aa r ei n s t r u m e n t a lf o rt h em o d e l i n ga n da n a l y s i so fm a n y p h e n o m e n o nw i t h i nc o m p u t e rs c i e n c e i np a r t i c u l a r , a u t o m a t at h e o r yp l a y sa n i m p o r t a n tr o l ei nt h ev e r i f i c a t i o no fc o n c u r r e n tf i n i t e s t a t es y s t e m s b u ti tc a no n l y d e s c r i b et h es e q u e n c eb yw h i c ht h ee v e n t so fs y s t e mh a p p e n i tc a n te x a c t l y e x p r e s st h ed e l a yb e t w e e nv a r i o u se v e n t sa n dt h et i m e dr e q u i r e m e n t s i no r d e rt o c a p t u r et h et i m e dr e q u i r e m e n t so fr e a l - t i m es y s t e m sb e h a v i o r s ，p e o p l ep r o p o s e d t i m e da u t o m a t a t i m e da u t o m a t ai so b t a i n e db ya d d i n gan o t i o no ft i m e1 0a u t o m a t a a n do f t e nb e i n gu s e dt om o d e lt h eb e h a v i o r so fr e a l t i m es y s t e m v e r i f i c a t i o no fa r e a l t i m es y s t e mc o n s i s t si nc h e c k i n gw h e t h e rt h ei m p l e m e n t a t i o no ft h es y s t e m s a t i s f i e sas e to fr e q u i r e dp r o p e r t i e s w eu s et i m e da u t o m a t aa it om o d e lt h e i m p l e m e n t a t i o na n da st om o d e lt h ep r o p e r t i e s i no r d e rt ov e r i f y , w eo n l yn e e dt o d e c i d ew h e t h e rt h el a n g u a g ea c c e p t e db ya ii sc o n t a i n e di nt h el a n g u a g ea c c e p t e db y a s i fa si sd e t e r m i n i s t i c ，t h ep r o b l e mc a nb es o l v e di np s p a c e ，h o w e v e r , i fa si s n o n d e t e r m i n i s t i c ，t h ep r o b l e mi su n d e c i d a b l e w ep r o p o s e df o r m u l a - c l o c ka u t o m a t ab a s e do np r o f o u n dl e a r n i n ga n d a n a l y s i s i n gt i m e da u t o m a t a i nt h ef o r m u l a - c l o c ka u t o m a t a ，a ne v e n tc o r r e s p o n d t oa p r o p o s i t i o n a n dw ed e f i n et w o c l o c k s ：f o r m u l a - r e c o r d i n g c l o c ka n d f o r m u l a - p r e d i c t i n gc l o c kf o re v e r yl i n e a rp r o p o s i t i o n a lt e m p o r a l1 0 9 i cf o r m u l aw h i c h i sb a s e do nt h eg i v e ns e to fp r o p o s i t o n s t h ef o r m e rr e c o r d st h ee l a p s eo ft i m ef r o m t h el a t e s tm o m e n ta tw h i c ht h ef o r m u l ac o r r e s p o n d i n gt h ec l o c kw a ss a t i s f i e d ，w h i l e t h el a t t e rp r e d i c t st h en e x tm o m e n ta tw h i c ht h ef o r m u l ac o r r e s p o n d i n gt h ec l o c kw i l l b es a t i s f i e d a tt h es a m et i m e ，w ed i s c u s st h ed e t e r m i n i s ma n dn o n d e t e r m i n i s mo f f o r m u l a - c l o c ka u t o m a t aa n dt h ec l o s u r ep r o p e r t i e du n d e rb o o l e a no p e r a t i o no ft h e l a n g u a g ew h i c hi sa c c e p t e db yf o r m u l a - c l o c ka u t o m a t a w ea l s op r o v et h e e x p r e s s i v ee q u i v a l e n c eb e t w e e nt h ed e t e r m i n i s t i cf o r m u l a - c l o c ka u t o m a t aa n dt h e n o n d e t e r m i n i s t i cf o r m u l a - c l o c ka u t o m a t a t h i sm e a n st h a te v e r yn o n d e t e r m i n i s t i c f o r m u l a - c l o c ka u t o m a t ac a nb et r a n s f o r m e dt oad e t e r m i n i s t i cf o r m u l a - c l o c k a u t o m a t aw h i c he x a c t l ya c c e p tt h et i m e dl a n g u a g ei d e n t i f i e db yt h ef o m e r w ea l s o i i 公式时钟自动机一种新的形式化验证工具 e x t e n dt i m e dw o r d st oi n f i n i t e n e s sa n dd e f i n et h ef o r m u l a c l o c kb f i c h ia u t o m a t aa n d t h ef o r m u l a c l o c km u l l e ra u t o m a t a a tl a s t ，w es h o wi t s a p p l i c a t i o ni nf o r m a l v e r i f i c a t i o na n dm o d e l i n go fr e a l t i m es y s t e m k e y w o r d s ：f o r m u l a r e c o r d i n gc l o c kf o r m u l a - p r e d i c t i n gc l o c kt e m p o r a lo p e r a t o r t i m e dw o r d s i l i 竺垄堕塑皂翌! ! = = = 苎堑塑兰塞些墼堡三墨) z 星2z 郑重声明 本人的学位论文是在导师指导下独立撰写并完成的，学位论文没有剽窃、 抄袭等违反学术道德、学术规范的侵权行为，否则，本人愿意承担由此产生的 一切法律责任和法律后果，特此郑重声明。 学位论文作者( 签名 ：李别家 锄略年g 月；1 日 钎 公式时钟自动机一种新的形式化验证工具 第一章引言 在计算机科学领域内，自动机是分析模拟许多现象的有力工具，特别是在并 行有限状态系统中，自动机理论有着较重要的地位【l 。2 1 。在并行计算的轨迹模型 中，系统是用其行为来区别的，若用一个状态序列或事件序列来代表行为，那么 一个系统的所有可能的行为集合就构成了一个形式化语言。由此，系统就用产生 该语言的自动机来模拟( 对于复杂的系统，我们分别用一个自动机模拟它的每一 个元素，然后对所有这些自动机的求积得到的自动机就是模拟此复杂系统的自动 机1 。由于系统所有允许的行为也构成了一个形式化语言，我们可以用另钤一个 产生此形式化语言的自动机来模拟该系统的需求规范。形式化验证就是完备地证 明设计实现是否与设计规范相一致。我们用时间自动机【1 进行形式化验证就是 将系统的实现用一个时间自动机( 假设为a i ) 来模拟，用另外一个自动机( 假设为 a s ) 模拟系统的规范。那么系统验证就转化为检验l ( a 1 ) 瘩l ( a s ) 是否成立。但求 解时间自动机的语言包含问题是p s p a c e ，完全问题 2 0 2 1 】，这类问题的复杂度太 高，无法直接求解。通常我们将此问题归结为检验l ( a i ) n l ( a s ) = m 是否成立。 求l ( a s ) 通常转化为求时间自动机a s 的补所识别的语言。若a s 是非确定的时 间自动机，那么求a s 的补的问题是p s p a c e 一完全的；若a s 是确定的时间自动 机，那么a s 在补运算下不封闭。并且确定的时间自动机与非确定的时间自动机 的表达能力是不等价的。在对时间自动机研究的基础上，我们提出了公式时钟自 动机，即在状态转换中加入逻辑公式作为转换约束条件，并通过不同的逻辑公式 派生出多种形式的时钟自动机，同时我们证明了确定的公式时钟自动机与非确定 的公式时钟自动机的等价性，这种等价性对形式化验证是有意义的。 1 1 有穷状态自动机的提出 有穷状态自动机 5 - 7 是许多重要类型的硬件和软件的有用模型。它在2 0 世纪 4 0 和5 0 年代被提出。起初研究者建议用这些自动机来为人脑功能建立模型，但 后来发现其在许多其它领域极为有用，如数字电路的设计和性能检查、典型编译 器的“词法分析器”及只有有穷多个不同状态的系统的验证软件等等。一般而言， 公式时钟自动机一种新的形式化验证工具 最简单的非平凡有穷状态自动机是鼹相开关。这个装置记住“开”状态或“关” 状态，允许用户按一个按钮，这个按钮根据开关状态起不同作用。也就是说，如 果开关处在关状态，按这个按钮就变成开状态；如果开关处在开状态，按这个按 钮就变成关状态。其有穷状态自动机模型如图l 所示： p u s h r u 曲 图1 ：为两相开关建立模型的有穷自动机 通常需要说明一个或多个状态是“终止”或“接受”状态。在经历一个输入 序列后进入这些状态之一，说明这个输入序列在某种程度上是好的。例如，可以 认为图1 中的0 1 1 状态是接受状态，因为在这个状态下，这个由开关控制的装置 将会运行。习惯上用双圆圈来说明接受状态，但在图1 中没有做这样的说明。 在给出有穷状态自动机的形式化定义前，先给出转换表的定义。 定义1 1 一个转换表a 是一个四元组 这里 ( 1 ) 是输入字母表 ( 2 ) s 是一个有穷状态集 ( 3 ) s o s 是开始状态集 ( 4 ) e s s 是边的集合 对字母表上的一个字盯= 盯l 盯2 ，我们称 r ：s 0 皿- s l 亟斗s 2 亚u 是a 在盯上的一个运行，若s o s o 且对v i l ， e 。对一个运 行，定义i n f ( r ) = s ls i c s 且在r 中出现无穷次) 。 通过对转换表增加不同的接受条件，我们可以得到不同类型的自动机。这里 我们介绍两种类型的自动机，即b l c h i 自动机( 简写为b a ) 和m u l l e r 自动机( 简写 为m a ) ： 定义1 2 一个b n c h i 自动机a 是一个五元组 。这里 是一个转换表，f c _ s 是接受状态集。一个b t i e h i 自动机a 在字 2 公式时钟自动机一种新的形式化验证工具 盯m 上的一个运行r 是接受运行i f f i n f ( f ) n f 。a 接受的语占l ( a ) = 盯i a 在盯上有一个接受运行) a ，ba 图2 ：b i i c h i 自动机 上图2 所示的b t i c h i 自动机其输入字母表为 a ，b ，状态集为 s o ，s 1 ) ，边集 为 ， ， ， ，开始状态集 为 s o j ，接受状态集为 s 1 ) ，其接受的语言为( a + b ) a 。 定义1 3 一个m u l l e r 自动机a 是一个五元组 。这里 是一个转换表，f c 2 8 是接受状态集簇。一个m u l l e r 自动机 a 在字盯国上的一个运行r 是接受运行i f f i n f ( r ) f 。a 接受语言的 定义类似b i c h i 自动机接受语言的定义。 b 图3 ：m u l l e r 自动机 图3 所示的m u l l e r 自动机其输入字母表为 a ，b ) ，状态集为 s o ，s i ) ，边集 为 ， ， ， ) ，开始状态集 为 s o ) ，接受状态集簇为 s 1 ，其接受的语言为：a 、b 的无穷序列且b 的个数 是有穷的。 定理1 1b i i c h i 自动机与m u l l e r 自动机接受的语言是等价的 通常我们所说的有穷自动机指的是b i l c h i 自动机。 定义1 4 一个转换表a = 是确定的，当且仅当 ( 1 ) 它只有一个开始状态 ( 2 ) 对v a e 、s l s ，存在且仅存在一个s 2 s ，使得 e 公式时钟自动机一种新的形式化验证工具 e 相应的，存在与之相应的确定的b f i c h i 自动机( d b a ) 与确定的m u l l e r 自 动机( d m a ) 。图3 中的m u l l e r 自动机是确定的，而图2 中的b f l c h i 自动机是非确 定的。 定理1 2 确定的b i i c h i 自动机接受的语言c 确定的m u l l e r 自动机接受的语言。 定理1 3 确定的m u l l e r 自动机接受的语言、b t i e h i 自动机接受的语言与m u l l e r 自动机接受的语言是互相等价的且都是国正则语言。 关于这两条定理的证明请参阅i8 。o i 。 1 2 时间自动机 虽然有穷自动机可以用来分析模拟许多现象，但它只能指明系统的事件发生 的先后顺序，而不能表达每一个事件发生的时间及其实时需求。为了捕捉实时系 统的行为，对有穷自动机用时间的概念进行扩展。 时间自动机( t i m e da u t o m a t o n ) 是在传统的有限状态自动机的基础上加入了 时间约束机制，使传统的有限状态自动机的行为带上了时间的特性，从而其有了一 定的表达时间的能力。 定义1 5 时间序列f = r l f2 是时间值的无限序列，f i r ( r 是非负实数集) 且 r ， o ，满足以下条件： ( 1 ) 单调性，r 单调递增，即r i t 定义1 6 字母表上的时间字是一序偶 ，盯= 盯l 盯2 是一个上的 无限字，r 是一个时间序列，而上的时间语言是上时间字集合。 定义1 7 对给定的字仃= 盯i 盯2 ，用盯j 表示从该字中删去前i - 1 个符号而得到 的新字，即口i = 盯i o i + l ，同理，对给定的时间序列f = f1 f2 ，f j 表示从该时间序列中删去前i - 1 个时间值而得到的新的时间序列，即fi = f i f i + l ，那么时间字 就表示从时间字 中删去 前i 1 个符号和前i - 1 个时间值两得到的新的时间字。 定义1 8 对一个在上的时间语言l ，u n t i m e ( l ) = 盯l 盯国并且存在着某个 时间序列r 使得 l ) 。 4 公式时钟自动机一种新的形式化验证工具 定义1 9x 是时钟变量集，时间约束占的集合定义如下： 占= x c lc x l 一万ij 1 八万2 其中，x x ，c 是有理数常量。 定义1 1 0 一个时钟集合x 的一个时钟解释v 是指给每个时钟赋值一个实数值； 即：它是一个从x 到非负实数集r 的一个映射。x 的一个时钟解释v 满 足x 上的一个时钟约束6 ，当且仅当依照v 给出的值，j 为真。对于 t r ，v + t 表示一个时钟解释，它对每一个时钟x 的赋值为v ( x ) + t 。 对y c _ x ，v y = o 】表示x 的一个时钟解释，它给每个x y 复位，并 使其余的时钟值保持增加( 不变) 。 定义1 1 1 时间转换表a 是一五元组 ，其中，、s 、s o 的 意义与前面相同，c 是有限时钟集，边集e s s 2 。中( c ) 。 边 e 表示a 读取输入符号a 时，从状态s 1 转换到状态s 2 ，集合五- c 表示复位时钟的集合，占是c 上的时间约 束。 由于在每一个时刻，一个时间转换表的将来的行为是由它当前的状态及每个 时钟当前的值决定的，因此我们可以定义它的扩展状态： 定义1 1 2 对一个时间转换表 ，一个扩展状态是一个二元 组 ，其中s c s 并且v 是对c 中时钟的一个解释。 与有穷自动机一样，通过对时间转换表增加不同的接受条件，我们可以分别 定义时间b i i c h i 自动机和时间m u l l e r 自动机： 定义1 1 3 一个时间b t i c h i 自动机( 简写为t b a ) 是一个六元组 。其中 是一个时间转换表，f s 是接受 状态集。 图4 ：时间b i i c h i 自动机 5 公式时钟自动机一种新的形式化验证工具 图4 中所示的时间b t i c h i 自动机其输入字母表为 a ，b ，状态集为 s o ，s 8 2 ，8 3 ) ，边集为 ， ， ， s 2 ，s 3 ，b ，x ， ，开始状态集 为 s o ，时钟集为 x ，接受状态集为 s 2 。其接受的时间语言为： “a b ) ，r ) l j i v j i ( 72 j r2 j - 1 + 2 ) ) 。 定义1 1 4 一个时间m u l l e r 自动机( 简写为t m a ) 是个六元组 。其中 是一个时间转换表，f 2 8 是接受 状态集簇。 图5 ：时间m l l l l e r 自动机 图5 中所示的时间m u l l e r 自动机其输入字母表为 a ，b ，c ，状态集为 s o ， s l ，s 2 ，边集为 s o ，s i ，a ，x ， ， s o ，s 2 ， a ，庐，x ， ) ，开始状态集为 s 0 ，时钟集为 x ， 接受状态集为“s o ，s 2 ) 。其接受的每一个时间字 满足： ( 1 ) 盯( a ( b + c ) ) + ( a c ) 珊 ( 2 ) 对任意的i l ，若第( 2 0 个输入符号为c ，则f2 i 一1 一f2 i - 2 2 ；否则r2 i l f2 i 一2 0 ，如果对于所有o il e ，”+ tl 满足将s 作为源状态 发生转换的边上的时钟约束，那么 一 ( 2 ) 状态可以通过读取输入字符而改变：对于一个状态 和一个 转换，如果d l 满足6 ，那么 与。 定理1 4 时间b i i c h i 自动机和时间m u l l e r 自动机识别的语言都只在并、交运算下 封闭，而在补运算下是不封闭的。 定理1 5 确定的时间m u l l e r 自动机识别的语言在并、交、补运算下都是封闭的。 定理1 6 确定的时间b i i c h i 自动机识别的语言只在并、交运算下封闭。 关于这三条定理的证明请参阅 3 - 4 1 。 1 3 模型验证 i 系统实现 i 模型 模 确定系 型 统的实 验 现是否 证 满足规 l 系统规格 工 格要求 具 l 模型 图6 ：模型验证的工作方式 计算机科学的一个重要研究方向就是要确定：在给定系统规格说明的前提下 所构造的系统模型( 或系统实现) 是否是正确的1 3 3 】。其中形式化方法起到了重要的 作用。形式化方法首先要求用一种形式化语言描述系统的规格说明，然后有两种 方法来保证系统模型的正确。一种方法是从系统的规格说明开始，利用推理规则， 逐步地推导出正确的系统模型，即定理证明。另一种方法是根据系统的规格说明 7 公式时钟自动机一种新的形式化验证工具 设计一个系统模型，并构造一种算法来验证系统模型是否满足系统的规格说明， 即验证。目前，验证领域中的一个重要方法就是模型验证( m o d e l 一c h e c k i n g ) 。2 “ 3 6 模型验证是对有限状态系统的一种形式化确认方法，具体做法是：采用一种 形式化语言描述系统的规格说明，构造一种算法来遍历根据系统规格说明设计的 实现模型，确认实现模型是否满足系统的规格说明。模型验证是保证系统设计正 确的一种重要的形式化方法。其一般工作方式如上图6 所示 3 1 1 ： 文献中，按照系统规格说明的表达方式，将目前存在的模型验证方法分为 两类。第一类是时序模型验证。这种方法是在2 0 世纪8 0 年代由c l a r k e 和e m e r s o n ， q u e i l l e 和s i f a k i s 独立开发的方法。在这种方法中，系统的规格说明用某种时序 逻辑表达。系统的实现用有限状态转换系统表达。一个有效的搜索过程用于检验 一个有限的转换系统模型是否满足规格的要求。第二类是自动机模型验证，在此 方法中规格说明用一个自动机描述，系统的实现也用自动机描述，通过比较系统 的实现和规格说明来确定系统的行为是否满足规格的要求。但这两种方法不是孤 立的，二者之间既有联系又有区别。 1 4 论文内容及结构 本文针对时间自动机在实时系统的形式化验证方面的不足，提出了公式时钟 自动机。第二章给出了公式时钟自动机的形式化定义，可以看到，公式时钟自动 机与时间自动机不同的是，前者时钟的选取不像后者那样时钟的选取是任意的， 它只有公式记录时钟和公式预测时钟。第三章给出了确定的公式时钟自动机的形 式化定义且证明了确定的公式时钟自动机和非确定的公式时钟自动机表达能力 的等价性。这表明了任一个非确定的公式时钟自动机都能转换为一个与它表达能 力等价的确定的公式时钟自动机。第四章研究了公式时钟自动机的一些性质，如 它在并、交、补运算下的封闭性。第五章给出了公式时钟自动机在实时系统的形 式化验证方面及对实时系统的建模应用的例子。第六章对本文进行总结，展望未 来的工作。 8 公式时钟自动机一种新的形式化验证工具 第二章公式时钟自动机 2 1 线性命题时态逻辑公式的语法 时态逻辑自1 9 7 7 年由m a n n e r 和p e n u l i 首先引入到计算机科学中，用于并 发性系统的验证f j 2 _ 羽。系统验证是指系统的实现是否满足系统的描述。二十年来， 时态逻辑尤其是线性命题时态逻辑啪3 ( 简写为l p t l ，即l i n e a rp r o p o s i t i o n a l t e m p o r a ll o g i c ) 受到了计算机界的重视，人们从语法和语义的角度对它进行了深 入的研究。 线性命题时态逻辑是由古典命题逻辑加四个时间算子构成的。这四个时间算 子是：o ( 称为n e x 0 ，( 称为s o m e t i m e s ) ，口( 称为a l w a y s ) ，u ( 称为u n t i l ) 。l p t l 在一个线性的无限状态序列( s 。，s 2 ，) 上解释它的语义，这四个时间算子的基 本含义是：在该序列中的某个状态s i ，口f 为真，如果f 在s i 后的所有状态均为 真；o f 为真，如果f 在s i 的下一个状态为真；f 为真，如果f 在s i 后的某个状 态为真；f u g 为真，如果g 在s j 驴i ) 为真，并且f 在s i 到s j 中间的所有状态为真。 定义2 1 设p = p ，q ，r ，) 为命题集，则在p 上的线性命题时态逻辑公式如 下定义： ( 1 ) 原子命题是公式 ( 2 ) 如果f i ，f 2 是公式，则一f l ，f l 八如，f l v f 2 ，o f l ，f l ，口f l ，f lu f 2 是公式； ( 3 ) 仅由以上两条规则构造的是公式 我们把在p 上的所有公式构成的集合记为f 。 2 2 线性命题时态逻辑公式的语义 用k r i p k e 结构来解释l p t l 公式的语义： 定义2 2 一个k r i p k e 结构是一个四元组k = ( s ，i ，r ，s o ) 。让a p 是原子公式 集合；s 是节点的集合；i ：s 一2 a p 是映射，它给每个节点的原子命题赋 一个真值，表示此原子命题在该节点被满足( 值为真) ；r sxs 是s 上 的有向边；s o 是初始节点。 9 公式时钟自动机一种新的形式化验证工具 用k ，s i 户f 表示在结构k 中，公式f 在节点s i 处被满足。当k 指定后，s f f 表示上述含义。对l p t l 公式的解释如下： ( 1 ) s i l = f i f f f i ( s i ) ( 2 ) s i 户一f 酊s i i f ( 3 ) s i f f l 八丘i f fs i i = f i ，并且s i p ( 4 ) s if _ f j v f 2 i f f s i l = f i ，或者s i 卜f 2 ( 5 ) s il = o f i f f s i + l 阿 ( 6 ) s il = o f i f f 3 j i ，s j f ( 7 ) s i 户c f i f f v j i ，s j _ f ( 8 ) s i f f i u f 2 i f f j j i ，s j f = 丘，并且v k 且i k = j ，s k i = f l 一个l p t l 公式是可满足的，当且仅当存在一个结构k = ( s ，i ，r ，s o ) 使得 对于某个i ，s i ) p f 成立。我们称这样的一个结构定义了f 的一个模型。 2 3 公式记录时钟与公式预测时钟 公式时钟自动机时钟的选取不像时间自动机中时钟的选取是任意的，它只选 取两种时钟：公式记录时钟与公式预测时钟。对一个给定的公式，公式记录时钟 的值等于该公式最后一次被满足时距目前的时间，若此前该公式从没有被满足 过，那么该时钟的值等于一个特殊的值上；公式预测时钟的值等于该公式下一次 将被满足时距目前的时间，若从此以后该公式不再被满足，该时钟的值也等于j _ 。 由于线性命题时态逻辑公式是在k r i p e 结构上定义其语义的，因此在公式时 钟自动机中选取时钟所用的公式就在其所在的自动机上解释。但此处我们要做一 个小小的修改，即在公式时钟自动机中，不是每个状态对应给定命题集的一个子 集，而是从一个状态变换到另一个状态时所读取的输入符号对应于命题集的一个 子集，此映射关系我们仍用i 表示。可以很容易证明此修改过的公式时钟自动机 与直接将它作为k r i p e 结构的公式时钟自动机的表达能力是等价的。 设f 为命题集p 上的公式集，妒f ，我们对每一个公式用x 表示该公式 的公式记录时钟。给定一个时间字t 9 = ( 盯1 ，r 1 ) ( 盯2 ，f2 ) ( 盯。，f 。) ，时钟x 够 在第j ( 1 j n ) 个位置的值为r j - - f i ( 1 i j ) ，其中c r i | - p 且i 为满足此条件的最 1 0 公式时钟自动机一种新的形式化验证工具 大值。 我们记r l 卸= r 0 u ( 上 表示所有的非负有理数与特殊值上构成的集合。 公式记录时钟x 妒在时间字玎的第j 个位置的值记为y ；( ) ( 妒) ，如下定义： 实际上，公式记录时钟x 舻就像在时间自动机中每次公式妒被满足时它被 重置为0 。因此，时钟x 口的值由输入时间字决定而不是由它所在的公式时钟自 于公式将来的信息。对于每一个公式妒f ，我们用y 妒表示该公式的公式预测 时钟。给定一个时间字珂= ( 盯1 ，f1 ) ( 盯2 ，f2 ) ( 盯。，fn ) ，时钟y p 在t d 的第 j 个位置的值为f i f j 0 i n ) ，其中仃ii _ p 且i 为满足此条件的最小值。公式 预测时钟y 伊在盯的第j 个位置的值记为y ：( y 妒) ，如下定义： f i 一7j若j i ，j i n 且牙i f 妒，但对v k ，j k i ， i口k i 伊 y j ( y 妒) 2t j 若对v k ， k n ，都有万。l 妒 公式预测时钟y 口相当于在时间自动机中每次该时钟被满足时，它被重置为 一个非正的开始值，随着时间的流逝它的值递增，直到下一次它被满足时检查其 我们用c f 表示公式记录时钟与公式预测时钟的集合，即c f = xc pi 妒 v 妒 对 萨 一 万 妒 有 户 部 巧 1 ： 勘 q q 妒 皲 萨 h ： 万 v j 育 对 相 椭 料 一 q 上 ，、，l = 妒 x 厂 公式时钟自动机一种新的形式化验证工具 f u y 口j 伊f ，其中f 为给定命题集上的公式集。那么，在给定的时问字6 7 的 第j 个位置，我们定义一个时钟赋值函数矿，它是一个从c f 到r 上”上的映射。 ， 时钟约束中的原子约束将时钟值与有理数常量或特殊值上进行比较。在给定的时 钟集上的时钟约束是形式为z c 或z c 的原子约束的布尔合取，其中z e c f 且 c r 上。时钟赋值函数，对c f 中的每一个时钟赋于一个时间值，它对定义在 c f 上的时钟约束进行解释，给定时钟赋值函数y 与时钟约束占，我们用，户j 表 示根据时钟赋值函数y ，时钟约束占的取值为真，即y 满足j 。 说明：原子约束j _ 上的值为真，所有其它涉及上的原子约束都为假。 2 4 公式时钟自动机的语法和语义 一个公式时钟自动机( f o r m u l a c l o c ka u t o m a t a ，简写为f c a ) 实际上也是一个 有穷自动机，但该自动机的边不但标记有输入符号，而且还标记有定义在公式记 录时钟和公式预测时钟上的时钟约束，并且该边的输入符号要映射到给定命题集 上的一个子集。下面给出公式时钟自动机的形式化定义： 定义2 3 一个公式时钟自动机a 是一个七元组( ，p ，i ，s ，s o ，s f ，e ) ，每一 个元素意义如下： ( 1 ) 是一个有穷输入字母表 ( 2 ) p 是命题集，实际上p 是事件的集合，若该事件发生，则与之对应 的原子命题的值为真，否则为假 ( 3 ) i 是一个映射，它将输入字母表中的每一个符号映射为p 的一个子 集 ( 4 ) s 是一个状态集 ( 5 ) s o s 是开始状态集 ( 6 ) s f s 是接受状态集 ( 7 ) e c _ s s i xo ( c f ) 是边的集合。每一条边是一个五元组 ，其中s l 、s 2 分别为源状态和目的状态，a 是输入符 公式时钟自动机一一种新的形式化验证r t 具 号，i 将a 映射为一个命题集、表示从状态s i 变换到状态s 2 过程中 有哪些事件发生，j 为定义在c f 上的时钟约束。由于一旦给定一个 公式时钟自动机，映射i 是确定的，以后针对给定的公式时钟自动 机，我们就将边表示为一个四元组而省去映射i 。 下面我们给出公式时钟自动机在给定时间字上的运行的定义。首先，我们将 给定的时间字限制为有穷的，稍后我们再将时间字扩展为无穷的。 定义2 4 一个公式时钟自动机a 在给定的时间字缸= ( 仃i ，r 1 ) ( 仃2 ，f2 ) ( 盯。， f 。) 上的一个运行是一个如下形式的有穷序列： s o 马s l 轴s 2 马s 3 马s n 其满足以下条件： ( 1 ) s i s ( 0 i n ) ，即s i 是一个合法的状态 ( 2 ) s o es o ，即s o 是一个开始状态 ( 3 ) 公式时钟自动机a 对输入时间字河从左至右扫描，每一步读取一个 输入符号及与之相应的时间。若该公式时钟自动机在状态s i _ l 读取第 i 个输入对( 盯i ，f i ) 后能变换到状态s i ，当且仅当存在边 e 且当前的时钟赋值函数矿满足艿。 定义2 5 一个运行是接受运行当且仪当读取最后一个输入符号盯。后变换到的状 态s n s f 。 定义2 6 公式时钟自动机a 接受的所有时间字记为l ( a ) = 万1 a 在玎上有一个接 受运行，称为a 所识别的时间语言。 例2 1 给定命题集p = p ，q ，r ) ，字母表= 口l ，仃2 ，状态集s = s o ，s i ， s 2 ) ，开始状态集s o = s o ，接受状态集s t = s 2 ，映射函数i 为：i ( 盯1 ) = p ，q ) 、i ( c r 2 ) = ( r ，边集e = ( 、 s l ，s 2 ，仃2 ，x p n 。 ，则对应的公式时钟自动机如下图7 所示： 图7 ：例2 4 1 对应的公式时钟自动机 经过分析，很容易看出此公式时钟自动机表达了实时需求“事件p 和事件q 同时发生，且在随后的3 秒内事件r 必定发生”。 公式时钟自动机一种新的形式化验证工具 例2 2 1 3 0 ：设计输油管道系统，使得该系统两次漏油发生的时侧至少间隔3 0 0 m i n ， 并且发生漏油后，系统保证在l m i n 内得到恢复。 分析系统设计的要求，可得出系统有两个状态：漏油状态与不漏油状态。当 系统处于不漏油状态时，可执行加油等一系列操作，而状态保持不变，一旦发生 漏油，系统变换到漏油状态。当系统处于漏油状态时，停止往其中加油等操作， 并保持此状态不变，一旦做修复操作，就变换到不漏油状态。所设计的系统的公 式时钟自动机如图8 所示： b ，x l i 图8 ：例2 4 2 对应的公式时钟自动机 上图所示的公式时钟自动机中，状态s o 表示不漏油状态，状态s - 表示漏油 状态，让输入符号a 映射到漏油事件的发生，输入符号b 映射到修复事件的发生， 输入符号c 映射到对非漏油状态所能做的所有操作但漏油事件除外，输入符号d 映射到对漏油状态所能做的所有操作但修复事件除外，用l 对应漏油事件。 定义2 7 若给定的公式时钟自动机a 上的时钟约束只涉及到给定命题集上公式 的公式记录时钟，我们又将a 称为公式记录自动机( f o r m u l a - r e c o r d i n g a u t o m a t a ，简写为f g a ) ；同理，若给定的公式时钟自动机a 上的时 钟约束只涉及到给定命题集上公式的公式预测时钟，我们将a 称为公 式预测自动机( f o r m u l a - p r e d i c t i n ga u t o m a t a ，简写为f p a ) 。 1 4 公式时钟自动机一种新的形式化验证工具 第三章确定性与非确定性公式时钟自动机的等价性 3 1 确定的公式时钟自动机 一个有穷状态自动机是确定的当且仅当标记有相同输入符号的边是相互不 同的。同样，在公式时钟自动机中，我们也考虑它的确定性。但我们看到，公式 时钟自动机的确定性要求与有穷状态机确定性的要求是不同的，但与时间自动机 的确定性要求类似。 定义3 1 一个公式时钟自动机a - - - - ( z ，p ，i ，s ，s o ，s f ，e ) 是确定的，当且仅 当： ( 1 ) 它至多有一个开始状态 ( 2 ) 具有相同源状态和相同的输入符号的边上的时钟约束是相互排斥 的：也就是说，若 和 都 属于e ，那么不存在时钟赋值函数，使得，p j j 八占2 不满足上述性质的公式时钟自动机称为非确定的公式时钟自动机。显然，确 定的公式时钟自动机在一个运行中的每一步的动作由自动机的当前状态、输入符 号、在给定时间字上的位置唯一决定。因此，确定的公式时钟自动机在任何给定 的输入时间字上至多有一个接受运行。 图9 ：确定的公式时钟自动机 显然，如上图9 所示的公式时钟自动机是确定的。 3 2 确定性与非确定性公式时钟自动机的等价性 众所周知，在有穷状态自动机理论中每一个非确定的自动机都可以确定化 公式时钟自动机一种瓶的形式化验证工具 即确定的有穷状态自动机与非确定的有穷状态自动机识别相同的语言类( 正则语 言) 。而在时间自动机理论中，非确定的时间自动机能比确定的时间自动机识别 更多的语言，它们的表达能力是不等价的。对公式时钟自动机而言，确定的公式 时钟自动机与非确定的公式时钟自动机的表达能力是等价的，即我们可以将每一 个非确定的公式时钟自动机转化为一个与之识别相同时间语言的确定的公式时 钟自动机。 定理3 1 确定的公式时钟自动机与非确定的公式时钟自动机识别相同的语言类 证明：为了证明确定的公式时钟自动机与非确定的公式时钟自动机的表达能力的 等价性，我们只需证明： ( 1 ) 确定的公式时钟自动机所识别的语言类非确定的公式