One-Pass Context-Based Tableaux Systems for CTL and ECTL

One-Pass Context-Based Tableaux Systems for CTL and ECTL Alex Abuin Ikerlan Technology Research Centre, Basque Research and Technology Alliance (BRTA), Arrasate-Mondragón Gipuzkoa, Spain [email protected] Alexander Bolotov University of Westminster, London, UK https://www.westminster.ac.uk/about-us/our-people/directory/bolotov-alexander [email protected] Montserrat Hermo University of the Basque Country, San Sebastián, Spain [email protected] Paqui Lucio University of the Basque Country, San Sebastián, Spain http://www.sc.ehu.es/paqui [email protected] Abstract When building tableau for temporal logic formulae, applying a two-pass construction, we first check the validity of the given tableaux input by creating a tableau graph, and then, in the second “pass”, we check if all the eventualities are satisfied. In one-pass tableaux checking the validity of the input does not require these auxiliary constructions. This paper continues the development of one-pass tableau method for temporal logics introducing tree-style one-pass tableau systems for Computation Tree Logic (CTL) and shows how this can be extended to capture Extended CTL (ECTL). A distinctive feature here is the utilisation, for the core tableau construction, of the concept of a context of an eventuality which forces its earliest fulfilment. Relevant algorithms for obtaining a systematic tableau for these branching-time logics are also defined. We prove the soundness and completeness of the method. With these developments of a tree-shaped one-pass tableau for CTL and ECTL, we have formalisms which are well suited for the automation and are amenable for the implementation, and for the formulation of dual sequent calculi. This brings us one step closer to the application of one-pass context-based tableaux in certified model checking for a variety of CTL-type branching-time logics. 2012 ACM Subject Classification Theory of computation →Modal and temporal logics Keywords and phrases Temporal logic, fairness, expressiveness, branching-time Digital Object Identifier 10.4230/LIPIcs.TIME.2020.14 Funding Alexander Bolotov: This author has been supported by the European Union (FEDER funds) under grant TIN2017-86727-C2-2-R, and by the University of the Basque Country under Project LoRea GIU18-182. Montserrat Hermo: This author has been supported by the European Union (FEDER funds) under grant TIN2017-86727-C2-2-R, and by the University of the Basque Country under Project LoRea GIU18-182. Paqui Lucio: This author has been supported by the European Union (FEDER funds) under grant TIN2017-86727-C2-2-R, and by the University of the Basque Country under Project LoRea GIU18-182. ©Alex Abuin, Alexander Bolotov, Montserrat Hermo, and Paqui Lucio; licensed under Creative Commons License CC-BY 27th International Symposium on Temporal Representation and Reasoning (TIME 2020). Editors: Emilio Muñoz-Velasco, Ana Ozaki, and Martin Theobald; Article No. 14; pp. 14:1–14:20 Leibniz International Proceedings in Informatics Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Dagstuhl Publishing, Germany 14:2 One-Pass Context-Based Tableaux Systems for CTL and ECTL 1 Introduction In this paper we continue our investigation of tableaux-based deductive techniques for temporal logic having in mind their potential application in model checking, more specifically, in certified model checking [ 16 ], which aims to generate proofs as certificates of the properties that are verified, as well as counterexamples for those properties that are invalidated. There are two known ways to build tableau constructions for temporal logic formulae (for the survey of tableau method for temporal logic we refer an interested reader to [ 13 ]). Twopass constructions check the validity of the given tableaux input in two passes - in the first pass a tableau graph is obtained and the second “pass” checks the satisfiability of all eventualities. In one-pass tableaux checking the validity of the input does not require these auxiliary constructions. This paper continues the development of one-pass tableau method for temporal logics [ 11 , 4 ], this time for Computation Tree Logic ( CTL ) and Extended Computation Tree Logic ( ECTL ) introduced, respectively, in [ 6 ] and [ 10 ]. The core tableau construction is based on the concept of a context of an eventuality, which is a set of formulae that “accompanies” the eventuality in the label of the node of a tableaux graph. Our specific tableau rules that involve context force the earliest fulfilment of eventualities. In previous works such a context-based one-pass tableaux approach has been developed for propositional linear-time temporal logic, PLTL [ 11 ], and for the branching-time logic ECTL# [ 4 ], which introduces a new class of fairness constraints utilising the “until” temporal operator. It has also been shown how, in the linear-time case, the method, being mingled with a SAT solver, can be invoked as part of the certified model checking for PLTL [ 2 ]. Aiming at similar developments for branching-time cases, in particular for CTL, we make two observations. Firstly, the satisfiability of a property ϕ in PLTL can be reduced to checking if a complete transition system satisfies ¬ϕ (since any counter-model of ¬ϕ is a model of ϕ ) and both the satisfiability and model checking are PSPACE-complete [ 18 ]. However, the CTL satisfiability problem cannot be reduced to the CTL model checking. In particular, a model checking algorithm for CTL properties (for example [ 5 ] implemented in NuSMV) cannot be adapted for testing CTL satisfiability: the model checking problem for CTL is known to be P-complete [ 7 ], while the satisfiability problem for CTL is EXPTIME-complete [ 9 ]. However, any decision procedure of CTL satisfiability can be used to perform model checking tasks. Secondly, note that in our previous work one-pass tableaux method was developed for a richer logic - ECTL# [ 4 ]. However, the application of such model checking procedure for CTL simply based on the existing one-pass tableaux for ECTL# would become too “non-intuitive” due to the complexity of its rules that are needed for this richer logic. We also note that the distinguished (and unavoidable) feature of one-pass technique for ECTL# is the utilisation of two types of context, unlike in the case of PLTL . Here the so-called “outer” (similar to PLTL ) context is a collection of state formulae, and is complemented by so called “inner” context, a collection of path formulae. Subsequently, the development of a simpler one-pass method for CTL is an important task. In our tableau method for CTL , similarly to PLTL , we only need the “outer” context, yet, similar to ECTL# the generated tableaux are AND-OR trees. Our results provide an intuitive tableau method that serves as a decision procedure of CTL satisfiability and can also be used in certified model checking of CTL properties hence the method presented in the paper would enable a subsequent study and implementation of a certified model checker. With the development of tree-shaped one-pass tableaux for CTL and ECTL, this paper has proved the effectiveness of the approach which now covers both linear-time and a range of branching-time logics. Moreover, the results of this paper give us formalisms which are well suited for the automation and are amenable for the A. Abuin, A. Bolotov, M. Hermo, and P. Lucio 14:3 implementation, and for the formulation of a dual sequent calculi - all these bring us one step closer to the application of these developments in certified model checking for a variety of branching-time logics. Additionally, aiming at the extension of the certified model checking to the branching-time framework, a proof system, e.g. sequent calculus, is required to check the proof certificates in the branching-time setting. Our extensive search for tableau methods for CTL has not shown a great variety of systems. For example, [ 3 ] presents a two-pass tableau, where in the first pass the tableau rules are applied creating a cyclic graph. In the second pass, “bad loops” are pruned (where a “bad loop” is a loop containing some eventuality that is not fulfilled along it). In [ 1 , 12 ] the authors introduce a single-pass tableaux decision procedure for CTL . It is based on Schwendimann’s one-pass procedure for PLTL [ 17 ]. This tableau method uses an additional mechanism for collecting information on the set of formulae in the nodes, and passing it, to subsequent nodes along branches. The information on previously generated nodes helps detecting “bad loops” without constructing the whole graph. Finally, we note that we have not found an explicit formulation of a tableaux (one or two pass) method for ECTL. To ensure that the presentation of quite technical details in the paper is clear and selfcontained, we supply all major technical details in the text. This determines the following structure of the paper. In §2 we give CTL and ECTL syntax and semantics as sublogics of CTL? . The formulation of the tableau method is presented in §3, where we first give some preliminaries and then overview the tableau construction as an AND-OR tree and provide examples. A systematic tableau construction is introduced in §4. In §5 we show further extension of the method for ECTL . In §6 we draw the conclusions and prospects of future work that the presented results open. Finally, in Appendix A we briefly recall the cyclic models characterization of satisfiability in branching temporal logics. The soundness and completeness of our tableau methods are proved in Appendix B. Finally, in Appendix C we depict the complete tableau for the running example in the paper. 2 Syntax and Semantics of CTL and ECTL The language of branching-time logic extends the language of classical propositional logic by future time temporal operators ◦ - “at the next moment of time”, ♦ - “eventually”,  - “always” and U - “until”, together with paths quantifiers A - “for all paths” quantifier, and E - “there exists a path” quantifier. The hierarchy of CTL -type family of Branching-time logics (BTL) is defined by releasing restrictions on the concatenations of temporal operators and paths quantifiers which define classes of admissible state formulae distinguished for these logics. As in CTL every temporal operator must be preceded by a path quantifier, this logic cannot express fairness which requires at least the concatenation of  and ♦ . These are tackled by ECTL [ 9 ] which enables simple fairness constraints but not their Boolean combinations. ECTL+ [ 10 ] further extends the expressiveness of ECTL allowing Boolean combinations of temporal operators and ECTL fairness constraints (but not permitting their nesting). The logic ECTL# [ 4 ] extends ECTL+ by allowing the combinations  ( AUB )or AUB , referred to as modalities U and U . The logic CTL? , often considered as the “full branching-time logic” overcomes all these restrictions on syntax allowing any arbitrary combinations of temporal operators and path quantifiers. For the sake of generality, as all logics we are interested in are subsumed by CTL? , we first recall CTL? syntax and then, by restricting it, derive the syntax for each of ECTL# , ECTL+ , ECTL and CTL. TIME 2020 14:4 One-Pass Context-Based Tableaux Systems for CTL and ECTL IDefinition 1 (Syntax of CTL? ) . Given Prop is a fixed set of propositions, and p∈Prop , we define sets of state ( σ ) and path ( π ) CTL? formulae over Prop as follows: σ ::= T|p| σ1∧σ2| ¬σ|Eπand πCTL?::= σ|π1∧π2| ¬π|◦π|πUπ. Observe that in Definition 1 for the set of path formulae we deliberately used an index CTL? and did not use any index for the set of state formulae: the syntax of CTL? sublogics we will define later, will be distinguished exactly by specific to these logics path formulae constructions, while the set of state formulae is preserved from the definition of CTL? syntax. Other usual Boolean operators can be derived from those introduced in the standard way while the “release” ( R ), ♦ and  operators can be defined as follows: ϕ1Rϕ2≡ ¬ ( ¬ϕ1U¬ϕ2 ), ♦ϕ≡TUϕ, and ϕ≡ ¬♦¬ϕ. We consider a Kripe-style semantics of CTL? : a Kripke structure, K , is a triple ( S, R, L ) where S6 = ∅ is a set of states, R⊆S×S is a total binary relation, called the transition relation, and L : S→ 2 Prop is a labelling function. Our Kripke structures are labelled directed graphs that correspond to Emerson’s R-generable structures, i.e. the transition relation R is suffix, fusion and limit closed [ 8 ]. A path x through a Kripke structure K is an infinite sequence of states si, si+1, si+2 . . . such that ( sj, sj+1 ) ∈R for any j≥i . A fullpath x through a Kripke structure K is an infinite sequence of states s0, s1, s2. . . , where s0 is the root. Given a path x = si, si+1, . . . and a state sk∈x such that k > i , we denote its finite prefix x≤k = si, si+1 ...,sk and its infinite suffix x≥k = sk, sk+1, . . . . The notation Kx ( i ) denotes a Kripke structure with the set of states of K restricted to those that are R -reachable from x ( i )and fullpaths ( K )is the set of all fullpaths in K . Given the structure K = ( S, R, L ), the relation | =evaluates path formulae in a given path x and state formulae at the state index i of x and is defined on atoms by K, x, i | = piff p∈L ( x ( i )). Omitting standard definitions for Booleans, we present the relation |=for temporal connectives and path quantifier E: K, x, i |=Eπiff there exists a path y∈fullpaths(Kx(i)) such that K, y |=π. K, x, i |=◦πiff K, x, i + 1 |=π. K, x, i |=π1Uπ2iff there exists k≥iwith K, x≥k|=π2and K, x≥j|=π1for all 0≤j≤k−1. For any set Σof state formulae, K, x, i | = Σ iff K, x, i | = σ, for all σ∈ Σ. Moreover, if for any fullpath x∈fullpaths ( K ), we have K, x, 0 | = Σ, then we simply write K | = Σ. For a state formula ϕ , the set of its models, Mod ( ϕ ), is formed by all triples ( K, x, i )such that K, x, i | = ϕ . Then ϕ is satisfiable ( Sat ( ϕ )) if Mod ( ϕ ) 6 = ∅ , otherwise ϕ is unsatisfiable ( UnSat ( ϕ )). For state formulae ϕ and ϕ0 , if Mod ( ϕ ) = Mod ( ϕ0 )then ϕ and ϕ0 are logically equivalent denoted as ϕ≡ϕ0 . Satisfiability and logical equivalence are generalised to sets of state formulae Σ, in the natural way (formally by substituting ϕ with Σin the relevant definitions and stating that Σis satisfied when all its formulae are satisfied). For each of BTL logics ECTL# , ECTL+ , ECTL and CTL its syntax is defined over a fixed set of propositions Prop , such that the definition of state formulae is the same as for CTL? (Def. 1), and the eventuality ♦ϕ is the abbreviation for TUϕ . The specific for these logics restrictions on the CTL? grammar in Definition 1 generate the corresponding sets for path formulae, as in Definition 2. For technical convenience, here we define  as the basic language operator. IDefinition 2 (Paths formulae for ECTL#,ECTL+, ECTL and CTL). πECTL#::= σ|π1∧π2| ¬π|◦σ|σU(σ∧ ♦σ)|(σ∨σ)|σU(σ)|(σUσ) πECTL+::= σ|π1∧π2| ¬π|◦σ|σUσ|σ|♦σ| ♦σ. πECTL ::= σ| ¬π|◦σ|σUσ|σ|♦σ| ♦σ. πCTL ::= σ| ¬π|◦σ|σUσ|σ. A. Abuin, A. Bolotov, M. Hermo, and P. Lucio 14:5 IDefinition 3 (Literals) . Let Prop be a fixed set of CTL ( ECTL ) propositions, and let ρ∈Prop . Then the set of CTL(ECTL) literals is defined as Lit ::= F|T|ρ| ¬ρ. It is well known that any given branching-time formula ϕ can be converted to a formula NNF ( ϕ )- the Negation Normal Form of ϕ obtained by pushing negations inwards until they only apply to literals. The conversion is based on well-known equivalences which ensure that ϕ and NNF ( ϕ )have exactly the same models, i.e. are logically equivalent. Consequently, we assume that inputs for the tableaux procedure in CTL and ECTL are given in NNF . For simplicity, we will write ∼ϕ instead of NNF ( ¬ϕ ). Also, for a finite set Φ = {ϕ1, . . . , ϕn} , we let ∼Φ = NNF(¬Vn i=1 ϕi). Further, it is important to note that the nesting of “pure path formulae”, totally unrestricted in CTL? , is now restricted in its sublogics by relevant grammar cases for paths formulae. For example, a CTL? formula (1) is not an ECTL# formula. Rewriting it as A(TU(◦p∧E◦¬p)) we can see A♦(◦p∧E◦¬p)(1) that ◦p∧E◦¬p is neither a state formula nor of the form σ . Note that the validity of (1) which is indicative for CTL? , is directly linked to the limit closure property [ 8 ]. Similarly, a ECTL# formula A (( pUq ) ∧ ( sU¬q )) is not an ECTL+ formula because pUq and sU¬q , hence their conjunction, are not admissible ECTL+ formulae. Further, an ECTL+ formula (2) does not belong to ECTL E(♦q∧♦¬q)(2) as ♦q∧ ♦¬q is not an admissible ECTL path formula. Finally, the fairness constraint (3) expressible in ECTL cannot be constructed in CTL syntax as every temporal operator E♦q(3) in a CTL formula must be preceded by a path quantifier. Note that it is important to distinguish the problem if a formula of a superlogic belongs to a sublogic and the problem if a formula of a superlogic can be expressed in a sublogic. For example, E ( ♦q∨ ♦¬q ), similarly to formula (2) does not belong to ECTL but unlike (2), it is expressible in this logic, as E(♦q∨ ♦¬q)≡E♦q∨E♦¬qwhich is an ECTL formula if we define ∨via ∧. Table 1 Classification of context-based tableaux systems for CTL-type logics and relevant difficult cases of concatenations of temporal operators and path quantifiers. BTL Logics E♦qE(♦q∧♦¬q)A((pUq) ∨ ( sU¬r )) A♦(◦p∧E◦¬p) One-pass Tableaux B(U,◦)(CTL)X X X X This paper B(U,◦,♦)(ECTL)√X X X This paper B+(U,◦,♦)(ECTL+)√ √ X X √ B+(U,◦,U)(ECTL#)√ √ √ X√ B?(U,◦)(CTL?)√ √ √ √ X Table 1 represents BTL logics classified by their expressiveness using “ B ” for “Branching”, followed by the set of only allowed modalities as parameters; B+ indicates admissible Boolean combinations of the modalities and B? reflects “no restrictions” in either concatenations TIME 2020 14:6 One-Pass Context-Based Tableaux Systems for CTL and ECTL of the modalities or Boolean combinations between them following the notation initially proposed in [ 8 ] and further tuned in [ 15 ]. The top row of the figure represents the indicative formulae (1)-(3) for the listed logics. The last column in Table 1 reflects the development of the context-based one-pass tableaux technique for CTL-type logics: the method has been developed for ECTL# ([ 4 ] where the motivation was to tackle complex cases of fairness). In this paper we introduce the technique for CTL and ECTL , while the case of ECTL+ can be tackled effectively by the technique developed for ECTL# . Indeed, ECTL+ and ECTL# have similar cases of the Boolean combination of eventualities in the scope of A and E , namely disjunctions of the eventualities in the scope of the A quantifier and conjunctions of eventualities in the scope of the E quantifier, see [ 4 ] for details. Thus, Table 1 also reflects syntactical cases of concatenations of temporal operators and path quantifiers that are difficult for context-based one-pass tableaux. To tackle these cases, in addition to α - and β -rules, that are standard to the tableaux, novel β+ -rules which use the context to force the eventualities to be fulfilled as soon as possible, were introduced. As ECTL# is more expressive than ECTL+ in allowing new type of fairness constraints that use the U operator, the relevant rules introduced in [ 4 ] would cover all difficult concatenations of operators in ECTL+ . Hence, simply treating the case of one-pass context-based tableaux for ECTL+ as solved by the relevant development for a richer logic ECTL# , in this paper we concentrate on bridging the gap in our roadmap in supplying BTL logics by this technique, by developing the method for CTL and ECTL . The ultimate target of this roadmap - the one-pass context-based tableaux for CTL?remains extremely difficult and an open problem. 3 Context-based One-pass Tableau Method for CTL We precede the presentation of the method by the introduction of a number of important concepts. Firstly, we introduce a concept of basic modality which reflects the restrictions on forming the basic admissible combinations of temporal operators in the scope of a path quantifier. Recall that formulae of CTL and ECTL logics are written in NNF . Abbreviating by Q either of the path quantifiers A or E , we consider a basic modality of CTL or ECTL logic to be of the form QT , where T is a temporal operator. The structure QT is generated by the grammar rules for these logics in Def. 2. We can identify all basic modalities in a given formula ϕ by finding its most embedded modality(es), say M1 , then looking at the next basic modality in which M1 is embedded, etc. For example, basic modalities for CTL are structures Q◦,QU , and Q while for ECTL these will be Q◦,QU , Q , Q♦ and Q♦ . If we analyse a CTL formula E◦A◦p then the most embedded basic modality, M1 , would be A◦p, which is embedded as E◦M1. These are generalised in Definition 4. IDefinition 4 (ECTL#,ECTL+, ECTL and CTL Basic Modalities). MECTL ::= c|Q◦M|Q(MUM)|QM|Q♦M|Q♦M. MCTL ::= c|Q◦M|Q(MUM)|QM. where c stands for a purely classical formula (we can consider a purely classical formula as a zero-degree basic modality) and Mstands for any basic modality of CTL in the definition of MCTL and of ECTL in the definition of MECTL . Note that we have “derived” cases of basic modalities for ♦M and MRM . In what follows, every CTL modality QU or Q♦ is called eventuality. CTL tableau rules are based on fixpoint characterisation of its basic modalities: (in the equations below ν and µ stand for “minimal fixpoint” and “maximal fixpoint” operators, respectively) A. Abuin, A. Bolotov, M. Hermo, and P. Lucio 14:7 Eϕ=νρ(ϕ∧E◦ρ)E(ϕRψ) = νρ(ψ∧(ϕ∨E◦ρ)) Aϕ=νρ(ϕ∧A◦ρ)A(ϕRψ) = νρ(ψ∧(ϕ∨A◦ρ)) (4) E♦ϕ=µρ(ϕ∨E◦ρ)E(ϕUψ) = µρ(ψ∨(ϕ∧E◦ρ)) A♦ϕ=µρ(ϕ∨A◦ρ)A(ϕUψ) = µρ(ψ∨(ϕ∧A◦ρ)) (5) This fixpoint characterisation of basic CTL and ECTL modalities as maximal or minimal fixpoints give rise to their analytical classification as α - or β -formulae which are associated, in the tableau with α - and β -rules: Q , and QR as maximal fixpoints are classified as α -formulae while Q♦ and QU as minimal fixpoints are β -formulae. This is also reflected in the known equivalences: Eϕ=ϕ∧E◦EϕE(ϕRψ) = ψ∧(ϕ∨E◦E(ϕRψ)) Aϕ=ϕ∧A◦AϕA(ϕRψ) = ψ∧(ϕ∨A◦A(ϕRψ)) (6) E♦ϕ=ϕ∨E◦E♦ϕE(ϕUψ) = ψ∨(ϕ∧E◦E(ϕUψ)) A♦ϕ=ϕ∨A◦A♦ϕA(ϕUψ) = ψ∨(ϕ∧A◦A(ϕUψ)) (7) The tableau method determines if a given set of CTL state formulae is satisfiable or not. We precede the formal introduction of the technique by its informal overview. The initial node of the tableaux is labelled by a CTL formula in NNF . To expand the root, and any subsequent node, we apply one of the following rules: α - and β -rules, the “next-state” rule, which reflects a “jump” from a “state” to a “pre-state”, and, finally, characteristic to our approach, β+ -rules, where the use of the context (of an eventuality) is essential. The use of the context in these rules, which is a collection of state formulae accompanying the eventuality in the label of the node, forces the soonest fulfillment of eventualities. We apply α -, β -, and β+ -rules repeatedly until we reach a node labelled by F or by an inconsistent set of formulae, or a node whose labels have already occurred within the path under consideration. In the former case the expansion of the given branch terminates with ⊥ as its leaf. In the latter case, a repetitive node in the branch means that the branch has a loop – where some subformulae of the given formula are satisfied forever – which could be “bad” or “good”. A loop is “bad” when it has a node which contains an unfulfilled eventuality, i.e. none of the nodes of the loop satisfies it. In our procedure, the application of β+ -rules to eventualities is essential to distinguish between “good” and “bad” loops - if β+ -rules have already been applied to every eventuality occurring in the branch then we have a ’good loop’ and this branch represents a model for the given formula. Otherwise, we choose an eventuality to which a corresponding β+ -rule has not been applied. IDefinition 5 (Syntactically Consistent Set of Formulae) . A set Σof state formulae σ is syntactically consistent abbreviated as Σ > if F6∈ Σand {σ, ∼σ} 6⊆ Σfor any σ ; otherwise, Σ is inconsistent denoted as Σ⊥. IDefinition 6 (Tableau, Consistent Node, Closed branch) . A tableau for a set of CTL state formulae Σis a labelled tree hT, τ, Σ i , where T is a tree, and τ is a mapping of the nodes of T to the state formulae, elements of Σ, such that the following two conditions hold: (i) The root is labelled by the set Σ. (ii) For any other node m∈T , its label τ ( m )is a set of state formulae obtained as the result of the application of one of the rules in Figures 1, 2 and 4 to its parent node n . Given the applied rule is R , we term m an R -successor of n . A node n of TIME 2020 14:8 One-Pass Context-Based Tableaux Systems for CTL and ECTL a tree T is consistent, abbreviated as n> , if its label, τ ( n ), is a syntactically consistent set of formulae (see Def. 5), else n is inconsistent, abbreviated as n⊥ . If a branch b of τ , contains n⊥∈b, then bis closed else bis open. (∧)Σ, σ1∧σ2 Σ, σ1, σ2 (Q)Σ,Qσ Σ, σ, Q◦Qσ (∨)Σ, σ1∨σ2 Σ, σ1|Σ, σ2 (QU)Σ,Q(σ1Uσ2) Σ, σ2|Σ, σ1,Q◦Q(σ1Uσ2) (QR)Σ,Q(σ1Rσ2) Σ, σ1, σ2|Σ, σ2,Q◦Q(σ1Rσ2)(Q♦)Σ,Q♦σ Σ, σ |Σ,Q◦Q♦σ Figure 1 αand β-Rules. The rules in Figure 1 follow the standard for the tableaux classification of rules into α -rules and β -rules that for the formulae with CTL modalities are based on their analytic classification reflected in Equations (6)-(7). Thus, if a node, n , in the tableau graph is labelled by a set of formulae, Σ , ϕ , and a designated formula for the application of tableau rules, ϕ , is an α -formula - Q or QR , then a corresponding α -rule applies, while if ϕ is a β -formula - Q♦ or QU then a corresponding β -rule applies. In the latter case we treat Σ as a (possibly empty) context for the eventuality ϕ . These applications of α - and β -rules generate a set of formulae in the conclusion as a label for the successor node, n + 1, in case of an α-rule, or as labels of two successors of n, in case of a β-rule. When a node n is labelled by an elementary set of formulae – i.e. a set which exclusively formed by literals and formulae of the form Q◦σ – then this structure is analogous to the construction to a “state” in the terminology of [ 19 ]; it enables us to construct the successors of n corresponding to “pre-states” [ 19 ]. According to the next proposition we are guaranteed to reach such a tree structure, where the last node of every branch, at this stage of the construction, is a state. IProposition 7. Any set of CTL state formulae has a tableau T such that the last node of every branch is labelled by an elementary set of state formulae. Proof. Repeatedly apply to every expandable node any applicable α - or β -rule until all expandable nodes are elementary. Then, the next-state rule must be applied to every expandable node. J (Q◦)Σ,A◦σ1,...,A◦σ`,E◦σ0 1,...,E◦σ0 k, σ1, . . . , σ`, σ0 1&. . . &σ1, . . . , σ`, σ0 k where Σis a set of literals. Figure 2 Next-state Rule. (“&” joins AND-successors in the conclusion.) Proposition 7 enables the application of the so-called “next-state rule” depicted in Figure 2. Applying this rule we split the current branch at node n where the set Σ ,A◦σ1,...,A◦σ`,E◦σ0 1, . . . , E◦σ0 k is satisfied, into k branches (i.e. into the number of branches equal to the number of E◦ constraints) where the successors of n along these branches are AND-successors, and are labelled each by a different set σ1, . . . , σ`, σ0 i , for i∈ { 1 , . . . , k} . This rule splits branches in a “conjunctive” way, and we use the symbol &to represent the generation of AND-successors of A. Abuin, A. Bolotov, M. Hermo, and P. Lucio 14:9 node n . Thus, the graphs generated by the tableaux with the application of the “next-state” rule are AND-OR trees. The subsequent construction of a tableau, additionally, involves rules that are applied to so called “uniform sets of formulae”. IDefinition 8 (Uniform Set of Formulae) . A set of CTL state formulae Σis uniform iff Σis exclusively formed by literals and basic CTL modalities and it has at most one E-formula. Applying Proposition 7 to construct a tableau with all its expandable nodes labelled by elementary sets of formulae, and then applying the rule ( Q◦ )(to every expandable node), and finally, repeatedly applying (to every expandable node) the rules ( ∧ )and ( ∨ ), we can prove Proposition 9 which states that we can also reach the stage where the last nodes of tableaux branches are labelled by uniform sets of formulae. IProposition 9. Any set of CTL state formulae Σhas a tableau T such that labels of all its expandable nodes are uniform sets of formulae. IDefinition 10 (Uniform Tableau) . For any set Σof CTL state formulae, the tableau for Σ provided by Proposition 9 is denoted Uniform_Tableau(Σ). Now we illustrate the procedure by a running example and in the subsequent text will gradually explain its main steps with illustrative figures for some parts. The whole tableau is depicted in Appendix C. A◦A(FR ¬q),E◦E(pUq)∧E◦¬q A◦A(FR ¬q),E◦E(pUq),E◦¬q A(FR ¬q),E(pUq)A(FR ¬q),¬q (∧) (Q◦) Figure 3 Example of uniform tableau. IExample 11. The given set of formulae {A◦A ( FR ¬q ) ,E◦E ( pUq ) ∧E◦¬q} is not uniform. Hence, by applying the rules ( ∧ )and ( ◦ ), we obtain the tableau in Figure 3. The two ANDsuccessors created by the “next-state” rule ( Q◦ )are respectively labelled by the uniform sets: A(FR ¬q),E(pUq)and A(FR ¬q),¬q. We extend our set of tableau rules with the new two rules named as β+ -rules (Figure 4). Note that the ( Q♦ ) + rule can be derived from the application of the ( QU ) + to the CTL formula TUσ . These rules, similarly to β -rules, also split a branch into two branches. These two β+ -rules are the only rules in our system that make use of the context - their application force the eventualities to be satisfied as soon as possible (from the point of the tableau construction where an eventuality is selected to be expanded with a β+ -rule). The context is given by the sets Σthat contain state formulae. In the conclusion of a β+ -rule we add to the conclusion of the corresponding β -rule, a conjunct ∼ Σ 0 . Recall that this is an NNF of the negation of the conjunction of all formulae in Σ 0 that are left from Σafter performing the set-theoretical difference constraint indicated in the formulation of the rule. The idea now is that ∼ Σ 0 should also be satisfied until σ2 becomes satisfied. This prevents the repetition of the context while σ2 is “delayed”. Note that Σ 0 does not include the A (with any prefix of TIME 2020 14:16 One-Pass Context-Based Tableaux Systems for CTL and ECTL B Soundness and Completeness Since CTL and ECTL are sublogics of ECTL# and the tableau method presented here is the adaptation of the method in [ 4 ], in this section we essentially adapt to CTL the soundness and completeness proofs developed in [ 4 ]. We firstly prove the soundness and completeness of the tableau method for CTL, and then we extend both results to ECTL. To prove the soundness of our tableau method for CTL (Theorem 22), we show that every tableau rule in Figures 1, 2 and 4 are sound (or preserve satisfiability) in the sense of the next Lemma 21. ILemma 21 (Soundness of the Tableau Rules for CTL ) . Consider all the rules in Figures 1, and 2 and 4. 1. For any α-rule Σ Σ0:Sat(Σ) if and only if Sat(Σ0). 2. For any βand β+-rule Σ Σ1|Σ2:Sat(Σ) if and only if Sat(Σ1)or Sat(Σ2). 3. If Σis a set of consistent literals, then Sat (Σ ,A◦σ1,...,A◦σ`,E◦σ0 1,...,E◦σ0 k )if and only if Sat(σ1, . . . , σ`, σ0 i)for all 1≤i≤k. Proof. All the items follows very easily by the “systematic” application of the semantic definitions of the modalities, except the “if” direction for the two of β+ -rules. We will prove here the “if” direction of the rules ( QU ) + for Q = E and Q = A , because the rules ( Q♦ ) + are particular cases by abbreviation ♦σ=TUσ. For the “if” direction of rule ( EU ) + , let K | = Σ ,E ( σ1Uσ2 )and let x be the path in K such that K, x, i | = Σ ,E ( σ1Uσ2 ). Then, let j be the least i≥ 0such that K, x, i | = σ2 . If j = i = 0, then K, x, 0 | = Σ , σ2 . Otherwise, if j > 0then K, x, m | = σ1 , for all 0 ≤m<j . Consider k to be the greatest such m for which K, x, k | = Σ. Hence, K, x, h | = ∼ Σ, for all h such that k + 1 ≤h < j . In particular, by definition of Σ 0 (obtained from Σ) it is easy to see that K, x, h | = σ for every σ∈ (Σ \ Σ 0 )and for all h such that 0 ≤h < j . Therefore, K, x, h | = ∼ Σ 0 , for all hsuch that k+ 1 ≤h < j. Thus, K, x, k |=, σ1,E◦E((σ1∧ ∼Σ0)Uσ2). For the “if” direction of rule (AU)+, let us suppose that UnSat(Σ, σ2)and UnSat(Σ, σ1,A◦A((σ1∧ ∼Σ0)Uσ2)). We will show that UnSat (Σ ,A ( σ1Uσ2 )). For that, let us consider any arbitrary K such that K | = Σ to show that K 6| = A ( σ1Uσ2 ). By the above unsatisfiability hypothesis, if K | = Σ, then both K 6| = σ2 and K 6| = σ1∧A◦A (( σ1∧ ∼ Σ 0 ) Uσ2 ). Then, there are two possible cases. First, if K | = ¬σ1∧ ¬σ2 , then it is obvious that K 6| = A ( σ1Uσ2 ). Second, if K | = ¬σ2∧¬A◦A (( σ1∧ ∼ Σ 0 ) Uσ2 ), then there exists x1∈fullpaths ( K )and i1> 0that satisfy both K, x1, j | = ¬σ2 for all j such that 0 ≤j≤i1 , and K, x1, i1| = ¬σ1∨ Σ 0 . Since all the formulae in Σ \ Σ 0 are satisfied in all states along all paths, indeed K, x1, i1| = ¬σ1∨ Σ. Therefore, if K, x1, i1| = ¬σ1 , then obviously K 6| = A ( σ1Uσ2 ). Otherwise, if K, x1, i1| = Σ, applying the same reasoning for Kx1 ( i1 )as we did above for K , we can conclude that there should be a path x2∈fullpaths ( Kx1 ( i1 )) and some i2> 0such that either Kx1 ( i1 ) , x2, j | = ¬σ2 for all j such that i1≤j≤i2 and Kx1 ( i1 ) , x2, i2| = ¬σ1∨ Σ. Hence, if Kx1 ( i1 ) , x2, i1| = ¬σ1 , then trivially K 6| = A ( σ1Uσ2 ). Otherwise, Kx1 ( i1 ) , x2, i1| = Σ. Hence, there are two possible scenarios: 1.) After a finite number of iterations we get a path y = x≤i1 1x≤i2 2· · · x≤ik k such that K, y, j | = ¬σ2 for all j such that 0 ≤j≤ik and K, y, ik| = ¬σ1 . 2.) The infinite iteration of the second case yields a path y = x≤i1 1x≤i2 2· · · x≤ik k· · · (that exists by the limit closure property) such that K, y, i | = ¬σ2 for all i≥ 0. In both scenarios we have K 6| = A ( σ1Uσ2 ) holds for any arbitrary Kthat satisfies Σ. Thus, UnSat(Σ,A(σ1Uσ2)).J A. Abuin, A. Bolotov, M. Hermo, and P. Lucio 14:17 ITheorem 22 (Soundness of the Tableau Method for CTL ) . Given any set of state formulae Σ, if there exists a closed tableau for Σthen UnSat(Σ). Proof. In a closed tableau for Σ, the set of formulae labelling at least one leaf in each bunch is inconsistent and therefore unsatisfiable. Then, by Lemma 21, the labelling of the root node, Σ, is unsatisfiable. J Next, we prove the refutational completeness of the tableau method for CTL (Theorem 29). For that, we firtsly define the notion of stage and prove some auxiliary properties on the stages and bunches of the systematic tableau, that are necessary to prove that every open bunch in the systematic tableau represents a model of the initial set of formulae (Lemma 28). IDefinition 23 (Stage) . Given a branch, b of a tableau T , a stage in T is every maximal subsequence of successive nodes ni, ni+1, . . . , nj in b such that τ ( nk )is not a ( Q◦ )-child of τ ( nk−1 ), for all k such that i<k≤j . We denote by stages ( b )the sequence of all stages of b . The successor relation on stages ( b )is induced by the successor relation on b . The labelling function τ is extended to stages as the union of the original τ applied to every node in a stage. IDefinition 24 ( αβ+ -saturated Stage) . We say that a stage s = ni, . . . , nj in Asys Σ is αβ+-saturated if and only if it satisfies the following conditions: 1. For all σ1∧σ2∈τ(s):{σ1, σ2} ⊆ τ(s). 2. For all Qσ∈τ(s):{σ, Q◦Qσ} ⊆ τ(s). 3. For all σ1∨σ2∈τ(s):σ1∈τ(s)or σ2∈τ(s). 4. For all Q(σ1Rσ2)∈τ(s):{σ1, σ2} ⊆ τ(s)or {σ2,Q◦Q(σ1Rσ2)} ⊆ τ(s). 5. For all Q(σ1Uσ2)∈τ(s):σ2∈τ(s)or {σ1,Q◦Q(σ1Uσ2)} ⊆ τ(s)or {σ1,Q◦Q((σ1∧ ∼Σ0)Uσ2)} ⊆ τ(s) where Σ0= (τ(ni)\ {Q(σ1Uσ2)})\ {(A◦)iAϕ|i≥0and (A◦)iAϕ∈τ(ni)}. 6. For all Q(♦σ)∈τ(s):σ∈τ(s)or {Q◦Q(♦σ)} ⊆ τ(s)or {Q◦Q((∼Σ0)Uσ)} ⊆ τ(s) where Σ0= (τ(ni)\ {Q♦σ})\ {(A◦)iAϕ|i≥0and (A◦)iAϕ∈τ(ni)}. IDefinition 25 (Expanded Bunch and Tableau) . An open branch b is expanded if each stage s∈stages ( b )is αβ+ -saturated and b is eventuality-covered. A bunch is expanded if all its open branches are expanded. A tableau is expanded if all its open bunches are expanded. The construction of the systematic tableau applies exactly one β+ -rule to exactly one selected eventuality (if any) at the first node of the stage, and then applies exhaustively all the applicable α - and β -rules to the formulas in the stage, until the branch closes, or its leaf is labelled by an elementary set, or it contains a loop-node. Consequently, the following Proposition 26 holds which can be trivially proved by construction. IProposition 26. Given any set of state formulae Σ, the systematic tableau Asys Σ is expanded. Next we prove a crucial property of the systematic tableau management of eventualities by means of the selection policy. IProposition 27. Let b be an open branch of Asys Σ and let Q ( σ1Uσ2 )be a formula that is selected at some stage si∈stages ( b ). Then, there exists some stage sk∈stages ( b )(for some k≥i) such that σ2∈τ(sk)and σ1∈τ(sj)for all j∈ {i, . . . , k −1}. Proof. By construction, the uniform set labelling the first node at each stage sj ( j≥i ) of b has the form Σ sj,Q (( σ1∧ ( ∼ Σ si∧· · · ∧ ∼ Σ sj−1 )) Uσ2 )where each Σ sj is the context of the selected formula containing the next-step variant of Q ( σ1Uσ2 )at the first node of each stage sj . Since TIME 2020 14:18 One-Pass Context-Based Tableaux Systems for CTL and ECTL no other β+ -rule is applied each Σ sj is a subset of the finite set formed by all state formulae that are subformulae of some formula in Σ si and their negations. Hence, there are a finite number of different Σ sj . Therefore, after finitely many applications of the β+ -rule, Σ sh = Σ sj , for some h > = i , for some j∈ {i, . . . , h − 1 } , and σ1∧ ( ∼ Σ si∧ · · · ∧ ∼ Σ sh−1 ) ∈τ ( sh ). In particular, ∼ Σ sh∈τ ( sh ), hence, Σ sh must be inconsistent. Since b is open, this is a contradiction. This means that, for some k≥i the application of the corresponding β+ -rule should force that σ2∈τ ( sk ). In addition, by Proposition 26 and Definition 24(5), σ1∈τ ( sj ) for all j∈ {i, . . . , k −1}.J ILemma 28 (Model Existence) . Let Σbe any set of formulae. For any expanded bunch H of Asys Σ, there exists a Kripke structure KHsuch that KH|= Σ. Proof. Let H be any expanded bunch of Asys Σ . We define KH = ( S, R, L )such that S = Sb∈Hstages ( b )and for any s∈S : L ( s ) = {p|p∈τ ( n ) ∩Prop for some node n∈s} ; and R is the relation induced in stages ( b )for each b∈H . Any branch in b∈H is open, hence b ends in a loop-node. Moreover, every eventuality has been selected in some stage of b . Hence, there exists a (possibly empty) uniform set Σ ` such that for some i≥ 0: b = s0, s1, . . . , si−1, si, si+1, . . . , sj, n` , where each sh stands for a stage and n` is a nonexpandable loop-node labelled by Σ ` whose companion node is the first node at stage si . We are going to prove the following fact: KH, sa,0|=σfor any a∈ {0, . . . , j}and any formula σin L(sa) by structural induction on the formula σ. The base of the induction, for σ=p∈Prop, follows by definition of KH. The cases where σ has one of the forms σ1∧σ2 , Qσ , σ1∨σ2 and Q ( σ1Rσ2 )are trivial by Definition 24 and the induction hypothesis. Hence, to complete the inductive proof we will show that KH, sa, 0 | = Q ( σ1Uσ2 )for any Q ( σ1Uσ2 ) ∈L ( sa ). The case for all Q♦σ∈L ( sa ) follows as a particular case by ♦σ≡TUσ. Consider any Q ( σ1Uσ2 ) ∈L ( sa ). Since b is eventuality-covered and n` is a loop-node, Q ( σ1Uσ2 )must be the selected eventuality at some node between the states sa and sj . Hence, by Proposition 27 and the definition of KH , there should be a state sk∈S (for some a≤k≤j ) such that σ2∈L ( sk )and σ1∈L ( sz )for all z∈ {a, . . . , k − 1 } . Then, by induction hypothesis, KH, sk, 0 | = σ2 and KH, sz, 0 | = σ1 for all z∈ {a, . . . , k − 1 } . Therefore, KH, sa,0|=Q(σ1Uσ2). To complete the proof, we show that the successor relation between states in KH is welldefined. For that, consider any tableau node in any stage sa that is labelled by an elementary set {Σ,A◦σ1,...,A◦σn,E◦σ0 1,...,E◦σ0 k} where Σis a consistent set of literals, by rule ( Q◦ ), sa has (in KH ) a successor state si a+1 , for each i∈ { 1 , . . . , k} , such that L ( si a+1 ) = {σ1, . . . , σn, σ0 i} . We can assume (by the above proved fact) that KH, si a+1, 0 | = {σ1, . . . , σn, σ0 i} for all i∈ { 1 , . . . , k} . Therefore, we can infer that KH, sa,0|={Σ,A◦σ1,...,A◦σn,E◦σ0 1,...,E◦σ0 k}.J Next, we prove the refutational completeness of the tableau method. ITheorem 29 (Refutational Completeness for CTL ) . For any set of state formulae Σ, if UnSat(Σ) then there exists a closed tableau for Σ. A. Abuin, A. Bolotov, M. Hermo, and P. Lucio 14:19 Proof. Suppose the contrary, that there exists no closed tableau for Σ. Then the systematic tableau Asys Σ is open. Hence, there is at least one expanded bunch H in Asys Σ . By Lemma 28, there exists a Kripke structure KHsuch that KH|= Σ. Consequently, Sat(Σ).J Finally, we prove the completeness of our tableau method for CTL. ITheorem 30 (Termination of the Tableau Method for CTL ) . For any set of state formulae Σ, the construction of the expanded tableau Asys Σterminates. Proof. Tableau rules produce a finite branching, hence König’s Lemma, applies. Therefore, it suffices to prove that every branch is finite. By Proposition 27, the application of a β+ -rule to a selected formula stops after a finite number of steps. Since the number of selectable eventualities in any open branch is finite, any open branch is eventuality-covered after a finite number of eventuality selections. Recall that we assume the eventuality selection strategy to be fair. J ITheorem 31 (Completeness of the Tableau Method for CTL ) . For any set of state formulae Σ, if Σis satisfiable then there exists a (finite) open expanded tableau for Σ. Proof. The existence of the systematic tableau Asys Σ suffices to prove this fact, by Theorem 30. J Now, we explain how the proofs of these metatheorems for CTL can be extended to ECTL . Firstly, we extend the soundness of the tableau rules, in the sense of Lemma 21, to the rules in Figure 7. ILemma 32. For any ECTL set of state formulae Σand any state formula σ: 1. Sat(Σ,Q♦σ)if and only if Sat(Σ,Q♦σ, Q◦Q♦σ). 2. Sat(Σ,Q♦σ)if and only if Sat(Σ,Qσ)or Sat(Σ,Q♦σ, Q◦Q♦σ). Proof. It follows by “systematic” application of the semantic definitions of the modalities Q♦and Q♦given by the equivalences (8) in Section 5. J To extend the refutational completeness result to ECTL , we firstly extend the Definition 24 with the following additional conditions for a stage to be αβ+-saturated: 7. For all Q♦σ∈τ(s):{Q♦σ, Q◦Q♦σ} ⊆ τ(s). 8. For all Q♦σ∈τ(s):{Qσ} ⊆ τ(s)or {Q♦σ, Q◦Q♦σ} ⊆ τ(s). It is obvious that these two additional conditions are satisfied in any stage of the systematic tableau by construction. Using these conditions, it is routine to prove that KH defined in Lemma 28 satisfies the fact that: KH, sa, 0 | = σ for any a∈ { 0 , . . . , j} and any formula of the forms Q♦σ, Q♦σ that belongs to L ( sa ). Therefore, refutational completeness (i.e. Theorem 29) extends to ECTL. Finally, to extend the termination result (see proof of Theorem 30), it suffices to ensure that the rules in Figure 7 do not affect the behaviour of the β+ -rules on the selected eventualities in the sense that Proposition 27 is preserved. Since each application of a rule in Figure 7 introduces a new Q♦σ , in Section 5 we have introduced the simplification rule ( <QU )(see (9) to subsume any occurrence of the eventuality ϕ by any next-step variant of ϕ. Therefore, Proposition 27 holds and hence Theorem 30 trivially extends to ECTL. TIME 2020 14:20 One-Pass Context-Based Tableaux Systems for CTL and ECTL C The Running Example Tableau In Figure 9 we depict the whole tableau for the running example we use in the paper. Note that the Q rule at step 2, denoted with a big circle generates two AND-successors, where the left successor has the closed tableau - this is explained in the paper. Hence, the bunch is closed, in spite of the open tableau at the right successor of the AND-node. A◦A(FR¬q),E◦E(pUq)∧E◦¬q A◦A(FR¬q),E◦E(pUq),E◦¬q E(pUq),A(FR¬q) q, A(FR¬q) q, F,¬q q, ¬q, A◦A(FR¬q) p, E◦E((p∧E(TUq))Uq),A(FR¬q) p, E◦E((p∧E(TUq))Uq),F,¬q p, E◦E((p∧E(TUq))Uq),¬q, A◦A(FR¬q) E((p∧E(TUq))Uq),A(FR¬q) q, A(FR¬q) q, F,¬q q, ¬q, A◦A(FR¬q) p∧E(TUq),E◦E((p∧E(TUq))Uq),A(FR¬q) p, E(TUq),E◦E((p∧E(TUq))Uq),A(FR¬q) A(FR¬q),¬q F,¬q¬q, A◦A(FR¬q) A(FR¬q) (∧) (Q◦) (EU)+ (AR) ⊗⊗ (AR) ⊗ (◦) (EU)+ (AR) ⊗⊗ (∧) ⊗ (AR) ⊗(Q◦) Figure 9 A closed tableau for {A◦A(FR¬q),E◦E(pUq)∧E◦¬q}.