Reasoning about strategies on collapsible pushdown arenas with imperfect information

TL;DR

This paper extends the decidability results of Strategy Logic with imperfect information from finite to infinite collapsible pushdown systems, using advanced automata techniques for hierarchical multi-agent reasoning.

Contribution

It introduces direction-guided collapsible pushdown automata and proves their stability, enabling model-checking of complex strategies in infinite systems with imperfect information.

Findings

Decidability is preserved for infinite collapsible pushdown systems with visible stacks.

Direction-guided automata are stable under key automata operations.

The approach generalizes finite system results to infinite higher-order systems.

Abstract

Strategy Logic with imperfect information (SLiR) is a very expressive logic designed to express complex properties of strategic abilities in distributed systems. Previous work on SLiR focused on finite systems, and showed that the model-checking problem is decidable when information on the control states of the system is hierarchical among the players or components of the system, meaning that the players or components can be totally ordered according to their respective knowledge of the state. We show that moving from finite to infinite systems generated by collapsible (higher-order) pushdown systems preserves decidability, under the natural restriction that the stack content is visible. The proof follows the same lines as in the case of finite systems, but requires to use (collapsible) alternating pushdown tree automata. Such automata are undecidable, but semi-alternating pushdown tree automata were introduced and proved decidable, to study a strategic problem on pushdown systems with two players. In order to tackle multiple players with hierarchical information, we refine further these automata: we define direction-guided (collapsible) pushdown tree automata, and show that they are stable under projection, nondeterminisation and narrowing. For the latter operation, used to deal with imperfect information, stability holds under some assumption that is satisfied when used for systems with visible stack. We then use these automata to prove our main result.