用于将 Rabin 自动机转换为奇偶自动机的索引出现记录
计算机科学中的逻辑
2021-02-02 v1 形式语言与自动机理论
摘要
将确定性 -自动机转换为确定性奇偶自动机传统上是使用出现记录的变体完成的。我们提出了一种针对 Rabin 自动机的更高效方法变体,以及适用于所有出现记录的几种优化。我们通过实验比较了这些方法,发现我们的方法比先前的方法产生更小的自动机。此外,实验证明了我们的方法在使用 LTL-to-Rabin 转换器进行 LTL 综合方面的潜力。与最先进的方法在复杂公式上相比,它产生了显著更小的奇偶自动机。
引用
@article{arxiv.1701.05738,
title = {Index appearance record for transforming Rabin automata into parity automata},
author = {Jan Křetínský and Tobias Meggendorfer and Clara Waldmann and Maximilian Weininger},
journal= {arXiv preprint arXiv:1701.05738},
year = {2021}
}