The Complexity of Model-Checking Tail-Recursive Higher-Order Fixpoint Logic

• Autorzy: Bruse Florian , Lange Martin , Lozes Etienne

Identyfikatory

DOI

10.3233/FI-2021-1996

• Języki publikacji: EN

Abstrakty

EN

Higher-Order Fixpoint Logic (HFL) is a modal specification language whose expressive power reaches far beyond that of Monadic Second-Order Logic, achieved through an incorporation of a typed λ -calculus into the modal μ -calculus. Its model checking problem on finite transition systems is decidable, albeit of high complexity, namely k -EXPTIME-complete for formulas that use functions of type order at most k > 0. In this paper we present a fragment with a presumably easier model checking problem. We show that so-called tail-recursive formulas of type order k can be model checked in (k − 1)-EXPSPACE, and also give matching lower bounds. This yields generic results for the complexity of bisimulation-invariant non-regular properties, as these can typically be defined in HFL.

Słowa kluczowe

EN

logic; finite; technical specifications; incorporation

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2021
• Tom: Vol. 178, nr 1/2
• Strony: 1--30
• Opis fizyczny: Bibliogr. 19 poz.

Twórcy

autor

Bruse Florian

• University of Kassel, Kassel, Germany

autor

Lange Martin

• University of Kassel, Kassel, Germany

autor

Lozes Etienne

• University of Nice Sophia Antipolis, I3S, CNRS, France

Bibliografia

• [1] Viswanathan M, Viswanathan R. A Higher Order Modal Fixed Point Logic. In: CONCUR’04, volume 3170 of LNCS. Springer, 2004 pp. 512-528. doi:10.1007/978-3-540-28644-8_33.
• [2] Kozen D. Results on the Propositional μ-calculus. TCS, 1983. 27:333-354. doi:10.1007/BFb0012782.
• [3] Janin D, Walukiewicz I. On the Expressive Completeness of the Propositional μ-Calculus with Respect to Monadic Second Order Logic. In: CONCUR. 1996 pp. 263-277. doi:10.1007/3-540-61604-7_60.
• [4] Lange M, Somla R. Propositional Dynamic Logic of Context-Free Programs and Fixpoint Logic with Chop. Information Processing Letters, 2006. 100(2):72-75. doi:10.1016/j.ipl.2006.04.019.
• [5] Lange M. Temporal Logics Beyond Regularity, 2007. Habilitation thesis, University of Munich, BRICS research report RS-07-13.
• [6] Axelsson R, Lange M, Somla R. The Complexity of Model Checking Higher-Order Fixpoint Logic. Logical Methods in Computer Science, 2007. 3:1-33. doi:10.2168/LMCS-3(2:7)2007.
• [7] Emerson EA. Uniform inevitability is tree automaton ineffable. Information Processing Letters, 1987. 24(2):77-79. doi:10.1016/0020-0190(87)90097-4.
• [8] Hartmanis J, Stearns RE. On the Computational Complexity of Algorithms. Trans. AMS, 1965. 117:285-306. doi:10.1090/S0002-9947-1965-0170805-7.
• [9] Andersen HR. A Polyadic Modal μ-Calculus. Technical Report ID-TR: 1994-195, Dept. of Computer Science, Technical University of Denmark, Copenhagen, 1994. doi:10.1.1.42.1859.
• [10] Otto M. Bisimulation-invariant PTIME and higher-dimensional μ-calculus. Theor. Comput. Sci., 1999. 224(1-2):237-265. doi:10.1016/S0304-3975(98)00314-4.
• [11] Lange M, Lozes É. Capturing Bisimulation-Invariant Complexity Classes with Higher-Order Modal Fixpoint Logic. In: Proc. 8th Int. IFIP Conf. on Theoretical Computer Science, TCS’14, volume 8705 of LNCS. Springer, 2014 pp. 90-103. doi:10.1007/978-3-662-44602-7.
• [12] Stearns RE, Hartmanis J, Lewis II PM. Hierarchies of memory limited computations. In: Proc. 6th Ann. Symp. on Switching Circuit Theory and Logical Design. IEEE, 1965 pp. 179-190.
• [13] Bruse F, Lange M, Lozes E. Space-Efficient Fragments of Higher-Order Fixpoint Logic. In: Proc. 11th Workshop on Reachability Problems, RP’17, volume 10506 of LNCS. Springer, 2017 pp. 26-41. doi:10.1007/978-3-319-67089-8_3.
• [14] Savitch WJ. Relationships between nondeterministic and deterministic tape complexities. Journal of Computer and System Sciences, 1970. 4:177-192.
• [15] Chandra AK, Kozen D, Stockmeyer LJ. Alternation. J. ACM, 1981. 28(1):114-133. doi:10.1145/322234.322243.
• [16] van Emde Boas P. The Convenience of Tilings. In: Sorbi A (ed.), Complexity, Logic, and Recursion Theory, volume 187 of Lecture notes in pure and applied mathematics, pp. 331-363. Marcel Dekker, Inc., 1997.
• [17] Jones ND. The expressive power of higher-order types or, life without CONS. Journal of Func. Prog., 2001. 11(1):5-94. doi:10.1017/S0956796800003889.
• [18] Axelsson R, Lange M. Model Checking the First-Order Fragment of Higher-Order Fixpoint Logic. In: Proc. 14th Int. Conf. on Logic for Programming, Artificial Intelligence, and Reasoning, LPAR’07, volume 4790 of LNCS. Springer, 2007 pp. 62-76. doi:10.1007/978-3-540-75560-9_7.
• [19] Lange M, Lozes E. Model Checking the Higher-Dimensional Modal μ-Calculus. In: Proc. 8th Workshop on Fixpoints in Computer Science, FICS’12, volume 77 of Electr. Proc. in Theor. Comp. Sc. 2012 pp. 39-46. doi:10.4204/EPTCS.77.

Uwagi

Opracowanie rekordu ze środków MNiSW, umowa Nr 461252 w ramach programu "Społeczna odpowiedzialność nauki" - moduł: Popularyzacja nauki i promocja sportu (2021).