Membership questions for timed and hybrid automata
Membership questions for timed and hybrid automata
复制标题
定时和混合自动机的成员资格问题
DOI：
--
复制
发表时间：
1998
期刊：
影响因子：
--
通讯作者：
Mahesh Viswanathan
中科院分区：
文献类型：
--
作者：
R. Alur;R. Kurshan;Mahesh Viswanathan
定时和混合自动机是有限状态机的扩展，用于对具有离散和连续组件的嵌入式系统进行形式化建模。这些自动机的可达性问题得到了充分研究，并已在验证工具中实现。为了有效的错误报告和测试，我们考虑此类自动机的成员资格问题。我们根据是否指定路径（即边缘序列）、跟踪（即事件序列）或定时跟踪（即带时间戳的事件序列）来考虑不同类型的成员资格问题。我们给出了关于不同类型自动机（例如定时自动机和线性混合自动机）的这些隶属度问题的复杂性的综合结果，有或没有 /spl epsiv/ 转换。特别是，我们给出了一种有效的 O(n/spl middot/m/sup 2/) 算法，用于生成与具有 m 个时钟的定时自动机中长度为 n 的路径相对应的时间戳。该算法在验证器 COSPAN 中实现，以改善其在时序验证期间的诊断反馈。其次，我们表明，对于没有 /spl epsiv/ 转换的自动机，对于不同类型的自动机，成员资格问题是 NP 完全的，无论时间戳是否与跟踪一起指定。第三，我们表明，对于具有 /spl epsiv/ 转换的自动机，即使对于定时跟踪，成员资格问题也与可达性问题一样困难：对于定时自动机来说，它是 PSPACE 完整的，并且对于轻微的概括是不可判定的。
Timed and hybrid automata are extensions of finite state machines for formal modeling of embedded systems with both discrete and continuous components. Reachability problems for these automata are well studied and have been implemented in verification tools. For the purpose of effective error reporting and testing, we consider the membership problems for such automata. We consider different types of membership problems depending on whether the path (i.e. edge sequence), or the trace (i.e. event sequence), or the timed trace (i.e. timestamped event sequence), is specified. We give comprehensive results regarding the complexity of these membership questions for different types of automata, such as timed automata and linear hybrid automata, with and without /spl epsiv/ transitions. In particular we give an efficient O(n/spl middot/m/sup 2/) algorithm for generating timestamps corresponding to a path of length n in a timed automaton with m clocks. This algorithm is implemented in the verifier COSPAN to improve its diagnostic feedback during timing verification. Second, we show that for automata without /spl epsiv/ transitions, the membership question is NP complete for different types of automata whether or not the timestamps are specified along with the trace. Third, we show that for automata with /spl epsiv/ transitions, the membership question is as hard as the reachability question even for timed traces: it is PSPACE complete for timed automata, and undecidable for slight generalizations.