（机械工程专业论文）复杂动态系统若干建模、分析、控制与调度问题研究.pdf

摘要 全文工作分为两部分：离散事件动态系统理论及其在自动化立体仓库中 的应用，复杂柔性隔振系统的动态特性分析及其主动控制。 ( 1 ) 基于时态逻辑和p e t r i 网方法研究离散事件系统的建模、分析与控制问 题，对自动化立体仓库运行过程的建模、分析与调度问题进行研究。 出了基于时态公式的离散事件系统的时态模型，针对有限状态系统 基于状态可达图的系统时态特征的判定方法。 基于p e t r i 网方法与扩展时态逻辑一实时时态逻辑对实时d e d s 进行了 研究，提出了面向对象实时时态着色p e t r i 网模型。 在时态逻辑框架下对自动化仓库中分拣系统和旋转货架系统的运行过 程进行了研究，基于时态公式对被控对象、控制器和闭环期望动态行为进 行描述与分析，并对系统期望行为的可达性问题进行了形式化证明。 对自动化仓库输送系统运行过程的调度问题进行研究，建立了系统的 面向对象着色p e t r i 网模型，讨论了该过程的死锁分析问题，给出了系统行 为的时态逻辑规范和死锁避免的最大允许反馈控制策略。夕 ( 2 ) 对复杂柔性隔振系统的动态特性分析及其主动控制问题进行研究。 ，一、p ( 以动力机械柔性安装的振动噪声控制问题为背景，建立了综合主、被 动控制方式的柔性隔振系统的一般动力学模型。对柔性板式基础上的主动 隔振进行了研究，用功率流指标描述主动隔振系统中能量的传输，运用予 结构导纳综合法推导主动隔振系统中功率流传递的控制表达式。 研究了旋转机械的主动隔振系统的功率流传递规律，提出了基于总功 率流最小的最优化控制策略，分析了优化控制力对总功率流和其它各功率 流分量传递的控制效果 ， 关健词t 离散事件动态系统，时态逻辑，p e t r i 网，自动化仓库，复杂柔性 隔振系统，传递特性分析，主动控制。 i 墓埘 1 a b s t r a c t t h i sp a p e ri n c l u d e st w o p a r t s ：t h e o r ya b o u td i s c r e t ee v e n td y n a m i cs y s t e m s ( d e d s ) a n d i t s a p p l i c a t i o n so na u t o m a t e dw a r e h o u s e ，d y n a m i cp r o p e r t ya n a l y s i sa n da c t i v ec o n t r o lf o rc o m p l e x f l e x i b l ei s o l a t i o ns y s t e m ( 1 ) t h em o d e l i n g ，a n a l y s i sa n dc o n t r o lp r o b l e m sa b o u td e d s a r es t u d i e db a s e do nt e m p o r a ll o g i c a n dp e t r in e t sm e t h o d s ，a n dt h em o d e l i n g ，a n a l y s i sa n ds c h e d u l i n gp r o b l e m sa b o u tt h ea u t o m a t e d w a r e h o u s ea r ea l s op r e s e n t e d t h et e m p o r a lm o d e lo fd e d sb a s e do nt e m p o r a lf o r m u l a si se s t a b l i s h e d f o rt h ef i n i t e s t a t e s y s t e m s ，t h ed e c i d i n gp r o c e d u r e sa b o u tt h et e m p o r a lc h a r a c t e r i s t i c so ft h es y s t e ma r ed e v e l o p e d b a s e do nt h er e a c h a b i l i t yg r a p h b a s e do np e t r in e t sa n dt h er e a lt i m et e m p o r a ll o g i c ，ak i n do ft h ee x t e n d e dt e m p o r a ll o g i c ，t h e r e a lt i m ed i s c r e t ee v e n t s y s t e m s a r ei n v e s t i g a t e d t h eo b j e c t - o r i e n t e dr e a lt i m et e m p o r a lc o l o r e dp e t r i n e t sm o d e li sp r e s e n t e d t h e s o r t i n gp r o c e s sa n d t h er u n n i n gp r o c e s so f t h ec a r o u s e ls y s t e mi nt h ea u t o m a t e dw a r e h o u s e a r es t u d i e di nt h et e m p o r a ll o g i cf r a m e w o r k t h ep l a n t , c o n t r o l l e r , a n dd e s i r e dc l o s e dl o o ps y s t e m b e h a v i o r sa r es p e c i f i e da n da n a l y z e di nt e m p o r a ll o g i cf o r m u l a s , a n dt h er e a c h a b i l i t yo f t h ed e s i r e d b e h a v i o ri sv e r i f i e df o r m a l l y t h e s c h e d u l i n gp r o b l e mo f t h er u n n i n gp r o c e s so f t r a n s p o r t i n gs y s t e mi ss t u d i e d ，t h ep r o c e s si s m o d e l e dw i t ho b j e c t - o r i e n t e dc o l o r e dp e t r in e t s ，t h ed e a d l o c ka n a l y s i s p r o b l e mi sd i s c u s s e d ，i t s s p e c i f i c a t i o nw i t ht e m p o r a ll o g i ca n dt h em a x i m a l l yp e r m i s s i v ef e e d b a c kc o n t r o ls t r a t e g yf o r d e a d l o c ka v o i d a n c ea r ep r e s e n t e d ( 2 ) r e s e a r c ho nd y n a m i cp r o p e r t ya n a l y s i sa n da c t i v ec o n t r o lf o r c o m p l e xf l e x i b l e i s o l a t i o n s y s t e m c o n s i d e r i n go ft h ef l e x i b l ei n s t a l l i n go ft h em a c h i n e s ，ag e n e r a ld y n a m i cm o d e lf o rt h e c o m p l e xa c t i v e - p a s s i v ef l e x i b l ei s o l a t i o ns y s t e m si sg i v e n a c t i v ec o n t r o lp r o b l e mf o rs y s t e m s b a s e do nt h ep l a t e - l i k ef o u n d a t i o ni s r e s e a r c h e d s u b s y s t e mm o b i l i t ys y n t h e s i st e c h n i q u ei sa p p l i e d t od e r i v et h ec o s tf u n c t i o no fp o w e rf l o wt h a t a c t sa sap e r f o r m a n c ei n d e xt oi n d i c a t et h e t r a n s m i s s i o no f t h ee n e r g y , t h et r a n s m i s s i o nr e g u l a t i o no f t h ea c t i v ep o w e rf l o wo ft h er o t a t i n gm a c h i n e si sr e s e a r c h e di n d e t a i l t h eo p t i m a lc o n t r o ls t r a t e g ya i m e da tm i n i m u m t o t a lp o w e rf l o wt r a n s m i s s i o ni sp r e s e n t e d ， a n dt h ec o n t r o le f f e c tt h a tt h e o p t i m a lf o r c ei n f l u e n c e st h et o t a lp o w e rf l o wa n dt h r e ep o w e r c o m p o n e n t s 仃a n s m i t t e di n t ot h ef l e x i b l ef o u n d a t i o ni sa n a l y z e d k e y w o r d s ：d i s c r e t ee v e n td y n a m i c s y s t e m ( d e d s ) ，t e m p o r a ll o g i c ，p e t r in e t s ，a u t o m a t e d w a r e h o u s e ，c o m p l e x f l e x i b l ev i b r a t i o ni s o l a t i o n s y s t e m ，t r a n s m i s s i o np r o p e r t y a n a l y s i s ，a c t i v ec o n t r o l 1 ，离散事件动态系统研究概论 1 1 离散事件动态系统的基本结构与特征 随着信息处理、计算机、机器人等技术的发展，出现了大批反映 高技术发展方向的人造系统，如计算机通讯网络、柔性制造系统、交通 运输网络、军事c 3 j ( 命令、控制、通讯集成) 系统等。这类人造系统的 运行过程是受大量的离散事件驱动的、在复杂的人为规则支配下的运行 过程。区别于连续变量系统，通常把这类人造系统称为离散事件动态系 统( d e d s ：d i s c r e t ee v e n t d y n a m i cs y s t e m ) 。这一概念是在八十年代初由 何毓琦( h o y c ) 先生提出的。到目前为止，关于离散事件动态系统仍 没有一个具有概括性、简明而同时又能为人们所广泛接受的标准定义。 但一般认为它具有如下的区别于传统动态系统的动力学特征【z 】： 1 ) 系统的动态行为由两类本质上离散的变量一状态与事件来描述， 它们构成了描述离散事件系统的两个最基本的要素； 设系统的状态变量为x 1x ：，x n ，事件变量为孝，变量集合为 y = z ，毋，z = 仁i ，工2 ，x 。 , t y p e ( x ，) = q f ，i = 1 , 2 ，t y p e ( 孝) = 2 6 。这里，q 为 状态一的值域，称为局部状态集；2 8 为事件毒的值域，孝通常取值为 一复合事件( 由两个或两个以上基本事件并发而构成的组合事件) ，e 为 系统的基本事件集；可将x 看作为向量，t y p e ( x ) = q ，q = q 1 0 2 a o ，q 为 系统的状态空间。( y ，q ，) 构成了对系统的基本静态描述，故称其为系统 的基本结构。 2 ) 系统内事件的发生受系统状态的制约；系统状态的演化由一系列 离散事件驱动，呈跳跃性变化，且具有一定的时问特征。 一个离散事件系统的动态行为可形象地描述为： ( x 、眚) 一= 可l ；q ，q 。，q ，“，q 1x 。= q l一百i 矿_ _x 1 ” f = 1 , 2 ，” ： 舌；盯l；。盯2 一：仃j ，仃2 ， x h 2 q n 在状态q q 下，如果事件盯e 能够发生，则称仃在q 下使能，记为g p 。 此时若盯e 真的发生，则系统将迁移至一个新的状态q q ，记为q a q 。 设 ，f = ( g ，a ) l q a ，q q ，仃) q 俨= ( g ，盯，g ) l q a q ，g ，q q ，仃) q q 这里称为系统事件的使能机制，f 为系统状态的迁移机制，且两者有 如下关系：= ( g ，l ( g ，盯，) f ，g ，矿q ，盯) ，可见，f 中含有系统事 件的使能机制。f 描述了系统状态与事件之间相互制约与作用的基本逻辑 关系，故称其为系统的逻辑结构。 通常，对于( 口，口) 玎，存在唯一g 。q ，使得( g ，口，q ) f ，或对于 ( g ，仃) s q ，至多有一个g e q 使得( g ，盯，g ) e f 。对此称系统为确定性的， 此刚可将f 看作为一个映射h q ，或一个部分映射q h q 。系统的 状态迁移通常具有一定的时间特征，即消耗一定的时间。 3 ) 事件发生在离散时间点上，具有自发性和不确定性；基本事件之间 存在有顺序性、异步和同步并发性、冲突性、公平性等关系。 事件的发生在状态的约束下通常呈现出自发性和不确定性。离散事 件的发生受系统状态的制约，并驱动系统状态的变化。随着系统状态的 演化，其基本事件之间将呈现出系列复杂的关系，概括有：顺序性、 异步和同步并发性、冲突性、公平性等。 a ) 顺序性：对于基本事件c ，c ：e ，c l e ：，如果( q k ) 一( q 8 ： ) ， 但( g 旧+ s g 。) n ( g 【p ： ) ，其中e ，+ s 表示e 与s 的连接，s 为任意事件串，则 称事件e i ，e ：在条件q 下有顺序关系。 b ) 并发性：对于基本事件g ，如e e ，q e ：，如果q ，e ：) 则称事什c ，如 在条件q 下是并发的。 设基本事件q ，岛在条件q 下是并发的，如果( g e - g ) ( g e ： ) v ( q l e ：，g ) ，、( g e ) _ ! j 1 0 称q ，e ：在条件q 卜是异步并发的：台则称c ，屹在条件 q 卜- 为同步并发。 c ) 冲突性：对于基本事件e ie ：e ，e 。口：，如果( g 【p 。 ) ( g 【g ： ) 但非 q ，e ： ，则称事件e t , e ：在条件q 下互相冲突。 d ) 公平性：对于基本事件e e e ，e 。e ：，如果v q o ，q s ，s 为在q 下 使能的任意串，并且若s 中包含e 。就必须包含e ：，或若包含e ：就必须包含 吼即e l 能发生e ：就能发生，或e ：能发生e ；就能发生。 以上这些关系都是以系统的行为演化过程为基础的，因此有必要将c ： 扩展为：f = ( g ，s ，q ) l q s g ，q ，q q ，j + o q 。设j = 盯i 口2 盯。若 j g i ，q 2 ，一，q 卅1 q 使得( g ，盯l ，q 1 ) ，( g l ，仃2 ，q 2 ) ( g 卅1 ，盯l ，q ) f ，贝0 ( g ，j ，q ) f 。 精确地讲，彳是f 的一个延拓，它含有比f 更为丰富的信息，某些由f 不能描述的特征，可由孑进行刻划。有时也记i 为霸即e k - o q 。 ( g a q t ) 表征了系统的一个具体的动态行为，而f q q 表征了系 统的总体动态行为。由于此类系统存在有不确定性，所以人们更为关注 的是系统的总体动态行为吼基于e 可以分别研究系统的事件行为： c = 删( q ，s ，g ) 霉，q = q o , q q ，j ) + 和它的状态行为： 月= g | ( q ，j ，q ) f ，q = q o , q q ，s ) q 这里，为系统事件生成的一个语言，月为系统的状态可达集，f 或 或月构成了对系统的行为描述。 4 ) 系统的控制机制主要是通过对事件行为的约束( 或禁止) 来实现 的。 在离散事件系统中，由于事件的发生在使能条件下常常表现为自发 性，因此对其只能采取一种约束型的控制，而不是强迫的。所谓约束型 控制是指通过改变事件的使能条件，对系统行为加以约束，以使系统的 行为达到某种要求。这与常规系统有着本质的区别。 综上所述，个离散事件系统在逻辑上可以从以下几个层次进行描 述：基本结构( y ，q ) ；逻辑结构f q q ；行为特征, i t 互q q 或 + 或月q 。 1 2 离散事件动态系统的研究现状 离散事件动态系统为动态系统理论研究提出了新课题，形成了系统与 控制科学中的一个新兴分支与前沿方向【3 】。d e d s 研究近二十年来取得了 很大进展，人们从不同的角度、在不同的层次上以不同的模型和方法提 出和解决了一大批各种各样的问题，特别地d e d s 在实际应用中的进展4 1 给d e d s 研究者很大的鼓舞。 目前研究d e d s 的模型与方法主要有：仿真方法、排队网络方法、 扰动分析方法、极大一极小代数方法、自动机形式语言方法、p e t r i 网方 法、马尔可夫链和广义半马尔可夫过程方法、通讯序贯过程与有限递归 进程、时态逻辑方法、受控序贯决策过程、事件驱动状态空间模型和向 量控制模型。人们基于这些模型方法，按问题抽象程度的高低和研究细 节的多少，从逻辑、时间、随机品质三个层次对d e d s 进行研究。值得 指出的是，虽然对d e d s 的研究是在三个层次分别展开的，但各层次的 研究方法之间存在着相互渗透、部分重叠。下面对这三个层次上的研究 方法及其新近进展做一简单概述。 1 ) 逻辑层次 三个层次的研究中逻辑层次是最基础的，它决定系统的基本结构和 功能，也只有在明确了系统的逻辑结构和定性行为( 事件路径、状态路 径) 的基础上，才能研究系统的定量指标。在这一层次上研究d e d s 的 定性结构框架，分析它的性能指标，解决逻辑正确性这一基本问题；其 实质是忽略d e d s 中事件发生的时间，只考虑事件发生顺序、相互间的 逻辑关系和状态的转化，抽象出d e d s 的逻辑模型，分析其固有的事件 轨迹和相应的状态轨迹是否符合事先给定的逻辑行为要求 ( s p e c i f i c a t i o n ) ；如果不符合要求，则进步研究是否可以通过对d e d s 施加控制作用，来改变其可能的事件、状态轨迹集合，使之满足系统设 计规范，这就是所谓的判定问题( d e c i s i o n ) ；如果可能就以最优的方式( 一 般是尽可能少地限制固有的逻辑行为) 规定控制作用的施加方式，称之 为综合( s y n t h e s i s ) ；最后验证( v e r i f y ) 控制作用是否达到预期效果。 在逻辑层次的研究所采用的大多是离散数学的模型，诸如有限自动 机形式语言1 5 1 、p e t r i 网【6 1 、有限递归进程【7 1 、通讯序贯进程乃至图论、有 限域代数等。它们的主要困难也是共同的，即离散运算的组合复杂性问 题，尽管在逻辑层次赋予代数结构有助于解决这一问题。这里已有的概 念和工具都是逻辑、代数或计算机专家们提供的，但有关控制的问题则 是近几年才提出的。其中r a m a d g e 和w o n h a m 提出的基于自动机形式语 言的监控理论是比较完整的- - i ，它能把现代控制理论的主要概念移植 过来。近几年来人们更注重有结构的模型，较多地谈论子系统集结、数 据结构、实时性、形式逻辑以及计算复杂性较低的综合算法之类的问题。 w o n h a m 和他的学生继续进行的工作包括：1 ) 分散控制【8 】；2 ) 实时 系统中的信息延迟问题【9 】；3 ) 实时系统的t t m r t t l ft t m ：t i m e d t r a n s i t i o nm o d e l s ；r t t l ：r e a l t i m e t e m p o r a ll o g i c ) 研究框架【1 0 1 ；4 ) 无穷 符号串b u c h i 自动机，u 一语言i ”i ；5 ) d e d s 事件状态的联合观测时的 监控问题研究，我国早在1 9 8 9 年即已取得一系列成果【l2 1 ，国外1 9 9 4 年 才开始发表这方面的文章。 其它较有意义的研究有： 1 ) 形式逻辑方面，广泛用于计算机形式规范和验证的模态逻辑被用 于d e d s 的形式规范和验证，它可研究无穷串的监控问题【1 3 】： 6 2 ) k u m a r 等人使用逻辑谓词来表示当前状态估计，用规则集表示控 制，逻辑谓词“使能”控制作用，而受控对象的动态特征和状态估计用 公理集描述，并用自动定理证明来实现控制策略【1 4 1 。 3 ) b r a v e 和h e y m a n n 用递阶状态机( h s m ) 研究“最经济”建模问 题。它在建模中通过状态集结而避免组合爆炸；除了状态分层外，还j f j “正交”的概念来描述没有共享的事件，亦即完全异步的过程 ”】； 4 1i n a n 和v a r a i y a 提出了一种子系统复合代数。它们把有限递门过程 模型用于监控问题并用同步复合算子来表示对象和监控器间的相互作 用，由此还以代数方式提出了分散控制问题【m 1 。 5 ) 基于p e t r i 网的建模和控制方法。这方面的研究是目前d e d s 研 究中重要的方向之一。 建模方面较突出的是向高层网的发展，基本思路是给托肯( t o k e n ) 赋予更多的结构内容以减少p n 的节点数目【17 1 。特别地，引入面向对象思 想的面向对象p e t r i 网【博】是很值得注意的研究方向，其基本思路是把系统 的各组成部分按功能划分为不同的对象类，个对象类用一个对象子网 建模，子网所带颜色区分对象类的个体，并表示进程，各子网之间通过 消息位置传递信息。区别于传统的面对过程的建模方法，采用面向对象 的思想更加易于揭示系统的本质特征，降低描述的复杂程度，提高模型 的可重用性。 控制手段可以是增加“控制位置”，通过用控制弧阻止某些变迁引发 或增加t o k e n 来实施控制。控制目标可以是某些状态集( 如禁止状态的 避免) 或“变迁串”的集( p n 语言) ，反馈信息可以是状态反馈或事件 ( 迁移) 反馈，关键问题也是计算的复杂性，p e t r i 网理论已有一些在制 造领域应用的实例【1 9 1 。 2 ) 时间层次 在模型中引入时间，不但可以研究d e d s 的实时动态性质，而且还 可进行系统性质的定量评估。这一层次上的主要模型方法有计时p e t r i 网、 d 一自动机、极大代数模型、2 一d 域代数模型【2 0 1 。其中在理论上比较 完整的是极大代数或更一般的d i o i d 理论 2 1 】。首先，它作为一种新的代数 结构上的数学理论，有极广的适用范围，例如可以把些非线性物理模 型系统划为“线性”的。从控制理论的角度看，用d i o i d 建立的时间层次 d e d s 模型酷似于传统的线性系统模型。尽管其物理含义有本质不同，人 们还是建立了一套与之平行的d e d s “线性”系统理论，并力图给以新的 解释。这套理论确实可以描述一些现象，回答一些问题，但基本上只对 应于赋时事件图( t e g ) 或标识图( m g ) ，即p e t r i 网的一个子类。另外， 极大代数的主要缺陷是仅适用于一类确定性的时序离散事件系统，难以 处理带决策的过程和具有随机变量的问题。近年来b a c c e l l i 等人建立了 套m a x 代数上的随机线性系统理论【2 2 1 。与之对应的是随机p e t r i 网或随机 事件图，它们适用于描述同步化、阻塞、f o r k j o i n 等性质。 时间层次模型具有定量的品质指标，从而可以提出明确的决策控制 优化问题。调度技术可以看成是对d e d s 进行的控制，旨在保证其基本 逻辑功能并优化其定量的性能指标( 往往与时间有关) 。分布式反馈调度 方法【2 3 】较好地体现了大系统递阶结构和反馈控制的思想，是当前调度问 题研究的重要方法之一。 8 3 ) 随机品质层次 随机现象在复杂系统中是非常普遍的，无论在制造系统、计算机系 统还是在通讯系统中，最后都要涉及随机品质评估和优化的问题。随机 d e d s 研究一直是该领域中最活跃的分支。这方面的模型主要有随机p e t r i 网、p 一自动机、排队网络、马尔可夫链、仿真模型等。这类模型更接近于 实际系统，侧重于系统的分析与评价，但其常常以具有随机参数的系统 作为研究对象，假设条件强，凶而实际应用时对系统的分析较为幽难， 耗时费力。 这一层次上的研究近几年在以下几个方面取得了较大的进展： 1 ) 扰动分析( p a ) 从一开始就以其新奇和巧妙的研究思路吸引了许 多研究者，但要把这种思路真正用于具体问题，仍要针对性地构造p a 算 法。近年来，一直有人致力于这方面的工作，使p a 的应用范围日益拓广。 作为理论基础的p a 算法无偏性和收敛性的证明，也取得不少进展。 2 ) 理论上，由单一轨线求取灵敏度信息的思想还可以用似然比方法 等加以实现。从p a 方法发展而成的“扰动分析r o b b i n s m o n r o 单轨 ( p a r m a r ) 算法”可以利用随机逼近的结果而保证其收敛性【2 4 1 。 y c h o 2 5 】进一步提出d e d s 的o r d i n a lo p t i m i z a t i o n 方法形成了一个新的 研究方向。 3 ) 随机d e d s 的最完备的模型g s m p 大多只能通过仿真进行研究。 但其中去除时间因素只构造逻辑轨迹的程式实际上正好反映了d e d s 的 多层次递阶建模的特征。这个程式框架的意义已经引起人们注意并称之 为g s m s ( g s ms c h e m e ) 。 4 ) 随机极大代数是由法国b a c c e l i 等人建立的。他们考虑一类具有同 步化阻塞和f o r k j o i n 特征的闭系统。其中一类可用随机事件图描述，另 一类是具随机先行关系的任务图，或者某类实时“再排序”模型。这类 系统的共同特点是可用( m a x ，+ ) 代数中的线性递推方程来表示。现在 已得到若干关键指标如队长、等待时间、闲置时间等的定常分布特征及 它们的唯一性的充要条件。 5 ) 排队网络能有效地进行处理的主要仍是具有乘积形式解的情形。 长期以来，人们力图扩大具乘积解的系统类并寻找有效的算法，但实际 中出现的一些问题要求人们直接研究非乘积解。 6 ) d e d s 的仿真研究仍然是最常用的途径之一。如p a 研究所示的 那样，仿真不仅是一种实验技术，而且已在相当程度上影响理论的内容、 风格，并成为理论的一部分。若干仿真语言本身已成为系统模型的一种 形式。 经过近二十年的发展，研究d e d s 的各派理论日趋成熟，它们也都 有一些成功的应用，但都是从不同的角度，基于不同的观点，采用不同 的数学方法而提出的，各有自己的优点和局限性，不足以支持整个领域， 所以d e d s 理论正面临着如何实用化和完善的问题。只有按照实际的需 求突出自己的研究特色，才能使d e d s 理论得以全面的发展。 1 3 研究动机和主要工作 在对离散型问题的研究中，计算机科学家做出了很大的贡献。目前关 于d e d s 研究中的许多概念和方法是由计算机科学家提供的，例如p e t r i 网方法，形式语言有限自动机理论等等。对时态逻辑的研究是当前计算 机科学界的一个研究热点，它被计算机科学家不断完善和发展，并已在 软件科学领域取得了令人瞩目的成果。这些已经引起了d e d s 研究者的 注意，w o n h a m ，o s t r o f f 等人在基于时态逻辑方法的d e d s 研究方面已开 展了定的工作。 相对于其它的d e d s 研究方法，时态逻辑具有更强的描述能力。以 往人们研究d e d s ，常常是基于状态或事件串，虽然能够对系统的行为进 行描述，并反映出一些微观上的行为特征，但难于直接描述系统的某些 宏观特征。例如有关系统的活性问题；当出现竞争时，系统要具备的公 平性问题。而时态逻辑描述应该说是接近自然语言的更高层次的描述， 它能更进一步地反映状态或事件串这些行为描述的时态特征。特别地， 对于某些复杂的实际系统，例如自动化立体仓库旋转货架系统，采用其 它d e d s 研究方法就很难描述其运行过程中的复杂逻辑关系和时序关系。 目前基于时态逻辑方法的d e d s 研究工作是比较零散和初步的，远 未形成一个象形式语言，有限自动机、p e t r i 网等方法那样的较完整的方法 体系。特别地，对于一些重要的问题，如证明过程的计算复杂性问题、 控制综合问题等都没有进行较深入的研究工作。 基于上述考虑，本文的研究工作注重基于时态逻辑研究d e d s 一般方 法的探讨和方法体系的建立，同时注重时态逻辑在d e d s 研究中的应用： 1 、我们采用一个比较成熟的系统m p t l ，给出了基于时态公式的离散事 件系统的时态模型，采用时态公式可以直接和简明地对系统期望行为进 行规范，使系统满足规范的时态特征的控制综合问题成为基于时态逻辑 方法解决d e d s 控制问题的关键。 2 、针对有限状态系统，给出了基于状态可达图的系统时态特征的判定 方法，相对于公式推导的方法，本方法直观、简单、有效。 3 、基于p e t r i 网方法与扩展时态逻辑一实时时态逻辑对实时d e d s 进行 了研究。提出了面向对象实时时态着色p e t r i 网模型，即保持了p e t r i 网的 直观图形描述的优点，又发挥了实时时态逻辑对时态性质和实时性质的 较强捕述能力，具有更强的可实用性和可操作性。 4 、d e d s 理论在自动化仓库中应用研究。在时态逻辑框架下对自动化仓 库中分拣系统的工作过程进行研究，基于时态公式对被控对象、控制器 和闭环期望动态行为进行了描述与分析，并对系统期望行为的可达性问 题进行了形式化的证明。自动化仓库中旋转货架系统的运行过程具有复 杂的离散事件特征，在时态逻辑框架下对此系统的运行过程进行描述与 分析，并给出了相应的控制策略，以使系统达到期望的动态行为。基于 面向对象时态着色p e t r i 网模型，对自动化仓库输送系统运行过程的调度 问题进行研究，建立了系统的面向对象着色p e t r i 网模型，讨论了该过程 的死锁分析问题，给出了系统行为的时态逻辑规范和死锁避免的最大允 许反馈控制策略。 2 。时态逻辑方法及应用 2 1 时态逻辑 自然语言中有一类词常用于表示事物的“势态”，人的“情态”，以 及过程的“变迁”( 历史的和未来的) 。例如“必然、可能”，“应该、允 许”，“知道、认可”，“一贯、偶然”等等。这类词被称为模态词( m o d a l i t i e s ) ， 它们和真值联结词相似，和命题相连接可以生成新的命题；例如，“火星 上可能有人”就是“可能”与“火星上有人”所组成的复合命题；它们 又和真值联结词不同，因为由真值联结词连接命题而组成的复合命题， 其真值完全由组成它的各成分命题的真值所确定，而由模态词连接命题 组成的复合命题就没有这种性质。任何人都不会同意“火星上有人”与 “火星上可能有人”具有相同的真值或具有相反的真值。 由于开始时模态词的语义不清楚，就有人认为模态词所反映的只是 “趋势”、“信念”，不是逻辑概念，甚至把它们看作文学修辞，主张“必 然a ”与a 相同，“不可能a ”与、a 一样( 其中a 为任一命题) 。如果 说这种做法在数学中勉强行得通，那么在日常推理中就寸步难行，因为 “a 真但是未必a 必然真”之类的说法几乎是常识。 亚里士多德( a r i s t o t l e ) 一开始便把“必然、可能”这一对模态词看 作逻辑概念，并对它们的逻辑性质作了相当详细的讨论，也许这可以说 是模态逻辑的起源。 逻辑学家和计算机科学家们为模态逻辑建议了多种不同的公理系统， 在不同的公理系统下有不同的模态公式成立。 模态逻辑是从对模态词“必然、可能”的研究开始的，这两个模态词 在自然语言中的意义如下： 必然a ( n e c e s s a r i l ya ) ，记为口a ，意思是：无论在什么场合( 现实 的场合或者可以想象到的非现实的场合) 均有事实a 。 可能a ( p o s s i b l ya ) ，记为o a ，意思是：对某些场合( 也许只是一 个，甚至只是想象得到的某个场合) 有事实a 。在不同的应用中，模态 词有不同的解释，从而对公理的选择有所不同。比较古老的解释有：真 理论模态逻辑、认识论模态逻辑和道义论模态逻辑；较新的解释有：时 态逻辑、经验论模态逻辑。下面逐一给予简单的介绍【2 6 】。 1 ) 真理论模态逻辑 真理论模态逻辑又称关于“必然”的模态逻辑。在这里研究的模态 词是“必然”和“可能”。由于模态逻辑的研究起源于对这对模态词的研 究，因此对真理论模态逻辑的讨论最为充分。 2 ) 认识论模态逻辑 认识论模态逻辑又称关于“知道”的模态逻辑。在这一逻辑中，口 和被分别解释为“知道”和“认口j ”。 3 ) 道义论模态逻辑 道义论模态逻辑也称关于“应该”的模态逻辑，它讨论模态词应该、 允许。我们可把 3 a 解释为“a 是应该真的”；可把o a 解释为“a 是允 许真的”。 4 ) 经验论模态逻辑 经验论模态逻辑也称关于经验的模态逻辑，讨论模态词“一贯地”、 “偶然地”、“经验地”以及“有先例地”。 5 ) 时态逻辑 时态逻辑讨论事件在时间上的将来永久性和可能性，是对模态逻辑 的一种时态解释。具体地说，它把模态词口解释为“将永远”，把模态 词解释为“将会有”，亦即 e 3 a表示r r a 将永远真 a表示“a 将会真” 下面对时态逻辑在计算机科学以及d e d s 研究中的应用进行论述。 2 2 时态逻辑在计算机科学中的应用 对时态逻辑的研究现在已成为计算机科学理论的一个重要研究课题， 它在并发程序的规范( s p e c i f i c a t i o n ) 、验证、语义形式化、操作系统与通 讯协议的分析以及数字化硬件系统的证明等方面的应用都已取得了令人 瞩目的成果【2 7 】。 时态逻辑不同于经典逻辑，其真假值依赖于时间而变化。对于程序 的数学处理，并不是静态的，它包含很重要的动态特征。一个典型的程 序执行模型就是状态序列，不同的状态，程序的属性如变量就具有不同 的值。时态逻辑正好可以用来描述一个情形( s i t u a t i o n ) 在时间上是如何 变化的，它被用作程序执行的数学基础，并且已广泛地应用于对动态性 质进行形式化描述和分析。现在，时态逻辑已成为程序规范和验证的一 个重要方法，特别是关于并发程序的验证；同时，时态逻辑又被计算机科 学家不断深化和发展【2 8 1 。 在文献中出现了多种形式的时态逻辑，基本时态算子集的定义和公 式的形成规则等语构的不同构成了各种时态逻辑间的差别；同时，在语 义上又存在着很大的差异，基本包含以下类型： 1 ) 区间语义( i n t e r v a ls e m a n t i c s ) ：基于时间区间，把系统行为分成 有限段。每个区间又可被分成两个相临区间，从而可以引入分割算子1 2 9 1 。 2 ) 点语义：把系统的行为对应于某一时间参考点来对时态公式进行 解释。过去算子指参考点之前的时间；将来算子指参考点之后的时间。 显然，点是不可以再分的，但点语义可进一步分为以下三种： a ) 线性语义( l i n e a rs e m a n t i c s ) ：相应于系统的演化的历史，每一 时刻都只有一个可能的将来( s u c c e s s o r ) 3 0 1 。 b ) 分支语义( b r a n c h i n gs e m a n t i c s ) ：时间有树状特征，在每删孩0 ， 时间可分成不同的趋向，表示系统的不同选择【3 1 1 。 c ) 偏序语义( p a r t i a l o r d e rs e m a n t i c s ) ：时态逻辑的解释域为一偏序， 这是最近才提出的较新的时态逻辑语义【3 2 】。 其中线性时间时态逻辑和分支时间时态逻辑是不可比的，都存在相 互间不可代替的描述能力。例如，分支时间逻辑不能描述公平性，而线 性时间逻辑则能直接规范公平性；另一方面，分支时间逻辑能描述某些 存在性路径条件，而这在线性时间时态逻辑中是不可能被描述的。 时态逻辑发展比较成熟，无论是在规范上还是在证明上，都具有了 一套完备的规则系统。目前已有了可执行的时态逻辑规范化语言i ，3 4 】，这 样在系统设计完成之后，就可以迅速地对系统进行验证。 对并发程序的验证，现在有两种不同的方法。一是将时态逻辑作为 一种推理系统，在此系统中构造出证明来，以说明系统( 程序) 满足其 规范。另外一种验证方法就是基于模型的模型校验( m o d e lc h e c k i n g ) 方 法，系统通过一个有穷状态转换图来表示，模型验证方法构造一个有效 算法来判定是否此系统是其时态规范的一个模型。对模型校验方法的研 究是当前软件科学的一个研究热点。 随着计算机技术的发展，人们对系统的要求不再仅仅是逻辑上的f 确性，同时更加注重系统的实时性质。关于实时系统的正确性验证是当 前软件科学的一个重要方向 3 6 , 3 7 1 。在采用的方法上，人们注意到了与其它 形式化方法的结合，特别是与p e t r i 网方法相结合 3 8 】，s u z u k i 等人提出时 态p e t r i 网的概念并在此模型框架下开展了一系列的研究工作 3 9 , 4 0 1 。 2 3 基于时态逻辑方法的d e d s 研究 把时态逻辑引入到对控制系统的研究，这方面的文章出现的较早，但 仅仅是对系统的某些性质进行规范，以增加对系统的描述能力】。真正 作为研究控制系统特别是d e d s 的方法被提出还是从八六年 4 2 1 开始的。 之后，基于时态逻辑研究d e d s 的文章在国际期刊和会议上逐渐多起来， 但仍然未形成一个完整的方法体系，研究工作主要是在针对某些问题的 典型特征进行规范这一层次上。在国内有关时态逻辑的研究工作不多， 基于此方法研究d e d s 的文献很少。文献【4 3 1 给出了一个基本研究思路， 但之后没见更深一步的研究。最近周剿臣教授提出了时段演算的方法， 并应用到对混杂动态系统的研究领域，时段演算可以认为是区间语义时 态逻辑的推广f “1 。 目前，基于时态逻辑研究d e d s 的核心思想是把系统的行为特征表述 为( y ，r ，e ) 上的时态公式，其中r = 兰n 卯e ( ) = 鱼q 。方法上大体可分为： 时态逻辑框架，t t m r t t l ( t t m ：t i m e dt r a n s i t i o nm o d e l ；r t t l ：r e a l t i m et e m p o r a ll o g i c ) 框架，与p e t r i 网和自动机方法相结合的研究框架。 下面对这三个框架下的研究思路、研究成果及存在的问题做一简要评述。 2 3 1 时态逻辑框架 在此框架下，采用时态公式的形式对系统本身的动态行为，系统的期 望动态行为及对系统所施加的控制策略进行描述，最后证明期望动态行 为的描述公式能由控制对象和控制策略的描述公式，采用时态逻辑证明 系统的有关定理和规则导出。 在此框架下，文献 4 2 ，4 5 1 讨论了系统的安全性和活性的分析问题，文 献 4 6 ，4 7 中，j y l i n 通过在时态逻辑中引入新的时态算子一确定性算子 ，表示概率为1 ，并定义可能算子三，( ( 一c o ) ，研究了点概率分布 己知情况下的一类非确定性离散事件系统。文献 6 9 则讨论了分支时间时 态逻辑对并发系统的描述与证明问题，不过在控制领域采用的较多的是 线性时间时态逻辑。 总的来说，在此框架下采用了更易于理解的高级描述方法和形式化 的证明过程。这一方法可以处理无穷状态系统，并避免了可能出现的状 态组合爆炸问题。但证明过程的计算复杂性问题和控制策略的综合问题 目前还没有很好地解决。 2