{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,14]],"date-time":"2025-10-14T11:28:34Z","timestamp":1760441314951,"version":"3.41.0"},"reference-count":20,"publisher":"Association for Computing Machinery (ACM)","issue":"2","license":[{"start":{"date-parts":[[2015,11,25]],"date-time":"2015-11-25T00:00:00Z","timestamp":1448409600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"ERC Starting Grant","award":["239962"],"award-info":[{"award-number":["239962"]}]},{"DOI":"10.13039\/501100002428","name":"FWF Austrian Science Fund","doi-asserted-by":"crossref","award":["P26200"],"award-info":[{"award-number":["P26200"]}],"id":[{"id":"10.13039\/501100002428","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Comput. Logic"],"published-print":{"date-parts":[[2016,3,28]]},"abstract":"<jats:p>We study the problem of checking whether an existential sentence (i.e., a first-order sentence in prefix form built using existential quantifiers and all Boolean connectives) is true in a finite partially ordered set (a poset). A poset is a reflexive, antisymmetric, and transitive digraph. The problem encompasses the fundamental embedding problem of finding an isomorphic copy of a poset as an induced substructure of another poset.<\/jats:p>\n          <jats:p>Model checking existential logic is already NP-hard on a fixed poset; thus, we investigate structural properties of posets yielding conditions for fixed-parameter tractability when the problem is parameterized by the sentence. We identify width as a central structural property (the width of a poset is the maximum size of a subset of pairwise incomparable elements); our main algorithmic result is that model checking existential logic on classes of finite posets of bounded width is fixed-parameter tractable. We observe a similar phenomenon in classical complexity, in which we prove that the isomorphism problem is polynomial-time tractable on classes of posets of bounded width; this settles an open problem in order theory.<\/jats:p>\n          <jats:p>We surround our main algorithmic result with complexity results on less restricted, natural neighboring classes of finite posets, establishing its tightness in this sense. We also relate our work with (and demonstrate its independence of) fundamental fixed-parameter tractability results for model checking on digraphs of bounded degree and bounded clique-width.<\/jats:p>","DOI":"10.1145\/2814937","type":"journal-article","created":{"date-parts":[[2015,11,30]],"date-time":"2015-11-30T19:03:44Z","timestamp":1448910224000},"page":"1-35","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":5,"title":["Model Checking Existential Logic on Partially Ordered Sets"],"prefix":"10.1145","volume":"17","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-1069-7257","authenticated-orcid":false,"given":"Simone","family":"Bova","sequence":"first","affiliation":[{"name":"Algorithms and Complexity Group, TU Wien, Vienna, Austria"}]},{"given":"Robert","family":"Ganian","sequence":"additional","affiliation":[{"name":"Algorithms and Complexity Group, TU Wien, Vienna, Austria"}]},{"given":"Stefan","family":"Szeider","sequence":"additional","affiliation":[{"name":"Algorithms and Complexity Group, TU Wien, Vienna, Austria"}]}],"member":"320","published-online":{"date-parts":[[2015,11,25]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/210332.210337"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1215\/S0012-7094-37-00334-X"},{"volume-title":"Finite Ordered Sets -- Concepts, Results and Uses","author":"Caspard Nathalie","key":"e_1_2_1_3_1","unstructured":"Nathalie Caspard , Bruno Leclerc , and Bernard Monjardet . 2012. Finite Ordered Sets -- Concepts, Results and Uses . Cambridge University Press , New York, NY . Nathalie Caspard, Bruno Leclerc, and Bernard Monjardet. 2012. Finite Ordered Sets -- Concepts, Results and Uses. Cambridge University Press, New York, NY."},{"volume-title":"Graph Structure and Monadic Second-Order Logic -- A Language-Theoretic Approach","author":"Courcelle Bruno","key":"e_1_2_1_4_1","unstructured":"Bruno Courcelle and Joost Engelfriet . 2012. Graph Structure and Monadic Second-Order Logic -- A Language-Theoretic Approach . Cambridge University Press , New York, NY . Bruno Courcelle and Joost Engelfriet. 2012. Graph Structure and Monadic Second-Order Logic -- A Language-Theoretic Approach. Cambridge University Press, New York, NY."},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/s002249910009"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0166-218X(99)00184-5"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1137\/S0097539794266766"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1023\/B:ORDE.0000034609.99940.fb"},{"volume-title":"Parameterized Complexity Theory","author":"Flum J\u00f6rg","key":"e_1_2_1_9_1","unstructured":"J\u00f6rg Flum and Martin Grohe . 2006. Parameterized Complexity Theory . Springer Verlag , Berlin . J\u00f6rg Flum and Martin Grohe. 2006. Parameterized Complexity Theory. Springer Verlag, Berlin."},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00403406"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01182098"},{"key":"e_1_2_1_12_1","series-title":"Vol. 1","volume-title":"Handbook of Combinatorics","author":"Graham Ronald L.","unstructured":"Ronald L. Graham , Martin Gr\u00f6tschel , and L\u00e1szl\u00f3 Lov\u00e1sz . 1995. Handbook of Combinatorics ( Vol. 1 ) . MIT Press , Cambridge, MA . Ronald L. Graham, Martin Gr\u00f6tschel, and L\u00e1szl\u00f3 Lov\u00e1sz. 1995. Handbook of Combinatorics (Vol. 1). MIT Press, Cambridge, MA."},{"key":"e_1_2_1_13_1","unstructured":"Martin Grohe. 2007. Logic graphs and algorithms. In Electronic Colloquium on Computational Complexity. TR--07--091.  Martin Grohe. 2007. Logic graphs and algorithms. In Electronic Colloquium on Computational Complexity. TR--07--091."},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/2591796.2591851"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/263867.263489"},{"key":"e_1_2_1_16_1","volume-title":"Hanne Riis Nielson, and Chris Hankin","author":"Nielson Flemming","year":"2005","unstructured":"Flemming Nielson , Hanne Riis Nielson, and Chris Hankin . 2005 . Principles of Program Analysis. Springer . Flemming Nielson, Hanne Riis Nielson, and Chris Hankin. 2005. Principles of Program Analysis. Springer."},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.5555\/2379577.2379588"},{"volume-title":"Problem Solving Handbook in Computational Biology and Bioinformatics","author":"Rausch Tobias","key":"e_1_2_1_18_1","unstructured":"Tobias Rausch and Knut Reinert . 2010. Problem Solving Handbook in Computational Biology and Bioinformatics . Springer . Tobias Rausch and Knut Reinert. 2010. Problem Solving Handbook in Computational Biology and Bioinformatics. Springer."},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-0053-6"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129500070079"}],"container-title":["ACM Transactions on Computational Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2814937","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2814937","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T05:07:38Z","timestamp":1750223258000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2814937"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,11,25]]},"references-count":20,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2016,3,28]]}},"alternative-id":["10.1145\/2814937"],"URL":"https:\/\/doi.org\/10.1145\/2814937","relation":{},"ISSN":["1529-3785","1557-945X"],"issn-type":[{"type":"print","value":"1529-3785"},{"type":"electronic","value":"1557-945X"}],"subject":[],"published":{"date-parts":[[2015,11,25]]},"assertion":[{"value":"2014-09-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2015-08-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2015-11-25","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}