Skip to main content
Erschienen in: Soft Computing 4/2018

29.12.2015 | Focus

A unifying survey on weighted logics and weighted automata

Core weighted logic: minimal and versatile specification of quantitative properties

verfasst von: Paul Gastin, Benjamin Monmege

Erschienen in: Soft Computing | Ausgabe 4/2018

Einloggen

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

search-config
loading …

Abstract

Logical formalisms equivalent to weighted automata have been the topic of numerous research papers in the recent years. It started with the seminal result by Droste and Gastin on weighted logics over semirings for words. It has been extended in two dimensions by many authors. First, the weight domain has been extended to valuation monoids, valuation structures, etc. to capture more quantitative properties. Along another dimension, different structures such as ranked or unranked trees, nested words, Mazurkiewicz traces, etc. have been considered. The long and involved proofs of equivalences in all these papers are implicitly based on the same core arguments. This article provides a meta-theorem which unifies these different approaches. Towards this, we first revisit weighted automata by defining a new semantics for them in two phases—an abstract semantics based on multisets of weight structures (independent of particular weight domains) followed by a concrete semantics. Then, we introduce a core weighted logic with a minimal number of features and a simplified syntax, and lift the new semantics to this logic. We show at the level of the abstract semantics that weighted automata and core weighted logic have the same expressive power. Finally, we show how previous results can be recovered from our result by logical reasoning. In this paper, we prove the meta-theorem for words, ranked and unranked trees, showing the robustness of our approach.

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!

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!

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!

Fußnoten
1
This valuation does not satisfy \(\mathsf {Sq}(s)=s\).
 
2
We do not require that \(\mathsf {Val}(r)=r\) for all \(r\in U\) as in Droste and Perevoshchikov (2013).
 
3
Actually, (3) holds for arbitrary multisets \(A_i,B_j\in \mathbb {N} \langle R \rangle \).
 
4
As already noticed in Droste and Meinecke (2012), a simple projection does not work. Indeed, it would result in transition labels that are multisets of weights, which is not possible since our theorem requires the same set of weights for the automaton and the formula.
 
5
We could also use an unambiguous automaton for \(\mathcal A_\varphi \).
 
6
These formulæ are call strongly \(\wedge \)-restricted in Droste and Meinecke (2012), in contrast with a slightly less restrained fragment of \(\wedge \)-restricted formulæ.
 
7
In Droste and Meinecke (2012), the regularity is defined with respect to some weighted automata. Here, we prefer to use a purely logical definition. However, using Corollary 11-2., those two definitions are equivalent.
 
8
The product in the semiring of weight sequences is based on the concatenation of sequences. There is no natural counterpart for trees.
 
9
Equivalently, we may assume that transitions are disjoint: if \((L,a,q),(L',a,q)\in \Delta \) then \(L=L'\) or \(L\cap L'=\emptyset \). In this case, a run can be defined as a simpler Q-tree \(\rho \) with \(\mathrm {dom}(\rho )=\mathrm {dom}(t)\) and such that for all \(u\in \mathrm {dom}(t)\) there is a (unique) transition \((L,t(u),\rho (u))\in \Delta \) with \(\rho (u\cdot 1)\ldots \rho (u\cdot \mathsf {ar}(u))\in L\).
 
10
An even simpler formula can be obtained in the simpler setting of ranked trees.
 
Literatur
Zurück zum Zitat Albert J, Kari J (2009) Digital image compression. In: Kuich W, Vogler H, Droste M (eds) Handbook of Weighted Automata, EATCS Monographs in Theoretical Computer Science, chap. 5. Springer, pp. 445–472 Albert J, Kari J (2009) Digital image compression. In: Kuich W, Vogler H, Droste M (eds) Handbook of Weighted Automata, EATCS Monographs in Theoretical Computer Science, chap. 5. Springer, pp. 445–472
Zurück zum Zitat Bollig B, Gastin P (2009) Weighted versus probabilistic logics. In: Proceedings of the 13th international conference on developments in language theory (DLT’09), Lecture Notes in Computer Science, vol. 5583, Springer, pp. 18–38 Bollig B, Gastin P (2009) Weighted versus probabilistic logics. In: Proceedings of the 13th international conference on developments in language theory (DLT’09), Lecture Notes in Computer Science, vol. 5583, Springer, pp. 18–38
Zurück zum Zitat Büchi JR (1960) Weak second-order arithmetic and finite automata. Zeitschrift für Mathematische Logik und Grundlagen der Mathematik 6:66–92MathSciNetCrossRefMATH Büchi JR (1960) Weak second-order arithmetic and finite automata. Zeitschrift für Mathematische Logik und Grundlagen der Mathematik 6:66–92MathSciNetCrossRefMATH
Zurück zum Zitat Černý P, Chatterjee K, Henzinger TA, Radhakrishna A, Singh R (2011) Quantitative synthesis for concurrent programs. In: Proceedings of the 23rd international conference on computer aided verification (CAV’11), Lecture Notes in Computer Science, vol 6806, Springer, pp. 243–259 Černý P, Chatterjee K, Henzinger TA, Radhakrishna A, Singh R (2011) Quantitative synthesis for concurrent programs. In: Proceedings of the 23rd international conference on computer aided verification (CAV’11), Lecture Notes in Computer Science, vol 6806, Springer, pp. 243–259
Zurück zum Zitat Droste M, Gastin P (2007) Weighted automata and weighted logics. Theor Comput Sci 380(1–2):69–86 Droste M, Gastin P (2007) Weighted automata and weighted logics. Theor Comput Sci 380(1–2):69–86
Zurück zum Zitat Droste M, Götze D, Märcker S, Meinecke I (2011) Weighted tree automata over valuation monoids and their characterization by weighted logics. In: Algebraic Foundations in Computer Science, Lecture Notes in Computer Science, vol 7020, Springer, pp. 30–55 Droste M, Götze D, Märcker S, Meinecke I (2011) Weighted tree automata over valuation monoids and their characterization by weighted logics. In: Algebraic Foundations in Computer Science, Lecture Notes in Computer Science, vol 7020, Springer, pp. 30–55
Zurück zum Zitat Droste M, Heusel D, Vogler H (2015) Weighted unranked tree automata over tree valuation monoids and their characterization by weighted logics. In: Proceedings of the 6th international conference on algebraic informatics (CAI’15), Lecture Notes in Computer Science, vol 9270, Springer, pp. 90–102 Droste M, Heusel D, Vogler H (2015) Weighted unranked tree automata over tree valuation monoids and their characterization by weighted logics. In: Proceedings of the 6th international conference on algebraic informatics (CAI’15), Lecture Notes in Computer Science, vol 9270, Springer, pp. 90–102
Zurück zum Zitat Droste M, Kuich W (2009) Semirings and formal power series. In: Droste M, Kuich W, Vogler H (eds) Handbook of weighted automata, EATCS monographs in theoretical computer science, chap. 1, Springer, pp. 3–27 Droste M, Kuich W (2009) Semirings and formal power series. In: Droste M, Kuich W, Vogler H (eds) Handbook of weighted automata, EATCS monographs in theoretical computer science, chap. 1, Springer, pp. 3–27
Zurück zum Zitat Droste M, Meinecke I (2012) Weighted automata and weighted MSO logics for average and long-time behaviors. Inf Comput 220–221:44–59MathSciNetCrossRefMATH Droste M, Meinecke I (2012) Weighted automata and weighted MSO logics for average and long-time behaviors. Inf Comput 220–221:44–59MathSciNetCrossRefMATH
Zurück zum Zitat Droste M, Perevoshchikov V (2013) Multi-weighted automata and MSO logic. In: Proceedings of the 8th international computer science symposium in Russia (CSR’13), Lecture Notes in Computer Science. vol. 7913, Springer, pp 418–430 Droste M, Perevoshchikov V (2013) Multi-weighted automata and MSO logic. In: Proceedings of the 8th international computer science symposium in Russia (CSR’13), Lecture Notes in Computer Science. vol. 7913, Springer, pp 418–430
Zurück zum Zitat Droste M, Perevoshchikov V (2014) A Nivat theorem for weighted timed automata and weighted relative distance logic. In: Proceedings of the 41st international colloquium on automata, languages and programming (ICALP’14), Lecture Notes in Computer Science, vol. 8573, Springer, pp. 171–182 Droste M, Perevoshchikov V (2014) A Nivat theorem for weighted timed automata and weighted relative distance logic. In: Proceedings of the 41st international colloquium on automata, languages and programming (ICALP’14), Lecture Notes in Computer Science, vol. 8573, Springer, pp. 171–182
Zurück zum Zitat Fülöp Z, Stüber T, Vogler H (2012) A Büchi-like theorem for weighted tree automata over multioperator monoids. Theory Comput Syst 50:241–278MathSciNetCrossRefMATH Fülöp Z, Stüber T, Vogler H (2012) A Büchi-like theorem for weighted tree automata over multioperator monoids. Theory Comput Syst 50:241–278MathSciNetCrossRefMATH
Zurück zum Zitat Knight K, May J (2009) Applications of weighted automata in natural language processing. In: Droste M, Kuich W, Vogler H (eds) Handbook of weighted automata, EATCS monographs in theoretical computer science, chap. 14, Springer, pp 555–579 Knight K, May J (2009) Applications of weighted automata in natural language processing. In: Droste M, Kuich W, Vogler H (eds) Handbook of weighted automata, EATCS monographs in theoretical computer science, chap. 14, Springer, pp 555–579
Zurück zum Zitat Kuich W, Salomaa A (1985) Semirings. Automata and Languages. EATCS Monographs in Theoretical Computer Science. Springer-Verlag Kuich W, Salomaa A (1985) Semirings. Automata and Languages. EATCS Monographs in Theoretical Computer Science. Springer-Verlag
Zurück zum Zitat Perevoshchikov V (2015) Multi-weighted automata models and quantitative logics. Ph.D. thesis, Universität Leipzig Perevoshchikov V (2015) Multi-weighted automata models and quantitative logics. Ph.D. thesis, Universität Leipzig
Zurück zum Zitat Thatcher JW, Wright JB (1968) Generalized finite automata theory with an application to a decision problem of second-order logic. Math Syst Theory 2(1):57–81MathSciNetCrossRefMATH Thatcher JW, Wright JB (1968) Generalized finite automata theory with an application to a decision problem of second-order logic. Math Syst Theory 2(1):57–81MathSciNetCrossRefMATH
Zurück zum Zitat Trakhtenbrot BA (1961) Finite automata and logic of monadic predicates. Doklady Akademii Nauk SSSR 149:326–329 Trakhtenbrot BA (1961) Finite automata and logic of monadic predicates. Doklady Akademii Nauk SSSR 149:326–329
Metadaten
Titel
A unifying survey on weighted logics and weighted automata
Core weighted logic: minimal and versatile specification of quantitative properties
verfasst von
Paul Gastin
Benjamin Monmege
Publikationsdatum
29.12.2015
Verlag
Springer Berlin Heidelberg
Erschienen in
Soft Computing / Ausgabe 4/2018
Print ISSN: 1432-7643
Elektronische ISSN: 1433-7479
DOI
https://doi.org/10.1007/s00500-015-1952-6

Weitere Artikel der Ausgabe 4/2018

Soft Computing 4/2018 Zur Ausgabe