Lasso games reveal complexities in graph-based winning strategies
Lasso Games
Computer Science and Game TheoryComputational Complexity
Summary
This paper looks at games played on small networks where the game stops when a loop is made, creating a shape like a lasso. The authors study how deciding the winner changes when you consider just the loop part or the whole lasso play. They find that including the whole play can make the game much harder to solve and may need much more memory to play well. Some types of these games stay easier and faster to decide even when using the whole play. The study also explores how the game's rules affect what kinds of strategies are possible.
What this means in practice
- •For formal verification engineers: Decide system correctness efficiently when looping behaviors must be fully considered in automated checks.
- •For game algorithm designers: Design algorithms for graph games that handle full-play memory requirements and complex winning conditions informed by lasso semantics.
A theory result. No direct application yet.
Authors
Krzysztof Żyndul
Abstract
We study games on finite graphs with labelled or weighted edges in which plays end as soon as the first loop is formed. The resulting play has a lasso shape: a path (head) followed by a cycle (loop). We consider two semantics for determining the winner: the loop semantics, where only the loop matters, and the lasso semantics, where the entire play is taken into account. We show that adopting the lasso semantics may have a dramatic impact on both the complexity of the game and the memory required to play optimally. Mean-payoff games with lasso semantics are no longer positionally determined, and the threshold problem â deciding whether the value of the game is at least 0 â is PSPACE-complete. In contrast, lasso parity games are equivalent to weak parity games, remain positionally determined and are solvable in polynomial time. Furthermore, we show that if a positionally determined winning objective is closed under cyclic permutation and both the objective and its complement are closed under concatenation, then it is equivalent to the parity objective. Finally, we consider mod-k games, where the winner depends on the length of the path modulo k >= 2. We show that these games, in both semantics, are PSPACE-complete. Alongside computational complexity, we analyze the memory required to play optimally. We establish that for any game positionally determined in loop semantics, memory of size 2^n is sufficient in lasso semantics. We complement this by showing exponential memory lower bounds for lasso mean-payoff and mod-k games.