使用重写规则和策略验证时间自动机
计算机科学中的逻辑
2009-07-20 v1
摘要
ELAN是一种强大的语言和环境，用于在基于由策略控制的重写规则的语言中指定和原型化演绎系统。时间自动机是一类反应系统的连续实时模型，已经为其设计了高效的模型检验算法。在本文中，我们展示了这些算法可以非常容易地在ELAN系统中进行原型化。通过这个例子，本文论证了基于重写规则和策略的系统是一个很好的框架，可以相当高效地对符号模型检验算法进行原型化、研究和测试，这些算法涉及图探索规则、演绎规则、约束求解技术和决策过程的组合。
引用
@article{arxiv.0907.3123,
title = {Verification of Timed Automata Using Rewrite Rules and Strategies},
author = {Emmanuel Beffara and Olivier Bournez and Hassen Kacem and Claude Kirchner},
journal= {arXiv preprint arXiv:0907.3123},
year = {2009}
}
备注
In the Proceedings BISFAI 2001, Seventh Biennial Bar-Ilan International Symposium on the Foundations of Artificial Intelligence. Ramat-Gan, 2001