The model checking fingerprints of CTL operators

TL;DR

This paper analyzes the expressive power of CTL operators by examining the complexity of model checking for various fragments, creating a hierarchy that reflects their relative strength.

Contribution

It introduces a systematic way to compare CTL operators based on their model checking complexity, providing a new hierarchy of operator expressive power.

Findings

Established complexity classifications for CTL fragments

Created a hierarchy of CTL operators based on their model checking fingerprints

Revealed the relative strength of CTL operators in model checking contexts

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.