|
 |
Research Themes
- Controller synthesis
- Real-time systems
- Timed automata
- Verification of open systems
- Observation
Partners
Names in bold shape correspond to the people who are responsible of this project in each unit.
Project
Context of the project. Our project addresses the controller synthesis problem for real-time open systems. Most of the safety critical systems nowadays include a control program to supervise a plant. Such systems are often called embedded systems (e.g. nuclear plant, transport software, communication protocols, etc). They are critical in the sense that error can lead to the loss of lives or a major loss of money. This is why a great deal of research has been devoted to the formal verification of such systems. Among other techniques, model-checking consists in verifying that a model (of the plant and the control program running concurrently) meets some specification. It is now widely used in an industrial context and has turned out very successful in the design of critical systems. However, model-checking requires that the whole system is designed and the control program is given a priori.A more difficult task consists in building a control program that supervises the plant in order to meet some requirements. In the automatic control community this problem has been extensively studied since the seminal work of Ramadge and Wonham about the supervisory control of discrete systems. How to build a controller for finite discrete event systems and when it can be done, are now well understood questions. This is not yet the case for timed systems, which involve real-time constraints. During the last decade, the model of timed automata (Alur and Dill) made it possible to reason about quantitative time. Model-checking was lifted to timed automata and is now supported by various tools (KRONOS, UPPAAL, CMC), which have been applied successfully to the verification of many industrial cases. The control synthesis problem for timed systems is of course more difficult, particularly because of the dense nature of time. It has been studied quite a lot recently but only partial results exist and there is no unified theory for the control of timed systems.
Core of the project. If we try to summarize the results about control synthesis for timed systems we find the following features:
- the systems are usually timed automata or hybrid automata where the transitions are partitioned into controllable and uncontrollable ones; another way of tackling the control problem is to assume that discrete transitions are controllable (triggered by the controller) while continuous transitions correspond to the evolution of the environment;
- there are different (un)decidability results according to the class of timed systems involved (timed automata, rectangular automata, hybrid automata) and the logic used for specifying the desired property of the system;
- different types of timed control can be defined: dense-time control, sampling control, and again different decidability results follow from the type of control involved;
- the controller synthesis problem is solved using a backward reachability algorithm [MPS95,WT97] on the model of the plant: this means that the synthetised controller (when there is one) has a structure (discrete part) determined by the model of the plant.
Meetings
- First meeting: friday, the 31st of october 2003 in Cachan
- ACI SI days in Rennes the 11th and 12th of december 2003
- Second meeting: friday, the 5th of march 2004 in Grenoble
- Third meeting: monday, the 7th and tuesday, the 6th of june 2004 in Nantes
- Fourth meeting: monday, the 20th and tuesday, the 21st of september 2004 in Grenoble
- ACI SI days in Toulouse the 13th, 14th and 15th november 2004 in Toulouse
- Fifth meeting: thursday, the 3rd and friday, the 4th february 2005 in Cachan
- Sixth meeting: monday, the 6th and thursday, the 7th june 2005 in Nantes
-
Conference MSR'05 : CORTOS has an invitation session
- Joint meeting of the ACI Cortos, Persée and Versydis : tuesday, the 14th and wednesday, the 15th march 2006 in Cachan
- Workshop CORTOS'06, co-located with CONCUR'06 : thursday the 31st august 2006 in Bonn (Germany)
Reports
Publications
- Patricia Bouyer, Franck Cassez, Emmanuel Fleury and Kim G. Larsen. Optimal strategies in priced timed game automata. Research Report RS-04-4, Basic Research in Computer Science, Denmark, February 2004. 32 pages. Web page.
- Moez Krichen and Stavros Tripakis. Black-box conformance testing for real-time systems. In Proc. 11th International SPIN Workshop on Model-Checking of Software (SPIN'04), LNCS 2989, pp.109-126, Springer, 2004.
- Patricia Bouyer, Ed Brinksma and Kim G. Larsen. Staying alive as cheaply as possible. In Proc. 7th International Workshop on Hybrid Systems: Computation and Control (HSCC'04), LNCS 2993, pp.203-218, Springer, 2004.
- Olivier (H.) Roux and Didier Lime. Time (Petri) Nets with Inhibitor Hyperarcs. (Formal) Semantics ans State Space Computation. In Proc. 25th International Conference on Application and Theory of (Petri) Nets (ICATPN'04), LNCS 3099, pp. 371-390, Springer, 2004.
- Patricia Bouyer, Franck Cassez, Emmanuel Fleury and Kim G. Larsen. Synthesis of optimal strategies using HyTech. In Proc. Workshop on Games in Design and Verification (GDV 2004), ENTCS 119(1), pp. 11-31. Elsevier, 2005.
- Franck Cassez and Olivier (H.) Roux. Structural Translation from Time (Petri) Nets to Timed Automata. In Proc. 4th International Workshop on Automated Verification of Critical Systems (AVoCS'04), ENTCS, Elsevier, 2004. To appear.
- Moez Krichen and Stavros Tripakis. Real-time testing with timed automata testers and coverage criteria. In Proc. Joint Conference on Formal Modelling and Analysis of Timed Systems and Formal Techniques in Real-Time and Fault Tolerant Systems (FORMATS+FTRTFT'2004), LNCS 3253, pp. 134-151. Springer, 2004
- Didier Lime and Olivier (H.) Roux. A Translation Based Method for the Timed Analysis of Scheduling Extended Time (Petri) Nets. In Proc. 25th IEEE International Real-Time Systems Symposium (RTSS'04), pp. 187-196. IEEE Computer Society Press, 2004.
- Patricia Bouyer, Franck Cassez, Emmanuel Fleury and Kim G. Larsen. Optimal strategies in priced timed game automata. In Proc. 24th Conference on Foundation of Software Technology and Theoretical Computer Science (FST&TCS 2004), LNCS 3328, pp. 148-160. Springer, 2004.
- Fabrice Chevalier. Détection d'erreurs dans les systèmes temporisés. Mémoire du DEA Algorithmique, 2004.
- Guillaume Gardey, Olivier (H.) Roux and Olivier (F.) Roux. State Space Computation and Analysis of Time (Petri) Nets. Journal Theory and Practice of Logic Programming (TPLP), Special Issue on Specification Analysis and Verification of Reactive Systems, 2005. To appear.
- Patricia Bouyer, Fabrice Chevalier and Deepak D'Souza. Fault Diagnosis using Timed Automata. In Proc. 8th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS'05), LNCS 3441, pp.219-233, Springer, 2005.
- Karine Altisen, Florence Maraninchi, and David Stauch. Exploring aspects in the context of reactive systems. In Proc. Workshop Foundations of Aspect-Oriented Languages (FOAL'04), pages 45--51, 2004.
- Karine Altisen, Florence Maraninchi, and David Stauch. Aspect-oriented programming for reactive systems: a proposal in the synchronous framework, 2005. Submitted to Science of Computer Programming, (Special Issue on Foundations of Aspect-Oriented Programming).
- Patricia Bouyer, Ed Brinksma, and Kim G. Larsen. Optimal infinite scheduling for multi-priced timed automata. Formal Methods in Systen Design, 2005. To appear.
- Patricia Bouyer, Franck Cassez, and François Laroussinie. Modal logics for timed control. Research Report RI-2005-3, IRCCyN/CNRS, Nantes, France, 2005.
- Bernard Berthomieu, Didier Lime, Olivier (H.) Roux, and François Vernadat. Reachability problems and abstract state spaces for time Petri nets with stopwatches. Technical Report 04483, LAAS, 2004.
- Thao Dang. Application of reachability analysis to idle speed control synthesis. International Journal of Software Engineering & Knowledge Engineering (IJSEKE), 2005. Special issue of selected papers from the International Embedded and Hybrid Systems Conference (IEHSC'05). To appear.
- Stavros Tripakis. Undecidable Problems in Decentralized Observation and Control for Regular Languages. In Information Processing Letters, vol. 90, issue 1, pp. 21-28, 2006
- Stavros Tripakis. Decentralized observation problems. CDC-ECC'05
- Stéphane Demri, Ranko Lazic, and David Nowak. On the freeze quantifier in constraint LTL: Decidability and complexity. In Proc. 12th International Symposium on Temporal Representation and Reasoning (TIME'05). IEEE Computer Society Press, 2005. To appear.
- Philippe Gerner and Thao Dang. Computing schedules for multithreaded real-time programs using geometry. In Proc. Joint Conference on Formal Modelling and Analysis of Timed Systems and Formal Techniques in Real-Time and Fault Tolerant System (FORMATS+FTRTFT'04), LNCS 3253, pp. 325-342. Springer, 2004.
- Moez Krichen and Stavros Tripakis. An expressive and implementable formal framework for testing real-time systems. In Proc. 17th IFIP International Conference on Testing of Communicating Systems (TESTCOM'05), LNCS, Springer, 2005. To appear.
- Saddek Bensalem, Marius Bozga, Moez Krichen, Stavros Tripakis. Testing conformance of real-time applications by automatic generation of observers. In Proc. 4th International Workshop Runtime Verification (RV'04), ENTCS, Elsevier, 2004. To appear.
- Stavros Tripakis. Undecidable problems of decentralized observation and control on regular languages. Information Processing Letters (IPL), 90(1):21--28, 2004.
- Stavros Tripakis. Two-phase distributed observation problems. In Proc. 5th International Conference on Application of Concurrency to System Design (ACSD'05). IEEE Computer Society Press, 2005. To appear.
- Karine Altisen, Patricia Bouyer, Thierry Cachat, Franck Cassez, Guillaume Gardey. Introduction au contrôle des systèmes temps-réel. Journal Européen des Systèmes Automatisés, vol. 39, p. 367-380, 2005.
- Patricia Bouyer, Fabrice Chevalier, Moez Krichen, Stavros Tripakis. Observation partielle des systèmes temporisés. Journal Européen des Systèmes Automatisés, vol. 39, p. 381-393, 2005.
- Karine Altisen, Nicolas Markey, Pierre-Alain Reynier, Stavros Tripakis. Implémentabilité des automates temporisés. Journal Européen des Systèmes Automatisés, vol. 39, p. 395-406, 2005.
- Patricia Bouyer, Franck Cassez and François Laroussinie. Modal Logics for Timed Control. In Proc. 16th International Conference on Concurrency Theory (CONCUR'05), LNCS 3653, pp. 81-94. Springer, 2005
- Sophie Pinchinat and Stéphane Riedweg. You Can Always Compute Maximally Permissive Controllers Under Partial Observation When They Exist. In Proc.24th American Control Conference (ACC'05), pp. 2287-2292, 2005
- Stéphane Demri, David Nowak. Reasoning about transfinite sequences (extended abstract). In Proc. 3rd International Symposium on Automated Technology for Verification and Analysis (ATVA'05), LNCS 3707, pp. 248-262. Springer, 2005
- Sophie Pinchinat and Stéphane Riedweg. On the Architectures in Decentralized Supervisory Control. In Proc. 44th IEEE Conference on Decision and Control and European Control Conference (CDC-ECC'05), pp. 12-17. IEEE Computer Society Press, 2005.
- Patricia Bouyer, Thomas Brihaye and Nicolas Markey. Improved Undecidability Results on Weighted Timed Automata. Information Processing Letters 98(5), pp. 188-194, 2006
- Patricia Bouyer and Fabrice Chevalier. On the Control of Timed and Hybrid Systems. EATCS Bulletin 89, pages 79-96, 2006
- Patricia Bouyer. Weighted Timed Automata: Model-Checking and Games. In Proc. 22nd Conference on Mathematical Foundations of Programming Semantics (MFPS'06), ENTCS 158, pp. 3-17. Elsevier Science Publishers, 2006
- Guillaume Gardey, Olivier (F.) Roux, and Olivier (H.) Roux. Safety control synthesis for time Petri nets. In Proc. 8th International Workshop on Discrete Event Systems (WODES'06), pp. 222-228. IEEE Computer Society Press, 2006 [ bib ]
- Karine Altisen, Franck Cassez and Stavros Tripakis. Monitoring and Fault Diagnosis with Digital Clocks. ACSD'06
- Patricia Bouyer, Thomas Brihaye and Fabrice Chevalier. Control in o-Minimal Hybrid Systems. In Proc. 21st Annual IEEE Symposium on Logic in Computer Science (LICS'06), pp. 367-378. IEEE Computer Society Press, 2006
- Patricia Bouyer, Laura Bozzelli and Fabrice Chevalier. Controller Synthesis for MTL Specifications. In Proc. 17th International Conference on Concurrency Theory (CONCUR'06), LNCS 4137, pp. 450-464. Springer, 2006
- François Laroussinie, Nicolas Markey and Ghassan Oreiby. Model Checking Timed ATL for Durational Concurrent Game Structures. In Proc. 4th International Conference on Formal Modelling and Analysis of Timed Systems (FORMATS'06), LNCS 4202, pages 245-259. Springer, 2006
- Régis Gascon and Laura Bozzelli. Branching Time Temporal Logic Extended with Presburger Constraints. In Proc. 13th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR'06), LNCS. Springer, 2006, to appear
- Thierry Cachat. Controller Synthesis & Ordinal Automata. In Proc. 4th International Symposium on Automated Technology for Verification and Analysis (ATVA'06), Springer, 2006, to appear
- Patricia Bouyer, Kim G. Larsen, Nicolas Markey and Jacob I. Rasmussen. Almost Optimal Strategies in One-Clock Priced Timed Automata. In Proc. 26th Conference on Fundations of Software Technology and Theoretical Computer Science (FSTTCS'06), LNCS. Springer, 2006. To appear
Last modifications, the 22nd november 2006 by Patricia Bouyer.
