{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:16:11Z","timestamp":1750306571546,"version":"3.41.0"},"reference-count":28,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2014,12,23]],"date-time":"2014-12-23T00:00:00Z","timestamp":1419292800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100000781","name":"European Research Council","doi-asserted-by":"publisher","award":["278410"],"award-info":[{"award-number":["278410"]}],"id":[{"id":"10.13039\/501100000781","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":[[2015,3]]},"abstract":"<jats:p>\n            Partially specified systems and specifications are used in formal methods such as stepwise design and query checking. Existing methods consider a setting in which systems and their correctness are Boolean. In recent years, there has been growing interest and need for quantitative formal methods, where systems may be weighted and specifications may be multivalued. Weighted automata, which map input words to a numerical value, play a key role in quantitative reasoning. Technically, every transition in a weighted automaton\n            <jats:italic>A<\/jats:italic>\n            has a cost, and the value\n            <jats:italic>A<\/jats:italic>\n            assigns to a finite word\n            <jats:italic>w<\/jats:italic>\n            is the sum of the costs on the transitions traversed along the most expensive accepting run of\n            <jats:italic>A<\/jats:italic>\n            on\n            <jats:italic>w<\/jats:italic>\n            . We study\n            <jats:italic>parameterized weighted containment<\/jats:italic>\n            : given three weighted automata\n            <jats:italic>A<\/jats:italic>\n            ,\n            <jats:italic>B<\/jats:italic>\n            , and\n            <jats:italic>C<\/jats:italic>\n            , with\n            <jats:italic>B<\/jats:italic>\n            being partial, the goal is to find an assignment to the missing costs in\n            <jats:italic>B<\/jats:italic>\n            so that we end up with\n            <jats:italic>B<\/jats:italic>\n            \u2032 for which\n            <jats:italic>B<\/jats:italic>\n            \u2032\u2264\n            <jats:italic>C<\/jats:italic>\n            , where \u2264 is the weighted counterpart of containment. We also consider a one-sided version of the problem, where only\n            <jats:italic>A<\/jats:italic>\n            or only\n            <jats:italic>C<\/jats:italic>\n            is given in addition to\n            <jats:italic>B<\/jats:italic>\n            , and the goal is to find a minimal assignment with which\n            <jats:italic>A<\/jats:italic>\n            \u2264\n            <jats:italic>B<\/jats:italic>\n            \u2032 or, respectively, a maximal one with which\n            <jats:italic>B<\/jats:italic>\n            \u2032 \u2264\n            <jats:italic>C<\/jats:italic>\n            . We argue that both problems are useful in stepwise design of weighted systems as well as approximated minimization of weighted automata.\n          <\/jats:p>\n          <jats:p>\n            We show that when the automata are deterministic, we can solve the problems in polynomial time. Our solution is based on the observation that the set of legal assignments to\n            <jats:italic>k<\/jats:italic>\n            missing costs forms a\n            <jats:italic>k<\/jats:italic>\n            -dimensional polytope. The technical challenge is to find an assignment in polynomial time even though the polytope is defined by means of exponentially many inequalities. We do so by developing a divide-and-conquer algorithm based on a separation oracle for polytopes. For nondeterministic automata, the weighted setting is much more complex, and in fact even nonparameterized containment is undecidable. We are able to show positive results for variants of the problems, where containment is replaced by simulation.\n          <\/jats:p>","DOI":"10.1145\/2665076","type":"journal-article","created":{"date-parts":[[2015,1,5]],"date-time":"2015-01-05T13:27:09Z","timestamp":1420464429000},"page":"1-25","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["Parameterized Weighted Containment"],"prefix":"10.1145","volume":"16","author":[{"given":"Guy","family":"Avni","sequence":"first","affiliation":[{"name":"Hebrew University, Jerusalem, Israel"}]},{"given":"Orna","family":"Kupferman","sequence":"additional","affiliation":[{"name":"Hebrew University, Jerusalem, Israel"}]}],"member":"320","published-online":{"date-parts":[[2014,12,23]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"crossref","unstructured":"S.\n      Almagor U.\n      Boker and \n      O.\n      Kupferman\n  . \n  2011\n  . What\u2019s decidable about weighted automata&quest; In 9th Int. Symp. on Automated Technology for Verification and Analysis volume \n  6996\n   of \n  Lecture Notes in Computer Science 482--491. \n  Springer\n  .   S. Almagor U. Boker and O. Kupferman. 2011. What\u2019s decidable about weighted automata&quest; In 9th Int. Symp. on Automated Technology for Verification and Analysis volume 6996 of Lecture Notes in Computer Science 482--491. Springer.","DOI":"10.1007\/978-3-642-24372-1_37"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/167088.167242"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-32940-1_8"},{"volume-title":"Proc. 16th IEEE Symp. on Logic in Computer Science, 409--420","author":"Bruns G.","key":"e_1_2_1_4_1","unstructured":"G. Bruns and P. Godefroid . 2001. Temporal logic query checking . In Proc. 16th IEEE Symp. on Logic in Computer Science, 409--420 . IEEE Computer Society. G. Bruns and P. Godefroid. 2001. Temporal logic query checking. In Proc. 16th IEEE Symp. on Logic in Computer Science, 409--420. IEEE Computer Society."},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.5555\/647769.733946"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-87531-4_28"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-6(3:10)2010"},{"key":"e_1_2_1_8_1","doi-asserted-by":"crossref","unstructured":"K. Culik and J. Kari. 1997. Digital images and formal languages. Handbook of formal languages vol. 3: beyond words 599--616. Springer-Verlag Berlin\/Heidelberg.   K. Culik and J. Kari. 1997. Digital images and formal languages. Handbook of formal languages vol. 3: beyond words 599--616. Springer-Verlag Berlin\/Heidelberg.","DOI":"10.1007\/978-3-642-59126-6_10"},{"volume-title":"A Discipline of Programming","author":"Dijkstra E. W.","key":"e_1_2_1_9_1","unstructured":"E. W. Dijkstra . 1976. A Discipline of Programming . Prentice-Hall . E. W. Dijkstra. 1976. A Discipline of Programming. Prentice-Hall."},{"volume-title":"Proc. 18th Int. Colloq. on Automata, Languages, and Programming, 93--114","author":"Fix L.","key":"e_1_2_1_10_1","unstructured":"L. Fix , N. Francez , and O. Grumberg . 1991. Program composition and modular verification . In Proc. 18th Int. Colloq. on Automata, Languages, and Programming, 93--114 . L. Fix, N. Francez, and O. Grumberg. 1991. Program composition and modular verification. In Proc. 18th Int. Colloq. on Automata, Languages, and Programming, 93--114."},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-32940-1_11"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0019-9958(78)90562-4"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF02579273"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF02579139"},{"key":"e_1_2_1_15_1","doi-asserted-by":"crossref","unstructured":"M. Gr\u00f6tschel L. Lov\u00e1sz and A. Schrijver. 1988. Geometric Algorithms and Combinatorial Optimization. Springer-Verlag New York.  M. Gr\u00f6tschel L. Lov\u00e1sz and A. Schrijver. 1988. Geometric Algorithms and Combinatorial Optimization. Springer-Verlag New York.","DOI":"10.1007\/978-3-642-97881-4"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/11513988_23"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1980.29"},{"key":"e_1_2_1_18_1","first-page":"1093","article-title":"A polynomial algorithm in linear programming","volume":"244","author":"Khachiyan L. G.","year":"1979","unstructured":"L. G. Khachiyan . 1979 . A polynomial algorithm in linear programming . Doklady Akademii Nauk SSSR , 244 , 1093 -- 1096 . L. G. Khachiyan. 1979. A polynomial algorithm in linear programming. Doklady Akademii Nauk SSSR, 244, 1093--1096.","journal-title":"Doklady Akademii Nauk SSSR"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1142\/S0218196794000063"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.5555\/972695.972698"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1006\/csla.2001.0184"},{"key":"e_1_2_1_22_1","unstructured":"M. W. Padberg and M. R. Rao. 1980. The Russian Method and Integer Programming. Working paper series. Salomon Brothers Center for the Study of Financial Institutions.  M. W. Padberg and M. R. Rao. 1980. The Russian Method and Integer Programming. Working paper series. Salomon Brothers Center for the Study of Financial Institutions."},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/584792.584833"},{"volume-title":"Theory of linear and integer programming","author":"Schrijver A.","key":"e_1_2_1_24_1","unstructured":"A. Schrijver . 1999. Theory of linear and integer programming . Wiley-Interscience series in discrete mathematics and optimization. Wiley . A. Schrijver. 1999. Theory of linear and integer programming. Wiley-Interscience series in discrete mathematics and optimization. Wiley."},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/1065010.1065045"},{"key":"e_1_2_1_26_1","doi-asserted-by":"crossref","unstructured":"W. Thomas. 1990. Automata on infinite objects. Handbook of Theoretical Computer Science 133--191.   W. Thomas. 1990. Automata on infinite objects. Handbook of Theoretical Computer Science 133--191.","DOI":"10.1016\/B978-0-444-88074-1.50009-3"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-27810-8_33"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1994.1092"}],"container-title":["ACM Transactions on Computational Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2665076","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2665076","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T06:13:25Z","timestamp":1750227205000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2665076"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,12,23]]},"references-count":28,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2015,3]]}},"alternative-id":["10.1145\/2665076"],"URL":"https:\/\/doi.org\/10.1145\/2665076","relation":{},"ISSN":["1529-3785","1557-945X"],"issn-type":[{"type":"print","value":"1529-3785"},{"type":"electronic","value":"1557-945X"}],"subject":[],"published":{"date-parts":[[2014,12,23]]},"assertion":[{"value":"2013-11-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2014-08-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2014-12-23","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}