Résumé de rapport du LIF


Rapport 23-2004
Nicolas Baudru and Peter Niebert
Controllers from proofs: An alternative approach to control synthesis for mu-calculus specifications


Téléchargement / Download : pdf 212k , ps.gz 188k , bibtex

Abstract

Given a "plant" S, the control synthesis problem can be understood as the search for a component C such that the combined system S*C meets a specification phi. The properties may range from simple reachability constraints to arbitrary finite state branching time properties such as specified in the mu-calculus. Previous works typically combine the (finite state transition) system S and the specification of the desired behavioural property phi into a specification psi(S,phi) of the controller C to be synthesized.

In a twist to this setting, we show how the control synthesis problem can be presented as controllability problem for the uncontrolled system S, i.e. we give a simple transformation of the control goal phi specification into a property sigma(phi) such that any system S satisfies sigma(phi) iff a controller C exists such that S*C satisfies phi. S models sigma(phi) can then be established by model-checking and we also show how to extract C from the result (tableau) of the model-checking process.

The proof technique used for the main theorem is based on transformations of proofs (tableaus) and may have an interest of its own. Beyond model-checking, and beyond previous works on control synthesis for the mu-calculus, our approach may also be applied to the algorithmic construction of controllers for provably controllable infinite state systems. However, we see the main potential advantage in opening an easy way of implementing general control synthesis in existing model-checking frameworks (like Spin, Murphi or CADP), including application of model-checking heuristics that may provide reduced size controllers.

Keywords

control synthesis, mu-calculus, model-checking, approximations, disjunctive formulas, control formulas.

Résumé

Etant donné un système S, le problème de la synthèse de contrôleurs peut être compris comme la recherche d'un composant C tel que le système combiné S*C rencontre une spécification phi. Les propriétés considérées peuvent aussi bien être de simples contraintes d'accessibilité que des propriétés temporelles arborescentes à état finis spécifiées dans le mu-calcul. Les travaux précédents combinent un système (de transition à états finis) S et une spécification de la propriété comportementale désirée phi en une spécification psi(S,phi) du contrôleur C à synthétiser.

Notre approche diffère des précédentes: nous montrons que le problème de la synthèse de contrôleurs peut être présenté comme \emph{un problème de contrôlabilité} du système à contrôler S: nous présentons une simple transformation de la spécification phi exprimant le but du contrôle en une propriété sigma(phi) telle qu'un système S satisfait sigma(phi) ssi un contrôleur C tel que S*C satisfait phi existe. S models sigma(phi) peut être alors établie par model-checking et nous montrons comment extraire C à partir du résultat (tableaux) du processus de model-checking.

La technique de preuve utilisée pour le théorème principal est basée sur des transformations de preuves (tableaux) et présente un intérêt en soi. Au-delà du model-checking, et au-delà des précédents travaux sur la synthèse de contrôleurs pour le mu-calcule, notre approche peut être aussi utilisée pour la construction algorithmique de contrôleurs pour des systèmes contrôlables avec un espace d'états infini. De plus, nous verrons que le principal avantage de notre méthode est qu'elle permet une implémentation facile du problème de la synthèse de contrôleurs dans des domaines particuliers du model-checking (comme Spin, Murphi ou CADP), incluant des heuristiques qui peuvent réduire la taille des contrôleurs.

Mots clés

synthèse de contrôleur, mu-calcul, model-checking, approximations, formules disjunctives, formules de contrôles.

Bibtex

@TECHREPORT{23-2004,
    AUTHOR	= {Nicolas Baudru and Peter Niebert},
    TITLE	= {{Controllers from proofs: An alternative approach to control synthesis for mu-calculus specifications}},
    INSTITUTION	= {{LIF}},
    ADDRESS	= {Marseille, France},
    TYPE	= {Research report},
    NUMBER	= {23-2004},
    MONTH	= {11},
    YEAR	= {2004},
    NOTE	= {http://pageperso.lif.univ-mrs.fr/~edouard.thiel/RESP/Rapports/23-2004.html},
}

[css]   [GenRap] [xhtml] Direction : François Denis - Secrétariat de direction : Martine Quessada
Tel. 04 91 11 36 00 - Fax : 04 91 11 36 02 - Mel. Martine.Quessada@cmi.univ-mrs.fr

webmaster - La dernière mise à jour de cette page date du 04 septembre 2008