Abstract

We compare two approaches for modelling imperfect information in infinite games by using finite-state automata. The first, more standard approach views information as the result of an observation process driven by a sequential Mealy machine. In contrast, the second approach features indistinguishability relations described by synchronous two-tape automata. The indistinguishability-relation model turns out to be strictly more expressive than the one based on observations. We present a characterisation of the indistinguishability relations that admit a representation as a finite-state observation function. We show that the characterisation is decidable, and give a procedure to construct a corresponding Mealy machine whenever one exists. Considering the strategy-synthesis problem, we present a solution for games with imperfect information modeled as indistinguishability relation by a generic reduction schema from imperfect-information to perfect-information games. If time permits, we present as an application a model of full-information protocols that features explicit communication actions, by which the entire observation history of a player is revealed to another player. Such protocols are common in asynchronous distributed systems; here, we consider a synchronous setting with a single active player who may communicate with multiple passive observers in an indeterminate environment. Full-information protocols induce indistinguishability relations that can be described by synchronous two-tape automata, and there exists a specific construction that satisfies the requirement of the reduction schema, making the strategy-synthesis problem decidable. Furthermore we show that the number of passive observers induces a strict hierarchy, both in terms of expressiveness and complexity: with n observers, a full-information protocol can express indistinguishability relations that are not expressible with n-1 observers, and the strategy-synthesis problem is (n+1)-EXPTIME-complete.