Abstract
A weighted automaton is functional if any two accepting runs on the same finite word have the same value. In this paper, we investigate functional weighted automata for four different measures: the sum, the mean, the discounted sum of weights along edges and the ratio between rewards and costs. On the positive side, we show that functionality is decidable for the four measures. Furthermore, the existential and universal threshold problems, the language inclusion problem and the equivalence problem are all decidable when the weighted automata are functional. On the negative side, we also study the quantitative extension of the realizability problem and show that it is undecidable for sum, mean and ratio. We finally show how to decide whether the language associated with a given functional automaton can be defined with a deterministic one, for sum, mean and discounted sum. The results on functionality and determinizability are expressed for the more general class of functional weighted automata over groups. This allows one to formulate within the same framework new results related to discounted sum automata and known results on sum and mean automata. Ratio automata do not fit within this general scheme and specific techniques are required to decide functionality.
This work was partially supported by ERC Starting Grant (279499: inVEST). We are very grateful to some anonymous reviewer for suggesting us the encoding of discounted-sum automata as a automata over a left semiring.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Almagor, S., Boker, U., Kupferman, O.: What’s Decidable about Weighted Automata? In: Bultan, T., Hsiung, P.-A. (eds.) ATVA 2011. LNCS, vol. 6996, pp. 482–491. Springer, Heidelberg (2011)
Aminof, B., Kupferman, O., Lampert, R.: Rigorous approximated determinization of weighted automata. In: LICS, pp. 345–354 (2011)
Andersson, D.: An improved algorithm for discounted payoff games. In: ESSLLI Student Session, pp. 91–98 (2006)
Beal, M.-P., Carton, O., Prieur, C., Sakarovitch, J.: Squaring transducers: An efficient procedure for deciding functionality and sequentiality. TCS 292 (2003)
Berstel, J., Reutenauer, C.: Rational Series and Their Languages. EATCS Monographs on TCS, vol. 12. Springer (1988)
Blattner, M., Head, T.: Single-valued a-transducers. JCSS 15(3), 310–327 (1977)
Bloem, R., Greimel, K., Henzinger, T.A., Jobstmann, B.: Synthesizing robust systems. In: FMCAD, pp. 85–92. IEEE (2009)
Boker, U., Chatterjee, K., Henzinger, T.A., Kupferman, O.: Temporal specifications with accumulative values. In: LICS, pp. 43–52 (2011)
Boker, U., Henzinger, T.A.: Determinizing discounted-sum automata. In: CSL, pp. 82–96 (2011)
Chatterjee, K., Doyen, L., Henzinger, T.A.: Quantitative languages. ACM Trans. Comput. Log 11(4) (2010)
Choffrut, C.: Une caractérisation des fonctions séquentielles et des fonctions sous-séquentielles en tant que relations rationnelles. TCS 5(3), 325–337 (1977)
de Alfaro, L., Faella, M., Henzinger, T.A., Majumdar, R., Stoelinga, M.: Model checking discounted temporal properties. TCS 345(1), 139–170 (2005)
Droste, M., Kuich, W., Vogler, H.: Handbook of Weighted Automata. Springer (2009)
Droste, M., Rahonis, G.: Weighted automata and weighted logics with discounting. Theor. Comput. Sci. 410(37), 3481–3494 (2009) ISSN: 0304-3975
Grunewald, F., Segal, D.: On the integer solutions of quadratic equations. Journal für die reine und angewandte Mathematik 569, 13–45 (2004)
Kirsten, D.: A burnside approach to the termination of mohri’s algorithm for polynomially ambiguous min-plus-automata. ITA 42(3), 553–581 (2008)
Kirsten, D., Mäurer, I.: On the determinization of weighted automata. Journal of Automata, Languages and Combinatorics 10(2/3), 287–312 (2005)
Klimann, I., Lombardy, S., Mairesse, J., Prieur, C.: Deciding unambiguity and sequentiality from a finitely ambiguous max-plus automaton. TCS 327(3), 349–373 (2004)
Krob, D.: The equality problem for rational series with multiplicities in the tropical semiring is undecidable. Journal of Algebra and Computation 4(3), 405–425 (1994)
Krob, D., Litp, P.: Some consequences of a fatou property of the tropical semiring. J. Pure Appl. Algebra 93, 231–249 (1994)
Lombardy, S., Mairesse, J.: Series which are both max-plus and min-plus rational are unambiguous. ITA 40(1), 1–14 (2006)
Minsky, M.L.: Computation: Finite and Infinite Machines. Prentice-Hall (1967)
Pnueli, A., Rosner, R.: On the synthesis of a reactive module. In: ACM Symposium on Principles of Programming Languages (POPL). ACM (1989)
Schützenberger, M.P.: Sur Les Relations Rationnelles. In: Brakhage, H. (ed.) GI-Fachtagung 1975. LNCS, vol. 33, pp. 209–213. Springer, Heidelberg (1975)
Thomas, W.: Church’s Problem and a Tour through Automata Theory. In: Avron, A., Dershowitz, N., Rabinovich, A. (eds.) Trakhtenbrot/Festschrift. LNCS, vol. 4800, pp. 635–655. Springer, Heidelberg (2008)
Weber, A., Klemm, R.: Economy of description for single-valued transducers. Inf. Comput. 118(2), 327–340 (1995)
Karianto, W., Krieg, A., Thomas, W.: On Intersection Problems for Polynomially Generated Sets. In: Bugliesi, M., Preneel, B., Sassone, V., Wegener, I. (eds.) ICALP 2006. LNCS, vol. 4052, pp. 516–527. Springer, Heidelberg (2006)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Filiot, E., Gentilini, R., Raskin, JF. (2012). Quantitative Languages Defined by Functional Automata. In: Koutny, M., Ulidowski, I. (eds) CONCUR 2012 – Concurrency Theory. CONCUR 2012. Lecture Notes in Computer Science, vol 7454. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-32940-1_11
Download citation
DOI: https://doi.org/10.1007/978-3-642-32940-1_11
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-32939-5
Online ISBN: 978-3-642-32940-1
eBook Packages: Computer ScienceComputer Science (R0)