Abstract
Reasoning about strategies has been a concern for several years, and many extensions of Alternating-time Temporal Logic have been proposed. One extension, ATLK irF , allows the user to reason about the strategies of the agents of a system under partial observability and unconditional fairness constraints. However, the existing model-checking algorithm for ATLK irF is inefficient when the user is only interested in the satisfaction of a formula in a small subset of states, such as the set of initial states of the system. We propose to generate fewer strategies by only focusing on partial strategies reachable from this subset of states, reducing the time needed to perform the verification. We also describe several practical improvements to further reduce the verification time and present experiments showing the practical impact of the approach.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Alur, R., Henzinger, T.A., Kupferman, O.: Alternating-time temporal logic. J. ACM 49(5), 672–713 (2002)
Schobbens, P.Y.: Alternating-time logic with imperfect recall. Electronic Notes in Theoretical Computer Science 85(2), 82–93 (2004)
Busard, S., Pecheur, C., Qu, H., Raimondi, F.: Reasoning about strategies under partial observability and fairness constraints. In: SR, pp. 71–79 (2013)
Dastani, M., Jamroga, W.: Reasoning about strategies of multi-agent programs. Proceedings of AAMAS 10, 997–1004 (2010)
Jamroga, W., van der Hoek, W.: Agents that know how to play. Fundamenta Informaticae 63(2), 185–219 (2004)
Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. MIT Press (1999)
Fagin, R., Halpern, J.Y., Moses, Y., Vardi, M.Y.: Reasoning about Knowledge. MIT Press, Cambridge (1995)
Dima, C., Enea, C., Guelev, D.: Model-checking an alternating-time temporal logic with knowledge, imperfect information, perfect recall and communicating coalitions. In: GANDALF, pp. 103–117 (2010)
Busard, S., Pecheur, C.: PyNuSMV: NuSMV as a python library. In: Brat, G., Rungta, N., Venet, A. (eds.) NFM 2013. LNCS, vol. 7871, pp. 453–458. Springer, Heidelberg (2013)
Stirling, C., Walker, D.: Local model checking in the modal mu-calculus. In: Díaz, J., Orejas, F. (eds.) TAPSOFT 1989. LNCS, vol. 351, pp. 369–383. Springer, Heidelberg (1989)
Bhat, G., Cleaveland, R., Grumberg, O.: Efficient on-the-fly model checking for ctl. In: LICS 1995, pp. 388–397 (1995)
Mateescu, S.: Efficient on-the-fly model-checking for regular alternation-free mu-calculus. Science of Computer Programming 46(3), 255–281 (2003)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer International Publishing Switzerland
About this paper
Cite this paper
Busard, S., Pecheur, C., Qu, H., Raimondi, F. (2014). Improving the Model Checking of Strategies under Partial Observability and Fairness Constraints. In: Merz, S., Pang, J. (eds) Formal Methods and Software Engineering. ICFEM 2014. Lecture Notes in Computer Science, vol 8829. Springer, Cham. https://doi.org/10.1007/978-3-319-11737-9_3
Download citation
DOI: https://doi.org/10.1007/978-3-319-11737-9_3
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-11736-2
Online ISBN: 978-3-319-11737-9
eBook Packages: Computer ScienceComputer Science (R0)