HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation

Quantified Loop-mu-calculus for Control under Partial Observation

Stéphane Riedweg 1 Sophie Pinchinat 1
1 S4 - System synthesis and supervision, scenarios
IRISA - Institut de Recherche en Informatique et Systèmes Aléatoires, Inria Rennes – Bretagne Atlantique
Abstract : 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.
Document type :
Complete list of metadata

Contributor : Rapport de Recherche Inria Connect in order to contact the contributor
Submitted on : Tuesday, May 23, 2006 - 6:22:00 PM
Last modification on : Friday, February 4, 2022 - 3:21:55 AM
Long-term archiving on: : Sunday, April 4, 2010 - 10:29:57 PM


  • HAL Id : inria-00071630, version 1


Stéphane Riedweg, Sophie Pinchinat. Quantified Loop-mu-calculus for Control under Partial Observation. [Research Report] RR-4949, INRIA. 2003. ⟨inria-00071630⟩



Record views


Files downloads