The Coq mailing list

[Stephane Demri <demri AT lsv.ens-cachan.fr>]

                               Séminaire 
                 Laboratoire Spécification et Vérification
                        http://www.lsv.ens-cachan.fr/


Mardi 17 Décembre 2002, à 11 h, Salle 206, Bât. Cournot, 


Jean-Francois Raskin (ULB, Bruxelles) fera un exposé sur
        
        ''A Comparison of Control Problems for Timed and Hybrid Systems''


Summary:

In the literature, we find several formulations of the control problem for
timed and hybrid systems. We argue that formulations where a controller can
cause an action at any point in dense (rational or real) time are problematic,
by presenting an example where the controller must act faster and faster, yet
causes no Zeno effects (say, the control actions are at times
$0,\frac{1}{2},1,1\frac{3}{4},2,2\frac{7}{8},3,3\frac{15}{16},\ldots$).
Such a controller is, of course, not implementable in software.
Such controllers are avoided by formulations where the controller can cause
actions only at discrete (integer) points in time.
While the resulting control problem is well-understood if the time unit, or
``sampling rate'' of the controller, is fixed a priori, we define a novel,
stronger formulation: the {\em discrete-time control problem with unknown
sampling rate\/} asks if a sampling controller exists for {\em some\/}
sampling rate. We prove that, surprisingly and unfortunately, this problem is
undecidable even in the special case of timed automata.







Cordialement,


---
Stéphane Demri

Laboratoire Spécification et Vérification 
CNRS UMR 8643, École Normale Supérieure de Cachan 
61, avenue du Président Wilson          
94235 CACHAN Cedex - France
demri AT lsv.ens-cachan.fr
                    http://www.lsv.ens-cachan.fr/~demri
Tel: ++ 33 1 47 40 55 68                Secret.: ++ 33 1 47 40 24 04
Fax: ++ 33 1 47 40 24 64                Office: RH-E-01b