×

zbMATH — the first resource for mathematics

Scheduling with timed automata. (English) Zbl 1088.68023
Summary: We present timed automata as a natural tool for posing and solving scheduling problems. We show how efficient shortest path algorithms for timed automata can find optimal schedules for the classical job-shop problem. We then extend these results to synthesize adaptive scheduling strategies for problems with uncertainty in task durations.

MSC:
68M20 Performance evaluation, queueing, and scheduling in the context of computer systems
68Q45 Formal languages and automata
Software:
IF-2.0; Kronos; Uppaal
PDF BibTeX Cite
Full Text: DOI
References:
[1] Y. Abdeddaı¨m, Scheduling with timed automata, Ph.D. Thesis, INPG, Grenoble, 2002.
[2] Y. Abdeddaı¨m, E. Asarin, O. Maler, On optimal scheduling under uncertainty, in: Proc. TACAS’03, Lecture Notes in Computer Science, vol. 2619, Springer, Berlin, 2003, pp. 240-255. · Zbl 1031.68030
[3] Y. Abdeddaı¨m, A. Kerbaa, O. Maler, Task graph scheduling using timed automata, in: Proc. FMPPTA’03, 2003.
[4] Y. Abdeddaı¨m, O. Maler, Job-shop scheduling using timed automata, in: Proc. CAV’01, Lecture Notes in Computer Science, vol. 2102, Springer, Berlin, 2001, pp. 478-492. · Zbl 0991.68507
[5] Y. Abdeddaı¨m, O. Maler, Preemptive job-shop scheduling using stopwatch automata, in: Proc. TACAS’02, Lecture Notes in Computer Science, vol. 2280, Springer, Berlin, 2002, pp. 113-126. · Zbl 1043.68510
[6] K. Altisen, G. Goessler, A. Pnueli, J. Sifakis, S. Tripakis, S. Yovine, A framework for scheduler synthesis, in: Proc. RTSS’99, IEEE, New York, 1999, pp. 154-163.
[7] Alur, R.; Courcoubetis, C.; Dill, D.L., Model checking in dense real time, Inform. and comput., 104, 2-34, (1993) · Zbl 0783.68076
[8] Alur, R.; Courcoubetis, C.; Henzinger, T.A., Computing accumulated delays in real-time systems, Formal methods system design, 11, 137-155, (1997)
[9] Alur, R.; Dill, D.L., A theory of timed automata, Theoret. comput. sci., 126, 183-235, (1994) · Zbl 0803.68071
[10] R. Alur, S. La Torre, G.J. Pappas, Optimal paths in weighted timed automata, in: Proc. HSCC’01, Lecture Notes in Computer Science, vol. 2034, Springer, Berlin, 2001, pp. 49-64. · Zbl 0991.93076
[11] E. Asarin, O. Maler, As soon as possible: time optimal control for timed automata, in: Proc. HSCC’99, Lecture Notes in Computer Science, vol. 1569, Springer, Berlin, 1999, pp. 19-30. · Zbl 0952.93064
[12] E. Asarin, O. Maler, A. Pnueli, Symbolic controller synthesis for discrete and timed systems, Hybrid Systems II, Lecture Notes in Computer Science, vol. 999, Springer, Berlin, 1995, pp. 1-20.
[13] E. Asarin, O. Maler, A. Pnueli, J. Sifakis, Controller synthesis for timed automata, in: Proc. IFAC Sympos. System Structure and Control, Elsevier, Amsterdam, 1998, pp. 469-474.
[14] G. Behrmann, A. Fehnker T.S. Hune, K.G. Larsen, P. Pettersson, J. Romijn, Efficient guiding towards cost-optimality in UPPAAL, in: Proc. TACAS’01, Lecture Notes in Computer Science, vol. 2031, Springer, Berlin, 2001, pp. 174-188. · Zbl 0978.68541
[15] G. Behrmann, A. Fehnker T.S. Hune, K.G. Larsen, P. Pettersson, J. Romijn, F.W. Vaandrager, Minimum-cost reachability for linearly priced timed automata, in: Proc. HSCC’01, Lecture Notes in Computer Science, vol. 2034, Springer, Berlin, 2001, pp. 147-161. · Zbl 0991.68037
[16] Berthomieu, B.; Diaz, M., Modeling and verification of time dependent systems using time Petri nets, IEEE trans. software eng., 17, 259-273, (1991)
[17] R. Boel, G. Stremersch, VHS case study 5: modelling and verification of scheduling for steel plant at SIDMAR, Draft, 1999.
[18] Boutilier, C.; Dean, T.; Hanks, S., Decision-theoretic planning: structural assumptions and computational leverage, J. artif. intell. res., 11, 1-94, (1999) · Zbl 0918.68110
[19] M. Bozga, C. Daws, O. Maler, A. Olivero, S. Tripakis, S. Yovine, Kronos: a model-checking tool for real-time systems, in: Proc. CAV’98, Lecture Notes in Computer Science, vol. 1427, Springer, Berlin, 1998.
[20] M. Bozga, S. Graf, L. Mounier, IF-2.0: a validation environment for component-based real-time systems, in: Proc. CAV’02, Lecture Notes in Computer Science, vol. 2404, Springer, Berlin, 2002. · Zbl 1010.68751
[21] S. Campos, E. Clarke, W. Marrero, M. Minea, H. Hiraishi, Computing quantitative characteristics of finite-state real-time systems, in: Proc. RTSS’94, IEEE, New York, 1994.
[22] W.Y. Chiang, M.S. Fox, Protection against uncertainty in a deterministic schedule, in: Proc. Fourth Internat. Conf. Expert Systems and Leading Edge in Production and Operations Management, 1990, pp. 184-197.
[23] C. Courcoubetis, M. Yannakakis, Minimum and maximum delay problems in real-time systems, in: Proc. CAV’91, Lecture Notes in Computer Science, vol. 575, Springer, Berlin, 1991, pp. 399-409. · Zbl 0777.68045
[24] A.J. Davenport, J.Ch. Beck, Managing uncertainty in scheduling: a survey, 2000, preprint.
[25] C. Daws, S. Yovine, Reducing the number of clock variables of timed automata, in: Proc. RTSS’96, IEEE, New York, 1996, pp. 73-81.
[26] M. Drummond, J. Bresina, K. Swanson, Just-in-case scheduling, in: Proc. AAAI-94, 1994.
[27] A. Fehnker, Scheduling a steel plant with timed automata, in: Proc. RTCSA’99, 1999.
[28] E. Fersman, P. Pettersson, W. Yi, Timed automata with asynchrounous processes: schedulability and decidability, in: Proc. TACAS’02, Lecture Notes in Computer Science, vol. 2280, Springer, Berlin, 2002, pp. 67-82. · Zbl 1043.68589
[29] Fisher, H.; Thompson, G.L., Probabilistic learning combinations of local job-shop scheduling rules, (), 225-251
[30] H. Gao, Building robust schedules using temporal protection, Master’s Thesis, Department of Industrial Engineering, University of Toronto, 1995.
[31] S. Ghosh, Guanranteeing fault-tolerance through scheduling in real-time systems, Ph.D. Thesis, University of Pittsburgh, 1996.
[32] S. Ghosh, R. Melhem, D. Mosse, Enhancing real-time schedules to tolerate transient faults, in: Proc. RTSS’95, 1995, pp. 120-129.
[33] Henzinger, T.A.; Nicollin, X.; Sifakis, J.; Yovine, S., Symbolic model-checking for real-time systems, Inform. and comput., 111, 193-244, (1994) · Zbl 0806.68080
[34] D.W. Hildum, Flexibility in a knowledge-based system for solving dynamic resource constrained scheduling problems, Ph.D. Thesis, Department of Computer Science, University of Massachusetts, 1994.
[35] Jain, A.S.; Meeran, S., Deterministic job-shop scheduling: past, present and future, European J. oper. res., 113, 390-434, (1999) · Zbl 0938.90028
[36] K.G. Larsen, P. Pettersson, W. Yi, UPPAAL in a nutshell, Software Tools for Tech. Transfer 1/2, 1997. · Zbl 1060.68577
[37] Leon, V.J.; Wu, S.D.; Storer, R.H., Robustness measures and robust scheduling for job shops, IIE trans., 26, 32-43, (1994)
[38] O. Maler, On the problem of task scheduling, Draft, February 1999.
[39] O. Maler, On optimal and sub-optimal control in the presence of adversaries, in: Proc. WODES’04, 2004, pp. 1-12.
[40] O. Maler, A. Pnueli, J. Sifakis, On the synthesis of discrete controllers for timed systems, in: Proc. STACS’95, Lecture Notes in Computer Science, vol. 900, Springer, Berlin, 1995, pp. 229-242. · Zbl 1379.68227
[41] McKay, K.N.; Safayeni, F.R.; Buzacott, J.A., Job-shop scheduling theory: what is relevant?, Interfaces, 18, 84-90, (1998)
[42] P. Niebert, S. Tripakis, S. Yovine, Minimum-time reachability for timed automata, IEEE Mediteranean Control Conf., 2000.
[43] Niebert, P.; Yovine, S., Computing optimal operation schemes for chemical plants in multi-batch mode, European J. control, 7, 440-453, (2001) · Zbl 1293.93526
[44] J. Sifakis, S. Yovine, Compositional specification of timed systems, in: Proc. STACS’96, Lecture Notes in Computer Science, vol. 1046, Springer, Berlin, 1996, pp. 347-359. · Zbl 1379.68240
[45] H. Wong-Toi, G. Hoffmann, The control of dense real-time discrete event systems, Technical Report STAN-CS-92-1411, Stanford University, 1992.
[46] Yovine, S., Kronos: a verification tool for real-time systems, Internat. J. software tools for tech. transfer, 1, (1997) · Zbl 1060.68606
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.