Dissertation![](/themes/Mirage2/images/Open_Access_logo_PLoS_transparent.svg)
Hybrid Branching-Time Logics
Abstract
We introduce and study an extension of the well-known and well-studied branching-time logics CTL, CTL+, FCTL+, CTL* and the modal μ-calculus with the so called "hybrid framework". This framework borrows ideas from first-order logic to enable more precise "structural" reasoning which is known to be impossible in the original logics. In particular, the extension with this framework enables these logics to uniquely name, reference and test for certain states, similarly to the concepts of variables and constants in first-order logic.
We especially study the decision procedures of these new hybrid branching-time logics -- especially their model checking problems -- and develop their model theory based on the already well-established model theory of the underlying branching-time logics.
We establish a hybrid branching-time hierarchy that ranks these new hybrid branching-time logics with respect to their expressive power and in doing so provide a clear understanding of what can and cannot be expressed in any of these logics and also characterise some of the limits of their expressive power.
Also, we present a complete analysis of the respective model checking problems of these hybrid branching-time logics. We present model checking algorithms, analyse their complexity and provide matching lower bounds showing that our algorithms are optimal from a complexity-theoretical point of view. Mostly, the model checking problems of the hybrid logics tend to have a slightly harder model checking problem than their non-hybrid counterparts with some exceptions like HCTL*ss which only has a PSPACE-complete model checking problem -- the same complexity as for CTL*.
We also show that this increase in computational complexity mostly comes from the unbounded use of names and disappears if we limit the number of names that can be used.
Lastly, we show that all these hybrid logics have an undecidable satisfiability problem and provide some still decidable fragments of these hybrid branching-time logics.
We especially study the decision procedures of these new hybrid branching-time logics -- especially their model checking problems -- and develop their model theory based on the already well-established model theory of the underlying branching-time logics.
We establish a hybrid branching-time hierarchy that ranks these new hybrid branching-time logics with respect to their expressive power and in doing so provide a clear understanding of what can and cannot be expressed in any of these logics and also characterise some of the limits of their expressive power.
Also, we present a complete analysis of the respective model checking problems of these hybrid branching-time logics. We present model checking algorithms, analyse their complexity and provide matching lower bounds showing that our algorithms are optimal from a complexity-theoretical point of view. Mostly, the model checking problems of the hybrid logics tend to have a slightly harder model checking problem than their non-hybrid counterparts with some exceptions like HCTL*ss which only has a PSPACE-complete model checking problem -- the same complexity as for CTL*.
We also show that this increase in computational complexity mostly comes from the unbounded use of names and disappears if we limit the number of names that can be used.
Lastly, we show that all these hybrid logics have an undecidable satisfiability problem and provide some still decidable fragments of these hybrid branching-time logics.
Citation
@phdthesis{doi:10.17170/kobra-20191209834,
author={Kernberger, Daniel},
title={Hybrid Branching-Time Logics},
school={Kassel, Universität Kassel, Fachbereich Elektrotechnik / Informatik},
year={2019}
}
0500 Oax 0501 Text $btxt$2rdacontent 0502 Computermedien $bc$2rdacarrier 1100 2019$n2019 1500 1/eng 2050 ##0##http://hdl.handle.net/123456789/11380 3000 Kernberger, Daniel 4000 Hybrid Branching-Time Logics / Kernberger, Daniel 4030 4060 Online-Ressource 4085 ##0##=u http://nbn-resolving.de/http://hdl.handle.net/123456789/11380=x R 4204 \$dDissertation 4170 5550 {{Temporale Logik}} 5550 {{Framework <Informatik>}} 5550 {{My-Kalkül}} 7136 ##0##http://hdl.handle.net/123456789/11380
2019-12-09T17:38:23Z 2019-12-09T17:38:23Z 2019 doi:10.17170/kobra-20191209834 http://hdl.handle.net/123456789/11380 eng Namensnennung - Nicht-kommerziell - Weitergabe unter gleichen Bedingungen 3.0 Deutschland Namensnennung - Nicht-kommerziell - Weitergabe unter gleichen Bedingungen 3.0 Deutschland http://creativecommons.org/licenses/by-nc-sa/3.0/de/ 004 Hybrid Branching-Time Logics Dissertation We introduce and study an extension of the well-known and well-studied branching-time logics CTL, CTL+, FCTL+, CTL* and the modal μ-calculus with the so called "hybrid framework". This framework borrows ideas from first-order logic to enable more precise "structural" reasoning which is known to be impossible in the original logics. In particular, the extension with this framework enables these logics to uniquely name, reference and test for certain states, similarly to the concepts of variables and constants in first-order logic. We especially study the decision procedures of these new hybrid branching-time logics -- especially their model checking problems -- and develop their model theory based on the already well-established model theory of the underlying branching-time logics. We establish a hybrid branching-time hierarchy that ranks these new hybrid branching-time logics with respect to their expressive power and in doing so provide a clear understanding of what can and cannot be expressed in any of these logics and also characterise some of the limits of their expressive power. Also, we present a complete analysis of the respective model checking problems of these hybrid branching-time logics. We present model checking algorithms, analyse their complexity and provide matching lower bounds showing that our algorithms are optimal from a complexity-theoretical point of view. Mostly, the model checking problems of the hybrid logics tend to have a slightly harder model checking problem than their non-hybrid counterparts with some exceptions like HCTL*ss which only has a PSPACE-complete model checking problem -- the same complexity as for CTL*. We also show that this increase in computational complexity mostly comes from the unbounded use of names and disappears if we limit the number of names that can be used. Lastly, we show that all these hybrid logics have an undecidable satisfiability problem and provide some still decidable fragments of these hybrid branching-time logics. open access Kernberger, Daniel 2019-10-31 xii, 213 Seiten Kassel, Universität Kassel, Fachbereich Elektrotechnik / Informatik Lange, Martin (Prof. Dr.) Schneider, Thomas (Prof. Dr.) Temporale Logik Framework <Informatik> My-Kalkül publishedVersion
The following license files are associated with this item: