The benefits of relaxing punctuality
The benefits of relaxing punctuality
复制标题
DOI：
10.1145/227595.227602
复制
发表时间：
1996-01-01
影响因子：
2.5
通讯作者：
Henzinger, TA
中科院分区：
文献类型：
--
作者：
Alur, R;Feder, T;Henzinger, TA
实时系统建模的最自然，组成的方式使用了一个密集的域。然而，已知能够表达守时的时间限制的满足性是不可决定的。我们引入了一种时间语言，该语言只能使用有限但任意的精确度来限制事件之间的时间差，并显示所得的逻辑是expspace-complete。该结果使我们能够开发一种算法，以验证具有密集语义的实时系统的定时属性。
The most natural, compositional, way of modeling real-time systems uses a dense domain for time. The satisfiability of timing constraints that are capable of expressing punctuality in this model however, is known to be undecidable. We introduce a temporal language that can constrain the time difference between events only with finite, yet arbitrary, precision and show the resulting logic to be EXPSPACE-complete. This result allows us to develop an algorithm for the verification of timing properties of real-time systems with a dense semantics.