Approximate verification of strategic abilities under imperfect information

摘要

Model checking of strategic ability under imperfect information is known to be hard. The complexity results range from NP-completeness to undecidability, depending on the precise setup of the problem. No less importantly, the usual fixpoint equivalences do not hold for imperfect information strategies, which seriously hampers incremental synthesis of winning strategies. In this paper, we propose translations of ATLir formulae that provide lower and upper bounds for their truth values, and are cheaper to verify than the original specifications. Most interestingly, the lower approximation is provided by a fixpoint expression that uses a nonstandard variant of the next-step ability operator. We show the correctness of the translations, establish their computational complexity, and validate the approach by experiments with several benchmarks, including a scalable scenario of Bridge play. We also demonstrate that the approximations leave much room for optimizations; in particular, optimizing the data structures can produce a significant speedup. Finally, we show that our fixpoint approximations of ATLir formulae can be combined with under- and overapproximations of models in the vein of may/must abstractions, providing very promising experimental results.