Date
2019Metadata
Show full item record
Dissertation
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
<resource xsi:schemaLocation="http://datacite.org/schema/kernel-2.2 http://schema.datacite.org/meta/kernel-2.2/metadata.xsd"> 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 </resource>
The following license files are associated with this item:
Except where otherwise noted, this item's license is described as Namensnennung - Nicht-kommerziell - Weitergabe unter gleichen Bedingungen 3.0 Deutschland