Paper Info
Title
The model checking fingerprints of CTL operators.
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.
Year
DOI
Venue
2015
10.1109/TIME.2015.13
Workshops
Keywords
Field
DocType
Model checking,temporal logics,complexity
Boolean function,Computation tree logic,Abstraction model checking,Boolean circuit,Model checking,Computer science,Algorithm,Linear temporal logic,Theoretical computer science,Operator (computer programming),CTL*
Journal
Volume
ISSN
Citations 
abs/1504.04708
1530-1311
0
PageRank 
References 
Authors
0.34
14
3
Name
Order
Citations
PageRank
Andreas Krebs1218.20
Arne Meier221.08
Martin Mundhenk3232.95