带整数重置的定时自动机的Myhill-Nerode风格刻画
A Myhill-Nerode style Characterization for Timed Automata With Integer Resets
AI总结：
本文为带整数重置的定时自动机提出依赖常数K的Nerode风格等价，建立Myhill-Nerode定理与规范自动机，并据此设计查询复杂度为多项式的Angluin风格主动学习算法。
摘要：
著名的有限词Nerode等价在我们理解正则语言类中起着基础性作用。该等价引出了Myhill-Nerode定理和一个规范自动机，而后者又是多种自动机学习算法的基础。针对各类定时语言，已有Nerode式等价的研究。本文聚焦于带整数重置的定时自动机。该类自动机已知具有良好的自动机理论性质，并且对实际建模也很有用。我们的主要贡献是为该类定义一个依赖于常数K的Nerode风格等价。我们证明该等价可导出Myhill-Nerode定理以及一个最大常数为K的规范单时钟整数重置定时自动机。基于该规范形式，我们开发了一个Angluin风格的主动学习算法，其查询复杂度是规范形式规模的多项式。
英文摘要：
The well-known Nerode equivalence for finite words plays a fundamental role in our understanding of the class of regular languages. The equivalence leads to the Myhill-Nerode theorem and a canonical automaton, which in turn, is the basis of several automata learning algorithms. A Nerode-like equivalence has been studied for various classes of timed languages. In this work, we focus on timed automata with integer resets. This class is known to have good automata-theoretic properties and is also useful for practical modeling. Our main contribution is a Nerode-style equivalence for this class that depends on a constant K. We show that the equivalence leads to a Myhill-Nerode theorem and a canonical one-clock integer-reset timed automaton with maximum constant K. Based on the canonical form, we develop an Angluin-style active learning algorithm whose query complexity is polynomial in the size of the canonical form.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
