S. Owre, J. Rushby, and N. Shankar, PVS : A prototype veriication system, Automated Deduction CADE, pp.748-752, 1992.

G. Dowek, A. Felty, H. Herbelin, G. Huet, C. Paulin et al., The Coq Proof assistant User's Guide, Version 6.6" INRIA, 1991.

C. B. Jones, Program speciication and veriication in VDM, 1986.

C. A. Hoare, An axiomatic basis for computer programming, Communications of the ACM, vol.12, issue.10, pp.576-583, 1969.
DOI : 10.1145/363235.363259
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.116.2392

A. Pnueli, The temporal Logic of Programss, 18th Annual symposium on Foundations of computer Science, pp.46-57, 1977.

R. Milner, A Calculus of Communication Systemss, LNCS, vol.92, 1980.

E. M. R-k-e, E. A. Emerson, and A. P. Sistla, Automatic Veriication of Finite-state Concurrent Systems Using Temporal-logic Speciicationss, ACM Transactions on Programming Languages and Systems, vol.8, 1986.

J. Queille and J. Sifakis, Speciication and Veriication of Concurrent Systems in CESARR, 5th International Symposium in Programming, p.3377351, 1981.

J. C. Fernandez, An Implementation of an EEcient Algorithm for Bisimulation Equivalencee, Science of Computer Programming, V ol, vol.13, pp.2-3, 1990.

R. Cleaveland, J. Parrow, and B. Steeen, The Concurrency Workbench, Workshop on Automatic Veriication Methods for Finite State Systemss, LNCS, vol.407, 1989.

J. Richier, C. Rodriguez, J. Sifakis, and J. Voiron, Xesar : A T ool for Protocol Validation. User's Guide, T echnical report of LGI-IMAG, 1987.

C. Courcoubetis, M. Vardi, P. Olper, and M. Yanakakis, Memory EEcient Algorithms for the Veriication of Temporal Propertiess International Workshop on Computer Aided V eriication, 1990.

R. E. Bryant, Graph-based Algorithms for Boolean Function Manipulationn, IEEE Transactions on Computers, issue.8, 1986.

O. Coudert, C. Berthet, and J. Madre, Formal Boolean Manipulations for the Veriication of Sequential Machiness IMEC-IFIP Internationnal Workshop on Applied F ormal Methods For Correct VLSI Design, 1990.

J. Fernandez, A. Kerbrat, and L. Mounier, Symbolic Equivalence Checkingg, Fifth Conference on Computer-Aided V eriication, Elounda (Greece), 1993.
DOI : 10.1007/3-540-56922-7_8
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.45.2980

A. Benveniste and G. Berry, Another Look at Real-Time Programmingg, Proceedings of the IEEE, p.79, 1991.

T. Bolognesi and E. Brinksma, Introduction to the ISO Speciication Language LOTOSS, Computer Networks and ISDN Systems, V ol, p.25529, 1988.

J. Perraud, O. Roux, and M. , Huou : Operational Semantics of a Kernel of the Language Electree,Theoretical Computer Science, N. 100, 1992.

O. Roux and V. Rusu, Decidable Hybrid Systems to Modelize and Verify Real-Time Applicationss , 2nd European Workshop on Real-Time and Hybrid Systems, pp.31-36, 1995.

Y. Kesten, A. Pnueli, J. Sifakis, and S. Yovine, Integration graphs: a class of decidable hybrid systemss Workshop on Theory of Hybrid Systems, LNCS, vol.736, 1993.

R. Alur, C. Courcoubetis, N. Halbwachs, T. Henzinger, P. Ho et al., The Algorithmic Analysis of Hybrid Systemss, 1995.

N. Halbwachs, Y. Proy, and P. , Veriication of Linear Hybrid Systems by Means of Convex Approximationss, International Symposium on Static Analysis, SAS'94, 1994.

T. A. Henzinger and P. Ho, Model Checking Strategies for Hybrid Systemss, Conference on Industrial Applications of Artiicial Intelligence and Expert Systems, 1994.

A. Bouajjani, Y. Laknech, and R. , Robbana From Duration Calculus to Linear Hybrid Automata To appear in the proceedings of the 7th International Conference on Computer-Aided Veriication, 1995.

R. Alur, C. Courcoubetis, and D. Dill, Model-checking for real-time systemss Proceedings of the fth annual IEEE symposium on Logics In Computer Science, 1990.

C. Astraudo and J. J. Borrelly, Simulation of Multiprocessor Robot Controllerss, Proc. IEEE Int. Conf. on Robotics and Automation, 1992.

D. Simon, P. Reedman, and E. Castillo, On the Validation of Robotics Control Systems. Part II: Analysis of real-time closed-loop control tasks, 1995.
URL : https://hal.archives-ouvertes.fr/inria-00073974

E. Coste-maniire, B. Espiau, and E. , Rutten: A Task-Level Robot Programming Language and its Reactive Executionn, Proceedings of the 1992 IEEE International Conference o n R obotics and Automation, pp.2751-2756, 1992.

G. Berry and G. Gonthier, The Esterel synchronous programming language: design, semantics, implementation, Science of Computer Programming, vol.19, issue.2, pp.87-152, 1992.
DOI : 10.1016/0167-6423(92)90005-V
URL : https://hal.archives-ouvertes.fr/inria-00075711

G. Boudol, V. Roy, R. De-simone, and D. Vergamini, Process calculi, from theory to practice: Veriication toolss, in International Workshop on Automatic Veriication Methods for Finite State Systems, LNCS, vol.407, 1990.

E. Castillo, Principes, techniques et outils de simulation, vvriication et exxcution d'actions robotiques, 1994.

E. M. Clarke, A. Emerson, and A. P. Sistla, Automatic Veriication of Finite State Concurrent Systems using Temporal Logic Speciications: a practical approachh, Proc. 10th ACM Symp. on Principles of Programming Languages, pp.117-126, 1983.

J. C. Fernandez, Alddbaran, a tool for veriication of communicating processes, T ech, Report Spectre, vol.14, 1988.

T. Henzinger, X. Nicollin, J. Sifakis, and S. Yovine, Symbolic Model-Checking for Real-Time Systemss, LICS, vol.92, 1992.
DOI : 10.1006/inco.1994.1045
URL : http://doi.org/10.1006/inco.1994.1045

M. Jourdan and F. , Maraninchi and A. Olivero Verifying quantitative real-time properties of synchronous programss, 5th International Conference on Computer-aided V eriication, L N C S 697, 1993.

M. Jourdan, Integrating formal veriication methods of quantitative real-time properties into a development environment for robotic controllers, 1995.

K. Kapellos, Environnement de programmation des applications robotiques ractives, P h D dissertation, 1994.

D. Simon, P. Reedman, and E. Castillo, Analyzing the Temporal Behavior of Real-time Closed-loop Robotic Taskss, IEEE Int. Conf. on Robotics and Automation, 1994.

D. Simon, B. Espiau, E. Castillo, and K. Kapellos, Computer-aided Design of a Generic Robot Controller Handling Reactivity and Real-time Control Issuess, IEEE Trans. on Control Systems Technology, issue.1 4, 1993.

C. Samson, M. Le-borgne, and B. , Espiau: Robot Control: the Task-Function Approach, 1991.

P. J. Ramadge and W. M. Wonham, The Control of Discrete Events Systemss, Proc. of the IEEE, 1989.

P. J. Ramadge and W. M. Wonham, Supervisory Control of a Class of Discrete Event Processes, SIAM Journal on Control and Optimization, vol.25, issue.1, pp.206-230, 1987.
DOI : 10.1137/0325013

D. Simon, K. Kapellos, B. Espiau, and M. Jourdan, Formal Veriication of Missions and Taskss 2nd European Workshop on Real-Time and Hybrid Systems, pp.31-36, 1995.

E. Rutten and P. L. Guernic, Sequencing Data Flow T asks in SIGNALL Workshop on Languages, Compilers and Tool Support for Real-Time Systems, )rlando, 1994.

R. Brooks, A robust layered control system for a mobile robott, IEEE Journal of Robotics and Automation, issue.2 1, pp.14-23, 1986.
DOI : 10.1109/jra.1986.1087032
URL : http://www.dtic.mil/get-tr-doc/pdf?AD=ADA160833

J. Kosecka, H. Christensen, and R. Bajcsy, Discrete event modeling of visually guided behaviors, International Journal of Computer Vision, vol.25, issue.3, pp.179-191, 1995.
DOI : 10.1007/BF01418982

B. A. Brandin and W. M. Wonham, Supervisory Control of Timed D i s c r ete Event Systems, T echnical Report, vol.9210, 1992.

K. T. Seow and R. Denavathan, A Temporal Logic Approach to Discrete Event C o n troll, IEEE Int. Conf. on Robotics and Automation, 1995.

R. Kumar, V. K. Garg, and S. I. Marcus, Predicate and Predicate Transformers for Supervisory Control of Discrete Event Dynamical Systemss, IEEE Trans. on Automatic Control, vol.8, pp.38-1214, 1993.

M. Antoniotti and B. Mishra, Discrete Event M o d e l s + T emporal Logics = Supervisory Controller: Automatic Synthesis of Locomotion Controllerss, IEEE International Conference o n R obotics and Automation, 1995.

M. Antoniotti, M. Jafari, and B. Mishra, Applying Temporal Logic Veriication and Synthesis to Manufacturing Systemss, IEEE International Conference on Systems, Man and Cybernetics, 1995.
DOI : 10.1109/icsmc.1995.538435

D. M. Lyons, A Process-Based Approach t o T ask-Plan Representationn, IEEE Int. Conf. on Robotics and Automation Cincinatti

T. G. Murphy, D. M. Ons, and A. J. Hendriks, Visually Guided Multi-Fingered Grasping as Dened by S c hemas and a Reactive Systemm, Workshop on Neural Architectures and Distributed AI

D. M. Lyons and A. J. Hendriks, Safely Adapting a Hierarchical Reactive Systemm, SPIE Symp. on Intelligent Robots and Computer Vision, XII, 1993.
DOI : 10.1117/12.150223

D. J. Musliner, E. H. Durfee, and K. G. Shin, Reasoning about Bounded Reactivity t o A c hieve Real-Time Guaranteess, Proc. AAAI Spring Symposium on Selective Perception, 1992.

O. Causse and H. I. Christensen, Hierarchical Control Design Based on Petri Net Modelling for an Autonomous Mobile Robott, Intelligent Autonomous Systems Conf (IAS 4), 1995.

X. Rahimi, A Framework for Software Safety V eriication of Industrial Robot Operationss, Computer and Industrial Engineering, issue.2, pp.279-287, 1991.

Z. Ying and A. K. Mackworth, Speciication and Veriication of Constraint Based Dynamic Systemss, 2nd Int. Workshop on Principles and Practice of Constraint Programming, 1994.

N. Lynch and H. B. Weinberg, Proving Correctness of a Vehicle Maneuver: Decelerationn 2nd European Workshop on Real-Time and Hybrid Systems, pp.31-36, 1995.

E. Coste-maniire, M. Perrier, and A. , Peuch Mission Programming: Application to Underwater Robotss 4th Int, Symp. on Experimental Robotics, 1995.

A. Deshpande and P. , Design and Evaluation Tools for Automated Highway Systemss 2nd European Workshop on Real-Time and Hybrid Systems, pp.31-36, 1995.
DOI : 10.1007/bfb0020941
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.32.4877

S. Gaubert, Timed Automata and Discrete Event Systemss, Proc. European Control Conf, 1993.

G. Cohen, P. Moller, J. P. Quadrat, and M. Viot, Algebraic Tools for the Performance Evaluation of Discrete Event Systemss, IEEE Proceedings: Special Issue on Discrete Event Systems, vol.77, issue.1, 1989.

R. Pissard-gibollet, K. Kapellos, P. Es, and J. J. Borrelly, Real-Time Programming of Mobile Robot Actions Using Advanced Control Techniquess 4th Int, Symp. on Experimental Robotics, 1995.

P. Es, R. Pissard-gibollet, and K. , Kapellos : Development of a Reactive Mobile Robot Using Real Time Visionn, Third International Symposium on Experimental Robotics, K y oto, 1993.

D. Simon, K. Kapellos, and B. , Espiau Formal Veriication of Missions and Tasks: Application to Underwater Roboticss Int, Conf. on Advanced R obotics, ICAR'95, 1995.

K. Kapellos, S. Abdou, M. Jourdan, and B. , Espiau Speciication, Formal Veriication and Implementation of Tasks ans Missions for an Autonomous Vehiclee 4th Int, Symp. on Experimental Robotics, 1995.

Y. Lu and J. Buisson, Analysis and Representations of Hybrid Systems with Singular Systemss, First Asian control Conference, T okyo, 1994.

I. Unité-de-recherche, V. Lorraine, and I. Le-`-sle-`-le-`-s-nancy-unité-de-recherche, Technopôle de Nancy-Brabois, Campus scientifique, 615 rue du Jardin Botanique, pp.38031-38032

I. Unité-de-recherche and . Rocquencourt, Domaine de Voluceau, Rocquencourt, BP 105, 78153 LE CHESNAY Cedex Unité de recherche INRIA Sophia-Antipolis, 2004.