nach oben

Erschienen in:

2021 | OriginalPaper | Buchkapitel

Quantitative vs. Weighted Automata

verfasst von : Udi Boker

Erschienen in: Reachability Problems

Verlag: Springer International Publishing

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config

KI-gestützte Suche

Aus

Abstract

Weighted automata are widely researched, but with a variety of different semantics, which mostly fit into either the “quantitative view” or the “algebraic view”. We argue that the two views result with incomparable automata families, each providing a different conceptual generalization of Boolean automata and having different natural extensions.

We propose to term the former “quantitative automata” and the latter “weighted automata”.

In both views, transitions are labeled with weights and the value of a path of transitions is given by some value function on the traversed weights. However, the main conceptual difference is in the generalization of nondeterminism and its dual (universality, in alternating automata).

Quantitative automata keep the preference meaning of choice and obligation to nondeterminism and universality, interpreted as supremum and infimum, respectively, and accordingly restrict weights and value functions to the totally ordered domain of real numbers.

Weighted automata, on the other hand, generalize nondeterminism to an arbitrary commutative operation (of a semiring or valuation monoid), and generally have no interpretation of universality. The weights and value functions can be from arbitrary domains.

On several aspects the algebraic view generalizes the quantitative one, allowing for richer weight domains and interpretations of nondeterminism, whereas on different aspects the quantitative view is more general, having alternation, inherent compatibility with games and adequacy to approximations.

We argue that clarifying the conceptual difference between the two automata families can enlighten their possible future extensions.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Nächstes Kapitel Theorem Proving Using Clausal Resolution: From Past to Present

We define first an automaton without an acceptance-condition/value-function/semi-ring/valuation-monoid, but with initial state(s). Usually, the term ‘automaton’ refers to an entity with them, while ‘semiautomaton’ to an entity that also lacks initial state(s).

This extra flexibility of allowing for “parallel” transitions with different weights is often omitted, since it is redundant for some value functions while important for others.

Nondeterministic automata are also often defined with a single initial state.

An equivalent definition goes via trees instead of games.

There are value functions that are more naturally defined over sequences of tuples of real values (see Remark 1), for example lexicographic-mean-payoff [9] and discounted-summation with multiple discount factors [13].

Considering algorithmic aspects of quantitative automata, labels are usually rational numbers, concretely represented.

It is sometimes defined analogously with infimum instead of supremum. Considering alternating quantitative automata, infimum relates to universal transitions.

A function in this context is called in [23] a “quantitative language”.

Automata with multiple weights on transitions can be defined with respect to structure monoids [39].

In [38], the original definition of a valuation monoid has additional restrictions that are loosened in [48].

Semiring weighted automata are sometimes defined with an acceptance condition (e.g., [48]) and sometimes without it, while having instead labels on both transitions and states (e.g., [34]). However, considering infinite words or valuation monoids, weighted automata have an acceptance condition [38].

For finite words, the acceptance condition is a set \(F\subseteq Q\) of final states, and a run satisfies it if it ends in a final state. For infinite words there are many acceptance conditions, such as Büchi or Muller. (More details on the different acceptance conditions can be found, for example, in [12]).

A function in this context is often viewed as a formal power series.

The “weighted automata” in the title of [49] refer to a variant of \({\mathsf {Sum}}\) automata, defined over infinite words with an acceptance condition on finite prefixes.

As ratio does not satisfy the triangle inequality, it is formally not a distance function, and one may speak instead of \(d(x,y) = |\log x - \log y|\).

Almagor, S., Boker, U., Kupferman, O.: Discounting in LTL. In: Ábrahám, E., Havelund, K. (eds.) TACAS 2014. LNCS, vol. 8413, pp. 424–439. Springer, Heidelberg (2014). https://doi.org/10.1007/978-3-642-54862-8_37CrossRef

Almagor, S., Boker, U., Kupferman, O.: Formalizing and reasoning about quality. J. ACM 63(3), 24:1–24:56 (2016)

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). https://doi.org/10.1007/978-3-642-24372-1_37CrossRef

Almagor, S., Kupferman, O.: Max and sum semantics for alternating weighted automata. In: Bultan, T., Hsiung, P.-A. (eds.) ATVA 2011. LNCS, vol. 6996, pp. 13–27. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-24372-1_2CrossRefMATH

Almagor, S., Kupferman, O., Ringert, J.O., Velner, Y.: Quantitative assume guarantee synthesis. In: Majumdar, R., Kunčak, V. (eds.) CAV 2017. LNCS, vol. 10427, pp. 353–374. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-63390-9_19CrossRef

Aminof, B., Kupferman, O., Lampert, R.: Reasoning about online algorithms with weighted automata. ACM Trans. Algorithms 6(2), 28:1–28:36 (2010)

Aminof, B., Kupferman, O., Lampert, R.: Rigorous approximated determinization of weighted automata. Theor. Comput. Sci. 480, 104–117 (2013)MathSciNetCrossRef

Babari, P.: Quantitative Automata and Logic for Pictures and Data Words. Ph.D. thesis, Leipzig University (2017)

Bloem, R., Chatterjee, K., Henzinger, T.A., Jobstmann, B.: Better quality in synthesis through quantitative objectives. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 140–156. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-02658-4_14CrossRef

10.

Boker, U., Chatterjee, K., Henzinger, T.A., Kupferman, O.: Temporal specifications with accumulative values. ACM Trans. Comput. Log. 15(4), 27:1–27:25 (2014)

11.

Boker, U., Henzinger, T.A.: Exact and approximate determinization of discounted-sum automata. Log. Methods Comput. Sci. 10(1), 1–33 (2014)

12.

Boker, U.: Why these automata types? In: Proceedings of the LPAR, pp. 143–163 (2018)

13.

Boker, U., Hefetz, G.: Discounted-sum automata with multiple discount factors. In: Proceedings of the CSL. LIPIcs, vol. 183, pp. 12:1–12:23 (2021)

14.

Boker, U., Henzinger, T.A.: Approximate determinization of quantitative automata. In: Proceedings of the FSTTCS. LIPIcs, vol. 18, pp. 362–373 (2012)

15.

Boker, U., Lehtinen, K.: Good for games automata: from nondeterminism to alternation. In: Fokkink, W.J., van Glabbeek, R. (eds.) Proceedings of the CONCUR. LIPIcs, vol. 140, pp. 19:1–19:16 (2019)

16.

Boker, U., Lehtinen, K.: History determinism vs. good for gameness in quantitative automata. In: Proceedings of FSTTCS. pp. 35:1–35:20 (2021)

17.

Bouyer, P., Markey, N., Matteplackel, R.: Averaging in LTL. In: Proceedings of the CONCUR, pp. 266–280 (2014)

18.

Brenguier, R., et al.: Non-zero sum games for reactive synthesis. In: Dediu, A.-H., Janoušek, J., Martín-Vide, C., Truthe, B. (eds.) LATA 2016. LNCS, vol. 9618, pp. 3–23. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-30000-9_1CrossRef

19.

Büchi, J.R.: On a decision method in restricted second order arithmetic. In: Proceedings of the International Congress on Logic, Method, and Philosophy of Science. 1960, pp. 1–12. Stanford University Press (1962)

20.

Buchsbaum, A.L., Giancarlo, R., Westbrook, J.: An approximate determinization algorithm for weighted finite-state automata. Algorithmica 30(4), 503–526 (2001)MathSciNetCrossRef

21.

Chandra, A.K., Kozen, D.C., Stockmeyer, L.J.: Alternation. J. ACM 28(1), 114–133 (1981)MathSciNetCrossRef

22.

Chandra, A.K., Stockmeyer, L.J.: Alternation. In: Proceedings of FOCS, pp. 98–108 (1976)

23.

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). https://doi.org/10.1007/978-3-540-87531-4_28CrossRef

24.

Chatterjee, K., Doyen, L., Henzinger, T.A.: Alternating weighted automata. In: Proceedings of FCT, pp. 3–13 (2009)

25.

Chatterjee, K., Doyen, L., Henzinger, T.A.: Quantitative languages. ACM Trans. Comput. Log. 11(4), 23:1–23:38 (2010)

26.

Chatterjee, K., Henzinger, T.A., Jobstmann, B., Singh, R.: QUASY: quantitative synthesis tool. In: Abdulla, P.A., Leino, K.R.M. (eds.) TACAS 2011. LNCS, vol. 6605, pp. 267–271. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-19835-9_24CrossRef

27.

Chatterjee, K., Henzinger, T.A., Otop, J.: Nested weighted automata. ACM Trans. Comput. Log. 18(4), 31:1–31:44 (2017)

28.

Colcombet, T.: The theory of stabilisation monoids and regular cost functions, pp. 139–150 (2009)

29.

Colcombet, T., Fijalkow, N.: Universal graphs and good for games automata: new tools for infinite duration games. In: Bojańczyk, M., Simpson, A. (eds.) FoSSaCS 2019. LNCS, vol. 11425, pp. 1–26. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-17127-8_1CrossRefMATH

30.

Culik, K., Karhumaki, J.: Finite automata computing real functions. SIAM J. Comput. 23(4), 789–814 (1994)MathSciNetCrossRef

31.

Dickhöfer, M., Wilke, T.: Timed alternating tree automata: the automata-theoretic solution to the TCTL model checking problem. In: Wiedermann, J., van Emde Boas, P., Nielsen, M. (eds.) ICALP 1999. LNCS, vol. 1644, pp. 281–290. Springer, Heidelberg (1999). https://doi.org/10.1007/3-540-48523-6_25CrossRefMATH

32.

Diekert, V., Gastin, P.: First-order definable languages. In: Flum, J., Grädel, E., Wilke, T. (eds.) Logic and Automata: History and Perspectives [in Honor of Wolfgang Thomas]. Texts in Logic and Games, vol. 2, pp. 261–306. Amsterdam University Press (2008)

33.

Doyen, L.: Games and automata: From Boolean to quantitative verification. Habilitation Thesis, École Normale Supérieure de Cachan (2011)

34.

Droste, M., Gastin, P.: Weighted automata and weighted logics. Theor. Comput. Sci. 380(1–2), 69–86 (2007)MathSciNetCrossRef

35.

Droste, M., Gastin, P.: Aperiodic weighted automata and weighted first-order logic. In: Proceedings of the MFCS. LIPIcs, vol. 138, pp. 76:1–76:15 (2019)

36.

Droste, M., Kuske, D.: Skew and infinitary formal power series. In: Baeten, J.C.M., Lenstra, J.K., Parrow, J., Woeginger, G.J. (eds.) ICALP 2003. LNCS, vol. 2719, pp. 426–438. Springer, Heidelberg (2003). https://doi.org/10.1007/3-540-45061-0_35CrossRefMATH

37.

Droste, M., Meinecke, I.: Describing average- and longtime-behavior by weighted MSO logics. In: Proceedings of the MFCS, pp. 537–548 (2010)

38.

Droste, M., Meinecke, I.: Weighted automata and weighted MSO logics for average and long-time behaviors. Inf. Comput. 220–221, 44–59 (2012)MathSciNetCrossRef

39.

Droste, M., Perevoshchikov, V.: Multi-weighted automata and MSO logic. In: Computer Science - Theory and Applications, pp. 418–430 (2013)

40.

Droste, M., Rahonis, G.: Weighted automata and weighted logics on infinite words. In: Ibarra, O.H., Dang, Z. (eds.) DLT 2006. LNCS, vol. 4036, pp. 49–58. Springer, Heidelberg (2006). https://doi.org/10.1007/11779148_6CrossRef

41.

Eilenberg, S.: Automata, Languages, and Machines. Academic Press Inc., USA (1974)MATH

42.

Elgot, C.: Decision problems of finite-automata design and related arithmetics. Trans. Am. Math. Soc. 98, 21–51 (1961)MathSciNetCrossRef

43.

Faella, M., Legay, A., Stoelinga, M.: Model checking quantitative linear time logic. Electron. Notes Theor. Comput. Sci. 220(3), 61–77 (2008)CrossRef

44.

Filiot, E., Gentilini, R., Raskin, J.: Quantitative languages defined by functional automata. Log. Methods Comput. Sci. 11(3), 1–32 (2015)

45.

Filiot, E., Jecker, I., Lhote, N., Pérez, G.A., Raskin, J.: On delay and regret determinization of max-plus automata. In: LICS, pp. 1–12 (2017)

46.

Filiot, E., Löding, C., Winter, S.: Synthesis from weighted specifications with partial domains over finite words. In: Saxena, N., Simon, S. (eds.) FSTTCS. LIPIcs, vol. 182, pp. 46:1–46:16. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2020)

47.

Gabbay, D.M., Pnueli, A., Shelah, S., Stavi, J.: On the temporal analysis of fairness. In: Proceedings of the POPL, pp. 163–173 (1980)

48.

Gastin, P., Monmege, B.: A unifying survey on weighted logics and weighted automata - core weighted logic: minimal and versatile specification of quantitative properties. Soft. Comput. 22(4), 1047–1065 (2018)CrossRef

49.

Halava, V., Harju, T., Niskanen, R., Potapov, I.: Weighted automata on infinite words in the context of attacker-defender games. In: Beckmann, A., Mitrana, V., Soskova, M. (eds.) CiE 2015. LNCS, vol. 9136, pp. 206–215. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-20028-6_21CrossRef

50.

Henzinger, T., Piterman, N.: Solving games without determinization, pp. 395–410 (2006)

51.

Hunter, P., Pérez, G.A., Raskin, J.-F.: Reactive synthesis without regret. Acta Inform. 54(1), 3–39 (2016). https://doi.org/10.1007/s00236-016-0268-zMathSciNetCrossRefMATH

52.

Kamp, J.: Tense Logic and the Theory of Order. Ph.D. thesis, UCLA (1968)

53.

Kostolányi, P., Misún, F.: Alternating weighted automata over commutative semirings. Theor. Comput. Sci. 740, 1–27 (2018)MathSciNetCrossRef

54.

Kupferman, O.: Automata theory and model checking. In: Handbook of Model Checking, pp. 107–151. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-10575-8_4CrossRefMATH

55.

Ladner, R., Lipton, R., Stockmeyer, L.: Alternating pushdown and stack automata. SIAM J. Comput. 13(1), 135–155 (1984)MathSciNetCrossRef

56.

Ladner, R.E.: Application of model theoretic games to discrete linear orders and finite automata. Inf. Control 33(4), 281–303 (1977)MathSciNetCrossRef

57.

Lindsay, P.A.: On alternating \(\omega \)-automata. Theoret. Comput. Sci. 43, 107–116 (1988)

58.

Loding, C., Thomas, W.: Alternating automata and logics over infinite words. In: van Leeuwen, J., Watanabe, O., Hagiya, M., Mosses, P.D., Ito, T. (eds.) TCS 2000. LNCS, vol. 1872, pp. 521–535. Springer, Heidelberg (2000). https://doi.org/10.1007/3-540-44929-9_36CrossRef

59.

M. Droste, W.K., Vogler, H.: Handbook of Weighted Automata, 1st edn. Springer Publishing Company, Incorporated, Heidelberg (2009)

60.

Mandrali, E.: Weighted LTL with discounting. In: Moreira, N., Reis, R. (eds.) CIAA 2012. LNCS, vol. 7381, pp. 353–360. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-31606-7_32CrossRef

61.

McNaughton, R., Papert, S.: Counter-free Automata. M.I.T Press, Cambridge (1971)

62.

Muller, D., Schupp, P.: Alternating automata on infinite trees. In: Automata on Infinite Words. LNCS, vol. 192, pp. 100–107 (1985)

63.

Perrin, D., Pin, J.: First-order logic and star-free sets. J. Comput. Syst. Sci. 32(3), 393–406 (1986)MathSciNetCrossRef

64.

Rabin, M.O.: Probabilistic automata. Inf. Control 6(3), 230–245 (1963)MathSciNetCrossRef

65.

Rabin, M.O., Scott, D.: Finite automata and their decision problems. IBM J. Res. Dev. 3(2), 114–125 (1959)MathSciNetCrossRef

66.

Salomaa, A., Soittola, M.: Automata-Theoretic Aspects of Formal Power Series. Texts and Monographs in Computer Science, Springer, Heidelberg (1978)

67.

Schützenberger, M.P.: On the definition of a family of automata. Inf. Control 4(2), 245–270 (1961)MathSciNetCrossRef

68.

Schützenberger, M.P.: On finite monoids having only trivial subgroups. Inf. Control 8(2), 190–194 (1965)MathSciNetCrossRef

69.

Thomas, W.: Star-free regular sets of omega-sequences. Inf. Control 42(2), 148–156 (1979)CrossRef

70.

Thomas, W.: A combinatorial approach to the theory of omega-automata. Inf. Control 48(3), 261–283 (1981)CrossRef

71.

Trakhtenbrot, B.A.: Finite automata and logic of monadic predicates. Doklady Akademii Nauk SSSR (1961). In Russian

72.

Vardi, M.Y.: Alternating automata and program verification. In: van Leeuwen, J. (ed.) Computer Science Today. LNCS, vol. 1000, pp. 471–485. Springer, Heidelberg (1995). https://doi.org/10.1007/BFb0015261CrossRef

73.

Vardi, M.: Verification of concurrent programs: the automata-theoretic framework, pp. 167–176 (1987)

74.

Wilke, T.: Alternating tree automata, parity games, and modal \(\mu \)-calculus. Bull. Belgian Math. Soc. Simon Stevin 8(2), 359 (2001)MathSciNetCrossRef

Titel: Quantitative vs. Weighted Automata
verfasst von: Udi Boker
Verlag: Springer International Publishing
Buch: Reachability Problems
Print ISBN: 978-3-030-89715-4

Electronic ISBN: 978-3-030-89716-1

Copyright-Jahr: 2021
DOI: https://doi.org/10.1007/978-3-030-89716-1_1

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Premium Partner