Advertisement

MCMAS-SLK: A Model Checker for the Verification of Strategy Logic Specifications

  • Petr Čermák
  • Alessio Lomuscio
  • Fabio Mogavero
  • Aniello Murano
Part of the Lecture Notes in Computer Science book series (LNCS, volume 8559)

Abstract

Model checking has come of age. A number of techniques are increasingly used in industrial setting to verify hardware and software systems, both against models and concrete implementations. While it is generally accepted that obstacles still remain, notably handling infinite state systems efficiently, much of current work involves refining and improving existing techniques such as predicate abstraction.

Keywords

Model Check MultiAgent System Autonomous Agent Reachable State Atomic Proposition 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

References

  1. 1.
    Ågotnes, T., Goranko, V., Jamroga, W.: Alternating-Time Temporal Logics with Irrevocable Strategies. In: Theoretical Aspects of Rationality and Knowledge 2007, pp. 15–24 (2007)Google Scholar
  2. 2.
    Ågotnes, T., Walther, D.: A Logic of Strategic Ability Under Bounded Memory. JLLI 18(1), 55–77 (2009)CrossRefzbMATHGoogle Scholar
  3. 3.
    Alur, R., Henzinger, T.A., Kupferman, O.: Alternating-Time Temporal Logic. Journal of the ACM 49(5), 672–713 (2002)CrossRefMathSciNetGoogle Scholar
  4. 4.
    Alur, R., Henzinger, T.A., Mang, F.Y.C., Qadeer, S., Rajamani, S.K., Tasiran, S.: MOCHA: Modularity in Model Checking.. In: Vardi, M.Y. (ed.) CAV 1998. LNCS, vol. 1427, pp. 521–525. Springer, Heidelberg (1998)CrossRefGoogle Scholar
  5. 5.
    Brihaye, T., Da Costa, A., Laroussinie, F., Markey, N.: ATL with strategy contexts and bounded memory. In: Artemov, S., Nerode, A. (eds.) LFCS 2009. LNCS, vol. 5407, pp. 92–106. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  6. 6.
    Bryant, R.E.: Graph-Based Algorithms for Boolean Function Manipulation. Transactions on Computers 35(8), 677–691 (1986)CrossRefzbMATHGoogle Scholar
  7. 7.
    Bulling, N., Dix, J., Jamroga, W.: Model Checking Logics of Strategic Ability: Complexity. In: Specification and Verification of Multi-Agent Systems, pp. 125–159. Springer (2010)Google Scholar
  8. 8.
    Chatterjee, K., Henzinger, T.A., Piterman, N.: Strategy Logic. Information and Computation 208(6), 677–693 (2010)CrossRefzbMATHMathSciNetGoogle Scholar
  9. 9.
    Chaum, D.: The Dining Cryptographers Problem: Unconditional Sender and Recipient Untraceability. Journal of Cryptology 1, 65–75 (1988)CrossRefzbMATHMathSciNetGoogle Scholar
  10. 10.
    Clarke, E.M., Emerson, E.A.: Design and Synthesis of Synchronization Skeletons Using Branching-Time Temporal Logic. In: Kozen, D. (ed.) Logic of Programs 1981. LNCS, vol. 131, pp. 52–71. Springer, Heidelberg (1982)CrossRefGoogle Scholar
  11. 11.
    Dima, C., Tiplea, F.L.: Model-checking ATL under Imperfect Information and Perfect Recall Semantics is Undecidable. Technical report, arXiv (2011)Google Scholar
  12. 12.
    Emerson, E.A., Halpern, J.Y.: “Sometimes” and “Not Never” Revisited: On Branching Versus Linear Time. Journal of the ACM 33(1), 151–178 (1986)CrossRefzbMATHMathSciNetGoogle Scholar
  13. 13.
    Even, S., Paz, A.: A Note on Cake Cutting. Discrete Applied Mathematics 7, 285–296 (1984)CrossRefzbMATHMathSciNetGoogle Scholar
  14. 14.
    Fagin, R., Halpern, J.Y., Moses, Y., Vardi, M.Y.: Reasoning about Knowledge. MIT Press (1995)Google Scholar
  15. 15.
    Finkbeiner, B., Schewe, S.: Coordination logic. In: Dawar, A., Veith, H. (eds.) CSL 2010. LNCS, vol. 6247, pp. 305–319. Springer, Heidelberg (2010)CrossRefGoogle Scholar
  16. 16.
    Gammie, P., van der Meyden, R.: MCK: Model Checking the Logic of Knowledge. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 479–483. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  17. 17.
    Jamroga, W., Murano, A.: On Module Checking and Strategies. In: Autonomous Agents and MultiAgent Systems 2014, pp. 701–708. International Foundation for Autonomous Agents and Multiagent Systems (2014)Google Scholar
  18. 18.
    Kacprzak, M., Nabialek, W., Niewiadomski, A., Penczek, W., Pólrola, A., Szreter, M., Wozna, B., Zbrzezny, A.: VerICS 2007 - a Model Checker for Knowledge and Real-Time. Fundamenta Informaticae 85(1-4), 313–328 (2008)zbMATHMathSciNetGoogle Scholar
  19. 19.
    Lomuscio, A., Qu, H., Raimondi, F.: MCMAS: A Model Checker for the Verification of Multi-Agent Systems. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 682–688. Springer, Heidelberg (2009)CrossRefGoogle Scholar
  20. 20.
    Lomuscio, A., Raimondi, F.: Model Checking Knowledge, Strategies, and Games in Multi-Agent Systems. In: Autonomous Agents and MultiAgent Systems 2006, pp. 161–168. International Foundation for Autonomous Agents and Multiagent Systems (2006)Google Scholar
  21. 21.
    Lopes, A.D.C., Laroussinie, F., Markey, N.: ATL with Strategy Contexts: Expressiveness and Model Checking. In: Foundations of Software Technology and Theoretical Computer Science 2010. LIPIcs, vol. 8, pp. 120–132. Leibniz-Zentrum fuer Informatik (2010)Google Scholar
  22. 22.
    MCMAS-SLK - A Model Checker for the Verification of Strategy Logic Specifications, http://vas.doc.ic.ac.uk/software/tools/
  23. 23.
    Mogavero, F., Murano, A., Perelli, G., Vardi, M.Y.: Reasoning About Strategies: On the Model-Checking Problem. Technical report, arXiv (2011)Google Scholar
  24. 24.
    Mogavero, F., Murano, A., Perelli, G., Vardi, M.Y.: What Makes Atl* Decidable? A Decidable Fragment of Strategy Logic. In: Koutny, M., Ulidowski, I. (eds.) CONCUR 2012. LNCS, vol. 7454, pp. 193–208. Springer, Heidelberg (2012)CrossRefGoogle Scholar
  25. 25.
    Mogavero, F., Murano, A., Sauro, L.: On the Boundary of Behavioral Strategies. In: Logic in Computer Science 2013, pp. 263–272. IEEE Computer Society (2013)Google Scholar
  26. 26.
    Mogavero, F., Murano, A., Sauro, L.: Strategy Games: A Renewed Framework. In: Autonomous Agents and MultiAgent Systems 2014, pp. 869–876. International Foundation for Autonomous Agents and Multiagent Systems (2014)Google Scholar
  27. 27.
    Mogavero, F., Murano, A., Vardi, M.Y.: Reasoning About Strategies. In: Foundations of Software Technology and Theoretical Computer Science 2010. LIPIcs, vol. 8, pp. 133–144. Leibniz-Zentrum fuer Informatik (2010)Google Scholar
  28. 28.
    Pnueli, A.: The Temporal Logic of Programs. In: Foundation of Computer Science 1977, pp. 46–57. IEEE Computer Society (1977)Google Scholar
  29. 29.
    Raimondi, F., Lomuscio, A.: Automatic Verification of Multi-Agent Systems by Model Checking via Ordered Binary Decision Diagrams. Journal of Applied Logic 5(2), 235–251 (2007)CrossRefzbMATHMathSciNetGoogle Scholar
  30. 30.
    van der Meyden, R., Su, K.: Symbolic Model Checking the Knowledge of the Dining Cryptographers. In: Computer Security Foundations Workshop 2004, pp. 280–291. IEEE Computer Society (2004)Google Scholar
  31. 31.
    Walther, D., van der Hoek, W., Wooldridge, M.: Alternating-Time Temporal Logic with Explicit Strategies. In: Theoretical Aspects of Rationality and Knowledge 2007, pp. 269–278 (2007)Google Scholar

Copyright information

© Springer International Publishing Switzerland 2014

Authors and Affiliations

  • Petr Čermák
    • 1
  • Alessio Lomuscio
    • 1
  • Fabio Mogavero
    • 2
  • Aniello Murano
    • 2
  1. 1.Imperial College LondonUK
  2. 2.Università degli Studi di Napoli Federico IIItaly

Personalised recommendations