Fairness with EXPTIME Bundled CTL Tableau

摘要

The Computational Tree Logic (CTL) has difficulty expressing some fairness properties. One solution is to instead use the syntactic extension Full CTL (CTL) or the more limited CTL+ extension, but either way the satisfiability problem then becomes doubly exponential. We discuss how the limit closure axiom of CTL makes representing fairness difficult. Removing this restriction results in Bundled CTL (BCTL). We present a singly exponential tableau for BCTL and show how BCTL can represent fairness properties in a similar way to CTL. We further show how to combine the BCTL tableau with an existing BCTL tableau, to give the full expressivity of BCTL while retaining a singly exponential running time when the number of BCTL operators is limited.