Automated Technology for Verification and Analysis - 21st International Symposium, ATVA 2023, Singapore, October 24-27, 2023, Proceedings, Part I
Automated Technology for Verification and Analysis - 21st International Symposium, ATVA 2023, Singapore, October 24-27, 2023, Proceedings, Part I
复制标题
验证和分析自动化技术 - 第 21 届国际研讨会，ATVA 2023，新加坡，2023 年 10 月 24-27 日，会议记录，第一部分
DOI：
10.1007/978-3-031-45329-8_3
复制
发表时间：
2023
期刊：
影响因子：
--
通讯作者：
Li Y
中科院分区：
文献类型：
--
作者：
Li Y
DFAs族（FDFA）最近被引入作为一种新的表示-正则语言。它们最终以周期性的词为目标，接受者围绕着接受某种表示。三个典型的FDFA已经提出，称为周期性，句法，和递归。我们提出了第四个，限制FDFA，它可以是指数粗糙比周期FDFA和更简洁的语法FDFA，而他们是无法比拟的（和双）经常性FDFA。我们表明，有限FDFA可以很容易地用来检查不仅是否语言是正规的，而且它们是否被接受的确定性Büchi自动机。我们还表明，规范形式可以在应用程序中被抛在后面：极限和经常性FDFA可以很好地相互补充，这可能是一个很好的方式来使用两者的组合。以这一观察为起点，我们探索更有效地利用Myhill-Nerode的右同余，积极增加不关心的情况下，以获得更小的进度自动机的数量。在追求这一目标的过程中，我们获得了简洁，但付出了失去建设性的高昂代价。
Families of DFAs (FDFAs) have recently been introduced as a new representation of-regular languages. They target ultimately periodic words, with acceptors revolving around accepting some representation. Three canonical FDFAs have been suggested, calledperiodic,syntactic, andrecurrent. We propose a fourth one,limit FDFAs, which can be exponentially coarser than periodic FDFAs and are more succinct than syntactic FDFAs, while they are incomparable (and dual to) recurrent FDFAs. We show that limit FDFAs can be easily used to check not only whether-languages are regular, but also whether they are accepted by deterministic Büchi automata. We also show that canonical forms can be left behind in applications: the limit and recurrent FDFAs can complement each other nicely, and it may be a good way forward to use a combination of both. Using this observation as a starting point, we explore making more efficient use of Myhill-Nerode’s right congruences in aggressively increasing the number of don’t-care cases in order to obtain smaller progress automata. In pursuit of this goal, we gain succinctness, but pay a high price by losing constructiveness.