What's decidable about hybrid automata?
What's decidable about hybrid automata?
复制标题
DOI：
10.1006/jcss.1998.1581
复制
发表时间：
1998-08-01
影响因子：
1.1
通讯作者：
Varaiya, P
中科院分区：
文献类型：
--
作者：
Henzinger, TA;Kopke, PW;Varaiya, P
具有数字和模拟组件的混合自动机模型系统，例如嵌入式控制程序。此类程序的许多验证任务可以表示为混合自动机的可达性问题。通过改进先前的可判定性和不可判定性结果，我们确定了混合自动机可达性问题的可判定性和不可判定性之间的边界。从积极的一面来看，我们针对初始化矩形自动机的情况给出了一种（最佳）PSPACE可达性算法，其中所有模拟变量都遵循分段线性包络内的独立轨迹，并且每当包络发生变化时都会重新初始化。我们的算法基于定时自动机的构造，其中包含有关给定初始化矩形自动机的所有可达性信息。该翻译对于验证具有实际意义，因为它保证了初始化矩形自动机的可达性分析的符号过程的终止。该翻译还保留了具有有限非确定性的初始化矩形自动机的欧米伽语言。从消极的一面来看，我们表明初始化矩形自动机的一些轻微的概括会导致不可判定的可达性问题。特别是，我们证明了可达性问题是用单个秒表增强的不可判定的远时自动机。 (C) 1998 年学术出版社。
Hybrid automata model systems with both digital and analog components, such as embedded control programs. Many verification tasks for such programs can be expressed as reachability problems for hybrid automata. By improving on previous decidability and undecidability results, we identify a boundary between decidability and undecidability for the reachability problem of hybrid automata. On the positive side, we give an (optimal) PSPACE reachability algorithm for the case of initialized rectangular automata, where all analog variables follow independent trajectories within piecewise-linear envelopes and are reinitialized whenever the envelope changes. Our algorithm is based on the construction of a timed automaton that contains all reachability information about a given initialized rectangular automaton. The translation has practical significance for verification, because it guarantees the termination of symbolic procedures for the reachability analysis of initialized rectangular automata. The translation also preserves the omega-languages of initialized rectangular automata with bounded nondeterminism. On the negative side, we show that several slight generalizations of initialized rectangular automata lead to an undecidable reachability problem. in particular, we prove that the reachability problem is undecidable far timed automata augmented with a single stopwatch. (C) 1998 Academic Press.