Skip to main content
SpringerLink
Log in

On using priced timed automata to achieve optimal scheduling

  • Published:
Formal Methods in System Design Aims and scope Submit manuscript

Abstract

In this paper, we describe an approach for solving the general class of energy-optimal task graph scheduling problems using priced timed automata. We provide an efficient zone-based algorithm for minimum-cost reachability. Furthermore, we show how the simple structure of the linear programs encountered during symbolic minimum-cost reachability analysis of priced timed automata can be exploited in order to substantially improve the performance of the current algorithm. The idea is rooted in duality of linear programs and we show that each encountered linear program can be reduced to the dual problem of an instance of the min-cost flow problem. Experimental results using Uppaal show a 70–80 percent performance gain. We provide priced timed automata models for the scheduling problems and provide experimental results illustrating the potential competitiveness of our approach compared to existing approaches such as mixed integer linear programming.

This is a preview of subscription content, log in via an institution to check access.

Access this article

Log in via an institution

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Institutional subscriptions

Fig. 1
Fig. 2
Fig. 3
Fig. 4
Fig. 5
Fig. 6
Fig. 7

Similar content being viewed by others

Notes

  1. We are not concerned with the successors given the monotonicity of cost evolution.

  2. The implementation used the lp_solve package by Michel Berkelaar, ftp://ftp.es.ele.tue.nl/pub/lp/solve.

  3. The STG set is available at http://www.kasahara.elec.waseda.ac.jp/schedule.

References

  1. Bozga M, Daws C, Maler O, Olivero A, Tripakis S, Yovine S (1998) Kronos: A model-checking tool for real-time systems. In: Proc. 10th International Conference on Computer Aided Verification vol. 1427, pp. 546–550

  2. Larsen KG, Pettersson P, Yi W (1997) UPPAAL in a nutshell. Int J Softw Tools Technol Transfer 1(1–2):134–152

    Google Scholar 

  3. Abdeddaïm Y, Kerbaa A, Maler O (2003) Task graph scheduling using timed automata. In: Proceedings of the International Parallel and Distributed Processing Symposium (IPDPS), pp. 8+

  4. Behrmann G, Fehnker A, Hune T, Larsen K, Petterson P, Romijn J (2001) Efficient guiding towards cost-optimality in UPPAAL. Lecture Notes Comp Sci 2031:174+

  5. Larsen K, Behrmann G, Brinksma E, Fehnker A, Hune T, Pettersson P, Romijn J (2001) As cheap as possible: Efficient cost-optimal reachability for priced timed automata. Lect Notes Comp Sci 2102:493+

  6. Alur R, La Torre S, Pappas GJ (2001) Optimal paths in weighted timed automata. Lect Notes Comp Sci 2034:49+

  7. Gruian F, Kuchcinski K (1999) Low-energy directed architecture selection and task scheduling. In: Proceeding of the 25th EuroMICRO Conference vol. 1, pp. 296–302

  8. Kwok Y-K, Ahmad I (1999) Benchmarking and comparison of the task graph scheduling algorithms. J Parallel Distrib Comp 59(3):381–422

    Google Scholar 

  9. Beasley JE, Krishnamoorthy M, Sharaiha YM, Abramson D (2000) Scheduling aircraft landings—the static case. Transp Sci 34(2):180–197

    Google Scholar 

  10. Berkelaar M (Oct. 2003) www.cs.sunysb.edu/~algorith/implement/lpsol%ve/implement.shtml

  11. Dantzig GB (1963) Linear programming and extensions. Princeton University Press, Princeton, NJ

  12. Ahuja RK, Magnanti TL, Orlin JB (1993) Network flows—theory, algorithms, and applications. Prentice Hall

  13. Cunningham WH (1976) A network simplex method. Math Prog 11:105–106

    Google Scholar 

  14. UPPAAL CORA (Nov. 2004) URL http://www.cs.aau.dk/behrmann/cora

  15. Behrmann G, Fehnker A, Hune T, Larsen K, Pettersson P, Romijn J, Vaandrager F (2001) Minimum-cost reachability for priced timed automata. Lect Notes Comp Sci 2034:147+

  16. Alur R, Dill D (1990) Automata for modelling real-time systems. In: Proc. of Int. Colloquium on Algorithms, Languages and Programming, Lect Notes Comp Sci 443:322–335

  17. Larsen K, Larsson F, Pettersson P, Yi W (1997) Efficient verification of real-time systems: Compact data structure and state space reduction. In: Proc. Real-Time Systems Symposium, pp. 14–24

  18. Tobita T, Kouda M, Kasahara H (2000) Performance evaluation of minimum execution time multiprocessor scheduling algorithms using standard task graph set. In: Proc. of PDPTA'00, pp 745–751

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science, Aalborg University, DK-9220, Aalborg, Denmark

    J. I. Rasmussen & K. G. Larsen

  2. Department of Computer Science and Electrical Engineering, West Virginia University, Morgantown, West Virginia, 26506, USA

    K. Subramani

Authors
  1. J. I. Rasmussen
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. K. G. Larsen
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. K. Subramani
    View author publications

    You can also search for this author in PubMed Google Scholar

Additional information

This research was conducted in part at Aalborg University, where the author was supported by a CISS Faculty Fellowship.

Rights and permissions

Reprints and permissions

About this article

Cite this article

Rasmussen, J.I., Larsen, K.G. & Subramani, K. On using priced timed automata to achieve optimal scheduling. Form Method Syst Des 29, 97–114 (2006). https://doi.org/10.1007/s10703-006-0014-1

Download citation

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s10703-006-0014-1

Keywords

Search

Navigation