天空非极限：Büchi 自动机补运算中电梯自动机的更紧秩界（技术报告）
计算机科学中的逻辑
2022-01-28 v2 形式语言与自动机理论
摘要
我们提出若干启发式方法，以缓解基于秩的 Büchi 自动机（BAs）补运算中组合爆炸的主要成因之一：对状态秩的不必要高界。首先，我们识别出电梯自动机，这是一类在实践中频繁出现的大型 BAs（推广了半确定型 BAs），其状态秩根据强连通分量的结构有界。电梯自动机的界也适用于包含电梯自动机作为子结构的一般 BAs。其次，我们引入两种利用自动机数据流分析精炼 BA 状态秩界的技术。我们将这些技术实现为 BA 补运算工具 Ranker 的扩展，并表明它们确实大幅剪枝了生成的状态空间，在大量基准上取得了显著更优的结果，并优于其他最先进的工具。
引用
@article{arxiv.2110.10187,
title = {Sky Is Not the Limit: Tighter Rank Bounds for Elevator Automata in B\"{u}chi Automata Complementation (Technical Report)},
author = {Vojtěch Havlena and Ondřej Lengál and Barbora Šmahlíková},
journal= {arXiv preprint arXiv:2110.10187},
year = {2022}
}
备注
An extended version of a paper accepted to TACAS'22