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.
Chapter PDF
Similar content being viewed by others
Keywords
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
Å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)
Ågotnes, T., Walther, D.: A Logic of Strategic Ability Under Bounded Memory. JLLI 18(1), 55–77 (2009)
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: Vardi, M.Y. (ed.) CAV 1998. LNCS, vol. 1427, pp. 521–525. Springer, Heidelberg (1998)
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)
Bryant, R.E.: Graph-Based Algorithms for Boolean Function Manipulation. Transactions on Computers 35(8), 677–691 (1986)
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)
Chatterjee, K., Henzinger, T.A., Piterman, N.: Strategy Logic. Information and Computation 208(6), 677–693 (2010)
Chaum, D.: The Dining Cryptographers Problem: Unconditional Sender and Recipient Untraceability. Journal of Cryptology 1, 65–75 (1988)
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)
Dima, C., Tiplea, F.L.: Model-checking ATL under Imperfect Information and Perfect Recall Semantics is Undecidable. Technical report, arXiv (2011)
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)
Even, S., Paz, A.: A Note on Cake Cutting. Discrete Applied Mathematics 7, 285–296 (1984)
Fagin, R., Halpern, J.Y., Moses, Y., Vardi, M.Y.: Reasoning about Knowledge. MIT Press (1995)
Finkbeiner, B., Schewe, S.: Coordination logic. In: Dawar, A., Veith, H. (eds.) CSL 2010. LNCS, vol. 6247, pp. 305–319. Springer, Heidelberg (2010)
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)
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)
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)
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)
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)
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)
MCMAS-SLK - A Model Checker for the Verification of Strategy Logic Specifications, http://vas.doc.ic.ac.uk/software/tools/
Mogavero, F., Murano, A., Perelli, G., Vardi, M.Y.: Reasoning About Strategies: On the Model-Checking Problem. Technical report, arXiv (2011)
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)
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)
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)
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)
Pnueli, A.: The Temporal Logic of Programs. In: Foundation of Computer Science 1977, pp. 46–57. IEEE Computer Society (1977)
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)
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)
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)
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
Čermák, P., Lomuscio, A., Mogavero, F., Murano, A. (2014). MCMAS-SLK: A Model Checker for the Verification of Strategy Logic Specifications. In: Biere, A., Bloem, R. (eds) Computer Aided Verification. CAV 2014. Lecture Notes in Computer Science, vol 8559. Springer, Cham. https://doi.org/10.1007/978-3-319-08867-9_34
Download citation
DOI: https://doi.org/10.1007/978-3-319-08867-9_34
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-08866-2
Online ISBN: 978-3-319-08867-9
eBook Packages: Computer ScienceComputer Science (R0)