停止它，并保持顽固！
计算机科学中的逻辑
2016-05-23 v1
摘要
一个系统是AG EF终止的，当且仅当从每个可达状态出发，均可到达一个终止状态。本文主张，试图使验证模型成为AG EF终止的，对于捕获无进展错误和顽固集状态空间约简均有益。以一个错误的互斥算法为例。除非将顾客的首次动作与其他动作区别建模，否则该错误不会显现。一种合适的方法是添加一个替代的首次动作，用于建模顾客永久停止。该方法通常使模型成为AG EF终止的。若模型是AG EF终止的，则基本强顽固集方法在无需任何解决忽略问题的附加条件下保持安全性和某些进展性质。此外，是否模型为AG EF终止可从约简状态空间高效检查。
引用
@article{arxiv.1504.02587,
title = {Stop It, and Be Stubborn!},
author = {Antti Valmari},
journal= {arXiv preprint arXiv:1504.02587},
year = {2016}
}