Abstract
Weighted automata are non-deterministic automata where the transitions are equipped with weights. They can model quantitative aspects of systems like costs or energy consumption. The value of a run can be computed, for example, as the maximum, limit average, or discounted sum of transition weights. In multi-weighted automata, transitions carry several weights and can model, for example, the ratio between rewards and costs, or the efficiency of use of a primary resource under some upper bound constraint on a secondary resource. Here, we introduce a general model for multi-weighted automata as well as a multi-weighted MSO logic. In our main results, we show that this multi-weighted MSO logic and multi-weighted automata are expressively equivalent both for finite and infinite words. The translation process is effective, leading to decidability results for our multi-weighted MSO logic.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
References
Bauer, S., Juhl, L., Larsen, K., Legay, A., Srba, J.: A logic for accumulated-weight reasoning on multiweighted modal automata. In: Proc. of the 6th Int. Symp. on Theoret. Aspects of Software Engineering (TASE 2012), pp. 77–84. IEEE Computer Society Press (2012)
Berstel, J., Reutenauer, C.: Rational Series and Their Languages. EATCS Monographs on Theoretical Computer Science, vol. 12. Springer (1988)
Bloem, R., Greimel, K., Henzinger, T.A., Jobstmann, B.: Synthesizing robust systems. In: Proc. of 9th Int. Conf. on Formal Methods in Computer-Aided Design (FMCAD 2009), pp. 85–92. IEEE (2009)
Bollig, B., Gastin, P.: Weighted versus probabilistic logics. In: Diekert, V., Nowotka, D. (eds.) DLT 2009. LNCS, vol. 5583, pp. 18–38. Springer, Heidelberg (2009)
Bouyer, P., Brinksma, E., Larsen, K.G.: Optimal infinite scheduling for multi-priced timed automata. Formal Methods in System Design 32(1), 3–23 (2008)
Bouyer, P., Brinksma, E., Larsen, K.G.: Staying alive as cheaply as possible. In: Alur, R., Pappas, G.J. (eds.) HSCC 2004. LNCS, vol. 2993, pp. 203–218. Springer, Heidelberg (2004)
Büchi, J.R.: Weak second-order arithmetic and finite automata. Z. Math. Logik und Grundl. Math. 6, 66–92 (1960)
Chatterjee, K., Doyen, L., Henzinger, T.A.: Quantitative languages. In: Kaminski, M., Martini, S. (eds.) CSL 2008. LNCS, vol. 5213, pp. 385–400. Springer, Heidelberg (2008)
Chatterjee, K., Doyen, L., Henzinger, T.A.: Expressiveness and closure properties for quantitative languages. Logical Methods in Comp. Sci. 6(3) (2010)
Droste, M., Gastin, P.: Weighted automata and weighted logics. In: Droste et.al.: [11], ch. 5
Droste, M., Kuich, W., Vogler, H. (eds.): Handbook of Weighted Automata. EATCS Monographs on Theoretical Computer Science. Springer (2009)
Droste, M., Gastin, P.: Weighted automata and weighted logics. Theoret. Comp. Sci. 380(1-2), 69–86 (2007)
Droste, M., Meinecke, I.: Weighted automata and regular expressions over valuation monoids. Int. J. Found. Comput. Sci. 22(8), 1829–1844 (2011)
Droste, M., Meinecke, I.: Weighted automata and weighted MSO logics for average and long-time behaviors. Inf. Comput. 221, 44–59 (2012)
Elgot, C.C.: Decision problems of finite automata design and related arithmetics. Trans. Amer. Math. Soc. 98, 21–51 (1961)
Fahrenberg, U., Juhl, L., Larsen, K.G., Srba, J.: Energy games in multiweighted automata. In: Cerone, A., Pihlajasaari, P. (eds.) ICTAC 2011. LNCS, vol. 6916, pp. 95–115. Springer, Heidelberg (2011)
Fahrenberg, U., Larsen, K.G., Thrane, C.R.: Model-based verification and analysis for real-time systems. In: Software and Systems Safety - Specification and Verification, NATO Science for Peace and Security Series - D: Information and Communication Security, vol. 30, pp. 231–259. IOS Press (2011)
Filiot, E., Gentilini, R., Raskin, J.F.: Quantitative languages defined by functional automata. In: Koutny, M., Ulidowski, I. (eds.) CONCUR 2012. LNCS, vol. 7454, pp. 132–146. Springer, Heidelberg (2012)
Kuich, W., Salomaa, A.: Semirings, Automata and Languages. EATCS Monographs on Theoretical Computer Science, vol. 5. Springer (1986)
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)
Quaas, K.: MSO logics for weighted timed automata. Form. Methods Syst. Des. 38(3), 193–222 (2011)
Salomaa, A., Soittola, M.: Automata-Theoretic Aspects of Formal Power Series. Texts and Monographs in Computer Science. Springer (1978)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Droste, M., Perevoshchikov, V. (2013). Multi-weighted Automata and MSO Logic. In: Bulatov, A.A., Shur, A.M. (eds) Computer Science – Theory and Applications. CSR 2013. Lecture Notes in Computer Science, vol 7913. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-38536-0_36
Download citation
DOI: https://doi.org/10.1007/978-3-642-38536-0_36
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-38535-3
Online ISBN: 978-3-642-38536-0
eBook Packages: Computer ScienceComputer Science (R0)