{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,6]],"date-time":"2026-03-06T09:05:16Z","timestamp":1772787916159,"version":"3.50.1"},"reference-count":23,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2015,3,1]],"date-time":"2015-03-01T00:00:00Z","timestamp":1425168000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Comput. Logic"],"published-print":{"date-parts":[[2015,3]]},"abstract":"<jats:p>\n            Traditional automata accept or reject their input and are therefore Boolean. In contrast, weighted automata map each word to a value from a semiring over a large domain. The special case of\n            <jats:italic>lattice automata<\/jats:italic>\n            , in which the semiring is a finite lattice, has interesting theoretical properties as well as applications in formal methods. A\n            <jats:italic>minimal deterministic automaton<\/jats:italic>\n            captures the combinatorial nature and complexity of a formal language. Deterministic automata are used in runtime monitoring, pattern recognition, and modeling systems. Thus, the minimization problem for deterministic automata is of great interest, both theoretically and in practice.\n          <\/jats:p>\n          <jats:p>For deterministic traditional automata on finite words, a minimization algorithm, based on the Myhill-Nerode right congruence on the set of words, generates in polynomial time a canonical minimal deterministic automaton. A polynomial algorithm is known also for deterministic weighted automata over the tropical semiring. For general deterministic weighted automata, the problem of minimization is open. In this article, we study minimization of deterministic lattice automata. We show that it is impossible to define a right congruence in the context of lattices, and that no canonical minimal automaton exists. Consequently, the minimization problem is much more complicated, and we prove that it is NP-complete. As good news, we show that while right congruence fails already for finite lattices that are fully ordered, for this setting we are able to combine a finite number of right congruences and generate a minimal deterministic automaton in polynomial time.<\/jats:p>","DOI":"10.1145\/2631915","type":"journal-article","created":{"date-parts":[[2015,3,25]],"date-time":"2015-03-25T16:03:43Z","timestamp":1427299423000},"page":"1-21","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":6,"title":["Minimizing Deterministic Lattice Automata"],"prefix":"10.1145","volume":"16","author":[{"given":"Shulamit","family":"Halamish","sequence":"first","affiliation":[{"name":"The Hebrew University, Jerusalem, Israel"}]},{"given":"Orna","family":"Kupferman","sequence":"additional","affiliation":[{"name":"The Hebrew University, Jerusalem, Israel"}]}],"member":"320","published-online":{"date-parts":[[2015,3,24]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-70545-1_23"},{"key":"e_1_2_1_2_1","volume-title":"Proceedings of the 11th International Conference on Computer Aided Verification. 274--287","author":"Bruns G.","unstructured":"G. Bruns and P. Godefroid . 1999. Model checking partial state spaces with 3-valued temporal logics . In Proceedings of the 11th International Conference on Computer Aided Verification. 274--287 . G. Bruns and P. Godefroid. 1999. Model checking partial state spaces with 3-valued temporal logics. In Proceedings of the 11th International Conference on Computer Aided Verification. 274--287."},{"key":"e_1_2_1_3_1","volume-title":"Proceedings of the 16th IEEE Symposium on Logic in Computer Science. IEEE Computer Society, 409--420","author":"Bruns G.","unstructured":"G. Bruns and P. Godefroid . 2001. Temporal logic query checking . In Proceedings of the 16th IEEE Symposium on Logic in Computer Science. IEEE Computer Society, 409--420 . G. Bruns and P. Godefroid. 2001. Temporal logic query checking. In Proceedings of the 16th IEEE Symposium on Logic in Computer Science. IEEE Computer Society, 409--420."},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.5555\/647769.733946"},{"key":"e_1_2_1_5_1","volume-title":"Proceedings of the 8th International SPIN Workshop on Model Checking Software. Springer, 16--36","author":"Chechik M.","unstructured":"M. Chechik , B. Devereux , and A. Gurfinkel . 2001. Model-checking infinite state-space systems with fine-grained abstractions using SPIN . In Proceedings of the 8th International SPIN Workshop on Model Checking Software. Springer, 16--36 . M. Chechik, B. Devereux, and A. Gurfinkel. 2001. Model-checking infinite state-space systems with fine-grained abstractions using SPIN. In Proceedings of the 8th International SPIN Workshop on Model Checking Software. Springer, 16--36."},{"key":"e_1_2_1_6_1","doi-asserted-by":"crossref","unstructured":"M. Droste W. Kuich and H. Vogler (Eds.). 2009. Handbook of Weighted Automata. Springer.   M. Droste W. Kuich and H. Vogler (Eds.). 2009. Handbook of Weighted Automata. Springer.","DOI":"10.1007\/978-3-642-01492-5"},{"key":"e_1_2_1_7_1","volume-title":"Proceedings of the 23rd International Conference on Software Engineering. IEEE Computer Society Press, 411--420","author":"Easterbrook S.","unstructured":"S. Easterbrook and M. Chechik . 2001. A framework for multi-valued reasoning over inconsistent viewpoints . In Proceedings of the 23rd International Conference on Software Engineering. IEEE Computer Society Press, 411--420 . S. Easterbrook and M. Chechik. 2001. A framework for multi-valued reasoning over inconsistent viewpoints. In Proceedings of the 23rd International Conference on Software Engineering. IEEE Computer Society Press, 411--420."},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.3115\/1073445.1073454"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706319"},{"key":"e_1_2_1_10_1","unstructured":"J. E. Hopcroft and J. D. Ullman. 1979. Introduction to Automata Theory Languages and Computation. Addison-Wesley.   J. E. Hopcroft and J. D. Ullman. 1979. Introduction to Automata Theory Languages and Computation. Addison-Wesley."},{"key":"e_1_2_1_11_1","volume-title":"Technical Report TR-2004-6. University of Cyprus.","author":"Hussain A.","year":"2004","unstructured":"A. Hussain and M. Huth . 2004 . On Model Checking Multiple Hybrid Views . Technical Report TR-2004-6. University of Cyprus. A. Hussain and M. Huth. 2004. On Model Checking Multiple Hybrid Views. Technical Report TR-2004-6. University of Cyprus."},{"key":"e_1_2_1_12_1","doi-asserted-by":"crossref","unstructured":"R. M. Karp. 1972. Reducibility among combinatorial problems. In Complexity of Computer Computations. 85--103.  R. M. Karp. 1972. Reducibility among combinatorial problems. In Complexity of Computer Computations. 85--103.","DOI":"10.1007\/978-1-4684-2001-2_9"},{"key":"e_1_2_1_13_1","first-page":"2","article-title":"On the determinization of weighted automata","volume":"10","author":"Kirsten D.","year":"2005","unstructured":"D. Kirsten and I. M\u00e4urer . 2005 . On the determinization of weighted automata . Journal of Automata, Languages and Combinatorics 10 , 2 -- 3 (2005), 287--312. D. Kirsten and I. M\u00e4urer. 2005. On the determinization of weighted automata. Journal of Automata, Languages and Combinatorics 10, 2--3 (2005), 287--312.","journal-title":"Journal of Automata, Languages and Combinatorics"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1142\/S0218196794000063"},{"key":"e_1_2_1_15_1","volume-title":"Proceedings of the 8th International Conference on Verification, Model Checking, and Abstract Interpretation. Springer, 199--213","author":"Kupferman O.","unstructured":"O. Kupferman and Y. Lustig . 2007. Lattice automata . In Proceedings of the 8th International Conference on Verification, Model Checking, and Abstract Interpretation. Springer, 199--213 . O. Kupferman and Y. Lustig. 2007. Lattice automata. In Proceedings of the 8th International Conference on Verification, Model Checking, and Abstract Interpretation. Springer, 199--213."},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1142\/S0129054110007192"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.fss.2007.03.003"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0020-0255(98)10073-7"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.5555\/972695.972698"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1090\/S0002-9939-1958-0135681-9"},{"key":"e_1_2_1_22_1","volume-title":"Automata: From Mathematics to Applications (AutoMathA).","author":"Network Programme ESF","year":"2010","unstructured":"ESF Network Programme . 2010 . Automata: From Mathematics to Applications (AutoMathA). Available at http:\/\/www.esf.org\/index.php&quest;id=1789. ESF Network Programme. 2010. Automata: From Mathematics to Applications (AutoMathA). Available at http:\/\/www.esf.org\/index.php&quest;id=1789."},{"key":"e_1_2_1_23_1","volume-title":"Proceedings of the 9th International Conference on Computer Aided Verification, O. Grumberg (Ed.)","volume":"1254","author":"Graf S.","unstructured":"S. Graf and H. Saidi . 1997. Construction of abstract state graphs with PVS . In Proceedings of the 9th International Conference on Computer Aided Verification, O. Grumberg (Ed.) , Vol. 1254 . Springer, 72--83. S. Graf and H. Saidi. 1997. Construction of abstract state graphs with PVS. In Proceedings of the 9th International Conference on Computer Aided Verification, O. Grumberg (Ed.), Vol. 1254. Springer, 72--83."},{"key":"e_1_2_1_24_1","volume-title":"Proceedings of the 2nd International Conference of Fuzzy Information and Engineering. 194--205","author":"Zekai L.","unstructured":"L. Zekai and S. Lan . 2007. Minimization of lattice automata . In Proceedings of the 2nd International Conference of Fuzzy Information and Engineering. 194--205 . L. Zekai and S. Lan. 2007. Minimization of lattice automata. In Proceedings of the 2nd International Conference of Fuzzy Information and Engineering. 194--205."}],"container-title":["ACM Transactions on Computational Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2631915","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2631915","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T07:19:13Z","timestamp":1750231153000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2631915"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,3]]},"references-count":23,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2015,3]]}},"alternative-id":["10.1145\/2631915"],"URL":"https:\/\/doi.org\/10.1145\/2631915","relation":{},"ISSN":["1529-3785","1557-945X"],"issn-type":[{"value":"1529-3785","type":"print"},{"value":"1557-945X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015,3]]},"assertion":[{"value":"2013-09-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2014-05-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2015-03-24","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}