Abstract of Paper

Quantified mu-calculus for control synthesis
by Stephane Riedweg and Sophie Pinchinat


We consider an extension of the mu-calculus as a general
framework to describe and synthesize controllers. This extension is
obtained by quantifying atomic propositions, we call the resulting logic
quantified mu-calculus. We study some of  its theoretical properties and
show its adequacy to control applications.  The proposed framework is
expressive: it offers a uniform way to describe as varied  parameters  
as the kind of systems (closed or open), the control objective, the type 
of interaction between the controller and the system, the optimality 
criteria (fairness, maximally permissive), etc. To our knowledge, none 
of the former approaches can capture  such a wide range of concepts.