Communications - September 2011

Conclusion

Timed automata and their priced and game extensions provide a uniform and expressive formalism for dynamic resource allocation problems with hard real-time constraints, that is, timing constraints that must be satisfied under all circumstances. This is in contrast to soft real-time constraints, which only need to be met with a certain probability, .999 say, and which require stochastic modeling formalisms such as discrete-time or contin-uous-time Markov chains, queueing models. While hard real-time focuses on worst-case analysis, soft real-time addresses more refined properties such as average-case performance.

However, within the setting of hard real-time, timed automata and their extensions allow for analysis of a wide collection of performance and optimization problems, with results competitive with respect to more traditional approaches such as mixed-integer linear programming or others.

Particularly challenging problems remaining to be settled include decidability of synthesis for priced timed games under partial observability, as well as a range of resource management problems in the setting of priced timed automata and games with both consumption and regaining of resources.

acknowledgments

The authors are partly supported by the European project Quasimodo (FP7-ICT-STREP-214755). The French authors are supported by project DOTS (ANR-06-SETI-003). The Danish authors are supported by the Danish Center of Excellence MT-LAB.

References

1. abdeddaïm, y., asarin, e., Maler, o. scheduling with timed automata. Theor. Comput. Sci. 354, 2 (2006), 272–300.

2. altisen, K. et al. a framework for scheduler synthesis. in IEEE Real- Time Systems Symposium, 1999, 154–163.

3. alur, r., bernadsky, M., Madhusudan, P. optimal reachability in weighted timed games. in Proceedings of the 31st International Colloquium on Automata, Languages and Programming (ICALP ’04), lecture notes in Computer science 3142, springer, 2004, 122–133.

4. alur, r., Courcoubetis, C., Dill, D.l. Model-checking for real-time systems. in Proceedings of the 5th Annual Symposium on Logic in Computer Science (LICS ’ 90), ieee Computer society Press, 1990, 414–425.

5. alur, r., Dill, D.l. automata for modeling
real-time systems. in Proceedings of the
17th International Colloquium on Automata,
Languages and Programming (ICALP ’ 90),
lecture notes in Computer science 443,
springer, 1990, 322–335.