{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T09:57:31Z","timestamp":1776333451469,"version":"3.51.2"},"reference-count":73,"publisher":"Association for Computing Machinery (ACM)","issue":"2","license":[{"start":{"date-parts":[[2017,4,30]],"date-time":"2017-04-30T00:00:00Z","timestamp":1493510400000},"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":["J. ACM"],"published-print":{"date-parts":[[2017,4,30]]},"abstract":"<jats:p>\n            Monadic predicates play a prominent role in many decidable cases, including decision procedures for symbolic automata. We are here interested in\n            <jats:italic>discovering<\/jats:italic>\n            whether a formula can be rewritten into a Boolean combination of monadic predicates. Our setting is quantifier-free formulas whose satisfiability is decidable, such as linear arithmetic. Here we develop a semidecision procedure for extracting a monadic decomposition of a formula when it exists.\n          <\/jats:p>","DOI":"10.1145\/3040488","type":"journal-article","created":{"date-parts":[[2017,5,1]],"date-time":"2017-05-01T14:55:23Z","timestamp":1493650523000},"page":"1-28","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":11,"title":["Monadic Decomposition"],"prefix":"10.1145","volume":"64","author":[{"given":"Margus","family":"Veanes","sequence":"first","affiliation":[{"name":"Microsoft Research, Redmond, WA, USA"}]},{"given":"Nikolaj","family":"Bj\u00f8rner","sequence":"additional","affiliation":[{"name":"Microsoft Research, Redmond, WA, USA"}]},{"given":"Lev","family":"Nachmanson","sequence":"additional","affiliation":[{"name":"Microsoft Research, Redmond, WA, USA"}]},{"given":"Sergey","family":"Bereg","sequence":"additional","affiliation":[{"name":"The University of Texas at Dallas, Richardson, TX, USA"}]}],"member":"320","published-online":{"date-parts":[[2017,4,30]]},"reference":[{"key":"e_1_2_1_1_1","volume-title":"Ullman","author":"Aho Alfred V.","year":"2006","unstructured":"Alfred V. Aho , Monica S. Lam , Ravi Sethi , and Jeffrey D . Ullman . 2006 . Compilers : Principles, Techniques, and Tools (2nd ed.). Addison Wesley . Alfred V. Aho, Monica S. Lam, Ravi Sethi, and Jeffrey D. Ullman. 2006. Compilers: Principles, Techniques, and Tools (2nd ed.). Addison Wesley."},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1004275029985"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1016\/B978-044450813-3\/50007-2"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.5555\/2032305.2032319"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/876638.876642"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-4(1:8)2008"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0305004100013463"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-59207-2"},{"key":"e_1_2_1_9_1","volume-title":"Symbolic learning of input-output specifications. ACM SIGPLAN Notices (POPL\u201913) 48, 1","author":"Botincan Matko","year":"2013","unstructured":"Matko Botincan and Domagoj Babic . 2013. Sigma* : Symbolic learning of input-output specifications. ACM SIGPLAN Notices (POPL\u201913) 48, 1 ( 2013 ), 443--456. Matko Botincan and Domagoj Babic. 2013. Sigma*: Symbolic learning of input-output specifications. ACM SIGPLAN Notices (POPL\u201913) 48, 1 (2013), 443--456."},{"key":"e_1_2_1_10_1","series-title":"Lecture Notes in Computer Science","volume-title":"Sipma","author":"Bradley Aaron R.","year":"2006","unstructured":"Aaron R. Bradley , Zohar Manna , and Henny B . Sipma . 2006 . What\u2019s decidable about arrays? In Proceedings of the 7th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI\u2019 06), Lecture Notes in Computer Science , Vol. 3855 . 427--442. Aaron R. Bradley, Zohar Manna, and Henny B. Sipma. 2006. What\u2019s decidable about arrays? In Proceedings of the 7th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI\u201906), Lecture Notes in Computer Science, Vol. 3855. 427--442."},{"key":"e_1_2_1_11_1","volume-title":"Methodology and Philosophy of Science (Proc. 1960 Internat. Congr.), E. Nagel, P. Suppes, and A. Tarski (Eds.)","author":"B\u00fcchi Julius Richard","year":"1962","unstructured":"Julius Richard B\u00fcchi . 1962 . On a decision method in restricted second order arithmetic. In Logic , Methodology and Philosophy of Science (Proc. 1960 Internat. Congr.), E. Nagel, P. Suppes, and A. Tarski (Eds.) . Stanford University Press, 1--11. Julius Richard B\u00fcchi. 1962. On a decision method in restricted second order arithmetic. In Logic, Methodology and Philosophy of Science (Proc. 1960 Internat. Congr.), E. Nagel, P. Suppes, and A. Tarski (Eds.). Stanford University Press, 1--11."},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1051\/ita:2006005"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1109\/TKDE.2003.1245282"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0020-0190(00)00184-8"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-35873-9_14"},{"key":"e_1_2_1_16_1","volume-title":"Minimization of symbolic automata. ACM SIGPLAN Notices - POPL\u201914 49, 1","author":"D\u2019Antoni Loris","year":"2014","unstructured":"Loris D\u2019Antoni and Margus Veanes . 2014. Minimization of symbolic automata. ACM SIGPLAN Notices - POPL\u201914 49, 1 ( 2014 ), 541--553. Loris D\u2019Antoni and Margus Veanes. 2014. Minimization of symbolic automata. ACM SIGPLAN Notices - POPL\u201914 49, 1 (2014), 541--553."},{"key":"e_1_2_1_17_1","volume-title":"Extended symbolic finite automata and transducers. Formal Methods in System Design (July","author":"D\u2019Antoni Loris","year":"2015","unstructured":"Loris D\u2019Antoni and Margus Veanes . 2015. Extended symbolic finite automata and transducers. Formal Methods in System Design (July 2015 ). Loris D\u2019Antoni and Margus Veanes. 2015. Extended symbolic finite automata and transducers. Formal Methods in System Design (July 2015)."},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009844"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/1995376.1995394"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1016\/0020-0190(79)90071-1"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(82)90026-3"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1016\/B978-044450813-3\/50011-4"},{"key":"e_1_2_1_24_1","series-title":"Lecture Notes in Computer Science","volume-title":"Computer-Aided Verification (CAV\u201914)","author":"Dutertre Bruno","unstructured":"Bruno Dutertre . 2014. Yices 2.2. In Computer-Aided Verification (CAV\u201914) , Lecture Notes in Computer Science , Vol. 8559 , Armin Biere and Roderick Bloem (Eds.). Springer , 737--744. Bruno Dutertre. 2014. Yices 2.2. In Computer-Aided Verification (CAV\u201914), Lecture Notes in Computer Science, Vol. 8559, Armin Biere and Roderick Bloem (Eds.). Springer, 737--744."},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1147\/rd.91.0047"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.4064\/fm-47-1-57-103"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-0-387-09680-3_29"},{"key":"e_1_2_1_28_1","volume-title":"Rabin","author":"Fischer Michael J.","year":"1974","unstructured":"Michael J. Fischer and Michael O . Rabin . 1974 . Super-exponential complexity of Presburger arithmetic. In SIAMAMS : Complexity of Computation: Proceedings of a Symposium in Applied Mathematics of the American Mathematical Society and the Society for Industrial and Applied Mathematics. 27--41. Michael J. Fischer and Michael O. Rabin. 1974. Super-exponential complexity of Presburger arithmetic. In SIAMAMS: Complexity of Computation: Proceedings of a Symposium in Applied Mathematics of the American Mathematical Society and the Society for Industrial and Applied Mathematics. 27--41."},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-27813-9_14"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1999.782582"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10472-009-9153-6"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.2307\/2586808"},{"key":"e_1_2_1_33_1","first-page":"90","article-title":"Why are modal logics so robustly decidable","volume":"68","author":"Gr\u00e4del Erich","year":"1999","unstructured":"Erich Gr\u00e4del . 1999 . Why are modal logics so robustly decidable ? Bulletin EATCS 68 (1999), 90 -- 103 . Erich Gr\u00e4del. 1999. Why are modal logics so robustly decidable? Bulletin EATCS 68 (1999), 90--103.","journal-title":"Bulletin EATCS"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/276304.276324"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0022481200051513"},{"key":"e_1_2_1_36_1","volume-title":"Monadic second-order theories","author":"Gurevich Yuri","unstructured":"Yuri Gurevich . 1985. Monadic second-order theories . In Model-Theoretical Logics, Jon Barwise and Sol Feferman (Eds.). Springer , Chapter XIII, 479--506. Yuri Gurevich. 1985. Monadic second-order theories. In Model-Theoretical Logics, Jon Barwise and Sol Feferman (Eds.). Springer, Chapter XIII, 479--506."},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/359657.359666"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.7146\/brics.v2i21.19923"},{"key":"e_1_2_1_39_1","volume-title":"Proceedings of the USENIX Security Symposium.","author":"Hooimeijer Pieter","year":"2011","unstructured":"Pieter Hooimeijer , Benjamin Livshits , David Molnar , Prateek Saxena , and Margus Veanes . 2011 . Fast and precise sanitizer analysis with Bek . In Proceedings of the USENIX Security Symposium. Pieter Hooimeijer, Benjamin Livshits, David Molnar, Prateek Saxena, and Margus Veanes. 2011. Fast and precise sanitizer analysis with Bek. In Proceedings of the USENIX Security Symposium."},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-18275-4_18"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1142\/S012905410200128X"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02959-2_14"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-37651-1_10"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-44199-2_47"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1090\/S0002-9947-1960-0111704-1"},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/322217.322232"},{"key":"e_1_2_1_47_1","volume-title":"Technical Report ATP-32","author":"Lankford Dallas S.","unstructured":"Dallas S. Lankford . 1975. Canonical Inference . Technical Report ATP-32 . Southwestern University . Dallas S. Lankford. 1975. Canonical Inference. Technical Report ATP-32. Southwestern University."},{"key":"e_1_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/937555.937557"},{"key":"e_1_2_1_49_1","first-page":"563","article-title":"Decidability of the monadic predicate calculus with unary function symbols","volume":"32","author":"L\u00f6b Martin","year":"1967","unstructured":"Martin L\u00f6b . 1967 . Decidability of the monadic predicate calculus with unary function symbols . Journal of Symbolic Logic 32 (1967), 563 . Martin L\u00f6b. 1967. Decidability of the monadic predicate calculus with unary function symbols. Journal of Symbolic Logic 32 (1967), 563.","journal-title":"Journal of Symbolic Logic"},{"key":"e_1_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01458217"},{"key":"e_1_2_1_51_1","unstructured":"Anatoli Mal\u2019cev. 1971. The Metamathematics of Algebraic Systems. North-Holland.  Anatoli Mal\u2019cev. 1971. The Metamathematics of Algebraic Systems. North-Holland."},{"key":"e_1_2_1_52_1","volume-title":"Data-parallel finite-state machines. ACM SIGPLAN Notices - ASPLOS\u201914 49, 4","author":"Mytkowicz Todd","year":"2014","unstructured":"Todd Mytkowicz , Madanlal Musuvathi , and Wolfram Schulte . 2014. Data-parallel finite-state machines. ACM SIGPLAN Notices - ASPLOS\u201914 49, 4 ( 2014 ), 529--542. Todd Mytkowicz, Madanlal Musuvathi, and Wolfram Schulte. 2014. Data-parallel finite-state machines. ACM SIGPLAN Notices - ASPLOS\u201914 49, 4 (2014), 529--542."},{"key":"e_1_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/357073.357079"},{"key":"e_1_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/322186.322198"},{"key":"e_1_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.1007\/11601524_14"},{"key":"e_1_2_1_56_1","volume-title":"Principles of Program Analysis","author":"Nielson Flemming","unstructured":"Flemming Nielson , Hanne R. Nielson , and Chris Hankin . 2010. Principles of Program Analysis . Springer . Flemming Nielson, Hanne R. Nielson, and Chris Hankin. 2010. Principles of Program Analysis. Springer."},{"key":"e_1_2_1_57_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71070-7_3"},{"key":"e_1_2_1_58_1","doi-asserted-by":"publisher","DOI":"10.5802\/aif.287"},{"key":"e_1_2_1_59_1","volume-title":"Comptes Rendus du I congr\u00e9s de Math\u00e9maticiens des Pays Slaves.","author":"Presburger Mojzesz","unstructured":"Mojzesz Presburger . 1929. \u00dcber die Vollst\u00e4ndigkeit eines gewissen systems der arithmetik ganzer zahlen, in welchem die addition als einzige operation hervortritt . In Comptes Rendus du I congr\u00e9s de Math\u00e9maticiens des Pays Slaves. Warsaw, Poland , 92--101. Mojzesz Presburger. 1929. \u00dcber die Vollst\u00e4ndigkeit eines gewissen systems der arithmetik ganzer zahlen, in welchem die addition als einzige operation hervortritt. In Comptes Rendus du I congr\u00e9s de Math\u00e9maticiens des Pays Slaves. Warsaw, Poland, 92--101."},{"key":"e_1_2_1_60_1","first-page":"1","article-title":"Decidability of second-order theories and automata on infinite trees","volume":"141","author":"Rabin Michael O.","year":"1969","unstructured":"Michael O. Rabin . 1969 . Decidability of second-order theories and automata on infinite trees . Transactions of the American Mathematical Society 141 (1969), 1 -- 35 . Michael O. Rabin. 1969. Decidability of second-order theories and automata on infinite trees. Transactions of the American Mathematical Society 141 (1969), 1--35.","journal-title":"Transactions of the American Mathematical Society"},{"key":"e_1_2_1_61_1","doi-asserted-by":"publisher","DOI":"10.1145\/800133.804361"},{"key":"e_1_2_1_62_1","doi-asserted-by":"publisher","DOI":"10.1090\/S0002-9947-1953-0053041-6"},{"key":"e_1_2_1_63_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1999.2792"},{"key":"e_1_2_1_64_1","volume-title":"Handbook of Formal Languages.","author":"Thomas Wolfgang","unstructured":"Wolfgang Thomas . 1996. Languages , automata, and logic . In Handbook of Formal Languages. Vol. 3 . Springer , 389--455. Wolfgang Thomas. 1996. Languages, automata, and logic. In Handbook of Formal Languages. Vol. 3. Springer, 389--455."},{"key":"e_1_2_1_65_1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511525919"},{"key":"e_1_2_1_66_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1012291501330"},{"key":"e_1_2_1_67_1","volume-title":"Neil Immerman and Phokion G. Kolaitis (Eds.)","volume":"31","author":"Vardi Moshe Y.","year":"1996","unstructured":"Moshe Y. Vardi . 1996 . Why is modal logic so robustly decidable? In Descriptive Complexity and Finite Models (DIMACS Series in Discrete Mathematics and Theoretical Computer Science) , Neil Immerman and Phokion G. Kolaitis (Eds.) , Vol. 31 . American Mathematical Society, 149--184. Moshe Y. Vardi. 1996. Why is modal logic so robustly decidable? In Descriptive Complexity and Finite Models (DIMACS Series in Discrete Mathematics and Theoretical Computer Science), Neil Immerman and Phokion G. Kolaitis (Eds.), Vol. 31. American Mathematical Society, 149--184."},{"key":"e_1_2_1_68_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28756-5_33"},{"key":"e_1_2_1_69_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-16242-8_45"},{"key":"e_1_2_1_70_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_42"},{"key":"e_1_2_1_71_1","doi-asserted-by":"crossref","unstructured":"Margus Veanes Pieter Hooimeijer Benjamin Livshits David Molnar and Nikolaj Bj\u00f8rner. 2012. Symbolic finite state transducers: Algorithms and applications. In POPL\u201912. 137--150.  Margus Veanes Pieter Hooimeijer Benjamin Livshits David Molnar and Nikolaj Bj\u00f8rner. 2012. Symbolic finite state transducers: Algorithms and applications. In POPL\u201912. 137--150.","DOI":"10.1145\/2103621.2103674"},{"key":"e_1_2_1_72_1","volume-title":"Data-parallel string-manipulating programs. ACM SIGPLAN Notices - POPL\u201915 50, 1","author":"Veanes Margus","year":"2015","unstructured":"Margus Veanes , Todd Mytkowicz , David Molnar , and Benjamin Livshits . 2015. Data-parallel string-manipulating programs. ACM SIGPLAN Notices - POPL\u201915 50, 1 ( 2015 ), 139--152. Margus Veanes, Todd Mytkowicz, David Molnar, and Benjamin Livshits. 2015. Data-parallel string-manipulating programs. ACM SIGPLAN Notices - POPL\u201915 50, 1 (2015), 139--152."},{"key":"e_1_2_1_73_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-59136-5_2"}],"container-title":["Journal of the ACM"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3040488","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3040488","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T03:50:38Z","timestamp":1750218638000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3040488"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,4,30]]},"references-count":73,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2017,4,30]]}},"alternative-id":["10.1145\/3040488"],"URL":"https:\/\/doi.org\/10.1145\/3040488","relation":{},"ISSN":["0004-5411","1557-735X"],"issn-type":[{"value":"0004-5411","type":"print"},{"value":"1557-735X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017,4,30]]},"assertion":[{"value":"2016-01-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2017-02-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2017-04-30","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}