Dissertation
Extremal Fixpoints for Higher-Order Modal Logic
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.
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.
Citation
@phdthesis{doi:10.17170/kobra-202008091547,
author={Bruse, Florian},
title={Extremal Fixpoints for Higher-Order Modal Logic},
school={Kassel, Universität Kassel, Fachbereich Elektrotechnik / Informatik},
month={10},
year={2018}
}
0500 Oax 0501 Text $btxt$2rdacontent 0502 Computermedien $bc$2rdacarrier 1100 2018$n2018 1500 1/eng 2050 ##0##http://hdl.handle.net/123456789/11681 3000 Bruse, Florian 4000 Extremal Fixpoints for Higher-Order Modal Logic / Bruse, Florian 4030 4060 Online-Ressource 4085 ##0##=u http://nbn-resolving.de/http://hdl.handle.net/123456789/11681=x R 4204 \$dDissertation 4170 5550 {{Logik}} 5550 {{Modallogik}} 5550 {{Modelltheorie}} 5550 {{Automatentheorie}} 7136 ##0##http://hdl.handle.net/123456789/11681
2020-08-12T06:20:01Z 2020-08-12T06:20:01Z 2018-10 doi:10.17170/kobra-202008091547 http://hdl.handle.net/123456789/11681 eng Attribution-NonCommercial-NoDerivatives 4.0 International http://creativecommons.org/licenses/by-nc-nd/4.0/ Modal Logics Higher-Order Logic Automata Theory 004 Extremal Fixpoints for Higher-Order Modal Logic Dissertation 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. open access Bruse, Florian 2018-11-23 viii, 198 Seiten Kassel, Universität Kassel, Fachbereich Elektrotechnik / Informatik Lange, Martin (Prof. Dr.) Hague, Matthew (Prof. Dr.) Logik Modallogik Modelltheorie Automatentheorie publishedVersion false
The following license files are associated with this item: