Details
| Originalsprache | Englisch |
|---|---|
| Seiten (von - bis) | 487-519 |
| Seitenumfang | 33 |
| Fachzeitschrift | Acta informatica |
| Jahrgang | 56 |
| Ausgabenummer | 6 |
| Frühes Online-Datum | 1 Aug. 2018 |
| Publikationsstatus | Veröffentlicht - 1 Sept. 2019 |
Abstract
The aim of this study is to understand the inherent expressive power of CTL operators. We investigate the complexity of model checking for all CTL fragments with one CTL operator and arbitrary Boolean operators. This gives us a fingerprint of each CTL operator. The comparison between the fingerprints yields a hierarchy of the operators that mirrors their strength with respect to model checking.
ASJC Scopus Sachgebiete
- Informatik (insg.)
- Software
- Informatik (insg.)
- Information systems
- Informatik (insg.)
- Computernetzwerke und -kommunikation
Zitieren
- Standard
- Harvard
- Apa
- Vancouver
- BibTex
- RIS
in: Acta informatica, Jahrgang 56, Nr. 6, 01.09.2019, S. 487-519.
Publikation: Beitrag in Fachzeitschrift › Artikel › Forschung › Peer-Review
}
TY - JOUR
T1 - The model checking fingerprints of CTL operators
AU - Krebs, Andreas
AU - Meier, Arne
AU - Mundhenk, Martin
N1 - Acknowledgements: The authors thank Stephan Fischer for helpful discussions on the proof of Lemma 4 and Martin Krejka for a simplification of the proof of Lemma 14. The authors also thank the referees for many valuable comments.
PY - 2019/9/1
Y1 - 2019/9/1
N2 - The aim of this study is to understand the inherent expressive power of CTL operators. We investigate the complexity of model checking for all CTL fragments with one CTL operator and arbitrary Boolean operators. This gives us a fingerprint of each CTL operator. The comparison between the fingerprints yields a hierarchy of the operators that mirrors their strength with respect to model checking.
AB - The aim of this study is to understand the inherent expressive power of CTL operators. We investigate the complexity of model checking for all CTL fragments with one CTL operator and arbitrary Boolean operators. This gives us a fingerprint of each CTL operator. The comparison between the fingerprints yields a hierarchy of the operators that mirrors their strength with respect to model checking.
UR - http://www.scopus.com/inward/record.url?scp=85051242304&partnerID=8YFLogxK
U2 - 10.48550/arXiv.1504.04708
DO - 10.48550/arXiv.1504.04708
M3 - Article
AN - SCOPUS:85051242304
VL - 56
SP - 487
EP - 519
JO - Acta informatica
JF - Acta informatica
SN - 0001-5903
IS - 6
ER -