2021/11/15 by Eugenia Ternovska, Ternovska, Eugenia
Computer Science · #Advanced Algebra and Logic #FOS: Computer and information sciences #Formal Methods in Verification #Fuzzy Logic and Control Systems #Logic in Computer Science (cs.LO) #Logic, Reasoning, and Knowledge #Logic, programming, and type systems #Speech and dialogue systems
paper · pdf · doi:10.48550/arxiv.2111.07978
openalex publication_date 2021/11/15 · openalex created_date 2022/07/25 · openalex updated_date 2026/07/28
The central open question in Descriptive Complexity is whether there is a\nlogic that characterizes deterministic polynomial time (PTIME) on relational\nstructures. Towards this goal, we define a logic that is obtained from\nfirst-order logic with fixed points, FO(FP), by a series of transformations\nthat include restricting logical connectives and adding a dynamic version of\nHilbert's Choice operator Epsilon. The formalism can be viewed, simultaneously,\nas an algebra of binary relations and as a linear-time modal dynamic logic,\nwhere algebraic expressions describing ``proofs'' or ``programs'' appear inside\nthe modalities. We show how counting, reachability and ``mixed'' examples (that\ninclude linear equations modulo two) are axiomatized in the logic, and how an\narbitrary PTIME Turing machine can be encoded. For each fixed Choice function,\nthe data complexity of model checking is in PTIME. However, there can be\nexponentially many such functions. A crucial question is under what syntactic\nconditions on algebraic terms checking just one Choice function is sufficient.\nAnswering this question requires a study of symmetries among computations. This\npaper sets mathematical foundations towards such a study via algebraic and\nautomata-theoretic techniques.\n