Algorithms for Omega-Regular Games with Imperfect Information

Abstract

We study observation-based strategies for two-player turn-based games on graphs with omega-regular objectives. An observation-based strategy relies on imperfect information about the history of a play, namely, on the past sequence of observations. Such games occur in the synthesis of a controller that does not see the private state of the plant. Our main results are twofold. First, we give a fixed-point algorithm for computing the set of states from which a player can win with a deterministic observation-based strategy for any omega-regular objective. The fixed point is computed in the lattice of antichains of state sets. This algorithm has the advantages of being directed by the objective and of avoiding an explicit subset construction on the game graph. Second, we give an algorithm for computing the set of states from which a player can win with probability 1 with a randomized observation-based strategy for a Buechi objective. This set is of interest because in the absence of perfect information, randomized strategies are more powerful than deterministic ones. We show that our algorithms are optimal by proving matching lower bounds.

24 pages. A preliminary version of this paper appeared in the Proceedings of the International Conference for Computer Science Logic (CSL), Lecture Notes in Computer Science 4207, Springer, 2006, pp. 287-302

Cited by in corpus (23)

• Qualitative Analysis of Partially-observable Markov Decision Processes
• Randomness for Free
• Antichains for the Automata-Based Approach to Model-Checking
• Linear Logic by Levels and Bounded Time Complexity
• Model-Checking an Alternating-time Temporal Logic with Knowledge, Imperfect Information, Perfect Recall and Communicating Coalitions
• Developing a Practical Reactive Synthesis Tool: Experience and Lessons Learned
• Output Feedback Controller Design with Symbolic Observers for Cyber-physical Systems
• Satisfiability-Based Methods for Reactive Synthesis from Safety Specifications
• Robust Equilibria in Concurrent Games
• Integrating active sensing into reactive synthesis with temporal logic constraints under partial observations
• Graph Searching, Parity Games and Imperfect Information
• Synthesizing Attack-Aware Control and Active Sensing Strategies under Reactive Sensor Attacks
• Energy mu-Calculus: Symbolic Fixed-Point Algorithms for omega-Regular Energy Games
• Games on graphs with a public signal monitoring
• Exact schedulability test for sporadic mixed-criticality real-time systems using antichains and oracles
• Boolean Observation Games
• Controllers with Minimal Observation Power (Application to Timed Systems)
• Probabilistic Opacity for Markov Decision Processes
• Computationally Feasible Strategies
• Coverability: Realizability Lower Bounds
• A Backward-traversal-based Approach for Symbolic Model Checking of Uniform Strategies for Constrained Reachability
• Safraless Synthesis for Epistemic Temporal Specifications
• Synthesis of coordination programs from linear temporal logic