=Paper=
{{Paper
|id=Vol-2240/invited2
|storemode=property
|title=Improving Efficiency of Model Checking for Variants of Alternating-time Temporal Logic
|pdfUrl=https://ceur-ws.org/Vol-2240/invited2.pdf
|volume=Vol-2240
|authors=Wojciech Penczek
|dblpUrl=https://dblp.org/rec/conf/csp/Penczek18
}}
==Improving Efficiency of Model Checking for Variants of Alternating-time Temporal Logic==
https://ceur-ws.org/Vol-2240/invited2.pdf
Improving Efficiency of Model Checking
for Variants of Alternating-time Temporal Logic
(Extended Abstract)
Wojciech Penczek1,2
1
Institute of Computer Science, PAS, Warsaw, Poland
2
University of Natural Sciences and Humanities, ICS, Siedlce, Poland
penczek@ipipan.waw.pl
1 Multi-agent Systems and ATL?
Multi-agent systems describe interactions of multiple entities called agents, often as-
sumed to be intelligent and autonomous [1, 14]. Alternating-time temporal logic (ATL? )
and its fragment ATL [2] are logics which allow for reasoning about strategic interac-
tions in such systems, by extending the framework of temporal logic with the game-
theoretic notion of strategic ability. Hence, ATL? enables to express statements about
what agents or their groups can achieve. Such properties can be useful for specification,
verification, and reasoning about interaction in agent systems [12, 13], as well as about
security and usability in e-voting protocols [4, 9]. They have become especially relevant
due to active development of algorithms and tools for verification [16], where the “cor-
rectness” property is given in terms of strategic ability. While model checking of ATL
under perfect information seems to be feasible in practice [5], model checking of ATL
under imperfect information [17] is still applicable only to small and medium size sys-
tems [10]. This lecture is about selected approaches which can make model checking
ATL? , ATL and its time extension TATL more efficient.
2 Model Reduction Methods for Variants of ATL?
Abstraction 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?4 , Moreover, we present a model-
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 infor-
mation 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 loca-
tions 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 compar-
ing the expressive power of the logics against ATL. We discuss a possible impact of this
hierarchy on improving efficiency of model checking for TATL≤,≥ .
References
1. T. Å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. É. André, 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 Proceed-
ings 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 Multi-
Agent 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 Au-
tonomous 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.
10. W. Jamroga, M. Knapik, D. Kurpiewski, and L. Mikulski. Approximate verification of strate-
gic abilities under imperfect information. Artificial Intelligence, 2018. To appear.
11. W. Jamroga, W. Penczek, P. Dembiński, and A. Mazurkiewicz. Towards partial order re-
ductions for strategic ability. In Proceedings of the 17th International Conference on Au-
tonomous 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 Alternating-
time 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 Dit-
marsch, 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 temporal-
epistemic logics over interleaved multi-agent systems. Fundamenta Informaticae, 101(1-
2):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 Theoreti-
cal Computer Science, 85(2):82–93, 2004.