This paper is available on arxiv under CC 4.0 license.
Authors:
(1) Falke B. Ø. Carlsen, Department of Computer Science, Aalborg University, Denmark & falkeboc@cs.aau.dk;
(2) Lars Bo P. Frydenskov, Department of Computer Science, Aalborg University, Denmark & larsbopark@gmail.com;
(3) Nicolaj Ø. Jensen, Department of Computer Science, Aalborg University, Denmark & noje@cs.aau.dk;
(4) Jener Rasmussen, jener@jener.dk;
(5) Mathias M. Sørensen, mathiasmehlsoerensen@gmail.com;
(6) Asger G. Weirsøe, asger@weircon.dk;
(7) Mathias C. Jensen, Department of Computer Science, Aalborg University, Denmark & mcje@cs.aau.dk;
(8) Kim G. Larsen, Department of Computer Science, Aalborg University, Denmark & kgl@cs.aau.dk. Table of Links Introduction Definitions Model Checking Tool Overview Evaluation Conclusion and References 6 Conclusion In this paper, we present CGAAL, our model checker of alternating-time temporal logic properties in concurrent games. CGAAL checks such properties by encoding the problem as an extended dependency graph and then computes the satisfaction relation using the distributed local on-the-fly CERTAINZERO algorithm by Dalsgaard et al. [4]. We provide multiple novel search strategies for the algorithm and allow concurrent games to be expressed in our language LCGS. Our experiments show that the local on the-fly algorithm outperforms the global algorithm in the majority of cases. We also find that CGAAL outperforms the state-of-the-art tool PRISM-games by being up to two orders of magnitude faster, especially in models where synchronisations affect the internal state of modules and whenever we are not required to compute the entire fixed point. However, this comparison is unfair, since our test only uses a fraction of PRISM-games feature set. CGAAL is still in early development and much work is needed before it competes with PRISM in terms of capabilities. However, dependency graphs have been used for encoding various model checking problems, and we intend to incorporate these techniques into CGAAL. References [1] Rajeev Alur, Thomas A. Henzinger & Orna Kupferman (2002): Alternating-Time Temporal Logic. J. ACM 49(5), p. 672–713, doi:10.1145/585265.585270. [2] Edmund M. Clarke & E. Allen Emerson (1982): Design and synthesis of synchronization skeletons using branching time temporal logic. In Dexter Kozen, editor: Logics of Programs, Springer Berlin Heidelberg, Berlin, Heidelberg, pp. 52–71, doi:10.1007/BFb0025774. [3] Edmund M Clarke, Thomas A Henzinger, Helmut Veith, Roderick Bloem et al. (2018): Handbook of model checking. 10, Springer, doi:10.1007/978-3-319-10575-8. [4] Dalsgaard, Andreas E. and Enevoldsen, Søren and Fogh, Peter and Jensen, Lasse S. and Jepsen, Tobias S. and Kaufmann, Isabella and Larsen, Kim G. and Nielsen, Søren M. and Olesen, Mads Chr. and Pastva, Samuel and Srba, Jiˇrí (2017): Extended Dependency Graphs and Efficient Distributed Fixed-Point Computation. In Wil van der Aalst & Eike Best, editors: Application and Theory of Petri Nets and Concurrency, Springer International Publishing, Cham, pp. 139–158, doi:10.1007/978-3-319-57861-3_10. [5] Søren Enevoldsen, Mathias Claus Jensen, Kim Guldstrand Larsen, Anders Mariegaard & Jiˇrí Srba (2020): Verification of Multiplayer Stochastic Games via Abstract Dependency Graphs. LOPSTR2020, doi:10.1007/978-3-030-68446-4_13. [6] Søren Enevoldsen, Kim Guldstrand Larsen & Jirí Srba (2022): Extended abstract dependency graphs. Int. J. Softw. Tools Technol. Transf. 24(1), pp. 49–65, doi:10.1007/s10009-021-00638-8. [7] Glen Jeh & Jennifer Widom (2002): SimRank: a measure of structural-context similarity. In: Proceedings of the Eighth ACM SIGKDD International Conference on Knowledge Discovery and Data Mining, July 23-26, 2002, Edmonton, Alberta, Canada, ACM, pp. 538–543, doi:10.1145/775047.775126. [8] Jonas F. Jensen, Thomas Nielsen, Lars K. Oestergaard & Jiˇrí Srba (2016): TAPAAL and Reachability Analysis of P/T Nets, pp. 307–318. Springer Berlin Heidelberg, Berlin, Heidelberg, doi:10.1007/978-3-662-53401-4_16. [9] Jonas Finnemann Jensen, Kim Guldstrand Larsen, Jiri Srba & Lars Kaerlund Østergaard (2016): Efficient model-checking of weighted CTL with upper-bound constraints. International Journal on Software Tools for Technology Transfer 18(4), pp. 409–426, doi:10.1007/s10009-014-0359-5. [10] Mathias Claus Jensen, Anders Mariegaard & Kim Guldstrand Larsen (2019): Symbolic model checking of weighted PCTL using dependency graphs. NASA Formal Methods Symposium, pp. 298–315, doi:10.1007/978-3-030-20652-9_20. [11] M. Kwiatkowska, G. Norman & D. Parker (2011): PRISM 4.0: Verification of Probabilistic Real-time Systems. In G. Gopalakrishnan & S. Qadeer, editors: Proc. 23rd International Conference on Computer Aided Verification (CAV’11), LNCS 6806, Springer, pp. 585–591, doi:10.1007/978-3-642-22110-1_47. [12] M. Kwiatkowska, G. Norman, D. Parker & G. Santos (2020): PRISM-games 3.0: Stochastic Game Verification with Concurrency, Equilibria and Time. In: Proc. 32nd International Conference on Computer Aided Verification (CAV’20), LNCS 12225, Springer, pp. 475–487, doi:10.1007/978-3-030-53291-8_25. [13] Sangkeun Lee, Minsuk Kahng & Sang goo Lee (2015): Constructing compact and effective graphs for recommender systems via node and edge aggregations. Expert Systems with Applications 42(7), pp. 3396–3409, doi:10.1016/j.eswa.2014.11.062. [14] Xinxin Liu & Scott A. Smolka (1998): Simple Linear-Time Algorithms for Minimal Fixed Points (Extended Abstract). In Kim Guldstrand Larsen, Sven Skyum & Glynn Winskel, editors: Automata, Languages and Programming, 25th International Colloquium, ICALP’98, Aalborg, Denmark, July 13-17, 1998, Proceedings, Lecture Notes in Computer Science 1443, Springer, pp. 53–66, doi:10.1007/BFb0055040. [15] Lawrence Page, Sergey Brin, Rajeev Motwani & Terry Winograd (1998): The PageRank Citation Ranking: Bringing Order to the Web. Technical Report, Stanford Digital Library Technologies Project. Available at http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.31.1768. This paper is available on Arxiv under CC 4.0 license. This paper is available on arxiv under CC 4.0 license. Authors: (1) Falke B. Ø. Carlsen, Department of Computer Science, Aalborg University, Denmark & falkeboc@cs.aau.dk; (2) Lars Bo P. Frydenskov, Department of Computer Science, Aalborg University, Denmark & larsbopark@gmail.com; (3) Nicolaj Ø. Jensen, Department of Computer Science, Aalborg University, Denmark & noje@cs.aau.dk; (4) Jener Rasmussen, jener@jener.dk; (5) Mathias M. Sørensen, mathiasmehlsoerensen@gmail.com; (6) Asger G. Weirsøe, asger@weircon.dk; (7) Mathias C. Jensen, Department of Computer Science, Aalborg University, Denmark & mcje@cs.aau.dk; (8) Kim G. Larsen, Department of Computer Science, Aalborg University, Denmark & kgl@cs.aau.dk. This paper is available on arxiv under CC 4.0 license. Authors: Authors: (1) Falke B. Ø. Carlsen, Department of Computer Science, Aalborg University, Denmark & falkeboc@cs.aau.dk; (2) Lars Bo P. Frydenskov, Department of Computer Science, Aalborg University, Denmark & larsbopark@gmail.com; (3) Nicolaj Ø. Jensen, Department of Computer Science, Aalborg University, Denmark & noje@cs.aau.dk; (4) Jener Rasmussen, jener@jener.dk; (5) Mathias M. Sørensen, mathiasmehlsoerensen@gmail.com; (6) Asger G. Weirsøe, asger@weircon.dk; (7) Mathias C. Jensen, Department of Computer Science, Aalborg University, Denmark & mcje@cs.aau.dk; (8) Kim G. Larsen, Department of Computer Science, Aalborg University, Denmark & kgl@cs.aau.dk. Table of Links Introduction Introduction Definitions Definitions Model Checking Model Checking Tool Overview Tool Overview Evaluation Evaluation Conclusion and References Conclusion and References 6 Conclusion In this paper, we present CGAAL, our model checker of alternating-time temporal logic properties in concurrent games. CGAAL checks such properties by encoding the problem as an extended dependency graph and then computes the satisfaction relation using the distributed local on-the-fly CERTAINZERO algorithm by Dalsgaard et al. [4]. We provide multiple novel search strategies for the algorithm and allow concurrent games to be expressed in our language LCGS. Our experiments show that the local on the-fly algorithm outperforms the global algorithm in the majority of cases. We also find that CGAAL outperforms the state-of-the-art tool PRISM-games by being up to two orders of magnitude faster, especially in models where synchronisations affect the internal state of modules and whenever we are not required to compute the entire fixed point. However, this comparison is unfair, since our test only uses a fraction of PRISM-games feature set. CGAAL is still in early development and much work is needed before it competes with PRISM in terms of capabilities. However, dependency graphs have been used for encoding various model checking problems, and we intend to incorporate these techniques into CGAAL. References [1] Rajeev Alur, Thomas A. Henzinger & Orna Kupferman (2002): Alternating-Time Temporal Logic. J. ACM 49(5), p. 672–713, doi:10.1145/585265.585270. [2] Edmund M. Clarke & E. Allen Emerson (1982): Design and synthesis of synchronization skeletons using branching time temporal logic. In Dexter Kozen, editor: Logics of Programs, Springer Berlin Heidelberg, Berlin, Heidelberg, pp. 52–71, doi:10.1007/BFb0025774. [3] Edmund M Clarke, Thomas A Henzinger, Helmut Veith, Roderick Bloem et al. (2018): Handbook of model checking. 10, Springer, doi:10.1007/978-3-319-10575-8. [4] Dalsgaard, Andreas E. and Enevoldsen, Søren and Fogh, Peter and Jensen, Lasse S. and Jepsen, Tobias S. and Kaufmann, Isabella and Larsen, Kim G. and Nielsen, Søren M. and Olesen, Mads Chr. and Pastva, Samuel and Srba, Jiˇrí (2017): Extended Dependency Graphs and Efficient Distributed Fixed-Point Computation. In Wil van der Aalst & Eike Best, editors: Application and Theory of Petri Nets and Concurrency, Springer International Publishing, Cham, pp. 139–158, doi:10.1007/978-3-319-57861-3_10. [5] Søren Enevoldsen, Mathias Claus Jensen, Kim Guldstrand Larsen, Anders Mariegaard & Jiˇrí Srba (2020): Verification of Multiplayer Stochastic Games via Abstract Dependency Graphs. LOPSTR2020, doi:10.1007/978-3-030-68446-4_13. [6] Søren Enevoldsen, Kim Guldstrand Larsen & Jirí Srba (2022): Extended abstract dependency graphs. Int. J. Softw. Tools Technol. Transf. 24(1), pp. 49–65, doi:10.1007/s10009-021-00638-8. [7] Glen Jeh & Jennifer Widom (2002): SimRank: a measure of structural-context similarity. In: Proceedings of the Eighth ACM SIGKDD International Conference on Knowledge Discovery and Data Mining, July 23-26, 2002, Edmonton, Alberta, Canada, ACM, pp. 538–543, doi:10.1145/775047.775126. [8] Jonas F. Jensen, Thomas Nielsen, Lars K. Oestergaard & Jiˇrí Srba (2016): TAPAAL and Reachability Analysis of P/T Nets, pp. 307–318. Springer Berlin Heidelberg, Berlin, Heidelberg, doi:10.1007/978-3-662-53401-4_16. [9] Jonas Finnemann Jensen, Kim Guldstrand Larsen, Jiri Srba & Lars Kaerlund Østergaard (2016): Efficient model-checking of weighted CTL with upper-bound constraints. International Journal on Software Tools for Technology Transfer 18(4), pp. 409–426, doi:10.1007/s10009-014-0359-5. [10] Mathias Claus Jensen, Anders Mariegaard & Kim Guldstrand Larsen (2019): Symbolic model checking of weighted PCTL using dependency graphs. NASA Formal Methods Symposium, pp. 298–315, doi:10.1007/978-3-030-20652-9_20. [11] M. Kwiatkowska, G. Norman & D. Parker (2011): PRISM 4.0: Verification of Probabilistic Real-time Systems. In G. Gopalakrishnan & S. Qadeer, editors: Proc. 23rd International Conference on Computer Aided Verification (CAV’11), LNCS 6806, Springer, pp. 585–591, doi:10.1007/978-3-642-22110-1_47. [12] M. Kwiatkowska, G. Norman, D. Parker & G. Santos (2020): PRISM-games 3.0: Stochastic Game Verification with Concurrency, Equilibria and Time. In: Proc. 32nd International Conference on Computer Aided Verification (CAV’20), LNCS 12225, Springer, pp. 475–487, doi:10.1007/978-3-030-53291-8_25. [13] Sangkeun Lee, Minsuk Kahng & Sang goo Lee (2015): Constructing compact and effective graphs for recommender systems via node and edge aggregations. Expert Systems with Applications 42(7), pp. 3396–3409, doi:10.1016/j.eswa.2014.11.062. [14] Xinxin Liu & Scott A. Smolka (1998): Simple Linear-Time Algorithms for Minimal Fixed Points (Extended Abstract). In Kim Guldstrand Larsen, Sven Skyum & Glynn Winskel, editors: Automata, Languages and Programming, 25th International Colloquium, ICALP’98, Aalborg, Denmark, July 13-17, 1998, Proceedings, Lecture Notes in Computer Science 1443, Springer, pp. 53–66, doi:10.1007/BFb0055040. [15] Lawrence Page, Sergey Brin, Rajeev Motwani & Terry Winograd (1998): The PageRank Citation Ranking: Bringing Order to the Web. Technical Report, Stanford Digital Library Technologies Project. Available at http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.31.1768. This paper is available on Arxiv under CC 4.0 license. Arxiv

CGAAL: Wrapping It Up and What Comes Next

About Author

Comments

TOPICS

THIS ARTICLE WAS FEATURED IN

Related Stories

5 Smart Heuristic Methods for Solving Bin Packing Problems

Introducing CGAAL: A Distributed On-The-Fly ATL Model Checker With Heuristics

CGAAL: A Distributed On-The-Fly ATL Model Checker: The Definitions You Should Know About

A Tool Overview of CGAAL: A Distributed On-The-Fly ATL Model Checker

How CGAAL Model-Checks: A Deeper Insight

How We Evaluated CGAAL: The Experiments That We Ran

5 Smart Heuristic Methods for Solving Bin Packing Problems

Introducing CGAAL: A Distributed On-The-Fly ATL Model Checker With Heuristics

CGAAL: A Distributed On-The-Fly ATL Model Checker: The Definitions You Should Know About

A Tool Overview of CGAAL: A Distributed On-The-Fly ATL Model Checker

How CGAAL Model-Checks: A Deeper Insight

How We Evaluated CGAAL: The Experiments That We Ran

Light-Mode

Classic

Newspaper

Minty

Dark-Mode

Neon Noir

Minty

HN StartUps