Games on Graphs: A Time-Efficient Algorithm for Solving Finite Reachability and Safety Games

TL;DR

This paper introduces a novel, time-efficient algorithm for solving finite reachability and safety games on graphs, leveraging their duality, and demonstrates its superior performance through extensive experiments.

Contribution

The work presents a new algorithm that efficiently solves both reachability and safety games by exploiting their duality, improving upon traditional methods.

Findings

The algorithm outperforms traditional methods in randomized tests.

It effectively addresses both reachability and safety games.

Experimental results show significant efficiency gains.

Abstract

In recent years, there has been a growing interest in games on graphs within the research community, fueled by their relevance in applications such as economics, politics, and epidemiology. This paper aims to comprehensively detail the design decisions involved in developing a time-efficient algorithm for solving finite reachability and safety games on graphs. The primary contribution of this work is the introduction of a novel algorithm that effectively addresses both reachability and safety games by exploiting their inherent duality. The performance of the proposed algorithm is rigorously evaluated against traditional methods using a randomized testing framework. The paper is organized as follows: first, we provide the reader with a theoretical overview of reachability and safety games, followed by an in-depth discussion on the construction of the playing arena. A formal definition of reachability and safety games and a review of traditional algorithms for their resolution are then presented. Subsequently, the multiple-perspective algorithm is introduced along with its optimizations. The paper concludes with an extensive set of experiments and a comprehensive discussion of their results.