寄存器自动机配置的有限精确表示
形式语言与自动机理论
2014-02-28 v1 计算机科学中的逻辑
摘要
寄存器自动机是一种具有有限个寄存器的有限自动机，这些寄存器取值于无限字母表。由于寄存器的赋值是无限的，因此存在无限多种配置。我们描述了一种将无限寄存器自动机配置分类为有限多个精确代表性配置的技术。利用这种有限表示，我们给出了一种求解寄存器自动机可达性问题的算法。此外，我们定义了寄存器自动机的计算树逻辑，并求解了其模型检验问题。
引用
@article{arxiv.1402.6783,
title = {A Finite Exact Representation of Register Automata Configurations},
author = {Yu-Fang Chen and Bow-Yaw Wang and Di-De Yen},
journal= {arXiv preprint arXiv:1402.6783},
year = {2014}
}
备注
In Proceedings INFINITY 2013, arXiv:1402.6610