MCMAS-SLK：用于验证策略逻辑规范的模型检测器
计算机科学中的逻辑
2014-05-19 v3
摘要
我们介绍了 MCMAS-SLK，这是一种基于 BDD 的模型检测器，用于针对以新型认知策略逻辑变体表达的规范来验证系统。我们给出了该规范语言的语法和语义，并引入了针对认知和策略逻辑模态的标记算法。我们提供了检测器的详细信息，该检测器也可用于综合智能体策略，以使系统满足特定规范。我们通过讨论在密码学家就餐协议和分蛋糕问题变体上获得的结果，评估了该实现的效率。
引用
@article{arxiv.1402.2948,
title = {MCMAS-SLK: A Model Checker for the Verification of Strategy Logic Specifications},
author = {Petr Čermák and Alessio Lomuscio and Fabio Mogavero and Aniello Murano},
journal= {arXiv preprint arXiv:1402.2948},
year = {2014}
}