Details
| Original language | English |
|---|---|
| Pages (from-to) | 487-519 |
| Number of pages | 33 |
| Journal | Acta informatica |
| Volume | 56 |
| Issue number | 6 |
| Early online date | 1 Aug 2018 |
| Publication status | Published - 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 subject areas
- Computer Science(all)
- Software
- Computer Science(all)
- Information Systems
- Computer Science(all)
- Computer Networks and Communications
Cite this
- Standard
- Harvard
- Apa
- Vancouver
- BibTeX
- RIS
In: Acta informatica, Vol. 56, No. 6, 01.09.2019, p. 487-519.
Research output: Contribution to journal › Article › Research › 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 -