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

Table of Links

Introduction

Definitions

Model Checking

Tool Overview

Evaluation

Conclusion and References

We present CGAAL, our efficient on-the-fly model checker for alternating-time temporal logic (ATL) on concurrent game structures (CGS). We present how our tool encodes ATL as extended dependency graphs with negation edges and employs the distributed on-the-fly algorithm by Dalsgaard et al.

Our tool offers multiple novel search strategies for the algorithm, including DHS which is inspired by PageRank and uses the in-degree of configurations as a heuristic, IHS which estimates instability of assignment values, and LPS which estimates the distance to a state satisfying the constituent property using linear programming.

CGS are input using our modelling language LCGS, where composition and synchronisation are easily described. We prove the correctness of our encoding, and our experiments show that our tool CGAAL is often one to three orders of magnitude faster than the popular tool PRISM-games on case studies from PRISM’s documentation and among case studies we have developed. In our evaluation, we also compare and evaluate our search strategies, and find that our custom search strategies are often significantly faster than the usual breadth-first and depth-first search strategies.

1 Introduction

Software plays a large role in our everyday lives, making decisions, enabling efficient communication, ensuring safety, and many more critical tasks. Furthermore, the complexity of the software and the decisions they have to make are ever-increasing due the to interconnectivity and reactive nature of modern systems. These software systems mutually depend on, communicate with, and guide each other based on their collective and internal states.

Even a few interconnected systems that are not necessarily themselves too complex can give rise to an extremely complex system as a whole. Safety-critical software that operates in contexts where errors could lead to human casualties or significant capital losses requires methods to verify their correctness. Unfortunately, such methods are difficult to implement due to the sheer state-space explosion that arises from the inherent parallel composition of systems.

In this paper, we consider systems that can be expressed as discrete multiplayer games in which the actors can perform actions concurrently. That is, in each configuration of the game, each player simultaneously chooses an action they wish to perform and the resulting decision vector then deterministically results in the next configuration of the game.

Such concurrent games are extremely expressive and can be used to model a variety of complex systems and lends themselves inherently, by their concurrent nature, to describing multi-actor systems. The properties that we wish to verify on these systems are those that can be expressed by Alternating-time Temporal Logic (ATL) [1], a game theoretic extension of Computation Tree Logic (CTL) [2, 3], that like CTL can be used to describe safety and liveness properties. ATL extends CTL by replacing the existential and universal path quantifiers with so-called coalition quantifiers.

These coalition quantifiers describe properties of the game in which a coalition of players can either enforce some desired outcome or cannot avoid an outcome. Of course, proof of satisfaction of such property is done by finding a strategy showing that the players can indeed enforce said property or by showing that no matter what strategy the players follow they cannot avoid said property.

One existing tool that can model check concurrent (stochastic) games is PRISM-games [12], an extension of the probabilistic model checker PRISM [11]. PRISM excels at stochastic models such as discreteand continuous-time Markov chains, Markov decision processes, and (priced) probabilistic timed automata, for which it can verify various properties described in LTL , CSL, and probabilistic CTL*. There are multiple verification engines in PRISM, both symbolic and explicit state.

The PRISM-games extension focuses on stochastic games in which game-theoretic approaches are needed. PRISM-games can among other things synthesise strategies and reason about equilibria-based properties, where players may have distinct, but not necessarily conflicting objectives. These properties are typically described with probabilistic ATL with rewards. In version 3.0 [12], PRISM-games added support for concurrent stochastic games.

In [14], Liu and Smolka present a global and a local algorithm to compute fixed-point boolean vertex assignments in dependency graphs with directed hyper-edges representing dependencies between vertex values. The global algorithm has a better worst-case running time of the two, but the on-the-fly local algorithm only explores the graph as needed to compute the fixed-point assignment. Many problems have since been encoded as dependency graphs.

Notably, model-checking problems for CTL can be encoded as dependency graphs and the algorithms by Liu and Smolka can be used to compute the satisfaction relation enabling model-checking using dependency graphs. J. F. Jensen et al. [9] show that weighted CTL can be encoded in dependency graphs as well and introduce symbolic edges to handle weights efficiently.

In [10], M. C. Jensen et al. introduce symbolic dependency graphs, an encoding of probabilistic weighted CTL, and an implementation of a local and global algorithm. A. Dalsgaard et al. [4] present a distributed extension to the local algorithm to boost the performance and show how to model Petri Nets problems using CTL and dependency graphs.

Furthermore, they extend dependency graphs by adding components and negation edges to solve formulae with negations. An abstract dependency graph framework is presented by S. Enevoldsen et al. in [6] where they generalise the various extensions of the dependency graphs with a general algorithm for any Noetherian partial order domain.

In the closely related work of [5], S. Enevoldsen et at. uses abstract dependency graphs to model check probabilistic ATL for weighted stochastic games. In multiple works [4, 10] the local algorithm is found to be faster more often than the global algorithm in practice.

In this paper, we introduce the tool CGAAL (Concurrent Games AALborg), a model checker implemented in Rust that allows for the verification of ATL properties on concurrent games. CGAAL works by encoding the model checking problem as an extended dependency graph and by implementing the on-the-fly local distributed algorithm by Dalsgaard et al. [4]. The concurrent games are described and inputted to the tool using LCGS, our PRISM-language inspired model language, and for specific ATL formulae, we can output a strategy describing how to ensure satisfaction given a positive result.

Furthermore, CGAAL implements a variety of strategies for searching the problem state space: a heuristic inspired by PageRank [15] and two heuristic search strategies that exploit the state vector representation of our model, alongside the usual breadth-first and depth-first approach. We conduct experiments comparing our different search strategies with each other on several case studies and show that having more available compute threads often leads to speed-ups of 1-2 orders of magnitude. We also perform experiments comparing our tool on a selection of case studies to the state-of-the-art PRISM-games.

Though while PRISM-games is a tool specialised for probabilistic games we find that our implementation often outperforms PRISM-games and especially whenever we are not required to compute the entire fixed point in which case we are often 1-3 orders of magnitude faster. Again, we emphasise that PRISM games is meant for probabilistic games and as such this is not a completely fair one-to-one comparison.

Outline. This paper is structured as follows. Section 2 introduces the formal definitions of concurrent games and alternating-time temporal logic. In Section 3 we present how model checking of ATL properties in concurrent games can be encoded in extended dependency graphs. We also give a short explanation of the CERTAINZERO algorithm and our search strategies.

In Section 4 we give a short example of how to use CGAAL and the LCGS language. An evaluation of our tool and a comparison with PRISM can be found in Section 5, and we conclude on our findings in Section 6.