-
摘要: 1．本文的创新点
本文的主要创新是创建了一种全新的形式结构混合区域用于矩形混合系统的可达性分析，证明了混合区域对于混合系统两种类型的可达性操作是封闭的，同时它对于矩形混合系统的模型检查规则也是封闭的。把混合区域转变成标准形之后，计算可达集的运算变的十分直接，给出了一套约束求解规则加以解决，而不用传统的量词消去这样的运算。通过转化为线性规划问题，利用经典线性规划算法解决了混合区域的标准形问题。
2．实现方法
目前混合系统算法验证的研究主要集中在线性混合系统领域，非线性混合系统主要是转换为线性混合系统进行间接验证。由于混合系统是无穷状态空间系统，不能采取状态空间穷尽搜索的办法进行其算法验证，因此，混合系统的算法验证关键是采用什么样的结构表示其无穷状态空间。线性混合系统主要采用凸多面体或类似于凸多面体的结构，但是，采用这样的结构必须利用量词消去这样的算法计算可达集，量词消去运算的复杂度是指数级的。作为线性混合系统的子集，我们当然可以采用凸多面体作为矩形混合系统状态空间搜索的基本单位，但是，本文建立了一种全新的结构混合区域。混合区域是线性不等式联立表示的线性空间，这些不等式要么是一个连续变量与一个有理数的比较，要么是两个变量构成的线性表达式与一个有理数的比较，并且两个变量构成的表达式的系数与这两个变量微分取值域的端点有关。证明了混合区域可用于矩形混合系统可达性分析和模型检查。也就是说混合区域对于矩形混合系统的连续的延迟转换操作、离散的跳跃转换操着和模型检查规则都是封闭的。把混合区域转变成标准形之后，基于混合区域的可达性分析和模型检查变得较为简单，可以直接由本文给出的五种约束求解规则方便地解决。因此，基于混合区域的矩形混合系统的算法验证，关键的问题是计算混合区域的标准形。本文通过转换为线性规划问题，采用经典线性规划算法解决了混合区域的标准型问题。为了在计算机中表示混合区域，本文定义了一种矩阵数据结构“不同上限矩阵”，它的每个元素都表示构成该矩阵所表示的混合区域的一个线性不等式，并且实现了“不同上限矩阵”的对应于混合区域的五种可达性操作和模型检查规则。
3．结论及未来待解决的问题
混合区域是满足特殊限制条件的线性不等式联立表示的线性空间，这种结构可用于矩形混合系统的可达性分析和模型检查，定义了相应的数据结构表示混合区域，并实现了相应的可达性操作和模型检查规则。本文的模型检测是基于时间树逻辑Timed Computation Tree Logic (TCTL)的，实现了部分TCTL公式的模型检测算法，并且要求构成待检验的TCTL公式的状态公式必须可以用矩形表示，作为未来的一个研究任务，我们将解决全部TCTL的模型检测问题和一般的TCTL公式与符合检验条件的TCTL公式的转换问题。
4．实用价值或应用前景
混合区域可用于混合系统的算法验证，包括可达性分析和模型检测。对于矩形混合系统，我们可以直接利用混合区域为基本结构，利用本文中定义的可达性操作和模型检测规则进行其算法验证；对于线性和非线性混合系统，可以通过抽象转换为矩形混合系统，利用混合区域对其进行间接验证。利用理论研究成果开发的验证工具可用于实际众多的混合系统的可靠性和安全性验证，对促进国民经济发展和加强国防建设以及提高人民生活水平，都有着极其重要的意义。Abstract: This paper investigates symbolic algorithmic analysis of rectangular hybrid systems. To deal with the symbolic reachability problem, a restricted constraint system called \emph{hybrid zone} is formalized for the representation and manipulation of rec\-tangular automata state-spaces. Hybrid zones are proved to be closed over symbolic reachability operations of rec\-tangular hybrid systems. They are also applied to model-checking procedures for verifying some important classes of timed computation tree logic formulas. To represent hybrid zones, a data structure called \emph{difference constraint matrix} is defined. These enable us to deal with the symbolic algorithmic analysis of rectangular hybrid systems in an efficient way.-
Keywords:
- hybrid systems /
- model checking /
- automata /
- temporal logic
-
-
[1] Alur R, Courcoubetis C, Halbwachs N, Henzinger T A, Ho P-H, Nicollin X, Olivero A, Sifakis J, Yovine S. The algorithmicanalysis of hybrid systems. In Proc. ICAOS'94, LNCS 199,Berlin: Springer-Verlag, June 15-17, 1994, pp.331-351.
[2] Henzinger T A, Majumdar R. Symbolic model check-ing for rectangular hybrid systems (Abstract). In Proc.TACAS'2000, LNCS 1785, Berlin: Springer-Verlag, March25-April 1, 2000, pp.142-156.
[3] Henzinger T A, Kopke P W, Puri A, Varaiya P. What's de-cidable about hybrid automata?. In Proc. STOC'95, ACMPress, May 29-June 1, 1995, pp.373-382.
[4] Zhang H, Duan Z. Symbolic algorithm analysis of hybrid sys-tems. In Proc. TAMC'08, LNCS 4978, Berlin: Springer-Verlag, April 25-29, 2008, pp.294-305.
[5] Zhang H, Duan Z. Symbolic reachability analysis of hybridsystems. Journal of Software, 2008, 19(12): 3111-3121.
[6] Annichini A, Asarin E, Bouajjani A. Symbolic techniques forparametric reasoning about counter and clock systems. InProc. CAV'2000, LNCS 1855, Berlin: Springer-Verlag, July15-19, 2000, pp.419-434.
[7] Alur R, Henzinger T A, Ho P-H. Automatic symbolic verifi-cation of embedded systems. IEEE Transactions on SoftwareEngineering, 1996, 22(3): 181-201.
[8] Dill D L. Timing assumptions and verification offinite-stateconcurrent systems. In Proc. CAV'89, LNCS 407, Berlin:Springer-Verlag, June 12-17, 1989, pp.197-212.
[9] Wang F. Symbolic parametric safety analysis of linear hybridsystems with BDD-like data-structures. In Proc. CAV'04,LNCS 3114, July 13-17, 2004, pp.295-307.
[10] Anai H, Weispfnening V. Reach set computation using realquantifier elimination. In Proc. HSCC'01, LNCS 2034,Berlin: Springer-Verlag, March 28-30, 2001, pp.63-76.
[11] Alur R, Henzinger T A, Lafferriere G, Pappas G J. Discreteabstractions of hybrid systems. Proc. the IEEE, 2000, 88(7):971-984.
[12] Henzinger T A, Ho P H, Wong-Toi H. Algorithmatic analy-sis of nonlinear hybrid systems. IEEE-AC Transitions, 1999,43(4): 540-554.
[13] Clarke E M, Grumberg O, Peled D A. Model Checking.Cambridge: The MIT Press, Massachusetts, London, 1999,pp.284-287.
[14] Alur R, Courcoubetis C, Dill D L. Model-checking in densereal-time. Inform. Computat, 1993, 104(1): 2-34.
[15] Karmarkar N. A new polynomial-time algorithm for linearprogramming. Combinatorica, 1984, 4(4): 373-395.
[16] Henzinger T A, Ho P H, Wong-Toi H. A user guideto HYTECH. In Proc. TACAS'95, LNCS 1019, Berlin:Springer-Verlag, May 19-20, 1995, pp.41-71.
计量
- 文章访问数: 12
- HTML全文浏览量: 0
- PDF下载量: 2465
下载:
