The model checking fingerprints of CTL operators
classification
💻 cs.LO
cs.CC
keywords
operatorscheckingmodelfingerprintsoperatorarbitrarybooleancomparison
read the original 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.
This paper has not been read by Pith yet.
discussion (0)
Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.