Quantified Loop-mu-calculus for Control under Partial Observation

In this paper, we consider control problems under partial observation in a logical setting. We extend the mu-calculus by adding to formulas quatifications over atomic propositions and force them inside loop mu-calculus definable classes of [2] . We obtain a very expressive logic having a necessary and sufficient condition on the syntactic normal forms of its formulas to decide their model-checking (and the synthesis of controllers they specify). For example, a maximal permissive controller among a class of controllers under partial observation can be synthesized, as well as decentralized controllers in some cases