Skip to Main content Skip to Navigation
Reports

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 :
Reports
Complete list of metadata

https://hal.inria.fr/inria-00071630
Contributor : Rapport de Recherche Inria <>
Submitted on : Tuesday, May 23, 2006 - 6:22:00 PM
Last modification on : Thursday, January 7, 2021 - 4:27:55 PM
Long-term archiving on: : Sunday, April 4, 2010 - 10:29:57 PM

Identifiers

  • HAL Id : inria-00071630, version 1

Citation

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

Share

Metrics

Record views

228

Files downloads

162