Maude中的策略、模型检验与分支时间属性
计算机科学中的逻辑
2024-01-17 v1
摘要
重写逻辑及其实现Maude是规约并发系统和逻辑的自然且富有表现力的框架。其非确定性局部转换由重写规则描述，这些规则可在更高层次上使用Maude~3内置的策略语言进行控制。若无分析其模型的工具，这种规约资源将意义不大，因此在先前工作中，我们扩展了Maude LTL模型检验器以验证策略控制的系统。本文在讨论了分支时间属性需要哪些适配之后，将CTL*和-演算添加到支持的逻辑库中。新的扩展依赖于一些外部模型检验器，这些检验器通过通用且高效的连接暴露Maude模型，有利于未来的扩展和进一步的应用。文中比较了这些模型检验器的性能。
引用
@article{arxiv.2401.07680,
title = {Strategies, model checking and branching-time properties in Maude},
author = {Rubén Rubio and Narciso Martí-Oliet and Isabel Pita and Alberto Verdejo},
journal= {arXiv preprint arXiv:2401.07680},
year = {2024}
}