Synthesizing Agent Protocols From LTL Specifications Against Multiple Partially-Observable Environments

We consider the problem of synthesizing an agent pro- tocol satisfying LTL specifications for multiple, partially- observable environments. We present a sound and complete procedure for solving the synthesis problem in this setting and show it is computationally optimal from a theoretical com- plexity standpoint. While this produces perfect-recall, hence unbounded, strategies we show how to transform these into agent protocols with bounded number of states.