Verification of Context-Free Timed Systems Using Linear Hybrid Observers
Verification of Context-Free Timed Systems Using Linear Hybrid Observers
复制标题
使用线性混合观测器验证上下文无关定时系统
DOI：
10.1007/3-540-58179-0_48
复制
发表时间：
1994
期刊：
影响因子：
--
通讯作者：
R. Robbana
中科院分区：
文献类型：
--
作者：
A. Bouajjani;R. Echahed;R. Robbana
我们讨论了无限时间系统的验证问题。我们将上下文无关时间系统定义为(正则)时间图[ACD90]的推广。然后，我们提出了用观测变量表示的验证这些系统不变性的判定程序。这些变量记录了有关被观测系统计算的相关信息。它们会随着这些计算永久更新，而不会对系统的行为产生任何干扰。观测变量可以是附加时钟(定时器)、无界整数变量(累加器)或常斜率连续(实数值)变量(积分器)。
We address the verification problem of infinite timed systems. We consider context-free timed systems defined as a generalization of the (regular) timed graphs [ACD90]. Then, we propose decision procedures for the verification of invariance properties of these systems, expressed by means of observation variables. These variables record relevant informations about the computations of the observed system. They are permanently updated along these computations without any interference with the behaviour of the system. Observation variables are either additional clocks (timers), nonbounded integer variables (accumulators), or constant slope continuous (real valued) variables (integrators).