Abstract
Model-checking alternating-time properties has recently attracted much interest in the verification of distributed protocols. While checking the validity of a specification in alternating-time temporal logic (ATL) against an explicit model is cheap (linear in the size of the formula and the model), the problem becomes EXPTIME-hard when symbolic models are considered. Practical ATL model-checking therefore often consumes too much computation time to be tractable.
In this paper, we describe a novel approach for ATL model-checking, which constructs an explicit weak model-checking game on-the-fly. This game is then evaluated using heuristic techniques inspired by efficient evaluation algorithms for and/or-trees.
To show the feasibility of our approach, we compare its performance to the ATL model-checking system MOCHA on some practical examples. Using very limited heuristic guidance, we achieve a significant speedup on these benchmarks.
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
Allis, L.V., van der Meulen, M., van der Herik, H.J.: Proof-number search. Artificial Intelligence 66(1), 91–124 (1994)
Alur, R., Henzinger, T.A., Kupferman, O.: Alternating-time temporal logic. Journal of the ACM 49(5), 672–713 (2002)
Alur, R., Henzinger, T.A., Mang, F.Y.C., Qadeer, S., Rajamani, S.K., Tasiran, S.: Mocha: Modularity in model checking. In: Y. Vardi, M. (ed.) CAV 1998. LNCS, vol. 1427, pp. 521–525. Springer, Heidelberg (1998)
Andersen, H.R.: Model checking and boolean graphs. Theor. Comput. Sci. 126(1), 3–30 (1994)
Burch, J.R., Clarke, E.M., McMillan, K.L., Dill, D.L., Hwang, L.J.: Symbolic model checking: 1020 states and beyond. Information and Computation 98(2), 142–170 (1992)
Chadha, R., Kremer, S., Scedrov, A.: Analysis of multi-party contract signing. Technical Report 516, Université Libre de Bruxelles (2004)
Clarke, E.M., Emerson, E.A.: Design and synthesis of synchronization skeletons using branching time temporal logic. In: Proc. IBM Workshop on Logics of Programs, pp. 52–71 (1981)
Cleaveland, R., Steffen, B.: A linear-time model-checking algorithm for the alternation-free modal μ-calculus. In: Larsen, K.G., Skou, A. (eds.) CAV 1991. LNCS, vol. 575, pp. 48–58. Springer, Heidelberg (1992)
Emerson, E.A., Jutla, C.S.: Tree automata, μ-calculus and determinacy. In: Proc. FOCS, pp. 368–377 (1991)
Garay, J.A., MacKenzie, P.D.: Abuse-free multi-party contract signing. In International Symposium on Distributed Computing. In: Jayanti, P. (ed.) DISC 1999. LNCS, vol. 1693, pp. 151–165. Springer, Heidelberg (1999)
Hoffmann, J., Nebel, B.: The FF planning system: Fast plan generation through heuristic search. Journal of Artificial Intelligence Research 14, 253–302 (2001)
Holzmann, G.J.: The model checker SPIN. Software Engineering 23(5), 279–295 (1997)
Knuth, D.E., Moore, R.W.: An analysis of alpha-beta pruning. Artificial Intelligence 6(4), 293–326 (1975)
Kremer, S.: Formal Analysis of Optimistic Fair Exchange Protocols. PhD thesis, Université Libre de Bruxelles, Brussels, Belgium (December 2003)
Kremer, S., Raskin, J.-F.: A game-based verification of non-repudiation and fair exchange protocols. Journal of Computer Security 11(3), 399–430 (2003)
Mahimkar, A., Shmatikov, V.: Game-based analysis of denial-of-service prevention protocols. In: IEEE Computer Security Foundations Workshop, pp. 287–301 (2005)
Ryan, M., Schobbens, P.-Y.: Agents and roles: Refinement in alternating-time temporal logic. In: Meyer, J.-J.C., Tambe, M. (eds.) ATAL 2001. LNCS (LNAI), vol. 2333, pp. 100–114. Springer, Heidelberg (2002)
van der Hoek, W., Lomuscio, A., Wooldridge, M.: On the complexity of practical ATL model checking. In: Proc. AAMAS (2006)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Helmert, M., Mattmüller, R., Schewe, S. (2006). Selective Approaches for Solving Weak Games. In: Graf, S., Zhang, W. (eds) Automated Technology for Verification and Analysis. ATVA 2006. Lecture Notes in Computer Science, vol 4218. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11901914_17
Download citation
DOI: https://doi.org/10.1007/11901914_17
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-47237-7
Online ISBN: 978-3-540-47238-4
eBook Packages: Computer ScienceComputer Science (R0)