Improving Efficiency of Model Checking for Variants of Alternating-time Temporal Logic (Extended Abstract)

Abstract

ion is a method which typically transforms large (or infinite) models into smaller (or finite) ones, but frequently defined over lattices of more that two truth values. We present multi-valued ATL? (mv-ATL?4), an expressive logic to specify strategic abilities in multi-agent systems [7]. We show how to identify constraints on mv-ATL?4 formulas for which the general method for model-independent translation from multi-valued to two-valued model, can be suitably adapted to mv-ATL? , Moreover, we present a model4 dependent reduction that can be applied to all formulas of mv-ATL?4. In all cases, the complexity of verification increases only polynomially when new truth values are added to the evaluation domain. Partial order reduction (POR) is another method used to alleviate the state space explosion in model checking [15]. We define a general semantics for strategic abilities of agents in asynchronous systems, with and without perfect information, and present some general complexity results for verification of strategic abilities in asynchronous

-

systems [11]. A methodology for POR in verification of agents with imperfect information is discussed, based on the notion of traces introduced by Mazurkiewicz. We define the logic simple ATL?, which is the restriction of ATL? such that the strategic modalities cannot be nested and the next step modality is not allowed. Two semantics of simple ATL? are considered and it is shown that for memoryless imperfect information contrary to memoryless perfect information, one can apply the partial order reduction techniques known for Linear-time Temporal Logic without the next step operator. 3

Timed ATL Finally, we discuss Timed Alternating-time Temporal Logic (TATL), a discrete-time extension of ATL. A new semantics, based on counting the number of visits in locations of the history, is introduced in addition to timed memoryful and memoryless ones [3]. We show that all the defined semantics are equivalent for TATL ; , i.e., when = is not allowed in the formulas. We provide a strategy analysis revealing that it suffices to consider only two actions per location to verify any TATL ; formula. This does not extend to TATL. The above results allow for building a hierarchy of strategies comparing the expressive power of the logics against ATL. We discuss a possible impact of this hierarchy on improving efficiency of model checking for TATL ; . 10. W. Jamroga, M. Knapik, D. Kurpiewski, and L. Mikulski. Approximate verification of strategic abilities under imperfect information. Artificial Intelligence, 2018. To appear. 11. W. Jamroga, W. Penczek, P. Dembin´ski, and A. Mazurkiewicz. Towards partial order reductions for strategic ability. In Proceedings of the 17th International Conference on Autonomous Agents and Multiagent Systems (AAMAS 2018), pages 156–165. IFAAMAS, 2018. 12. M. Kacprzak and W. Penczek. Unbounded model checking for Alternating-time Temporal Logic. In Proceedings of the 3rd International Joint Conference on Autonomous Agents and Multiagent Systems (AAMAS 2004), pages 646–653, 2004. 13. M. Kacprzak and W. Penczek. Fully symbolic unbounded model checking for Alternatingtime Temporal Logic. Autonomous Agents and Multi-Agent Systems 11 ( 1 ), 69–89, 2005. 14. A. Lomuscio and W. Penczek. Model checking temporal epistemic logic. In H.P. van Ditmarsch, J.Y. Halpern, W. van der Hoek, and B.P. Kooi, editors, Handbook of Epistemic Logic, pages 397–442. College Publications, 2015. 15. A. Lomuscio, W. Penczek, and H. Qu. Partial order reductions for model checking temporalepistemic logics over interleaved multi-agent systems. Fundamenta Informaticae, 101(12):71–90, 2010. 16. A. Lomuscio, H. Qu, and F. Raimondi. MCMAS: An open-source model checker for the verification of multi-agent systems. International Journal on Software Tools for Technology Transfer, 17( 1 ):9–30, 2017. Availabe online. 17. P. Y. Schobbens. Alternating-time logic with imperfect recall. Electronic Notes in Theoretical Computer Science, 85( 2 ):82–93, 2004.

References

1. T. A˚gotnes , V. Goranko , W. Jamroga , and M. Wooldridge . Knowledge and ability . In H.P. van Ditmarsch, J.Y. Halpern , W. van der Hoek, and B.P. Kooi, editors, Handbook of Epistemic Logic , pages 543 - 589 . College Publications, 2015 .

2. R. Alur , T. A. Henzinger , and O. Kupferman . Alternating-time Temporal Logic . Journal of the ACM , 49 : 672 - 713 , 2002 .

3. E ´ . Andre´, L. Petrucci , W. Jamroga , M. Knapik , and W. Penczek . Timed ATL: forget memory just count . In Proceedings of the 16th International Conference on Autonomous Agents and Multiagent Systems (AAMAS 2017 ), pages 1460 - 1462 . IFAAMAS, 2017 .

4. F. Belardinelli , R. Condurache , C. Dima , W. Jamroga , and A.V. Jones . Bisimulations for verification of strategic abilities with application to ThreeBallot voting protocol . In Proceedings of the 16th International Conference on Autonomous Agents and Multiagent Systems (AAMAS 2017 ), pages 1286 - 1295 . IFAAMAS, 2017 .

5. N. Bulling , J. Dix , and W. Jamroga . Model checking logics of strategic ability: Complexity . In M. Dastani, K. Hindriks , and J.-J. Meyer, editors, Specification and Verification of MultiAgent Systems , pages 125 - 159 . Springer, 2010 .

6. E.M. Clarke , O. Grumberg , and D. Peled . Model Checking. MIT Press, 1999 .

7. W. Jamroga , B. Konikowska , and W. Penczek . Multi-valued verification of strategic ability . In Proceedings of the 15th International Conference on Autonomous Agents and Multiagent Systems (AAMAS 2016 ), pages 1180 - 1189 . IFAAMAS, 2016 .

8. W. Jamroga , M. Knapik , and D. Kurpiewski . Fixpoint approximation of strategic abilities under imperfect information . In Proceedings of the 16th International Conference on Autonomous Agents and Multiagent Systems (AAMAS 2017 ), pages 1241 - 1249 . IFAAMAS, 2017 .

9. W. Jamroga , M. Knapik , and D. Kurpiewski . Model checking the Selene e-voting protocol in multi-agent logics . In Proceedings of the 3rd International Joint Conference on Electronic Voting (E-VOTE-ID 2018), Lecture Notes in Computer Science . Springer, 2018 . To appear.