Reachability Games Modulo Theories with a Bounded Safety Player

Authors

  • Marco Faella University of Naples Federico II
  • Gennaro Parlato University of Molise

DOI:

https://doi.org/10.1609/aaai.v37i5.25779

Keywords:

KRR: Automated Reasoning and Theorem Proving, MAS: Adversarial Agents, RU: Sequential Decision Making

Abstract

Solving reachability games is a fundamental problem for the analysis, verification, and synthesis of reactive systems. We consider logical reachability games modulo theories (in short, GMTs), i.e., infinite-state games whose rules are defined by logical formulas over a multi-sorted first-order theory. Our games have an asymmetric constraint: the safety player has at most k possible moves from each game configuration, whereas the reachability player has no such limitation. Even though determining the winner of such a GMT is undecidable, it can be reduced to the well-studied problem of checking the satisfiability of a system of constrained Horn clauses (CHCs), for which many off-the-shelf solvers have been developed. Winning strategies for GMTs can also be computed by resorting to suitable CHC queries. We demonstrate that GMTs can model various relevant real-world games, and that our approach can effectively solve several problems from different domains, using Z3 as the backend CHC solver.

Downloads

Published

2023-06-26

How to Cite

Faella, M., & Parlato, G. (2023). Reachability Games Modulo Theories with a Bounded Safety Player. Proceedings of the AAAI Conference on Artificial Intelligence, 37(5), 6330-6337. https://doi.org/10.1609/aaai.v37i5.25779

Issue

Section

AAAI Technical Track on Knowledge Representation and Reasoning