{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,11]],"date-time":"2025-10-11T17:10:49Z","timestamp":1760202649088,"version":"3.41.0"},"reference-count":55,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2013,2,1]],"date-time":"2013-02-01T00:00:00Z","timestamp":1359676800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100001871","name":"Funda\u00e7\u00e3o para a Ci\u00eancia e a Tecnologia","doi-asserted-by":"publisher","award":["SFRH\/BPD\/71956\/2010"],"award-info":[{"award-number":["SFRH\/BPD\/71956\/2010"]}],"id":[{"id":"10.13039\/501100001871","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Comput. Logic"],"published-print":{"date-parts":[[2013,2]]},"abstract":"<jats:p>\n            Coalgebras provide a uniform framework for studying dynamical systems, including several types of automata. In this article, we make use of the coalgebraic view on systems to investigate, in a uniform way, under which conditions calculi that are sound and complete with respect to behavioral equivalence can be extended to a coarser coalgebraic language equivalence, which arises from a generalized powerset construction that determinizes coalgebras. We show that soundness and completeness are established by proving that expressions modulo axioms of a calculus form the rational fixpoint of the given type functor. Our main result is that the rational fixpoint of the functor\n            <jats:italic>FT<\/jats:italic>\n            , where\n            <jats:italic>T<\/jats:italic>\n            is a monad describing the branching of the systems (e.g., non-determinism, weights, probability, etc.), has as a quotient the rational fixpoint of the determinized type functor\n            <jats:italic>F<\/jats:italic>\n            , a lifting of\n            <jats:italic>F<\/jats:italic>\n            to the category of\n            <jats:italic>T<\/jats:italic>\n            -algebras. We apply our framework to the concrete example of weighted automata, for which we present a new sound and complete calculus for weighted language equivalence. As a special case, we obtain nondeterministic automata in which we recover Rabinovich\u2019s sound and complete calculus for language equivalence.\n          <\/jats:p>","DOI":"10.1145\/2422085.2422092","type":"journal-article","created":{"date-parts":[[2013,2,22]],"date-time":"2013-02-22T19:25:04Z","timestamp":1361561104000},"page":"1-52","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":32,"title":["Sound and Complete Axiomatizations of Coalgebraic Language Equivalence"],"prefix":"10.1145","volume":"14","author":[{"given":"Marcello M.","family":"Bonsangue","sequence":"first","affiliation":[{"name":"Leiden Institute of Advanced Computer Science"}]},{"given":"Stefan","family":"Milius","sequence":"additional","affiliation":[{"name":"Technische Universit\u00e4t Braunschweig"}]},{"given":"Alexandra","family":"Silva","sequence":"additional","affiliation":[{"name":"Radboud University Nijmegen"}]}],"member":"320","published-online":{"date-parts":[[2013,2]]},"reference":[{"key":"e_1_2_1_1_1","volume-title":"Proceedings of the Category Theory and Computer Science (CTCS). Lecture Notes in Computer Science","volume":"389","author":"Aczel P.","unstructured":"Aczel , P. and Mendler , N . 1989. A final coalgebra theorem . In Proceedings of the Category Theory and Computer Science (CTCS). Lecture Notes in Computer Science , vol. 389 . Springer, Berlin, 357--365. Aczel, P. and Mendler, N. 1989. A final coalgebra theorem. In Proceedings of the Category Theory and Computer Science (CTCS). Lecture Notes in Computer Science, vol. 389. Springer, Berlin, 357--365."},{"key":"e_1_2_1_2_1","doi-asserted-by":"crossref","unstructured":"Ad\u00e1mek J. and Rosick\u00fd J. 1994. Locally Presentable and Accessible Categories. Cambridge University Press.  Ad\u00e1mek J. and Rosick\u00fd J. 1994. Locally Presentable and Accessible Categories . Cambridge University Press.","DOI":"10.1017\/CBO9780511600579"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129502003924"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129506005706"},{"key":"e_1_2_1_5_1","unstructured":"Ad\u00e1mek J. Herrlich H. and Strecker G. E. 2009. Abstract and Concrete Categories: The Joy of Cats 2nd Ed. Dover Publications Mineola NY.  Ad\u00e1mek J. Herrlich H. and Strecker G. E. 2009. Abstract and Concrete Categories: The Joy of Cats 2nd Ed. Dover Publications Mineola NY."},{"key":"e_1_2_1_6_1","doi-asserted-by":"crossref","unstructured":"Ad\u00e1mek J. Milius S. and \n      Velebil J\n  . \n  2009\n  . Semantics of higher-order recursion schemes. In Proceedings of the International Conference on Algebra and Coalgebra in Computer Science (CALCO\u201909) A. Kurz M. Lenisa and A. Tarlecki Eds. Lecture Notes in Computer Science vol. \n  5728\n  . \n  Springer Berlin 49--63.   Ad\u00e1mek J. Milius S. and Velebil J. 2009. Semantics of higher-order recursion schemes. In Proceedings of the International Conference on Algebra and Coalgebra in Computer Science (CALCO\u201909) A. Kurz M. Lenisa and A. Tarlecki Eds. Lecture Notes in Computer Science vol. 5728. Springer Berlin 49--63.","DOI":"10.1007\/978-3-642-03741-2_5"},{"key":"e_1_2_1_7_1","doi-asserted-by":"crossref","unstructured":"Ad\u00e1mek J. Rosick\u00fd J. and Vitale E. 2011a. Algebraic Theories. Cambridge University Press.  Ad\u00e1mek J. Rosick\u00fd J. and Vitale E. 2011a. Algebraic Theories . Cambridge University Press.","DOI":"10.1017\/CBO9780511760754"},{"key":"e_1_2_1_8_1","volume-title":"Proceedings of the 20th Conference on Computer Science Logic (CSL\u201911)","volume":"12","author":"Ad\u00e1mek J.","unstructured":"Ad\u00e1mek , J. , Milius , S. , Moss , L. S. , and Sousa , L . 2011. Power-set functor and saturated trees . In Proceedings of the 20th Conference on Computer Science Logic (CSL\u201911) . LIPICS, vol. 12 , 5--19. Ad\u00e1mek, J., Milius, S., Moss, L. S., and Sousa, L. 2011. Power-set functor and saturated trees. In Proceedings of the 20th Conference on Computer Science Logic (CSL\u201911). LIPICS, vol. 12, 5--19."},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(93)90076-6"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129500000104"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.5555\/170320"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2009.02.003"},{"key":"e_1_2_1_15_1","volume-title":"Proceedings of the Foundations of Software Science and Computation Structures (FOSSACS). Lecture Notes in Computer Science","volume":"4962","author":"Bonsangue M. M.","unstructured":"Bonsangue , M. M. , Rutten , J. J. M. M. , and Silva , A . 2008. Coalgebraic logic and synthesis of Mealy machines . In Proceedings of the Foundations of Software Science and Computation Structures (FOSSACS). Lecture Notes in Computer Science , vol. 4962 . Springer, Berlin, 231--245. Bonsangue, M. M., Rutten, J. J. M. M., and Silva, A. 2008. Coalgebraic logic and synthesis of Mealy machines. In Proceedings of the Foundations of Software Science and Computation Structures (FOSSACS). Lecture Notes in Computer Science, vol. 4962. Springer, Berlin, 231--245."},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2007.11.018"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.dam.2006.03.013"},{"volume-title":"Regular Algebra and Finite Machines","author":"Conway J. H.","key":"e_1_2_1_18_1","unstructured":"Conway , J. H. 1971. Regular Algebra and Finite Machines . Chapman and Hall , London . Conway, J. H. 1971. Regular Algebra and Finite Machines. Chapman and Hall, London."},{"key":"e_1_2_1_19_1","volume-title":"Eds","author":"Droste M.","year":"2009","unstructured":"Droste , M. , Kuich , W. , and Vogler , H. , Eds . 2009 . Handbook of Weighted Automata. Monographs in Theoretical Computer Science. Springer . Droste, M., Kuich, W., and Vogler, H., Eds. 2009. Handbook of Weighted Automata. Monographs in Theoretical Computer Science. Springer."},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0049-237X(08)71949-9"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2011.09.020"},{"key":"#cr-split#-e_1_2_1_22_1.1","doi-asserted-by":"crossref","unstructured":"\u00c9sik Z. and Kuich W. 2012. Free iterative and iteration k-semialgebras. Algebra Univ. published online March 3 2012. DOI:10.1007\/s00012-012-0179-y. 10.1007\/s00012-012-0179-y","DOI":"10.1007\/s00012-012-0179-y"},{"key":"#cr-split#-e_1_2_1_22_1.2","doi-asserted-by":"crossref","unstructured":"\u00c9sik Z. and Kuich W. 2012. Free iterative and iteration k -semialgebras. Algebra Univ . published online March 3 2012. DOI:10.1007\/s00012-012-0179-y.","DOI":"10.1007\/s00012-012-0179-y"},{"volume-title":"Proceedings of the 6th International Conference on Foundations of Computer Science, H. R. Arabnia, G. A. Gravvanis, and A. M. G. Solo Eds., 119--122","author":"\u00c9sik Z.","key":"e_1_2_1_23_1","unstructured":"\u00c9sik , Z. and Maletti , A . 2010. Simulation vs. equivalence . In Proceedings of the 6th International Conference on Foundations of Computer Science, H. R. Arabnia, G. A. Gravvanis, and A. M. G. Solo Eds., 119--122 . \u00c9sik, Z. and Maletti, A. 2010. Simulation vs. equivalence. In Proceedings of the 6th International Conference on Foundations of Computer Science, H. R. Arabnia, G. A. Gravvanis, and A. M. G. Solo Eds., 119--122."},{"key":"e_1_2_1_24_1","doi-asserted-by":"crossref","unstructured":"\u00c9sik Z.\n     and \n      Maletti A\n  . \n  2011\n  . Simulations of weighted tree automata. In Proceedings of the 15th International Conference on Implementation and Application of Automata (CIAA) M. Domaratzki and K. Salomaa Eds. Lecture Notes in Computer Science vol. \n  6482\n  . \n  Springer Berlin 321--330.   \u00c9sik Z. and Maletti A. 2011. Simulations of weighted tree automata. In Proceedings of the 15th International Conference on Implementation and Application of Automata (CIAA) M. Domaratzki and K. Salomaa Eds. Lecture Notes in Computer Science vol. 6482. Springer Berlin 321--330.","DOI":"10.1007\/978-3-642-18098-9_34"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0020-0190(97)00162-2"},{"key":"e_1_2_1_26_1","first-page":"4","article-title":"Redei\u2019s finiteness theorem for commutative semigroups","volume":"19","author":"Freyd P.","year":"1968","unstructured":"Freyd , P. 1968 . Redei\u2019s finiteness theorem for commutative semigroups . Proc. Amer. Math. Soc. 19 , 4 . Freyd, P. 1968. Redei\u2019s finiteness theorem for commutative semigroups. Proc. Amer. Math. Soc. 19, 4.","journal-title":"Proc. Amer. Math. Soc."},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(79)90032-1"},{"key":"e_1_2_1_28_1","series-title":"Lecture Notes in Mathematics","volume-title":"Proceedings of the Categorical Aspects of Topology and Analysis","author":"Giry M.","unstructured":"Giry , M. 1981. A categorical approach to probability theory . In Proceedings of the Categorical Aspects of Topology and Analysis . Lecture Notes in Mathematics , vol. 915 . Springer , Berlin , 68--85. Giry, M. 1981. A categorical approach to probability theory. In Proceedings of the Categorical Aspects of Topology and Analysis. Lecture Notes in Mathematics, vol. 915. Springer, Berlin, 68--85."},{"volume-title":"Semirings and Their Application","author":"Golan J. S.","key":"e_1_2_1_29_1","unstructured":"Golan , J. S. 1999. Semirings and Their Application . Kluwer Academic Publishers . Golan, J. S. 1999. Semirings and Their Application. Kluwer Academic Publishers."},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0661(04)80908-3"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(91)90356-7"},{"key":"e_1_2_1_32_1","doi-asserted-by":"crossref","unstructured":"Hasuo I. Jacobs B. and Sokolova A. 2007. Generic trace semantics via coinduction. Log. Methods Comput. Sci. 3 4:11 1--36.  Hasuo I. Jacobs B. and Sokolova A. 2007. Generic trace semantics via coinduction. Log. Methods Comput. Sci. 3 4:11 1--36.","DOI":"10.2168\/LMCS-3(4:11)2007"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1112\/blms\/7.3.294"},{"volume-title":"Number 34 in Annals of Mathematics Studies","author":"Kleene S. C.","key":"e_1_2_1_34_1","unstructured":"Kleene , S. C. 1956. Representation of events in nerve nets and finite automata . In Automata Studies, C. E. Shannon and J. McCarthy Eds., Number 34 in Annals of Mathematics Studies . Princeton University Press , Princeton, NJ . 3--41. Kleene, S. C. 1956. Representation of events in nerve nets and finite automata. In Automata Studies, C. E. Shannon and J. McCarthy Eds., Number 34 in Annals of Mathematics Studies. Princeton University Press, Princeton, NJ. 3--41."},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1994.1037"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(91)90395-I"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1142\/S0218196794000063"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01110627"},{"edition":"2","volume-title":"Lang, S. 1984. Algebra","key":"e_1_2_1_39_1","unstructured":"Lang, S. 1984. Algebra 2 nd Ed. Addison-Wesley , Boston, MA . Lang, S. 1984. Algebra 2nd Ed. Addison-Wesley, Boston, MA."},{"key":"e_1_2_1_40_1","volume-title":"Categories for the Working Mathematician","author":"MacLane S.","unstructured":"MacLane , S. 1998. Categories for the Working Mathematician 2 nd Ed. Springer . MacLane, S. 1998. Categories for the Working Mathematician 2nd Ed. Springer.","edition":"2"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2010.11"},{"key":"e_1_2_1_42_1","series-title":"International Series in Computer Science","volume-title":"Communication and Concurrency","author":"Milner R.","unstructured":"Milner , R. 1989. Communication and Concurrency . International Series in Computer Science . Prentice Hall , Upper Saddle River, NJ. Milner, R. 1989. Communication and Concurrency. International Series in Computer Science. Prentice Hall, Upper Saddle River, NJ."},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(83)90014-2"},{"volume-title":"Proceedings of the IEEE Symposium on Logic in Computer Science (LICS).","author":"Plotkin G. D.","key":"e_1_2_1_45_1","unstructured":"Plotkin , G. D. and Turi , D . 1997. Towards a mathematical operational semantics . In Proceedings of the IEEE Symposium on Logic in Computer Science (LICS). Plotkin, G. D. and Turi, D. 1997. Towards a mathematical operational semantics. In Proceedings of the IEEE Symposium on Logic in Computer Science (LICS)."},{"key":"e_1_2_1_46_1","series-title":"Lecture Notes in Computer Science","volume-title":"Proceedings of the Mathematical Foundations of Programming Semantics (MFPS\u201993)","author":"Rabinovich A. M.","unstructured":"Rabinovich , A. M. 1994. A complete axiomatization for trace congruence of finite state behaviors . In Proceedings of the Mathematical Foundations of Programming Semantics (MFPS\u201993) , S. Brookes, M. Main, A. Melton, M. Mislove, and D. Schmidt Eds., Lecture Notes in Computer Science , vol. 802 . Springer , Berlin , 530--543. Rabinovich, A. M. 1994. A complete axiomatization for trace congruence of finite state behaviors. In Proceedings of the Mathematical Foundations of Programming Semantics (MFPS\u201993), S. Brookes, M. Main, A. Melton, M. Mislove, and D. Schmidt Eds., Lecture Notes in Computer Science, vol. 802. Springer, Berlin, 530--543."},{"volume-title":"The Theory of Finitely Generated Commutative Semigroups","author":"R\u00e8dei L.","key":"e_1_2_1_47_1","unstructured":"R\u00e8dei , L. 1965. The Theory of Finitely Generated Commutative Semigroups . Pergamon , Oxford-Edinburgh- New York . R\u00e8dei, L. 1965. The Theory of Finitely Generated Commutative Semigroups. Pergamon, Oxford-Edinburgh-New York."},{"volume-title":"Finitely Generated Commutative Monoids","author":"Rosales J. C.","key":"e_1_2_1_48_1","unstructured":"Rosales , J. C. and Garcia-S\u00e1nchez , P. A. 1999. Finitely Generated Commutative Monoids . Novascience Publishers, New York , NY. Rosales, J. C. and Garcia-S\u00e1nchez, P. A. 1999. Finitely Generated Commutative Monoids. Novascience Publishers, New York, NY."},{"key":"e_1_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(00)00056-6"},{"key":"e_1_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(02)00895-2"},{"key":"e_1_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1006\/jabr.1999.7930"},{"key":"e_1_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/321312.321326"},{"key":"e_1_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0019-9958(61)80020-X"},{"key":"e_1_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-6(3:23)2010"},{"key":"e_1_2_1_55_1","volume-title":"Proceedings of the IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS\u201910)","volume":"8","author":"Silva A.","unstructured":"Silva , A. , Bonchi , F. , Bonsangue , M. M. , and Rutten , J. J. M. M. 2010. Generalizing the powerset construction, coalgebraically . In Proceedings of the IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS\u201910) , K. Lodaya and M. Mahajan Eds., Leibniz International Proceedings in Informatics (LIPIcs) Series , vol. 8 . 272--283. Silva, A., Bonchi, F., Bonsangue, M. M., and Rutten, J. J. M. M. 2010. Generalizing the powerset construction, coalgebraically. In Proceedings of the IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS\u201910), K. Lodaya and M. Mahajan Eds., Leibniz International Proceedings in Informatics (LIPIcs) Series, vol. 8. 272--283."},{"key":"e_1_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2010.09.007"},{"key":"e_1_2_1_57_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2004.12.009"}],"container-title":["ACM Transactions on Computational Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2422085.2422092","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2422085.2422092","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T08:18:35Z","timestamp":1750234715000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2422085.2422092"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013,2]]},"references-count":55,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2013,2]]}},"alternative-id":["10.1145\/2422085.2422092"],"URL":"https:\/\/doi.org\/10.1145\/2422085.2422092","relation":{},"ISSN":["1529-3785","1557-945X"],"issn-type":[{"type":"print","value":"1529-3785"},{"type":"electronic","value":"1557-945X"}],"subject":[],"published":{"date-parts":[[2013,2]]},"assertion":[{"value":"2011-07-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2012-03-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2013-02-01","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}