Top

International Journal on Software Tools for Technology Transfer

Published in:

28-09-2018 | Regular Paper

Comparing approaches for model-checking strategies under imperfect information and fairness constraints

Authors: Simon Busard, Charles Pecheur, Hongyang Qu, Franco Raimondi

Published in: International Journal on Software Tools for Technology Transfer | Issue 4/2019

Activate our intelligent search to find suitable subject content or patents.

search-config

AI-assisted search

Off

Abstract

Starting from alternating-time temporal logic, many logics for reasoning about strategies in a system of agents have been proposed. Some of them consider the strategies that agents can play when they have partial information about the state of the system. \(ATLK_{irF}\) is such a logic to reason about uniform strategies under unconditional fairness constraints. While this kind of logics has been extensively studied, practical approaches for solving their model-checking problem appeared only recently. This paper considers three approaches for model-checking strategies under partial observability of the agents, applied to \(ATLK_{irF}\). These three approaches have been implemented in PyNuSMV, a Python library based on the state-of-the-art model checker NuSMV. Thanks to the experimental results obtained with this library and thanks to the comparison of the relative performance of the approaches, this paper provides indications and guidelines for the use of these verification techniques, showing that different approaches are needed in different situations.

previous article Complementary test selection criteria for model-based testing of security components

next article ASAP: A Source Code Authorship Program

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

The problem of model-checking strategies under imperfect information is \(\varDelta ^P_2\)-complete [20, 21].

Alur, R., Henzinger, T.A., Kupferman, O.: Alternating-time temporal logic. J. ACM 49(5), 672–713 (2002). https://doi.org/10.1145/585265.585270 MathSciNetCrossRefMATH

Bozianu, R., Dima, C., Filiot, E.: Safraless synthesis for epistemic temporal specifications. In: Biere, A., Bloem, R. (eds.) Computer Aided Verification. Lecture Notes in Computer Science, vol. 8559, pp. 441–456. Springer, Berlin (2014). https://doi.org/10.1007/978-3-319-08867-9_29 CrossRef

Bryant, R.E.: Graph-based algorithms for boolean function manipulation. IEEE Trans. Comput. 100(8), 677–691 (1986)CrossRefMATH

Bulling, N., Jamroga, W.: Comparing variants of strategic ability: how uncertainty and memory influence general properties of games. Auton. Agents Multi-Agent Syst. 28(3), 474–518 (2014). https://doi.org/10.1007/s10458-013-9231-3 CrossRef

Busard, S.: Symbolic model checking of multi-modal logics: uniform strategies and rich explanations. Ph.D. thesis, Université catholique de Louvain (2017)

Busard, S., Pecheur, C.: PyNuSMV: NuSMV as a Python library. In: Brat, G., Rungta, N., Venet, A. (eds.) Nasa Formal Methods 2013, LNCS, vol. 7871, pp. 453–458. Springer, Berlin (2013)CrossRef

Busard, S., Pecheur, C., Qu, H., Raimondi, F.: Reasoning about strategies under partial observability and fairness constraints. In: Mogavero, F., Murano, A., Vardi, M.Y. (eds.) Proceedings 1st International Workshop on Strategic Reasoning, SR 2013, Rome, Italy, March 16–17, 2013., EPTCS, vol. 112, pp. 71–79 (2013). https://doi.org/10.4204/EPTCS.112.12

Busard, S., Pecheur, C., Qu, H., Raimondi, F.: Improving the model checking of strategies under partial observability and fairness constraints. In: Merz, S., Pang, J. (eds.) Formal Methods and Software Engineering. Lecture Notes in Computer Science, vol. 8829, pp. 27–42. Springer, Berlin (2014). https://doi.org/10.1007/978-3-319-11737-9_3 CrossRef

Busard, S., Pecheur, C., Qu, H., Raimondi, F.: Reasoning about memoryless strategies under partial observability and unconditional fairness constraints. Inf. Comput. 242, 128–156 (2015). https://doi.org/10.1016/j.ic.2015.03.014 MathSciNetCrossRefMATH

10.

Calta, J., Shkatov, D., Schlingloff, H.: Finding uniform strategies for multi-agent systems. In: Dix, J., Leite, J., Governatori, G., Jamroga, W. (eds.) Computational Logic in Multi-Agent Systems. Lecture Notes in Computer Science, vol. 6245, pp. 135–152. Springer, Berlin (2010). https://doi.org/10.1007/978-3-642-14977-1_12

11.

Cavada, R., Cimatti, A., Jochim, C.A., Keighren, G., Olivetti, E., Pistore, M., Roveri, M., Tchaltsev, A.: NuSMV 2.5 User manual

12.

Cimatti, A., Clarke, E., Giunchiglia, E., Giunchiglia, F., Pistore, M., Roveri, M., Sebastiani, R., Tacchella, A.: NuSMV 2: an opensource tool for symbolic model checking. In: Brinksma, E., Larsen, K.G. (eds.) Computer Aided Verification. Lecture Notes in Computer Science, vol. 2404, pp. 359–364. Springer, Berlin (2002). https://doi.org/10.1007/3-540-45657-0_29 CrossRef

13.

Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (1999)

14.

Dastani, M., Jamroga, W.: Reasoning about strategies of multi-agent programs. Proc. AAMAS 10, 997–1004 (2010)

15.

Dima, C., Tiplea, F.L.: Model-checking ATL under imperfect information and perfect recall semantics is undecidable. arXiv:1102.4225 (2011)

16.

Fagin, R., Halpern, J.Y., Moses, Y., Vardi, M.Y.: Reasoning About Knowledge. MIT Press, Cambridge (1995)MATH

17.

Huang, X., van der Meyden, R.: An epistemic strategy logic (extended abstract). In: Mogavero, F., Murano, A., Vardi, M.Y. (eds.) Proceedings 2nd International Workshop on Strategic Reasoning, Grenoble, France, April 5–6, 2014, Electronic Proceedings in Theoretical Computer Science, vol. 146, pp. 35–41. Open Publishing Association (2014). https://doi.org/10.4204/EPTCS.146.5

18.

Huang, X., van der Meyden, R.: Symbolic model checking epistemic strategy logic. In: Proceedings of the Twenty-Eighth AAAI Conference on Artificial Intelligence, July 27- -31, 2014, Québec City, Québec, Canada., pp. 1426–1432 (2014)

19.

Jamroga, W., Ågotnes, T.: Constructive knowledge: what agents can achieve under imperfect information. J. Appl. Non-Class. Logics 17(4), 423–475 (2007). https://doi.org/10.3166/jancl.17.423-475 MathSciNetCrossRefMATH

20.

Jamroga, W., Dix, J.: Model checking abilities under incomplete information is indeed \(\varDelta ^P_2\)-complete. In: EUMAS’06 (2006)

21.

Jamroga, W., Dix, J.: Model checking abilities of agents: a closer look. Theory Comput. Syst. 42(3), 366–410 (2008). https://doi.org/10.1007/s00224-007-9080-z MathSciNetCrossRefMATH

22.

Jamroga, W., van der Hoek, W.: Agents that know how to play. Fundam. Inf. 63(2), 185–219 (2004)MathSciNetMATH

23.

Lomuscio, A., Qu, H., Raimondi, F.: MCMAS: an open-source model checker for the verification of multi-agent systems. Int. J. Softw. Tools Technol. Transf. (2015). https://doi.org/10.1007/s10009-015-0378-x

24.

Lomuscio, A., Raimondi, F.: Model checking knowledge, strategies, and games in multi-agent systems. In: 5th International Joint Conference on Autonomous Agents and Multiagent Systems (AAMAS 2006), Hakodate, Japan, May 8–12, 2006, pp. 161–168 (2006). https://doi.org/10.1145/1160633.1160660

25.

Pilecki, J., Bednarczyk, M.A., Jamroga, W.: Synthesis and verification of uniform strategies for multi-agent systems. In: Bulling, N., van der Torre, L., Villata, S., Jamroga, W., Vasconcelos, W. (eds.) Computational Logic in Multi-Agent Systems. Lecture Notes in Computer Science, vol. 8624, pp. 166–182. Springer, Berlin (2014). https://doi.org/10.1007/978-3-319-09764-0_11

26.

Raskin, J., Chatterjee, K., Doyen, L., Henzinger, T.A.: Algorithms for omega-regular games with imperfect information. Logical Methods Comput. Sci. (2007). https://doi.org/10.2168/LMCS-3(3:4)2007 MathSciNetMATH

27.

Schobbens, P.Y.: Alternating-time logic with imperfect recall. Electron. NotesTheor. Comput. Sci. 85(2), 82–93 (2004). https://doi.org/10.1016/S1571-0661(05)82604-0 MathSciNetCrossRefMATH

28.

van Ditmarsch, H., Knight, S.: Partial information and uniform strategies. In: Bulling, N., van der Torre, L., Villata, S., Jamroga, W., Vasconcelos, W. (eds.) Computational Logic in Multi-Agent Systems. Lecture Notes in Computer Science, vol. 8624, pp. 183–198. Springer, Berlin (2014). https://doi.org/10.1007/978-3-319-09764-0_12

29.

van Ditmarsch, H., Kooi, B.: One hundred prisoners and a light bulb. In: One Hundred Prisoners and a Light Bulb, pp. 83–94. Springer International Publishing (2015). https://doi.org/10.1007/978-3-319-16694-0_9

Title: Comparing approaches for model-checking strategies under imperfect information and fairness constraints
Authors: Simon Busard
Charles Pecheur
Hongyang Qu
Franco Raimondi
Publication date: 28-09-2018
Publisher: Springer Berlin Heidelberg
Published in: International Journal on Software Tools for Technology Transfer / Issue 4/2019
Print ISSN: 1433-2779
Electronic ISSN: 1433-2787
DOI: https://doi.org/10.1007/s10009-018-0505-6

Springer Professional

Abstract

Please log in to get access to your license.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Other articles of this Issue 4/2019

Complementary test selection criteria for model-based testing of security components

Fast detection of concurrency errors by state space traversal with randomization and early backtracking

Parallel reachability analysis of hybrid systems in XSpeed

ASAP: A Source Code Authorship Program

Premium Partner