Branching-time logic ECTL# and its tree-style one-pass tableau: Extending fairness expressibility of ECTL+

Abstract Temporal logic has become essential for various areas in computer science, most notably for the specification and verification of hardware and software systems. For the specification purposes rich temporal languages are required that, in particular, can express fairness constraints. For linear-time logics which deal with fairness in the linear-time setting, one-pass and two-pass tableau methods have been developed. In the repository of the CTL-type branching-time setting, the well-known logics ECTL and ECT L + were developed to explicitly deal with fairness. However, due to the syntactical restrictions, these logics can only express restricted versions of fairness. The logic CT L ⋆ , often considered as ‘the full branching-time logic’ overcomes these restrictions on expressing fairness. However, CT L ⋆ is extremely challenging for the application of verification techniques, and the tableau technique, in particular. For example, there is no one-pass tableau construction for CT L ⋆ , while one-pass tableau has an additional benefit enabling the formulation of dual sequent calculi that are often treated as more ‘natural’ being more friendly for human understanding. These two considerations lead to the following problem - are there logics that have richer expressiveness than ECT L + , allowing the formulation of a new range of fairness constraints with ‘until’ operator, yet ‘simpler’ than CT L ⋆ , and for which a one-pass tableau can be developed? Here we give a positive answer to this question, introducing a sub-logic of CT L ⋆ called ECT L # , its tree-style one-pass tableau, and an algorithm for obtaining a systematic tableau, for any given admissible branching-time formulae. We prove the termination, soundness and completeness of the method. As tree-shaped one-pass tableaux are well suited for the automation and are amenable for the implementation and for the formulation of sequent calculi. Our results also open a prospect of relevant developments of the automation and implementation of the tableau method for ECT L # , and of a dual sequent calculi.