×

Up-to techniques for weighted systems. (English) Zbl 1452.68100

Legay, Axel (ed.) et al., Tools and algorithms for the construction and analysis of systems. 23rd international conference, TACAS 2017, held as part of the European joint conferences on theory and practice of software, ETAPS 2017, Uppsala, Sweden, April 22–29, 2017. Proceedings. Part I. Berlin: Springer. Lect. Notes Comput. Sci. 10205, 535-552 (2017).
Summary: 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.
For the entire collection see [Zbl 1360.68015].

MSC:

68Q45 Formal languages and automata
68Q42 Grammars and rewriting systems
68Q70 Algebraic theory of languages and automata
PDFBibTeX XMLCite
Full Text: DOI arXiv

References:

[1] 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 · Zbl 1284.68337 · doi:10.1007/978-3-642-12002-2_14
[2] 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 Structures · Zbl 1021.08002 · doi:10.1016/S0304-3975(02)00864-2
[3] 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 · Zbl 1348.68089 · doi:10.1007/978-3-642-24372-1_37
[4] 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 · Zbl 1185.68381 · doi:10.1007/11753728_9
[5] Bezhanishvili, G., Gabelaia, D., Jibladze, M.: Funayama’s theorem revisited. Algebra Univers. 70(3), 271-286 (2013) · Zbl 1285.06004 · doi:10.1007/s00012-013-0247-y
[6] 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) · Zbl 1279.68235 · doi:10.1016/j.ic.2011.12.002
[7] Bonchi, F., König, B., Küpper, S.: Up-to techniques for weighted systems (extended version) arXiv:1701.05001 (2017)
[8] 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) · Zbl 1395.68195
[9] Bonchi, F., Pous, D.: Checking NFA equivalence with bisimulations up to congruence. In: Proceedings of POPL 2013, pp. 457-468. ACM (2013) · Zbl 1301.68169
[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 · Zbl 1254.68130 · doi:10.1007/978-3-642-04081-8_12
[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 · Zbl 1415.03019 · doi:10.1007/3-540-61511-3_107
[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) · Zbl 0900.68283
[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 · Zbl 1284.68348 · doi:10.1007/978-3-642-12002-2_2
[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 · Zbl 1498.15034 · doi:10.1007/BFb0023465
[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 · Zbl 1398.68353
[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) · Zbl 0834.68058 · doi:10.1142/S0218196794000063
[18] Milner, R.: Communication and Concurrency. Prentice Hall, Upper Saddle River (1989) · Zbl 0683.68008
[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) · Zbl 1285.68111
[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 · Zbl 1380.68300
[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) · Zbl 1089.68062
[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 · Zbl 1417.68139 · doi:10.1007/978-3-662-44584-6_31
[23] Wulf, M. · Zbl 1188.68171 · doi:10.1007/11817963_5
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.