| HAL-Inria | Publications, software ... of Inria's scientists |
Conference papers
Capturing Bisimulation-Invariant Complexity Classes with Higher-Order Modal Fixpoint Logic
Abstract : Polyadic Higher-Order Fixpoint Logic (PHFL) is a modal fixpoint logic obtained as the merger of Higher-Order Fixpoint Logic (HFL) and the Polyadic μ-Calculus. Polyadicity enables formulas to make assertions about tuples of states rather than states only. Like HFL, PHFL has the ability to formalise properties using higher-order functions. We consider PHFL in the setting of descriptive complexity theory: its fragment using no functions of higher-order is exactly the Polyadic μ-Calculus, and it is known from Otto’s Theorem that it captures the bisimulation-invariant fragment of PTIME. We extend this and give capturing results for the bisimulation-invariant fragments of EXPTIME, PSPACE, and NLOGSPACE.
Cited literature [20 references]
https://hal.inria.fr/hal-01402031
Contributor : Hal Ifip <>
Submitted on : Thursday, November 24, 2016 - 10:48:52 AM
Last modification on : Tuesday, November 13, 2018 - 11:50:04 AM
Long-term archiving on: : Tuesday, March 21, 2017 - 8:36:28 AM
Contributor : Hal Ifip <>
Submitted on : Thursday, November 24, 2016 - 10:48:52 AM
Last modification on : Tuesday, November 13, 2018 - 11:50:04 AM
Long-term archiving on: : Tuesday, March 21, 2017 - 8:36:28 AM
File
978-3-662-44602-7_8_Chapter.pd...
Files produced by the author(s)
Licence
Distributed under a Creative Commons Attribution 4.0 International License