Abstract
During the last years, weighted timed automata (WTA) have received much interest in the real-time community. Weighted timed automata form an extension of timed automata and allow us to assign weights (costs) to both locations and edges. This model, introduced by Alur et al. (2001) and Behrmann et al. (2001), permits the treatment of continuous consumption of resources and has led to much research on scheduling problems, optimal reachability and model checking. Also, several authors have derived Kleene-type characterizations of (unweighted) timed automata and their accepted timed languages. The goal of this paper is to provide a characterization of the possible behaviours of WTA by rational power series. We define WTA with weights taken in an arbitrary semiring, resulting in a model that subsumes several WTA concepts of the literature. For our main result, we combine the methods of Schützenberger, a recent approach for a Kleene-type theorem for unweighted timed automata by Bouyer and Petit as well as new techniques. Our main result also implies Kleene-type theorems for several subclasses of WTA investigated before, e.g., for weighted finite automata, timed automata and timed automata with stopwatch observers.
Chapter PDF
Similar content being viewed by others
References
Alur, R., Bernadsky, M., Madhusudan, P.: Optimal reachability in weighted timed games. In: Díaz, J., Karhumäki, J., Lepistö, A., Sannella, D. (eds.) ICALP 2004. LNCS, vol. 3142, pp. 122–133. Springer, Heidelberg (2004)
Alur, R., Dill, D.L.: A theory of timed automata. Theoretical Computer Science 126(2), 183–235 (1994)
Alur, R., La Torre, S., Pappas, G.J.: Optimal paths in weighted timed automata. In: Di Benedetto, M.D., Sangiovanni-Vincentelli, A.L. (eds.) HSCC 2001. LNCS, vol. 2034, pp. 49–62. Springer, Heidelberg (2001)
Alur, R., Madhusudan, P.: Decision problems for timed automata: A survey. In: Bernardo, M., Corradini, F. (eds.) SFM-RT 2004. LNCS, vol. 3185, pp. 1–24. Springer, Heidelberg (2004)
Asarin, E., Caspi, P., Maler, O.: A Kleene theorem for timed automata. In: LICS 1997, pp. 160–171. IEEE Computer Society Press, Los Alamitos (1997)
Asarin, E., Caspi, P., Maler, O.: Timed regular expressions. Journal of the ACM 49(2), 172–206 (2002)
Asarin, E., Dima, C.: Balanced timed regular expressions. In: Vogler, W., Larsen, K.G. (eds.) MTCS. ENTCS, vol. 68, pp. 16–33. Elsevier, Amsterdam (2002)
Behrmann, G., Fehnker, A., Hune, T., Larsen, K., Pettersson, P., Romijn, J., Vaandrager, F.: Minimum-cost reachability for priced timed automata. In: Di Benedetto, M.D., Sangiovanni-Vincentelli, A.L. (eds.) HSCC 2001. LNCS, vol. 2034, pp. 147–161. Springer, Heidelberg (2001)
Di Benedetto, M.D., Sangiovanni-Vincentelli, A.L. (eds.): HSCC 2001. LNCS, vol. 2034. Springer, Heidelberg (2001)
Berstel, J., Reutenauer, C.: Rational Series and their Languages. Springer, New York, USA (1988)
Bouyer, P., Brihaye, T., Bruyère, V., Raskin, J.-F.: On the optimal reachability problem on weighted timed automata. Formal Methods in System Design 31(2), 135–175 (2007)
Bouyer, P., Brihaye, T., Markey, N.: Improved undecidability results on weighted timed automata. Inf. Process. Lett. 98(5), 188–194 (2006)
Bouyer, P., Brinksma, E., Larsen, K.G.: Optimal infinite scheduling for multi-priced timed automata. Formal Methods in System Design (to appear, 2007)
Bouyer, P., Larsen, K.G., Markey, N.: Model-checking one-clock priced timed automata. In: Seidl, H. (ed.) FOSSACS 2007. LNCS, vol. 4423, pp. 108–122. Springer, Heidelberg (2007)
Bouyer, P., Petit, A.: Decomposition and composition of timed automata. In: Wiedermann, J., Van Emde Boas, P., Nielsen, M. (eds.) ICALP 1999. LNCS, vol. 1644, pp. 210–219. Springer, Heidelberg (1999)
Bouyer, P., Petit, A.: A Kleene/Büchi-like theorem for clock languages. J. Autom. Lang. Comb. 7(2), 167–186 (2001)
Bozga, M., Daws, C., Maler, O., Olivero, A., Tripakis, S., Yovine, S.: Kronos: A model-checking tool for real-time systems. In: Hu, A.J., Vardi, M.Y. (eds.) CAV 1998. LNCS, vol. 1427, pp. 546–550. Springer, Heidelberg (1998)
Brihaye, T., Bruyère, V., Raskin, J.-F.: Model-checking weighted timed automata. In: Lakhnech, Y., Yovine, S. (eds.) FORMATS 2004 and FTRTFT 2004. LNCS, vol. 3253, pp. 277–292. Springer, Heidelberg (2004)
Droste, M., Gastin, P.: Weighted automata and weighted logics. Theor. Comput. Sci. 380(1–2), 69–86 (2007)
Fox, M., Long, D.: Modelling mixed discrete-continuous domains for planning. Journal of AI Research 27, 235–297 (2006)
Henzinger, T.: The theory of hybrid automata. In: LICS 1996, pp. 278–292. IEEE Computer Society Press, Los Alamitos (1996)
Henzinger, T.A., Ho, P.-H., Wong-Toi, H.: HYTECH: A model checker for hybrid systems. International Journal on Software Tools for Technology Transfer 1(1–2), 110–122 (1997)
Kristoffersen, K., Larsen, K., Pettersson, P., Weise, C.: VHS Case Study 1 - Experimental Batch Plant using UPPAAL, BRICS, University of Aalborg, Denmark (May 1999)
Kuich, W., Salomaa, A.: Semirings, Automata, Languages. EATCS Monographs on Theoretical Computer Science, vol. 5. Springer, Berlin (1986)
Larsen, K.G., Pettersson, P., Yi, W.: UPPAAL in a nutshell. International Journal on Software Tools for Technology Transfer 1(1-2), 134–152 (1997)
Larsen, K.G., Rasmussen, J.I.: Optimal conditional reachability for multi-priced timed automata. In: Sassone, V. (ed.) FOSSACS 2005. LNCS, vol. 3441, pp. 234–249. Springer, Heidelberg (2005)
Niebert, P., Yovine, S.: Computing optimal operation schemes for chemical plants in multi-batch mode. In: Lynch, N.A., Krogh, B.H. (eds.) HSCC 2000. LNCS, vol. 1790, Springer, Heidelberg (2000)
Illum Rasmussen, J., Larsen, K.G., Subramani, K.: Resource-optimal scheduling using priced timed automata. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 220–235. Springer, Heidelberg (2004)
Salomaa, A., Soittola, M.: Automata-Theoretic Aspects of Formal Power Series. Springer, New York (1978)
Schützenberger, M.P.: On the definition of a family of automata. Information and Control 4, 245–270 (1961)
Wilke, T.: Specifying Timed State Sequences in Powerful Decidable Logics and Timed Automata. In: Langmaack, H., de Roever, W.-P., Vytopil, J. (eds.) FTRTFT 1994 and ProCoS 1994. LNCS, vol. 863, pp. 694–715. Springer, Heidelberg (1994)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Droste, M., Quaas, K. (2008). A Kleene-Schützenberger Theorem for Weighted Timed Automata. In: Amadio, R. (eds) Foundations of Software Science and Computational Structures. FoSSaCS 2008. Lecture Notes in Computer Science, vol 4962. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-78499-9_11
Download citation
DOI: https://doi.org/10.1007/978-3-540-78499-9_11
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-78497-5
Online ISBN: 978-3-540-78499-9
eBook Packages: Computer ScienceComputer Science (R0)