{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,1]],"date-time":"2025-12-01T02:46:31Z","timestamp":1764557191706,"version":"3.41.2"},"reference-count":0,"publisher":"Centre pour la Communication Scientifique Directe (CCSD)","license":[{"start":{"date-parts":[[2007,6,29]],"date-time":"2007-06-29T00:00:00Z","timestamp":1183075200000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/arxiv.org\/licenses\/assumed-1991-2003"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"<jats:p>Higher-Order Fixpoint Logic (HFL) is a hybrid of the simply typed\n\\lambda-calculus and the modal \\lambda-calculus. This makes it a highly\nexpressive temporal logic that is capable of expressing various interesting\ncorrectness properties of programs that are not expressible in the modal\n\\lambda-calculus.\n  This paper provides complexity results for its model checking problem. In\nparticular we consider those fragments of HFL built by using only types of\nbounded order k and arity m. We establish k-fold exponential time completeness\nfor model checking each such fragment. For the upper bound we use fixpoint\nelimination to obtain reachability games that are singly-exponential in the\nsize of the formula and k-fold exponential in the size of the underlying\ntransition system. These games can be solved in deterministic linear time. As a\nsimple consequence, we obtain an exponential time upper bound on the expression\ncomplexity of each such fragment.\n  The lower bound is established by a reduction from the word problem for\nalternating (k-1)-fold exponential space bounded Turing Machines. Since there\nare fixed machines of that type whose word problems are already hard with\nrespect to k-fold exponential time, we obtain, as a corollary, k-fold\nexponential time completeness for the data complexity of our fragments of HFL,\nprovided m exceeds 3. This also yields a hierarchy result in expressive power.<\/jats:p>","DOI":"10.2168\/lmcs-3(2:7)2007","type":"journal-article","created":{"date-parts":[[2008,6,3]],"date-time":"2008-06-03T15:00:09Z","timestamp":1212505209000},"source":"Crossref","is-referenced-by-count":17,"title":["The Complexity of Model Checking Higher-Order Fixpoint Logic"],"prefix":"10.46298","volume":"Volume 3, Issue 2","author":[{"given":"Roland","family":"Axelsson","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1621-0972","authenticated-orcid":false,"given":"Martin","family":"Lange","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Rafal","family":"Somla","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"25203","published-online":{"date-parts":[[2007,6,29]]},"container-title":["Logical Methods in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/lmcs.episciences.org\/754\/pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/lmcs.episciences.org\/754\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,4,11]],"date-time":"2023-04-11T19:55:22Z","timestamp":1681242922000},"score":1,"resource":{"primary":{"URL":"https:\/\/lmcs.episciences.org\/754"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2007,6,29]]},"references-count":0,"URL":"https:\/\/doi.org\/10.2168\/lmcs-3(2:7)2007","relation":{"is-same-as":[{"id-type":"arxiv","id":"0704.3931","asserted-by":"subject"},{"id-type":"doi","id":"10.48550\/arXiv.0704.3931","asserted-by":"subject"}]},"ISSN":["1860-5974"],"issn-type":[{"type":"electronic","value":"1860-5974"}],"subject":[],"published":{"date-parts":[[2007,6,29]]},"article-number":"754"}}