迹有界WSTS的前向分析与模型检验
计算机科学中的逻辑
2016-03-07 v4
摘要
我们研究了良结构迁移系统(WSTS)的一个子类，即Ginsburg和Spanier (Trans. AMS 1964)意义下的有界完全确定系统，我们声称它为Finkel和Goubault-Larrecq (Logic. Meth. Comput. Sci. 2012)所发展的前向分析研究提供了充分的基础。事实上，我们证明了与之前考虑的用于前向分析终止性的其他条件不同，有界性是可判定的。有界性被证明是WSTS验证的一个有价值的约束，因为我们进一步表明它还能判定系统无穷迹集合上的所有-正则性质。
关键词
引用
@article{arxiv.1004.2802,
title = {Forward Analysis and Model Checking for Trace Bounded WSTS},
author = {Pierre Chambart and Alain Finkel and Sylvain Schmitz},
journal= {arXiv preprint arXiv:1004.2802},
year = {2016}
}