时间自动机的更优抽象
计算机科学中的逻辑
2016-07-29 v7 形式语言与自动机理论
摘要
我们考虑时间自动机的可达性问题。该问题的标准解法涉及计算一棵搜索树，其节点为区域的抽象。这些抽象保持了自动机状态空间上的底层模拟关系。出于有效性和效率的考虑，它们由自动机守卫(guard)中出现的最大下界和上界（LU-bounds）参数化。我们考虑Behrmann等人定义的aLU抽象。由于该抽象可能产生非凸集合，它尚未在实现中使用。我们证明了aLU抽象是关于LU-bounds的最大抽象，且对于可达性是 sound 和 complete 的。我们还提供了一种利用aLU抽象求解可达性问题的高效技术。
引用
@article{arxiv.1110.3705,
title = {Better abstractions for timed automata},
author = {Frédéric Herbreteau and B. Srivathsan and Igor Walukiewicz},
journal= {arXiv preprint arXiv:1110.3705},
year = {2016}
}
备注
Extended version of LICS 2012 paper (conference paper till v6). in Information and Computation, available online 27 July 2016