Extremal Fixpoints for Higher-Order Modal Logic
| dc.contributor.corporatename | Kassel, Universität Kassel, Fachbereich Elektrotechnik / Informatik | |
| dc.contributor.referee | Lange, Martin (Prof. Dr.) | |
| dc.contributor.referee | Hague, Matthew (Prof. Dr.) | |
| dc.date.accessioned | 2020-08-12T06:20:01Z | |
| dc.date.available | 2020-08-12T06:20:01Z | |
| dc.date.issued | 2018-10 | |
| dc.identifier | doi:10.17170/kobra-202008091547 | |
| dc.identifier.uri | http://hdl.handle.net/123456789/11681 | |
| dc.language.iso | eng | |
| dc.rights | Attribution-NonCommercial-NoDerivatives 4.0 International | * |
| dc.rights.uri | http://creativecommons.org/licenses/by-nc-nd/4.0/ | * |
| dc.subject | Modal Logics | eng |
| dc.subject | Higher-Order Logic | eng |
| dc.subject | Automata Theory | eng |
| dc.subject.ddc | 004 | |
| dc.subject.swd | Logik | ger |
| dc.subject.swd | Modallogik | ger |
| dc.subject.swd | Modelltheorie | ger |
| dc.subject.swd | Automatentheorie | ger |
| dc.title | Extremal Fixpoints for Higher-Order Modal Logic | eng |
| dc.type | Dissertation | |
| dc.type.version | publishedVersion | |
| dcterms.abstract | In this dissertation, we investigate the interplay between extremal fixpoints and higher-order constructs. The main Focus here is Higher-Order Modal Fixpoint Logic (HFL), an extension of the modal mu-calculus by a simply typed lambda calculus. The resulting logic is very expressive, yet the interplay of its components has not been systematically investigated so far. Goal of this thesis is to characterize the interplay of the components of HFL. A first characterization is given by converting the denotational semantics of HFL into an equivalent operational semantics. The result of this is the class of so-called Alternating Parity Krivine Automata (APKA), which are an extension of the automata-theoretic counterpart of the mu-calculus, parity automata. The extension matching HFL is obtained by adding the behavior of Krivine's Machine, which computes normal forms for the simply typed lambda calculus. APKA are the first class of automata capturing the semantics of HFL over the class of all structures. This capturing result is proved in this thesis. The main challenge in designing APKA correctly is their acceptance condition. The usual parity condition, which is a standard choice for fixpoint logics, cannot adapted straightforwardly to HFL. Instead, the acceptance condition of APKA uses an additional auxiliary structure thatin the run of an APKA, separates infinite fixpoint recursion from higher-order effects. In preparation of the capturing result for APKA and HFL, this thesis also contains a model-checking game for HFL. This game also correctly captures the semantics of HFL, but has an infinite state space in general. As a second topic, in this thesis we investigate the behavior of extremal fixpoints in settings where the interaction of said fixpoints with higher-order effects is limited. Here, we investigate the so-called tail-recursive fragment of HFL, which has a lower model-checking complexity than full HFL. We give a matching model-checking algorithm for the tail-recursive fragment and prove its optimality by a matching lower bound. Moreover, we investigate questions concerning strictness of the alternation hierarchy for HFL. The first result here is a characterization of alternation classes in HFL via automata-theoretic methods. Different, syntax-based characterizations were not available. We then prove strictness of the alternation hierarchy for two fragments oF HFL, adapting a result by Arnold. This result is obtained by encoding runs of an automaton over a tree as a tree again. Strictness then follows by an invocation of the Banach Fixpoint Theorem. Finally, in another section, we investigate fragments where it is possible to reverse the polarity of a fixpoint definition. | eng |
| dcterms.accessRights | open access | |
| dcterms.creator | Bruse, Florian | |
| dcterms.dateAccepted | 2018-11-23 | |
| dcterms.extent | viii, 198 Seiten | |
| kup.iskup | false |