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

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 4 Tool Overview CGAAL (https://github.com/d702e20/CGAAL) is written in Rust and consists of a command-line interface and a verification engine. The primary feature of CGAAL is the verification of ATL properties for CGSs. Verification is either done with a global algorithm or local algorithm, both of which are described in Section 3. If requested, a partial strategy witness can also be computed, which instructs how the given players must play to satisfy the given property. Another feature converts the model into dot graph format such that it can be visually rendered with Graphviz.[2] To model concurrent game structures for CGAAL, we designed a declarative Language for Concurrent Game Structure, called LCGS. In LCGS a CGS is defined with a series of declarations such that it is possible to find the successors of any state from the declarations alone. The language acts as an abstract representation of the CGS and allows us to save memory at the small cost of having to evaluate the expressions of declarations whenever successors are explored. The syntax of the language is inspired by PRISM-lang [11] used by the PRISM model checker to model stochastic multi-player games with rewards. However, LCGS differs in multiple ways. For instance, LCGS has player templates instead of modules, and templates have no effect unless there exists an instance of it. Additionally, synchronisations affecting the internal state of a player are much easier to declare. Example Use As an example, we want to check if a cowboy can guarantee to stay alive in a three way Mexican standoff. The standoff is simulated in rounds and in each round a cowboy can choose to wait, shoot the cowboy to the right, or shoot the cowboy to the left. If a cowboy is hit by two bullets, he dies. We model this scenario in Listing 1. The cowboy template is declared on lines 3-17. Herein, on line 6, we define that each cowboy can be hit by two bullets before being incapacitated, but we make this number a constant on line 1 so it is easy to change. Each cowboy has their own health variable and the combination of the values of these variables makes up a state. Line 7 defines how the health of a cowboy is updated in each transition. The value of opp_right.shoot_left and opp_left.shoot_right are 1 if this cowboy was shot by the given opponent to the right or left, respectively, otherwise 0. On line 10 we define a label called alive, which is a proposition that is true if the cowboy has more than zero health. Lines 13-15 define the actions of the cowboy template, and the expression to the right of the name is a condition defining in which states the action is available. As can be seen, a cowboy can always wait, but only shoot if they and their target are alive. Lastly, we declare three instances of the cowboy template on lines 20-22. We define the right and left opponent in the relabelling function after the name of the template. Any identifier in a template can be relabelled to another expression as long as the result is syntactically and semantically correct. The ATL formula ⟪billy⟫□billy.alive is satisfied if the cowboy billy has a strategy to stay alive. We can now run CGAAL with the following command: ./cgaal solver -m standoff.lcgs -f billy-can-stay-alive.atl, and CGAAL will tell us that the property is not satisfied. Billy has no strategy that can guarantee his survival. [2] Graphviz: https://graphviz.org/ 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 4 Tool Overview CGAAL (https://github.com/d702e20/CGAAL) is written in Rust and consists of a command-line interface and a verification engine. The primary feature of CGAAL is the verification of ATL properties for CGSs. Verification is either done with a global algorithm or local algorithm, both of which are described in Section 3. If requested, a partial strategy witness can also be computed, which instructs how the given players must play to satisfy the given property. Another feature converts the model into dot graph format such that it can be visually rendered with Graphviz.[2] To model concurrent game structures for CGAAL, we designed a declarative Language for Concurrent Game Structure, called LCGS. In LCGS a CGS is defined with a series of declarations such that it is possible to find the successors of any state from the declarations alone. The language acts as an abstract representation of the CGS and allows us to save memory at the small cost of having to evaluate the expressions of declarations whenever successors are explored. The syntax of the language is inspired by PRISM-lang [11] used by the PRISM model checker to model stochastic multi-player games with rewards. However, LCGS differs in multiple ways. For instance, LCGS has player templates instead of modules, and templates have no effect unless there exists an instance of it. Additionally, synchronisations affecting the internal state of a player are much easier to declare. Example Use As an example, we want to check if a cowboy can guarantee to stay alive in a three way Mexican standoff. The standoff is simulated in rounds and in each round a cowboy can choose to wait, shoot the cowboy to the right, or shoot the cowboy to the left. If a cowboy is hit by two bullets, he dies. Example Use We model this scenario in Listing 1. The cowboy template is declared on lines 3-17. Herein, on line 6, we define that each cowboy can be hit by two bullets before being incapacitated, but we make this number a constant on line 1 so it is easy to change. Each cowboy has their own health variable and the combination of the values of these variables makes up a state. Line 7 defines how the health of a cowboy is updated in each transition. The value of opp_right.shoot_left and opp_left.shoot_right are 1 if this cowboy was shot by the given opponent to the right or left, respectively, otherwise 0. On line 10 we define a label called alive, which is a proposition that is true if the cowboy has more than zero health. Lines 13-15 define the actions of the cowboy template, and the expression to the right of the name is a condition defining in which states the action is available. As can be seen, a cowboy can always wait, but only shoot if they and their target are alive. Lastly, we declare three instances of the cowboy template on lines 20-22. We define the right and left opponent in the relabelling function after the name of the template. Any identifier in a template can be relabelled to another expression as long as the result is syntactically and semantically correct. The ATL formula ⟪billy⟫□billy.alive is satisfied if the cowboy billy has a strategy to stay alive. We can now run CGAAL with the following command: ./cgaal solver -m standoff.lcgs -f billy-can-stay-alive.atl, and CGAAL will tell us that the property is not satisfied. Billy has no strategy that can guarantee his survival. [2] Graphviz: https://graphviz.org/ This paper is available on Arxiv under CC 4.0 license. Arxiv