Optimal scheduling using priced timed automata

ABSTRACT

This contribution reports on the considerable effort made recently towards extending and applying well-established timed automata technology to optimal scheduling and planning problems. The effort of the authors in this direction has to a large extent been carried out as part of the European projects VHS [20] and AMETIST [16] and are available in the recently released UPPAAL CORA [12], a variant of the real-time verification tool UPPAAL [18, 5] specialized for cost-optimal reachability for the extended model of so-called priced timed automata.

REFERENCES

• 1: Yasmina Abdeddaïm , Abdelkarim Kerbaa , Oded Maler, Task Graph Scheduling Using Timed Automata, Proceedings of the 17th International Symposium on Parallel and Distributed Processing, p.237.2, April 22-26, 2003
• 2: Rajeev Alur , David L. Dill, A theory of timed automata, Theoretical Computer Science, v.126 n.2, p.183-235, April 25, 1994 [doi>10.1016/0304-3975(94)90010-8 ]
• 3: Rajeev Alur , Salvatore La Torre , George J. Pappas, Optimal Paths in Weighted Timed Automata, Proceedings of the 4th International Workshop on Hybrid Systems: Computation and Control, p.49-62, March 28-30, 2001
• 4: J. E. Beasley , M. Krishnamoorthy , Y. M. Sharaiha , D. Abramson, Scheduling Aircraft Landings--The Static Case, Transportation Science, v.34 n.2, p.180-197, May 2000 [doi>10.1287/trsc.34.2.180.12302]
• 5: G. Behrmann, A. David, and K. Larsen. A tutorial on Uppaal. In Formal Methods for the Design of Real-Time Systems, number 3185 in Lecture Notes in Computer Science, pages 200--236. Springer Verlag, 2004.
• 6: Gerd Behrmann , Ansgar Fehnker, Efficient Guiding Towards Cost-Optimality in UPPAAL, Proceedings of the 7th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, p.174-188, April 02-06, 2001
• 7: Gerd Behrmann , Ansgar Fehnker , Thomas Hune , Kim Guldstrand Larsen , Paul Pettersson , Judi Romijn , Frits W. Vaandrager, Minimum-Cost Reachability for Priced Timed Automata, Proceedings of the 4th International Workshop on Hybrid Systems: Computation and Control, p.147-161, March 28-30, 2001
• 8: P. Bouyer, E. Brinksma, and K. Larsen. Staying alive as cheaply as possible. In Proc. of HSCC'04, volume 2993 of Lecture Notes in Computer Science, pages 203--218. Springer-Verlag, 2004.
• 9: P. Bouyer, F. Cassez, E. Fleury, and K. Larsen. Optimal strategies in priced timed game automata. In Proc. of FSTTCS'04, volume 3328 of Lecture Notes in Computer Science, pages 148--160. Springer-Verlag, 2004.
• 10: P. Bouyer, F. Cassez, E. Fleury, and K. Larsen. Synthesis of optimal strategies using HyTech. In Proc. GDV'04, Electronic Notes in Theoretical Computer Science. Elsevier Science Publishers, 2004. To appear.
• 11: Marius Bozga , Conrado Daws , Oded Maler , Alfredo Olivero , Stavros Tripakis , Sergio Yovine, Kronos: A Model-Checking Tool for Real-Time Systems, Proceedings of the 10th International Conference on Computer Aided Verification, p.546-550, June 28-July 02, 1998
• 12: UPPAAL CORA. http://www.cs.aau.dk/-behrmann/cora, Jan. 2005.
• 13: Ansgar Fehnker, Scheduling a Steel Plant with Timed Automata, Proceedings of the Sixth International Conference on Real-Time Computing Systems and Applications, p.280, December 13-15, 1999
• 14: Thomas Hune , Kim G. Larsen , Paul Pettersson, Guided synthesis of control programs using UPPAAL, Nordic Journal of Computing, v.8 n.1, p.43-64, Spring 2001
• 15: IF. http://www-verimag.imag.fr/~async/IF, Jan. 2005.
• 16: Advanced Methods in Timed Systems (AMETIST). http://ametist.cs.utwente.nl, Jan. 2005.
• 17: Kim Guldstrand Larsen , Gerd Behrmann , Ed Brinksma , Ansgar Fehnker , Thomas Hune , Paul Pettersson , Judi Romijn, As Cheap as Possible: Efficient Cost-Optimal Reachability for Priced Timed Automata, Proceedings of the 13th International Conference on Computer Aided Verification, p.493-505, July 18-22, 2001
• 18: K. Larsen, P. Pettersson, and W. Yi. Uppaal in a nutshell. Int. Journal on Software Tools for Technology Transfer, 1(1--2):134--152, 1997.
• 19: K. Larsen and J. Rasmussen. Optimal conditional reachability for multi-priced timed automata. To appear in proceedings of FOSSACS'05, 2005.
• 20: Verification of Hybrid Systems (VHS). http://www-verimag.imag.fr/VHS/, Jan. 2005.
• 21: J. Rasmussen, K. Larsen, and K. Subramani. Resource-optimal scheduling using priced timed automata. In Proc. of TACAS'04, volume 2988 of Lecture Notes in Computer Science, pages pp. 220--235. Springer Verlag, 2004.
• 22: M. Stobbe. Results on scheduling the sidmar steel plant using constraint programming. Internal report, 2000.
• 23: UPPAAL. http://www.uppaal.com, Jan. 2005.

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.2 ANALYSIS OF ALGORITHMS AND PROBLEM COMPLEXITY
      F.2.2 Nonnumerical Algorithms and Problems
          Subjects: Sequencing and scheduling

Additional Classification:
  F. Theory of Computation
  F.1 COMPUTATION BY ABSTRACT DEVICES
      F.1.1 Models of Computation
          Subjects: Automata (e.g., finite, push-down, resource-bounded)
  F.2 ANALYSIS OF ALGORITHMS AND PROBLEM COMPLEXITY
      F.2.2 Nonnumerical Algorithms and Problems
          Subjects: Routing and layout

General Terms:
Algorithms, Theory