IMITATOR4AMAS: Strategy Synthesis for STCTL

TL;DR

The paper tackles the challenge of synthesizing memoryless strategies for agents with imperfect information in real-time multi-agent systems modeled by timed automata under $STCTL$. It extends the existing model checker, IMITATOR, to support native strategy synthesis for $STCTL$, by augmenting the global state with strategy information and constraining BFS exploration to strategy-consistent paths, producing sound results even when termination is not guaranteed. Experimental results demonstrate substantial speedups over prior approaches, notably outperforming the previous IMITATOR-based method and Maude on benchmark scenarios such as voting, and showcasing additional demonstrations. The work delivers a practical, Docker-distributed, push-button workflow that lowers the barrier to performing strategy synthesis in real-time, imperfect-information settings, with future directions including broader strategy semantics and partial-view models, broadening applicability to safety-critical domains.

Abstract

IMITATOR4AMAS supports model checking and synthesis of memoryless imperfect information strategies for STCTL, interpreted over networks of parametric timed automata with asynchronous execution. While extending the verifier IMITATOR, IMITATOR4AMAS is the first tool for strategy synthesis in this setting. Our experimental results show a substantial speedup over previous approaches.