You have just completed your registration at OpenAire.
Before you can login to the site, you will need to activate your account.
An e-mail will be sent to you with the proper instructions.
Important!
Please note that this site is currently undergoing Beta testing.
Any new content you create is not guaranteed to be present to the final version
of the site upon release.
International audience; The problems of time-dependent behavior in general, and dynamic resource allocation in particular, pervade many aspects of modern life. Prominent examples range from reliability and efficient use of communication resources in a telecommunication network to the allocation of tracks in a continental railway network, from scheduling the usage of computational resources on a chip for durations of nanoseconds to the weekly, monthly or longer-range reactive planning in a factory or a supply chain. These problems have been subject to substantial research for decades by different communities such as operational research, computer systems performance evaluation as well as planning and scheduling, witnessed by large ACM communities such as SIGMETRICS and PERFORMANCE. In this paper we argue that the formalism of timed automata together with recent extensions provides an alternative framework with complementary, yet competitive, results in terms of modeling ca-pabilities and efficiency of analysis.
6. REFERENCES automata with energy constraints. In Proc. 6th
[1] Y. Abdeddaïm, E. Asarin, and O. Maler. International Conference on Formal Modeling Scheduling with timed automata. Theoretical and Analysis of Timed Systems (FORMATS'08), Computer Science, 354(2):272-300, 2006. Lecture Notes in Computer Science, Lecture
[2] K. Altisen et al. A framework for scheduler syn- Notes in Computer Science. Springer, 2008. thesis. In IEEE Real-Time Systems Symposium, [15] P. Bouyer et al. Almost optimal strategies p. 154-163, 1999. in one-clock priced timed automata. In Proc.
[3] R. Alur, M. Bernadsky, and P. Madhusu- 26th Conference on Foundations of Software dan. Optimal reachability in weighted timed Technology and Theoretical Computer Science games. In Proc. 31st International Colloquium (FSTTCS'06), Lecture Notes in Computer Scion Automata, Languages and Programming ence 4337, p. 345-356. Springer, 2006. (ICALP'04), Lecture Notes in Computer Science [16] M. Bozga et al. Verification of asynchronous cir3142, p. 122-133. Springer, 2004. cuits using timed automata. Electronic Notes in
[4] R. Alur, C. Courcoubetis, and D. L. Dill. Model- Theoretical Computer Science, 65(6), 2002. checking for real-time systems. In Proc. 5th An- [17] Th. Brihaye, V. Bruyère, and J.-F. Raskin. On opnual Symposium on Logic in Computer Science timal timed strategies. In Proc. 3rd International (LICS'90), p. 414-425. IEEE Computer Society Conference on Formal Modeling and Analysis of Press, 1990. Timed Systems (FORMATS'05), Lecture Notes
[5] R. Alur and D. L. Dill. Automata for modeling in Computer Science 3821, p. 49-64. Springer, real-time systems. In Proc. 17th International 2005. Colloquium on Automata, Languages and Pro- [18] F. Cassez et al. Efficient on-the-fly algorithms gramming (ICALP'90), Lecture Notes in Com- for the analysis of timed games. In Proc. 16th Inputer Science 443, p. 322-335. Springer, 1990. ternational Conference on Concurrency Theory
[6] R. Alur, S. La Torre, and G. J. Pappas. Opti- (CONCUR'05), Lecture Notes in Computer Scimal paths in weighted timed automata. In Proc. ence 3653, p. 66-80. Springer, 2005. 4th International Workshop on Hybrid Systems: [19] F. Cassez et al. Timed control with observaComputation and Control (HSCC'01), Lecture tion based and stuttering invariant strategies. Notes in Computer Science 2034, p. 49-62. In Proc. 5th International Symposium on AutoSpringer, 2001. mated Technology for Verification and Analysis
[7] E. Asarin and O. Maler. As soon as possi- (ATVA'07), Lecture Notes in Computer Science ble: Time optimal control for timed automata. 4762, p. 192-206. Springer, 2007. In Proc. 2nd International Workshop on Hybrid [20] F. Cassez et al. Automatic synthesis of robust Systems: Computation and Control (HSCC'99), and optimal controllers - an industrial case Lecture Notes in Computer Science 1569, p. 19- study. In Proc. 12th International Workshop 30. Springer, 1999. on Hybrid Systems: Computation and Control
[8] E. Asarin et al. Controller synthesis for timed (HSCC'09), Lecture Notes in Computer Science automata. In Proc. IFAC Symposium on System 5469. Springer, 2009. Structure and Control, p. 469-474. Elsevier Sci- [21] A. Chakrabarti et al. Resource interfaces. In ence, 1998. Proc. 3rd International Workshop on Embedded
[10] G. Behrmann et al. Minimum-cost reachability chapter 4, p. 93-119. CRC Press, 2009. for priced timed automata. In Proc. 4th Interna- [23] H. Dierks. PLC-automata: a new class of impletional Workshop on Hybrid Systems: Computa- mentable real-time automata. Theoretical Comtion and Control (HSCC'01), Lecture Notes in puter Science, 253(1):61-93, 2001. Computer Science 2034, p. 147-161. Springer, [24] H. Dierks. Finding optimal plans for domains 2001. with continuous effects with UPPAAL CORA.
[11] B. Bérard and C. Dufourd. Timed automata and In Proc. ICAPS'05 Workshop on Verification additive clock constraints. Information Process- and Validation of Model-Based Planning and ing Letters, 75(1-2):1-7, 2000. Scheduling Systems, 2005.
[12] P. Bouyer. Forward analysis of updatable timed [25] U. Fahrenberg and K. G. Larsen. Discountautomata. Formal Methods in System Design, optimal infinite runs in priced timed automata. 24(3):281-320, 2004. Electronic Notes in Theoretical Computer Sci-
[13] P. Bouyer, E. Brinksma, and K. G. Larsen. Op- ence, 239:179-191, 2009. timal infinite scheduling for multi-priced timed [26] E. Fersman et al. Schedulability analysis of automata. Formal Methods in System Design, fixed-priority systems using timed automata. 32(1):2-23, 2008. Theoretical Computer Science, 354(2):301-317,
[14] P. Bouyer et al. Infinite runs in weighted timed 2006.
[27] K. Havelund et al. Formal modeling and analysis of an audio/video protocol: An industrial case study using UPPAAL. In Proc. 18th IEEE Real-Time Systems Symposium (RTSS'97), p. 2- 13. IEEE Computer Society Press, 1997.
[28] M. Hendriks, B. van den Nieuwelaar, and F. W. Vaandrager. Model checker aided design of a controller for a wafer scanner. STTT, 8(6):633- 647, 2006.
[29] Th. A. Henzinger et al. What's decidable about hybrid automata? Journal of Computer and System Sciences, 57(1):94-124, 1998.
[30] Th. A. Henzinger et al. Symbolic modelchecking for real-time systems. Information and Computation, 111(2):193-244, 1994.
[32] J. J. Jessen et al. Guided controller synthesis for climate controller using UPPAAL-TIGA. In Proc. 5th International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS'07), Lecture Notes in Computer Science 4763, p. 227-240. Springer, 2007.
[33] Y. Kesten et al. Decidable integration graphs. Information and Computation, 150(2):209-243, 1999.
[34] K. G. Larsen et al. As cheap as possible: Efficient cost-optimal reachability for priced timed automata. In Proc. 13th International Conference on Computer Aided Verification (CAV'01), Lecture Notes in Computer Science 2102, p. 493-505. Springer, 2001.
[35] K. G. Larsen and J. I. Rasmussen. Optimal reachability for multi-priced timed automata. Theoretical Computer Science, 390(2-3):197-213, 2008.
[37] M. Schuts et al. Modelling clock synchronization in the Chess gMAC WSN protocol. CoRR, abs/0912.1901, 2009.
[38] S. Tripakis and K. Altisen. Controller synthesis for discrete and dense-time systems. In Proc. World Congress on Formal Methods in the Development of Computing Systems (FM'99), Lecture Notes in Computer Science 1708, p. 233- 252. Springer, 1999.
[39] S. Tripakis and S. Yovine. Timing analysis and code generation of vehicle control software using TAXYS. Electronic Notes in Theoretical Computer Science, 55(2), 2001.
[40] L. Waszniowski and Z. Hanzálek. Formal verification of multitasking applications based on timed automata model. Real-Time Systems, 38(1):39-65, 2008.
6. REFERENCES automata with energy constraints. In Proc. 6th
[1] Y. Abdeddaïm, E. Asarin, and O. Maler. International Conference on Formal Modeling Scheduling with timed automata. Theoretical and Analysis of Timed Systems (FORMATS'08), Computer Science, 354(2):272-300, 2006. Lecture Notes in Computer Science, Lecture
[2] K. Altisen et al. A framework for scheduler syn- Notes in Computer Science. Springer, 2008. thesis. In IEEE Real-Time Systems Symposium, [15] P. Bouyer et al. Almost optimal strategies p. 154-163, 1999. in one-clock priced timed automata. In Proc.
[3] R. Alur, M. Bernadsky, and P. Madhusu- 26th Conference on Foundations of Software dan. Optimal reachability in weighted timed Technology and Theoretical Computer Science games. In Proc. 31st International Colloquium (FSTTCS'06), Lecture Notes in Computer Scion Automata, Languages and Programming ence 4337, p. 345-356. Springer, 2006. (ICALP'04), Lecture Notes in Computer Science [16] M. Bozga et al. Verification of asynchronous cir3142, p. 122-133. Springer, 2004. cuits using timed automata. Electronic Notes in
[4] R. Alur, C. Courcoubetis, and D. L. Dill. Model- Theoretical Computer Science, 65(6), 2002. checking for real-time systems. In Proc. 5th An- [17] Th. Brihaye, V. Bruyère, and J.-F. Raskin. On opnual Symposium on Logic in Computer Science timal timed strategies. In Proc. 3rd International (LICS'90), p. 414-425. IEEE Computer Society Conference on Formal Modeling and Analysis of Press, 1990. Timed Systems (FORMATS'05), Lecture Notes
[5] R. Alur and D. L. Dill. Automata for modeling in Computer Science 3821, p. 49-64. Springer, real-time systems. In Proc. 17th International 2005. Colloquium on Automata, Languages and Pro- [18] F. Cassez et al. Efficient on-the-fly algorithms gramming (ICALP'90), Lecture Notes in Com- for the analysis of timed games. In Proc. 16th Inputer Science 443, p. 322-335. Springer, 1990. ternational Conference on Concurrency Theory
[6] R. Alur, S. La Torre, and G. J. Pappas. Opti- (CONCUR'05), Lecture Notes in Computer Scimal paths in weighted timed automata. In Proc. ence 3653, p. 66-80. Springer, 2005. 4th International Workshop on Hybrid Systems: [19] F. Cassez et al. Timed control with observaComputation and Control (HSCC'01), Lecture tion based and stuttering invariant strategies. Notes in Computer Science 2034, p. 49-62. In Proc. 5th International Symposium on AutoSpringer, 2001. mated Technology for Verification and Analysis
[7] E. Asarin and O. Maler. As soon as possi- (ATVA'07), Lecture Notes in Computer Science ble: Time optimal control for timed automata. 4762, p. 192-206. Springer, 2007. In Proc. 2nd International Workshop on Hybrid [20] F. Cassez et al. Automatic synthesis of robust Systems: Computation and Control (HSCC'99), and optimal controllers - an industrial case Lecture Notes in Computer Science 1569, p. 19- study. In Proc. 12th International Workshop 30. Springer, 1999. on Hybrid Systems: Computation and Control
[8] E. Asarin et al. Controller synthesis for timed (HSCC'09), Lecture Notes in Computer Science automata. In Proc. IFAC Symposium on System 5469. Springer, 2009. Structure and Control, p. 469-474. Elsevier Sci- [21] A. Chakrabarti et al. Resource interfaces. In ence, 1998. Proc. 3rd International Workshop on Embedded
[10] G. Behrmann et al. Minimum-cost reachability chapter 4, p. 93-119. CRC Press, 2009. for priced timed automata. In Proc. 4th Interna- [23] H. Dierks. PLC-automata: a new class of impletional Workshop on Hybrid Systems: Computa- mentable real-time automata. Theoretical Comtion and Control (HSCC'01), Lecture Notes in puter Science, 253(1):61-93, 2001. Computer Science 2034, p. 147-161. Springer, [24] H. Dierks. Finding optimal plans for domains 2001. with continuous effects with UPPAAL CORA.
[11] B. Bérard and C. Dufourd. Timed automata and In Proc. ICAPS'05 Workshop on Verification additive clock constraints. Information Process- and Validation of Model-Based Planning and ing Letters, 75(1-2):1-7, 2000. Scheduling Systems, 2005.
[12] P. Bouyer. Forward analysis of updatable timed [25] U. Fahrenberg and K. G. Larsen. Discountautomata. Formal Methods in System Design, optimal infinite runs in priced timed automata. 24(3):281-320, 2004. Electronic Notes in Theoretical Computer Sci-
[13] P. Bouyer, E. Brinksma, and K. G. Larsen. Op- ence, 239:179-191, 2009. timal infinite scheduling for multi-priced timed [26] E. Fersman et al. Schedulability analysis of automata. Formal Methods in System Design, fixed-priority systems using timed automata. 32(1):2-23, 2008. Theoretical Computer Science, 354(2):301-317,
[14] P. Bouyer et al. Infinite runs in weighted timed 2006.
[27] K. Havelund et al. Formal modeling and analysis of an audio/video protocol: An industrial case study using UPPAAL. In Proc. 18th IEEE Real-Time Systems Symposium (RTSS'97), p. 2- 13. IEEE Computer Society Press, 1997.
[28] M. Hendriks, B. van den Nieuwelaar, and F. W. Vaandrager. Model checker aided design of a controller for a wafer scanner. STTT, 8(6):633- 647, 2006.
[29] Th. A. Henzinger et al. What's decidable about hybrid automata? Journal of Computer and System Sciences, 57(1):94-124, 1998.
[30] Th. A. Henzinger et al. Symbolic modelchecking for real-time systems. Information and Computation, 111(2):193-244, 1994.
[32] J. J. Jessen et al. Guided controller synthesis for climate controller using UPPAAL-TIGA. In Proc. 5th International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS'07), Lecture Notes in Computer Science 4763, p. 227-240. Springer, 2007.
[33] Y. Kesten et al. Decidable integration graphs. Information and Computation, 150(2):209-243, 1999.
[34] K. G. Larsen et al. As cheap as possible: Efficient cost-optimal reachability for priced timed automata. In Proc. 13th International Conference on Computer Aided Verification (CAV'01), Lecture Notes in Computer Science 2102, p. 493-505. Springer, 2001.
[35] K. G. Larsen and J. I. Rasmussen. Optimal reachability for multi-priced timed automata. Theoretical Computer Science, 390(2-3):197-213, 2008.
[37] M. Schuts et al. Modelling clock synchronization in the Chess gMAC WSN protocol. CoRR, abs/0912.1901, 2009.
[38] S. Tripakis and K. Altisen. Controller synthesis for discrete and dense-time systems. In Proc. World Congress on Formal Methods in the Development of Computing Systems (FM'99), Lecture Notes in Computer Science 1708, p. 233- 252. Springer, 1999.
[39] S. Tripakis and S. Yovine. Timing analysis and code generation of vehicle control software using TAXYS. Electronic Notes in Theoretical Computer Science, 55(2), 2001.
[40] L. Waszniowski and Z. Hanzálek. Formal verification of multitasking applications based on timed automata model. Real-Time Systems, 38(1):39-65, 2008.