论文标题
基于SAT的ATL满意度检查
SAT-Based ATL Satisfiability Checking
论文作者
论文摘要
模型和策略的综合是软件工程中非常重要的问题。这里的主要元素是检查表达要实现的系统规范的公式的满意度。本文提出了一种新的方法，用于确定交替时间时间逻辑公式（ATL）的满意度。介绍的方法扩展了用于CTL开发SAT Modulo单调理论求解器的一种扩展。与CTL情况类似，我们的方法似乎非常有效。实验结果表明，我们可以快速测试现有方法无法触及的大型ATL公式的满意度。
Synthesis of models and strategies is a very important problem in software engineering. The main element here is checking the satisfiability of formulae expressing the specification of a system to be implemented. This paper puts forward a novel method for deciding the satisfiability of formulae of Alternating-time Temporal Logic (ATL). The method presented expands on one for CTL exploit ing SAT Modulo Monotonic Theories solvers. Similarly to the CTL case, our approach appears to be very efficient. The experimental results show that we can quickly test the satisfiability of large ATL formulae that have been out of reach of the existing approaches.
