nach oben

Erschienen in:

2017 | OriginalPaper | Buchkapitel

Up-To Techniques for Weighted Systems

verfasst von : Filippo Bonchi, Barbara König, Sebastian Küpper

Erschienen in: Tools and Algorithms for the Construction and Analysis of Systems

Verlag: Springer Berlin Heidelberg

Einloggen

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

search-config

KI-gestützte Suche

Aus

Abstract

We show how up-to techniques for (bi-)similarity can be used in the setting of weighted systems. The problems we consider are language equivalence, language inclusion and the threshold problem (also known as universality problem) for weighted automata. We build a bisimulation relation on the fly and work up-to congruence and up-to similarity. This requires to determine whether a pair of vectors (over a semiring) is in the congruence closure of a given relation of vectors. This problem is considered for rings and l-monoids, for the latter we provide a rewriting algorithm and show its confluence and termination. We then explain how to apply these up-to techniques to weighted automata and provide runtime results.

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

Vorheriges Kapitel Forward Bisimulations for Nondeterministic Symbolic Finite Automata

Nächstes Kapitel Rigorous Simulation-Based Analysis of Linear Hybrid Systems

Completely distributive l-monoids are often referred to as unital quantales.

We will sometimes use \(\min \) as an infix operator (i.e., \(a\min \ b\)).

A sub-semimodule for a ring is called submodule.

The accepted notions of language and language equivalence can be given for states rather than for vectors by assigning to each state \(x\in X\) the corresponding unit vector \(e_x\in \mathbb S^X\). On the other hand, when weighted automata are given with an initial vector i – which is often the case in literature – one can define the language of an automaton as \([\![i ]\!]\).

Whenever \(v\le v'\), the rule can be omitted, since it is never applicable.

Abdulla, P.A., Chen, Y.-F., Holík, L., Mayr, R., Vojnar, T.: When simulation meets antichains. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol. 6015, pp. 158–174. Springer, Heidelberg (2010). doi:10.1007/978-3-642-12002-2_14 CrossRef

Aceto, L., Ésik, Z., Ingólfsdóttir, A.: Equational theories of tropical semirings. Theor. Comput. Sci. 298(3), 417–469 (2003). Foundations of Software Science and Computation StructuresMathSciNetCrossRefMATH

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). doi:10.1007/978-3-642-24372-1_37 CrossRef

Béal, M.-P., Lombardy, S., Sakarovitch, J.: Conjugacy and equivalence of weighted automata and functional transducers. In: Grigoriev, D., Harrison, J., Hirsch, E.A. (eds.) CSR 2006. LNCS, vol. 3967, pp. 58–69. Springer, Heidelberg (2006). doi:10.1007/11753728_9 CrossRef

Bezhanishvili, G., Gabelaia, D., Jibladze, M.: Funayama’s theorem revisited. Algebra Univers. 70(3), 271–286 (2013)MathSciNetCrossRefMATH

Bonchi, F., Bonsangue, M.M., Boreale, M., Rutten, J.J.M.M., Silva, A.: A coalgebraic perspective on linear weighted automata. Inf. Comput. 211, 77–105 (2012)MathSciNetCrossRefMATH

Bonchi, F., König, B., Küpper, S.: Up-to techniques for weighted systems (extended version) arXiv:1701.05001 (2017)

Bonchi, F., Petrisan, D., Pous, D., Rot, J.: Coinduction up-to in a fibrational setting. In: Henzinger, T.A., Miller, D. (eds.) Proceedings of CSL-LICS 2014, pp. 20:1–20:9. ACM (2014)

Bonchi, F., Pous, D.: Checking NFA equivalence with bisimulations up to congruence. In: Proceedings of POPL 2013, pp. 457–468. ACM (2013)

10.

Boreale, M.: Weighted bisimulation in linear algebraic form. In: Bravetti, M., Zavattaro, G. (eds.) CONCUR 2009. LNCS, vol. 5710, pp. 163–177. Springer, Heidelberg (2009). doi:10.1007/978-3-642-04081-8_12 CrossRef

11.

Cyrluk, D., Lincoln, P., Shankar, N.: On Shostak’s decision procedure for combinations of theories. In: McRobbie, M.A., Slaney, J.K. (eds.) CADE 1996. LNCS, vol. 1104, pp. 463–477. Springer, Heidelberg (1996). doi:10.1007/3-540-61511-3_107 CrossRef

12.

Dershowitz, N., Jouannaud, J.-P.: Rewrite systems. In: van Leeuwen, J. (ed.) Formal Models and Semantics, Handbook of Theoretical Computer Science, vol. B, pp. 243–320. Elsevier (1990)

13.

Doyen, L., Raskin, J.-F.: Antichain algorithms for finite automata. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol. 6015, pp. 2–22. Springer, Heidelberg (2010). doi:10.1007/978-3-642-12002-2_2 CrossRef

14.

Gaubert, S., Plus, M.: Methods and applications of (max,+) linear algebra. In: Reischuk, R., Morvan, M. (eds.) STACS 1997. LNCS, vol. 1200, pp. 261–282. Springer, Heidelberg (1997). doi:10.1007/BFb0023465 CrossRef

15.

Hopcroft, J.E., Karp, R.M.: A linear algorithm for testing equivalence of finite automata. Technical report TR 114, Cornell University (1971)

16.

König, B., Küpper, S.: A generalized partition refinement algorithm, instantiated to language equivalence checking for weighted automata. Soft Comput. 1–18 (2016). http://link.springer.com/article/10.1007/s00500-016-2363-z

17.

Krob, D.: The equality problem for rational series with multiplicities in the tropical semiring is undecidable. Int. J. Algebra Comput. 4(3), 405–425 (1994)MathSciNetCrossRefMATH

18.

Milner, R.: Communication and Concurrency. Prentice Hall, Upper Saddle River (1989)MATH

19.

Pous, D., Sangiorgi, D.: Enhancements of the coinductive proof method. In: Sangiorgi, D., Rutten, J. (eds.) Advanced Topics in Bisimulation and Coinduction. Cambridge University Press, Cambridge (2011)

20.

Rot, J., Bonchi, F., Bonsangue, M., Pous, D., Rutten, J., Silva, A.: Enhanced coalgebraic bisimulation. Math. Struct. Comput. Sci. 1–29 (2015). https://www.cambridge.org/core/journals/mathematical-structures-in-computer-science/article/div-classtitleenhanced-coalgebraic-bisimulationdiv/C588A590E7DB3A73F1C86487D0F8DE19

21.

Stark, E.W.: On behaviour equivalence for probabilistic i/o automata and its relationship to probabilistic bisimulation. J. Automata Lang. Comb. 8(2), 361–395 (2003)MathSciNetMATH

22.

Urabe, N., Hasuo, I.: Generic forward and backward simulations III: quantitative simulations by matrices. In: Baldan, P., Gorla, D. (eds.) CONCUR 2014. LNCS, vol. 8704, pp. 451–466. Springer, Heidelberg (2014). doi:10.1007/978-3-662-44584-6_31

23.

Wulf, M., Doyen, L., Henzinger, T.A., Raskin, J.-F.: Antichains: a new algorithm for checking universality of finite automata. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 17–30. Springer, Heidelberg (2006). doi:10.1007/11817963_5 CrossRef

Titel: Up-To Techniques for Weighted Systems
verfasst von: Filippo Bonchi
Barbara König
Sebastian Küpper
Verlag: Springer Berlin Heidelberg
Buch: Tools and Algorithms for the Construction and Analysis of Systems
Print ISBN: 978-3-662-54576-8

Electronic ISBN: 978-3-662-54577-5

Copyright-Jahr: 2017
DOI: https://doi.org/10.1007/978-3-662-54577-5_31

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"