离散控制连续系统的时态算法

220[2014 -05-23]∞[理论计算机科学电子笔记42（2001）网址：http://www.elsevier.nl/locate/entcs/volume42.html12页离散控制连续系统的时态算法Tetsuya Mizutania、Shigeru Igarashia和Masayuki Shioba筑波大学信息科学研究所，1-1-1，Tenjiai，邮编：3050006b日本水户县美和市1-430-1，常盘大学社区发展学院，邮编3108585摘要作为离散控制连续系统的一个例子，车辆控制系统的规范在一个称为有理数时间并发程序的时态算法的正式系统中表示和验证。在这种形式主义中，计算序列的特点，或索引，由spurs，是推广的程序设计师，也是时间命题。我们的形式主义描述了从观察时间分析下一个动作的唤醒时间，并且我们获得了下一个动作何时发生的实际合理时间值。此外，我们引入了连续变量及其一阶和二阶导数，以分析和验证离散控制某些连续物理或其他外部系统的程序。1介绍本文以离散控制连续系统为例，描述并分析了一个车辆控制系统[6]，用时态算法[8]（简称TA）来验证包含有理数时间的并发程序这种形式主义有三个特点。首先，它明确地处理理性时间，称为时态。第二，它用P的时态来解释扩展的有理数理论中的每个公式P，用P来表示，也就是说，从观察时间（比如t）到P在t之后第一次成立的时间之间的时间长度。（作为false的缩写引入。）此外，我们还引入了未来性算子“;“，将观测时间向前第三，观察时间t被视为现在时或现在，即，0，所以我们可以省去时间变量t。在本文中，我们将这种形式主义治疗连续系统。为此，将引入连续变量及其一阶和二阶导数。 使用这些变量，我们可以分析和验证离散控制某些连续物理或其他外部系统的程序。2001年由ElsevierS cienceB. V. 操作访问和C CB Y-NC-ND许可证。水谷，我GARASHI和SHIO221···[2014 -05-23]···人们已经提出了许多用于验证实时系统的形式化方法，包括时态逻辑[9]、TCSP [4]、持续时间演算[2]、混合自动机[1]、[3]、[14]等，以及与本文密切相关的我们的工作[6]、[7]、[11]在[13]中找到并验证了自主车辆控制系统的规范持续时间演算和混合自动机只能处理一阶微分方程，而我们的形式主义可以处理低阶和高阶微分方程。第2节展示了TA的形式系统和语义，其原始版本可以在[8]中找到第3节介绍并分析了车辆控制系统在这个例子中，我们考虑的情况下，汽车合并与交通在T型交叉口。我们制定这个问题，然后正式分析和验证的条件下，合并的汽车不撞到别人。2时态算术2.1语言学设TQ是任何适当的有理数的一阶理论。设VQ是T Q的自由变量的集合。VQ的一个元素称为有理变量。我们通过增加单独的常数J，J1，J2，，对应于有理数上的程序变量，称为特殊有理数常数;通过添加与程序内的标签对应的谓词常数l，l1，l2，···;以及通过添加谓词常数γstec，γstec 1，γstec 2，，对应于我们用来构造杂散的原子杂散。 这些谓词常量称为特殊布尔常量。 spurs是程序设计者的概括（见2.4节）。此外，我们还引入了其他特殊的有理常数，1，2，·· ·，η，η1，η2，···称为连续变量，它们的（一阶和二阶）导数为J，1J，2 J，···，ηJ，η1J，η2J，···，jJ，1 J J，2 J J，· ··，ηJ J，η1J J，η2J J，· ··，来描述连续系统。TA的项和公式称为时态项和时态公式，特别是，为了区分它们与TCQ。设VT是可数无限时态变量的集合定义2.1时态术语定义如下：(i) TCQ中的项e是时态项，称为关系时态项，(ii) 时态变量x是时态项，(iii) F或a对于TCQ的mulaP，[P]是时态项，称为P的时态，(iv) 如果s是时态项，则s; e，s; x和s;[P]都是时态项。✷符号将被称为时态符号，而符号s被称为s的前缀;x。一般来说，s被称为s的前缀;s1。水谷，我GARASHI和SHIO222[2014 -05-23][2014-05 -23]1[2014 -05-23]111定义2.2时态公式定义如下：(i) TCQ的mulaP的F或a，P是mula的时态(ii) 如果s和s1是时态项，则s=s1和s≤s1是时态公式，(iii) 如果x是时态变量，r是有理数变量，F和G是时态公式，则<$F、F<$G、<$xF和<$rF是时态公式。✷时态表示相对于观察时间的时间，称为现在。作为时态项，值为r的有理表达式e表示时态r。0代表现在。由P表示的P的时态是P在现在之后保持的最早时间。对于未来运算符(i) 二、0;J= 0表示程序变量J在2.0个时间单位后达到值0时的时态，(ii) 二、0;[J = 0]= ∞表示“J在2之后永远不会变成0。0”。2.2顺序和证明系统定义2.3对于时态公式F1，···，Fm，G1，···，Gn（m，n≥0），F1，···，Fm→G1，···，Gn是一个（TA的）符号m= 0的情况被理解为n = 0为“假”。✷A<$F1，···，F m→ G1，···，G n直观地意味着F1<$···<$F m<$G1<$··<$Gn对任何“世界”（随时间变化）和任何观察时间都成立。 因此，该序列与时序逻辑中的形式模（F1< $ ···<$Fm <$G1<$··<$Gn）表示相同的内容.定义2.4符号∞是[false ∞]的缩写，因此，∞=[false]，“x：（s≤s）def （x;s）≤（x;s），x：（s=s）def （x;s）=（x;s），x：（FG）defdef（x：F）（x：G），x：（<$F）defdef（x：F），r（x：F）惠x：（rF），惠y（x：F）惠x：（yF），以及x：Pdef x=（x;[P]）.在“：“的定义中，✷冒号“：“作为一个符号被称为巧合运算符，它直观地在s;P中，s或s内的任何前缀都称为s的前缀：F。⇔⇔⇔⇔⇔水谷，我GARASHI和SHIO223∀¬∨ ∀∀→···定义2.5TA的推理规则由与结构规则和逻辑运算符规则具有相同形式的类LK规则组成、和而在《易经》中，只有一条规则，那就是：x和r是相互独立的。此外，采用了未来性规则如下：→x：F→F0≤s1···0 ≤sn其中s1，，sn是F中等式或不等式的所有时态项的前缀。✷定义2.6 TA的派生词由以树的形式排列的序列组成。一个初始的变量，即，叶，其派生是以下任何一种：(i) 咨询热线： F→F，(ii) 公理化推理：→A，对于TA的任何公理A每一个推理结果的推理规则之一，通过一个通常的subjuvenation。最后，即，求导的根S称为可导的(in TA），整个推导过程称为S的一个证明。✷定义2.7如果一个形式为F的矩阵是可导的，我们说F是（在TA中）是可证明的，F是（TA的）定理，该事实将被表示为：► F.✷2.3公理我们引入TA的逻辑或真公理 必须注意的是，r和r1被限制在有理数内（不包含 ∞ ） 。 符 号 = 和 ≤ 与 TQ 和 TCQ 中 使 用 的 符 号 相 同 ， 因 此 0<1 ， <$rr1（r+r1=r1+r），J = J1<$J +1 = J1+ 1等，举个例子。(i) 的顺序公理。(ii) 时态公理(a) 时态公理：<$x（<$r（x=r）<$x=∞），(b) <‘Never Land’ (unreachability)axiom(c) 真值公理：[true] = 0，(d) 无用公理：x（∞=x;∞），(iii) 未来公理(a) 现在公理：x（0 ≤x<$0;x=x），(b) 通道公理：xy（x≤x;y），(c) 延拓公理：rrr1（0≤r1<$r;r1=r+r1<$r10<$r;r1=r），(d) 前缀替换公理：xyz（x=yx;z=y;z），(iv) 时态符号的公理[1]：(a) 幂等公理：[P=[P;[P，水谷，我GARASHI和SHIO2242···M(b) 优先公理：x（0≤xx：P [P≤x），(c) 超前推论公理：[Q<$≤ [P <$]，对任意P和Q，使得P<$Q是TCQ的一个定理，不含连续变量，(d) 单调性公理：[P]xy（x ≤y <$x;[P<$≤y; [P<$]），(v) 作为公理的TCQ定理：T C Q的 一个y定理是TA的一个公理。(vi) 连续变量公理：J=c 1 0且x|=<$F1<$···<$F m<$G1<$···<$G n。 ✷定义2.14推导的合理性对于TA的序列S1，···，Sn和S，从TA的序列S1，···，Sn导出S是可靠的当且仅当满足所有序列S1，···，Sn的每个轨迹χ也满足S.水谷，我GARASHI和SHIO228−原TA的可靠性定理在[8]中得到了保证。对于修改后的系统，下面的可靠性定理可以很容易地以类似的方式证明定理2.15如果f∈ F，则χ |F对每个x都成立。✷3一种车辆控制系统让我们考虑两条道路在一个T形交叉口交汇的情况。许多汽车car1、car2、···、carn、carn+1、···以恒定速度v[m/s]在道路上单向行驶，并且每对汽车i、i + 1在这对汽车内具有距离i。 汽车汽车0想要以初始速度0和加速度a=a0（>0）[m/s2]i在汽车n和汽车n+1之间合并，如果n小于或等于d。驾驶员而且，当车速为v（ 755/ 36[m]（约21 m），汽车n+1不会撞到汽车0。水谷，我GARASHI和SHIO2334结论本文简要地介绍了一种新的并行和实时控制程序的形式化TA，并分析了两个智能控制系统。在车辆控制系统的分析中，我们已经使用连续变量公理显示了避免两辆车之间碰撞所需的实际和合理的值我们未来的工作是使公理更加复杂，以便以统一的方式描述每一个n确认这项工作得到了日本教育、科学和文化部科学研究补助金的部分支持。09680322和10680332）和Fuji Xerox。引用[1] 巴尔河，菲克斯湖和Henzinger，T. A.事件时钟自动机：一个可确定的时间自动机类，Theor。Comp. Sci. ，（1999），pp.252-273。[2] 赵朝晨：持续时间演算：概述，国际软件技术研究所，联合国大学，UNI/IIST报告，10（1993）。[3] Henzinger，T.A. 和Kopke，P.魏： 矩形混合自动机的 离 散 时 间 控 制 。Comp. Sci. ，211（1999），pp.369-392.[4] 霍 尔 角 A. R. ： Communicating sequential processes ， Prentice-HallInternat. ，1985年。[5] Igarashi，S：V-转换和分析语义学，R。E. A. Mason（ed.），信息处理83，Elsevier Sci.Publ. B. 五、（1983），pp. 769-774。[6] Igarashi，S.， Mizutani，T.， Shirogane，T. 和Shio，M：程序控制的连续系统的形式化分析，并发性和并行性，编程，网络和安全，计算机科学讲义，1179（1996），pp. 347-348.[7] Igarashi，S，Shio，M.，Shirogane，T.和Mizutani，T.：正式核查 以及信封理论中的执行时间评估，并发性和并行性，编程，网络和安全，计算机科学讲义，1179，（1996），pp. 299-308[8] Igarashi，S.，Shirogane，T.，Shio，M.和Mizutani，T.：Tense arithmeticsI ： formalizationof properties of programs in rational arithmetics ，Tensor，N. S. ，59（1998），在印刷中。[9] 陈文，程序设计的基本原理，北京：计算机科学出版社，1998.水谷，我GARASHI和SHIO234[10] McCarthy，J.：A basis for a mathematical theory of computation，P. BraBrachort and D. Hirschberg（eds.），计算机程序设计与形式系统，逻辑与数学基础系列研究，北荷兰出版社，Amsterdam，1963，pp. 33比70[11] Mizutani，T.，Igarashi，S.，Tomita，K.和Shio，M. ：离散控制连续系统在面向软件的形式分析中的表示，计算机科学进展，计算机课程讲义。Sci. ，1345（1997），pp. 110-120[12] Takeuti，G：Two Applications of Logic to Mathematics，Princeton Univ.Press，Princeton，1978.[13] Tomita，K.，Igarashi，S.，细野角Mizutani，T.和Tsugawa，S. 自主实时系统的表示，TENSOR，N。S. ，59（1998），在印刷中。[14] 宣洞湖，洪氏D. V.和陶，Z：检查线性持续时间不变量的混合自动机，计算机科学进展，计算机科学进展，计算机科学讲义。，1345（1997），pp.166比180