Towards Certified Model Checking for PLTL Using One-Pass Tableaux

Towards Certified Model Checking for PLTL Using One-Pass Tableaux Alex Abuin Ikerlan Technology Research Centre, P. J. M. Arizmendiarrieta, 2 20500 Arrasate-Mondragón Gipuzkoa, Spain [email protected] Alexander Bolotov University of Westminster, W1W 6UW, London, UK https://www.westminster.ac.uk/about-us/our-people/directory/bolotov-alexander [email protected] Unai Díaz de Cerio Ikerlan Technology Research Centre, P. J. M. Arizmendiarrieta, 2 20500 Arrasate-Mondragón Gipuzkoa, Spain [email protected] Montserrat Hermo University of the Basque Country, P. Manuel de Lardizabal, 1, 20018-San Sebastián, Spain [email protected] Paqui Lucio University of the Basque Country, P. Manuel de Lardizabal, 1, 20018-San Sebastián, Spain http://www.sc.ehu.es/paqui [email protected] Abstract The standard model checking setup analyses whether the given system specification satisfies a dedicated temporal property of the system, providing a positive answer here or a counter-example. At the same time, it is often useful to have an explicit proof that certifies the satisfiability. This is exactly what the certified model checking (CMC) has been introduced for. The paper argues that one-pass (context-based) tableau for PLTL can be efficiently used in the CMC setting, emphasising the following two advantages of this technique. First, the use of the context in which the eventualities occur, forces them to fulfil as soon as possible. Second, a dual to the tableau sequent calculus can be used to formalise the certificates. The combination of the one-pass tableau and the dual sequent calculus enables us to provide not only counter-examples for unsatisfied properties, but also proofs for satisfied properties that can be checked in a proof assistant. In addition, the construction of the tableau is enriched by an embedded solver, to which we dedicate those (propositional) computational tasks that are costly for the tableaux rules applied solely. The combination of the above techniques is particularly helpful to reason about large (system) specifications. 2012 ACM Subject Classification Theory of computation →Modal and temporal logics Keywords and phrases Temporal logic, fairness, expressiveness, linear-time, Certified model checking Digital Object Identifier 10.4230/LIPIcs.TIME.2019.12 Funding Alexander Bolotov: This author has been partially supported by the UK Knowledge Transfer Partnership KTP011063 Lumina Learning & University of Westminster, and the Spanish Project TIN201786727-C2-2-R, and by the University of the Basque Country under Project LoRea GIU18-182. Montserrat Hermo: This author has been partially supported by Spanish Project TIN2017-86727C2-2-R, and by the University of the Basque Country under Project LoRea GIU18-182. Paqui Lucio: This author has been partially supported by Spanish Project TIN2017-86727-C2-2-R, and by the University of the Basque Country under Project LoRea GIU18-182. ©Alex Abuin, Alexander Bolotov, Unai Díaz de Cerio, Montserrat Hermo, and Paqui Lucio; licensed under Creative Commons License CC-BY 26th International Symposium on Temporal Representation and Reasoning (TIME 2019). Editors: Johann Gamper, Sophie Pinchinat, and Guido Sciavicco; Article No. 12; pp. 12:1–12:18 Leibniz International Proceedings in Informatics Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Dagstuhl Publishing, Germany 12:2 Towards Certified Model Checking for PLTL Using One-Pass Tableaux 1 Introduction and Problem Setup Model Checking [ 10 , 31 , 11 ] is an algorithmic method for determining whether a complex hardware or software system satisfies a given property. Many important properties to be verified reflect the system’s dynamics and are expressed in some temporal logic. If the property does not hold, the checker returns a counter-example: a trace/model of the system that does not satisfy the property. This counter-model acts as a “certificate” of the failure and its role is to help the user to identify the source of the problem which could be in the system design, in the property, and even in the model checker. However, there are a number of scenarios where another certification is needed. One of these scenarios consists on proving, only once, the correction of the underlying algorithm of the model checker. For this task, interactive proof assistants such as Coq or Isabelle are good tools. They allow us to certify a model checker and even obtain an executable program by the refinement of some extraction mechanism. For instance Amjad [1] described how to code BDD-based symbolic model checking algorithms into an automatic theorem prover. More recently, Esparza et al. [ 13 ] have verified an automata-based model checker with Isabelle theorem prover. The second scenario involves the model checker to certify that a particular property is true. For example, the user may deal with a very complex specification and is not sure if the specification is well written. Here it is important to have techniques that provide not only a counter-example, but also certify that the system meets the property. This is exactly what the certified model checking (CMC) has been introduced for. In this second scenario a number of techniques have been previously proposed. Some of the techuiques that deal with finite-state systems can be found in [ 23 , 29 ]. In [ 23 ] an automata-theoretic approach to model checking is addressed. In [ 29 ] a deductive proof system was introduced for verifying branching time properties expressed in the mu-calculus. For infinite-state systems, Mebsout et al. [ 28 ] recently presented a new technique for generating and verifying proof certified in SMT-based model checkers, focusing on proofs of invariant properties. The use of invariants has been exploited in [ 17 , 22 ], where the proof is generated from the inductive invariant obtained with the k -liveness algorithm [ 9 ]. The resulting approach can be implemented as a model checker based on the combination of k -liveness with an engine for invariant properties that is capable of producing inductive invariants. A drawback of this approach is that, although it is very competitive, the task of finding counter-examples and the task of generating proofs (in this case via finding invariants), are very different requiring for the latter the addition of extra mechanisms to the own model checker. In this paper, we propose an CMC based on dual systems of tableaux and sequent calculus, originally introduced in [ 14 , 15 ]. It produces certificate proofs, formal proofs in the sequent calculus, and counterexamples - open branches in the tableau. This is also one of the main advantages of our approach: the same reasoning mechanism applies for both tasks - certificates and counterexamples. The CMC (see Figure 1) differs from the traditional model checking in providing a proof of the satisfiability of the given property, and not only a counter-example. Incorporating the notation of [ 21 ] (and slightly modifying it) we represent the methodology of the certified model checking as the following signature: CMC :: System ×ϕ−→ B×(Proof |Counter-example) where, given a specification of a system, S , and a property, ϕ , a certified model checking produces a Boolean result, B, indicating whether Ssatisfies ϕ, along with a proof (or certification), in the positive case, or a counter-example, in the negative case. A. Abuin, A. Bolotov, U. Díaz de Cerio, M. Hermo, and P. Lucio 12:3 System Specification Property to verify Counter-example Formal Proof No Yes CMC Does the system satisfy the property? Figure 1 General schema of CMC. However, we believe that to take the full advantage of CMC, and enabling its industrial application to real systems, we need to ensure that CMC meets the following requirements. (i) Proofs should be generated automatically. (ii) An CMC needs to offer a CMC user sufficient information to understand the proof without additional “costs” related to specialist knowledge of the underlying proof technique. (iii) The presentation of the proof should enable the CMC users to easily navigate through its trace. This becomes particularly important when the system is badly defined – here the navigation through the trace can help to detect errors. (iv) Finally, when developing a safety critical system following a safety process (e.g. processes of standard ISO26262 [ 19 ], IEC61508 [ 18 ] or EN50128 [ 7 ]), it is mandatory to analyse how a bug in a tool (a model checker in our case) may affect the safety of the developed system. Depending on the level of these effects, some actions are required to increase our confidence in the model checker. One of the mechanisms to increase the probability of finding a failure is to re-evaluate the outputs of the CMC by an independent tool developed by an independent team. We propose a particular CMC method of realising the CMC philosophy (see Figure 2) meeting the characteristics (i)-(iv) above while maintaining the common (for the traditional Model Checker) functionality. Our method is centered on a context-based temporal one-pass tableaux technique whose performance is optimised by a SAT solver. Various tableaux techniques have been proposed for a rich variety of temporal logics, linear and branching: Propositional Linear-Time Temporal Logic (PLTL); Computation Tree Logic (CTL); CTL ∗ which generalizes PLTL and CTL, etc. (an excellent survey can be found in [ 16 ]). One of the core ideas of the tableaux methods is to identify eventualities within the given temporal input and to check that they are fulfilled. Traditional tableaux techniques require two phases to perform this test. In the first phase, a graph which gives all possible pre-models for the tableau input, in constructed. In the second phase, for each state, s in this graph, that contains some “eventually ϕ ”, a graph-theoretic algorithm looks for a state, reachable from s , that satisfies ϕ . Note also that the two-pass tableaux methods fail to maintain the classical correspondence between tableaux and sequents that associates a sequent proof with the closed tableau. TIME 2019 12:4 Towards Certified Model Checking for PLTL Using One-Pass Tableaux System Specification Property to verify Counter-example Formal Proof No Yes CMC Formalization of rules in Isabelle/HOL Formal proof Re-verification SAT-Solver Tableaux method Figure 2 General schema of the proposal. To avoid the second phase and, hence, to keep the ability of generating (sequent) proofs from tableaux, in [ 14 , 15 ], dual systems of tableaux and sequents, for PLTL, were presented. Every logic defined in [ 14 , 15 ] was proved to be sound and complete. In particular, [ 15 ] contains a proof that the tableau system we use in the present paper, is a decision method for the full PLTL, i.e. it is sound, refutationally complete, and terminating. The termination property is achieved on the basis of any fair selection strategy. A very similar sequent calculus is presented in [ 6 ] (see [ 15 ] for more details about the similarities and differences of these systems). The one-pass tableau method [ 15 ] has been extended to a concurrent constraint logic in [12], and also to ECTL]- a branching-time sublogic of CTL∗in [5]. The tableau method in [ 15 ] makes use of the so-called context of an eventuality to force its fulfillment. The context of an eventuality is simply the set of formulae that “accompanies” the eventuality in the label of the node. When a one-pass tableau checks whether a property ϕholds or not, it is always able to issue a certificate: either a counter-model or a complete explanation (formal proof) of why ϕis true. We abbreviate the one-pass tableau method as τ↑ pltl and its dual sequent calculus as TTC. Considering one-pass tableau method as one of the core components of the CMC solution we present in this paper, we argue that it conforms with the properties (i)-(iv) mentioned above. Indeed, the method automatically checks whether the specification of the system satisfies the property (i). 1 If it does not then it provides a counter-example. A counterexample is given by a trace which is intuitively clear (ii). In the case of a positive answer, a relevant proof certifies it. Again, the output proof is represented as a trace enabling an easy navigation through it (iii). Moreover, one of the attractive features of our method is that it forces the eventualities to be fulfilled as soon as possible, thus, the method will potentially generate shorter paths (with fewer nodes) than those produced by non-context based tableaux. In our proposal, the performance of the one-pass tableau technique is complemented, for efficiency, by the SAT solving. Note that the idea of encoding of transition systems into propositional SAT was first proposed in [ 20 ] for AI planning problems, where the authors show that SAT algorithms scale much better on the SAT-encodings than planing algorithms 1 For the purposes of the paper, we let the specification, S , be in a dedicated form S = Init ∧T R , where Init is a PLTL formula that represents the initial states and T R is the representation of all the transitions allowed, see §3 for details. A. Abuin, A. Bolotov, U. Díaz de Cerio, M. Hermo, and P. Lucio 12:5 on the original graph formulation. Following this success, SAT solvers have been also used in Bounded Model Checking (BMC). In both frameworks, a propositional formula is used to encode the input problem. Planning problems deal with finite paths along a finite graph, hence the encoding is complete w.r.t. the original problem. In model checking, paths within the transition systems are, in general, infinite. SAT-based BMC utilises the encoding of the model-checking problems in satisfiability checking, more precisely, the propositional encoding of statements expressing that there exists a lengthk path (along the transition system) that does not satisfy a given property. The BMC increases k until either the SAT’s answer is “yes” (i.e. a counter-example is found), or the search becomes intractable, or k reaches a certain bound. The original SAT-based BMC algorithm [ 3 ], although complete for finite state, is limited in practice to falsification. Many additional strategies have been introduced to make BCM complete, see [ 4 ] for a good survey. There is also a large amount of work, starting with [ 32 ], on using SAT solving for improving the satisfiability test of the full PLTL. Recent papers [ 24 , 25 ] use SAT solvers to seek for a model for an input formula. This model is essentially a graph/automaton produced by the first pass of a two-pass tableau method, which should be followed for testing the fulfilment of eventualities. SAT solvers are called for the generation of all (different) successors of every state in the graph. The authors use well-known temporal equivalences (like pUq≡ ( q∨ ( p∧◦ ( pUq ))) to compute the successors of the given state. Here, the method utilises the renaming of subformulae containing temporal modalities (such as pUq ) by fresh propositional variables and utilise the SAT solving to calculate different successor states of each state in the transition system. This prevents the repeated generation of “propositionally equivalent” states. The relevant heuristics for pruning the search-space and on-the-fly mechanism for testing eventuality fulfilment are introduced in the implementation. Our proposal uses SAT solvers in a similar way, but is very different in the primary goals. In our method, SAT solvers are employed to calculate a set of the “next” states in the tableau: being in the “current state”, SAT solver calculates those successor states in the transition systems that satisfy the negation of the tested property. For that, we do not rename all temporal modalities in the label of the tableau node, but only those of the form ◦ϕ , where ϕ only contains classical operators. Moreover, our proposal of using the one-pass tableau technique (helped, for efficiency, by the SAT solver) is complete for deciding (unbounded) model checking problems and works on infinite traces. The most remarkable difference of our proposal (regarding [ 24 , 25 ]) is related to the fact that we pursue CMC, i.e. we would like to generate proofs in a calculus for PLTL, hence we use the one-pass context-based tableau along with its dual sequent calculus. In addition, the context-based tableau is particularly well suited for dealing with the specifications of transition systems (“always”-formulae); the context plays the role “of forcing eventualities to be fulfilled as soon as possible” and acts as a semantic constraint that prevents the generation of several states (which are generated in the two-pass approach). In building the proof, we invoke Isabelle/HOL [ 30 ] to verify the construction of the tableaux in order to avoid possible errors caused by the implementation (iv). This external validation is carried out by a sequent calculus TTC which is formalized in Isabelle/HOL and is dual to the one-pass tableau method. We also note that the same reasoning mechanism based on the one-pass tableau is applied in our approach to counter-examples and proofs which makes the tool easy to understand. This facilitates the industrial spreading of CMC. The remaining of the paper is organised as follows. In §2 we review the technique to construct a one-pass tableau τ↑ pltl . In §3 we present one-pass tableau based model checking. This follows by the description of the certification utilising Isabelle in §4. Finally, in §5 we summarise the results and provide an account of future work. TIME 2019 12:6 Towards Certified Model Checking for PLTL Using One-Pass Tableaux 2 One-pass Context-based Tableau To make the paper self-contained and easier to read, in this section we first recall the syntax and semantics of the underlying logic, PLTL and then we will review the one-pass tableau method. 2.1 Syntax and Semantics of PLTL IDefinition 1 (PLTL Language).The language of PLTL comprises A set, Prop, of propositional symbols. Propositional connectives ¬,∧,∨, and constants Tand F Future-time temporal connectives, “  ” (always), “ ♦ ” (eventually) “ ◦ ” (at the next moment in time), “U” (until), and “R” (release). IDefinition 2 (WFF PLTL ) . The set of well-formed formulae of PLTL, denoted by WFF PLTL , is inductively defined as the smallest set satisfying the following. Any element of P rop,Tand Fare in WFFPLTL. If Aand Bare in WFFPLTL then so are ¬A, A ∧B, A ∨B, A, ♦A, AUB, and ARB. A literal is either a propositional symbol (a positive literal) or the negation of a propositional symbol (a negative literal). Definition 1 introduces PLTL with the set of temporal operators that are convenient for our representation in the paper. We note that this set is richer than {U,◦} which is known to be sufficient to represent all other linear-time temporal operators. For example, ‘ ♦ϕ ’ can be defined as TUϕ while ϕRψ can be defined via U as ¬ ( ¬ϕU¬ψ )(here and in the remaining of the paper ϕand ψare meta-symbols denoting PLTL formulae). Formulae of the type ♦ϕ and ϕUψ are called eventualities, and formulae of the type ϕ are called always-formulae. A model, M = s0, s1, s2, s3, . . . , for PLTL formulae is a discrete, linear sequence of states, isomorphic to natural numbers, N . Each state, si, 0 ≤i , is a set of positive literals, which are satisfied at the i -th moment of time. We write hM, ii | = ϕ to indicate that ϕ is true in the model Mat the (state) index i∈N. Below we inductively define the relation | =which evaluates PLTL formulae in a model M at i -th moment of time. Note that here we follow so called “anchored” version of PLTL that defines the PLTL validity and satisfiability (see below) at the “beginning” of time, the initial state, s0of a model. hM, ii |=T hM, ii 6|=F hM, ii |=¬ϕiff hM, ii 6|=ϕ hM, ii |=ϕ∧ψiff hM, ii |=ϕand hM, ii |=ψ hM, ii |=ϕ∨ψiff hM, ii |=ϕor hM, ii |=ψ hM, ii |=◦ϕiff hM, i + 1i |=ϕ hM, ii |=ϕiff hM, ji |=ϕfor every j≥i. hM, ii |=♦ϕiff there exists j≥isuch that hM, ji |=ϕ. hM, ii | = ϕUψ iff there exists j≥i such that hM, ji | = ψ and for every k, i ≤k < j , we have hM, ki |=ϕ. hM, ii | = ϕRψ iff for every j≥i , either hM, ji | = ψ or there exists k such that i≤k < j and hM, ki |=ϕ. A. Abuin, A. Bolotov, U. Díaz de Cerio, M. Hermo, and P. Lucio 12:7 IDefinition 3 (PLTL satisfiability, validity) . If, for a formula ϕ , there exists a model, M , such that ( M, 0) | = ϕ then ϕ is satisfiable. Formula ϕ is called valid if it is satisfiable in all models. In the remaining of the paper we will use capital letters Φ , Ψ , ∆ , . . . to denote sets of PLTL formulae. The semantics above can be extended to sets of formulae in the standard way: given a set of PLTL formulae Φ = γ1, γ2,...γn , the following holds: hM, ii | = Φ iff hM, ii |=γk, for all k, 1≤k≤n. 2.2 Useful PLTL properties In this section we recall those PLTL syntactic and semantic properties that are useful for our tableau construction. First, the tableau procedure will take as an input PLTL formulae converted to their negated normal forms (NNF). IDefinition 4 (Procedure for obtaining NNF) . For a given PLTL formula, ϕ , push the negations in ϕ inward until they are applied only to propositions. This involves applying the standard set of rewrite rules used to obtain NNF in classical logic (including ¬T−→ F and ¬F−→ T) with the additional transformations for temporal operators: ¬◦ϕ−→ ◦¬ϕ¬ϕ−→ ♦¬ϕ¬♦ϕ−→ ¬ϕ ¬(ϕUψ)−→ ¬ϕR¬ψ¬(ϕRψ)−→ ¬ϕU¬ψ The following result [26] can be easily established. IProposition 5 (Translation into NNF preserves satisfiability) . For any PLTL formula ϕ , the following holds hM,0i |=ϕiff hM,0i |=NNF(ϕ). As a simple example, NNF(¬◦¬a) = ◦♦a. We will utilise this in §3. In what follows we deal with sets of formulae in NNF . Literals and formulae in NNF of the form F , T and ◦ϕ are called elementary, the remaining formulae are subsequently called non-elementary. In addition, sets of elementary formulae are also called elementary. IDefinition 6 (Consistent set of PLTL formulae in NNF) . A set of PLTL formulae in NNF is consistent if it does neither contain F , nor {ϕ, NNF ( ¬ϕ ) } for any formula ϕ . Otherwise it is called inconsistent. Note that the above notion of consistency is syntactic. To check whether {ϕ, ψ} is inconsistent we test if ϕ=NNF(¬ψ). The cost of this check is linear on the length of the formula. Since our transition system specifications are given by sets of PLTL formulae and PLTL has the finite model property [ 33 ] we can consider its interpretation over cyclic structures. Noting that an infinite sequence s0, s1, . . . , sk, . . . induces the successor relation, R , such that ( si, si+1 ) ∈R for all i∈π , we define below the notions of a cyclic sequence, cyclic path and cyclic model. IDefinition 7 (Cyclic Sequence, Cyclic Path) . Let π be a finite sequence of states π = s0, s1, . . . , sj. Then πis cyclic iff there exists si,0≤i≤jsuch that (sj, si)∈R. A sequence si, . . . , sjis a loop with a cycling element siabbreviated as hsi, . . . , sjiω. A cyclic path over a cyclic sequence πis an infinite sequence ξ(π) = s0, s1, . . . , si−1hsi, si+1, . . . , sjiω. TIME 2019 12:8 Towards Certified Model Checking for PLTL Using One-Pass Tableaux IDefinition 8 (Cyclic Model).A model Mis cyclic if it is a cyclic path. Now, assuming that PLTL formulae are interpreted over cyclic models, we overview the construction of the one-pass tableau τ↑ pltl applied to some input Σ, in symbols τ↑ pltl (Σ), adapting the technique developed in [ 15 ]. We will see, in the subsequent sections, the benefits of its main feature – checking the validity of the given input in “one pass”, without the second “pass” where an auxiliary graph is built to check if all the eventualities are satisfied or not. IDefinition 9 (Tableau, Consistent Node, Closed branch) . A one-pass tableau for a set of formulae Σ, abbreviated as τ↑ pltl (Σ) is a labelled tree T , where nodes are labeled with sets of formulae, such that the following two conditions hold: (a) The root is labelled by the tableau input, Σ. (b) Any other node, m , is labelled with sets of formulae as the result of the application of one of the expansion rules to the parent node, n. A node n∈T is consistent, abbreviated as n> , if its label is a consistent set of formulae (see Def. 6), else nis inconsistent, abbreviated as n⊥. If a branch, b, of T, contains an inconsistent node n⊥, then bis closed, else bis open. Informal Introduction to one-pass tableau. In the set of expansion rules, on the top of the standard α−β rules, we also have β+ rules that are characteristic (and crucial!) for our construction. These rules (which were originally introduced in [ 14 , 15 ]) reflect our dedicated account of the eventualities, namely, we treat an eventuality as occurring in some context. By the context of the selected eventuality, we understand a collection of all other formulae within the label of the node. Subsequently, β+ rules use the context to force eventualities to be fulfilled as soon as possible. The tableau expansion rules apply repeatedly until they produce an inconsistent node, n⊥ , or a node with the labels that already occurred within the given path. In the former case the expansion of the given branch terminates with n⊥ as a leaf. In the latter case, a repetitive node in the branch witnesses that the branch is open. Once no more expansion ( α−β, β+ type) rules are applicable to the given branch with the last consistent node n> , the expansion rules ensure that its labelling is similar to a “state” in the standard temporal tableau. Then the “next-state” rule applies which generates successors with the labels that are arguments of all ◦ modalities and the whole cycle of applying the expansion and the “next-state” rules is repeated until the tableau construction terminates. The nature of our rules ensures that the terminated tableau is either closed, indicating that the input does not have a model, hence unsatisfiable, or open, indicating a model for the tableau input. 2.3 τ↑ pltl Rules Recall that all formulae in the input of the tableau have been already transformed into their NNF. Presenting α -, β - and “next-state” rules for the construction of the semantic tableaux, we assume that these apply respectively, to α -formulae, β -formulae and “next”-formulae such that α1 denotes the set of formulae in the conclusion of an α -rule, while β1, β2 denote the sets of formulae in the alternative conclusions of a β -rule, and γ1 denotes the result of “jumping” from a state to a pre-state. The sets of α−β rules are given in Table 1. These are standard in temporal tableaux construction (see, for instance, [2]). A. Abuin, A. Bolotov, U. Díaz de Cerio, M. Hermo, and P. Lucio 12:9 Table 1 α−β-rules. α α1 (∧)ϕ∧ψ ϕ, ψ ()ϕ ϕ, ◦ϕ β β1β2 (U)ϕUψ ψ ϕ, ◦(ϕUψ) (R)ϕRψ ϕ, ψ ψ, ◦(ϕRψ) (∨)ϕ∨ψ ϕ ψ (♦)♦ϕ ϕ ◦♦ϕ Table 2 β+-rules, where ∆is a (possibly empty) set (conjunction) of formulae, If ∆ 6 = ∅ then ∆ 0 is a set (conjunction) of all elements of ∆except for  -formulae and ¬ ∆ 0 is the disjunction of all negated elements of ∆0, else ¬∆0is F. β β1β2 (U)+∆, ϕUψ∆, ψ ∆, ϕ, ◦((ϕ∧(NNF(¬∆0)))Uψ) (♦)+∆,♦ϕ∆, ϕ ∆,◦((NNF(¬∆0))Uϕ) β+ rules (see Table 2) are crucial in the construction of τ↑ pltl as they use the so-called context,∆, to force the eventuality ϕUψ to be fulfilled as soon as possible. We illustrate this concept on the ( U ) + rule. When ( U ) + is applied to a node labelled by a set of formulae { ∆ , ϕUψ} , then the context is ∆and the resulting labelling of the next node contains the formula ( ϕ∧ ¬ ∆) Uψ , where ¬ ∆means the disjunction of all negated elements of ∆. Therefore, if ψ is not satisfied, then ¬ ∆also belongs to the label of that node. This means that the context, ∆, of the previous label is not repeated. As ∆is a finite set/conjunction of formulae and ¬ ∆is the finite disjunction of the negations of the formulae in ∆, the ( U ) + rule forces at least one formula in ∆to be falsified during the transition from the previous node to the subsequent one, whenever ψis not satisfied. Note that the (U)+rule only applies to some selected eventuality, and in this sense, the unique eventuality, which becomes marked. Each application of the ( U ) + rule to the set { ∆ , ϕUψ} introduces the so-called next-step variant ( ϕ∧ ( NNF ( ¬ ∆ 0 )) Uψ where ∆ 0 , as we know, is a conjunction of all elements of ∆ except for  -formulae, which keeps the mark for the selected eventuality. Note that any formula of the type ϕ , which was a member of ∆, will be repeated forever and if we keep it in ∆ 0 it would appear in the resulting NNF ( ¬ ∆ 0 )as a disjunct ♦¬ϕ which would never be satisfied. Hence, any  - formula can be immediately dropped when we form ∆ 0 . For the soundness of the construction, each node of the tableau must have at most one marked eventuality, i.e. the one to which the ( U ) + has been applied. Note that when a node of the tableau does not contain any marked eventuality, then one of them is randomly marked. The ( U ) + rule allows us to avoid the construction of the auxiliary graph of stages (the second pass in two-pass tableau methods) which is used to determine whether all eventualities are satisfied or not. The other β+ rule, ( ♦ ) + , is obviously derivable from the ( U ) + rule. However, we present it as part of the tableau as its application makes proofs more transparent to the reader and the user of the tableau as a model checker. We will explain this in the subsequent sections of the paper. It is worth noting that, because in the β+ rules, ¬ ∆ 0 = F whenever ∆ = ∅ , the β rules ( U )and ( ♦ )become particular cases of β+ rules ( U ) + and ( ♦ ) + when ∆ = ∅ . In this case the β2 child of the ( U ) + rule is reduced to ϕ, ◦ ( FUψ ), from which we can derive the β2 child of the (U)rule. TIME 2019 12:16 Towards Certified Model Checking for PLTL Using One-Pass Tableaux We have also implemented a method one_step_solver_print which prints into a file of text all applications of the TTC rules that are hidden in the big-step proof. Indeed, it is a printing version of the method one_step_solver. Calling one_step_solver_print, instead of one_step_solver, we can generate a small-step proof (see lemma runningExample_smallStep_proof) for the user wishing to check the Isabelle’s subgoals step by step. This proof is the result of the substitution, in the big-step proof, of each of the five occurrences of apply one_step_solver by the list of “apply” instructions of TTC_Calculus rules. The method one_step_solver_print prints such a list, in a text file, while it is solving the goal. 5 Conclusions In this paper we have presented a novel framework of applying a Certified Model Checking methodology. Our method involves the representation of the system specification, S , in a specific format that reflects the dynamic behaviour of the system. First, it involves the formalization of the “initial conditions”, (the Init PLTL formula), that specifies the initial states of the model to be build. Second, we use the representation, TR , of the transition relation to build a state space of the system, as a “global invariant”. Finally, the property, P , to be checked against the specification S is written as a PLTL formula. This task is performed by a one-pass temporal tableau, τ↑ pltl . It takes S, ¬P as its input (converted into the NNF). For an eventuality to be fulfilled, the tableau technique essentially uses its context. Tableau rules that deal with the eventualities in NNF ( ¬P ), force their fulfilment “as soon as possible”. This process is optimised by a SAT solver, which tackles non-temporal content of the tableau nodes. The tableau method, in one pass, either returns a negative answer, producing a counter-example, thus showing that P is not satisfied by S , or verifies P against the system specification. In the latter case, our method generates an explicit and easily readable evidence in Isabelle/HOL. In this way the tableau result is formally proven and the user can review the test to make sure that everything is working as expected (or that no errors have been made with the specification). Our future work will cover three directions. First, it is further work on the implementation of and experimentation with the one-pass tableau and the embedded SAT solver. Second, the developed Isabelle automatic solver for proof generation is only an initial prototype and we will improve its efficiency. Finally, note that the one-pass tableau method has been also developed for the branching-time setting, tackling Computation Tree Logic CTL ([ 6 ]), widely used in model checking, and for a richer logic, ECT L] ([ 5 ]). This will enable us to extend the use of the one-pass tableau as a model checker to the branching-time setting, as the extensions are conceptually intuitive. References 1 Hasan Amjad. Programming a Symbolic Model Checker in a Fully Expansive Theorem Prover. In Theorem Proving in Higher Order Logics, pages 171–187. Springer Berlin Heidelberg, 2003. doi:10.1007/10930755_11. 2 Mordechai Ben-Ari. Mathematical Logic for Computer Science. Springer-Verlag, London, 2012. doi:10.1007/978-1-4471-4129-7. 3 Armin Biere, Alessandro Cimatti, Edmund M. Clarke, Masahiro Fujita, and Yunshan Zhu. Symbolic Model Checking Using SAT Procedures Instead of BDDs. In Proceedings of the 36th Annual ACM/IEEE Design Automation Conference, DAC ’99, pages 317–320, New York, NY, USA, 1999. ACM. doi:10.1145/309847.309942. A. Abuin, A. Bolotov, U. Díaz de Cerio, M. Hermo, and P. Lucio 12:17 4 Armin Biere and Daniel Kröning. SAT-based model checking. In Edmund M. Clarke, Thomas A. Henzinger, Helmut Veith, and Roderick Bloem, editors, Handbook of Model Checking, pages 277– 303. Springer International Publishing, Cham, 2018. doi:10.1007/978-3-319-10575-8_10. 5 Alexander Bolotov, Montserrat Hermo, and Paqui Lucio. Extending Fairness Expressibility of ECTL+: A Tree-Style One-Pass Tableau Approach. In Natasha Alechina, Kjetil Nørvåg, and Wojciech Penczek, editors, 25th International Symposium on Temporal Representation and Reasoning (TIME 2018), volume 120 of Leibniz International Proceedings in Informatics (LIPIcs), pages 5:1–5:22, Dagstuhl, Germany, 2018. Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik. doi:10.4230/LIPIcs.TIME.2018.5. 6 Kai Brünnler and Martin Lange. Cut-free sequent systems for temporal logic. The Journal of Logic and Algebraic Programming, 76(2):216–225, 2008. doi:10.1016/j.jlap.2008.02.004. 7 CENELEC and EN50128. 50128. Railway applications-Communication, Signaling and Processing Systems-Software for Railway Control and Protection Systems, 2011. 8 Alessandro Cimatti, Edmund Clarke, Fausto Giunchiglia, and Marco Roveri. NUSMV: a new symbolic model checker. International Journal on Software Tools for Technology Transfer, 2(4):410–425, March 2000. doi:10.1007/s100090050046. 9 Koen Claessen and Niklas Sörensson. A liveness checking algorithm that counts. In Gianpiero Cabodi and Satnam Singh, editors, Formal Methods in Computer-Aided Design, FMCAD 2012, Cambridge, UK, pages 52–59. IEEE, 2012. 10 Edmund M. Clarke and E. Allen Emerson. Design and Synthesis of Synchronization Skeletons Using Branching-Time Temporal Logic. In Logics of Programs, Workshop, Yorktown Heights, New York, May 1981, pages 52–71, 1981. doi:10.1007/BFb0025774. 11 Edmund M. Clarke, Orna Grumberg, and Doron A. Peled. Model Checking. MIT Press, Cambridge, MA, USA, 1999. 12 Marco Comini, Laura Titolo, and Alicia Villanueva. Abstract Diagnosis for tccp using a Linear Temporal Logic. Theory and Practice of Logic Programming, 14(4-5):787–801, 2014. doi:10.1017/S1471068414000349. 13 Javier Esparza, Peter Lammich, René Neumann, Tobias Nipkow, Alexander Schimpf, and JanGeorg Smaus. A Fully Verified Executable LTL Model Checker. In Computer Aided Verification, pages 463–478. Springer Berlin Heidelberg, 2013. doi:10.1007/978-3-642-39799-8_31. 14 Joxe Gaintzarain, Montserrat Hermo, Paqui Lucio, Marisa Navarro, and Fernando Orejas. A Cut-Free and Invariant-Free Sequent Calculus for PLTL. In Jacques Duparc and Thomas A. Henzinger, editors, Computer Science Logic, 21st International Workshop, CSL 2007, 16th Annual Conference of the EACSL, Lausanne, Switzerland, September 11-15, 2007, Proceedings, volume 4646 of Lecture Notes in Computer Science, pages 481–495. Springer, 2007. doi: 10.1007/978-3-540-74915-8_36. 15 Joxe Gaintzarain, Montserrat Hermo, Paqui Lucio, Marisa Navarro, and Fernando Orejas. Dual Systems of Tableaux and Sequents for PLTL. The Journal of Logic and Algebraic Programming, 78(8):701–722, 2009. doi:10.1016/j.jlap.2009.05.001. 16 Rajeev Goré. Tableau Methods for Modal and Temporal Logics. In Marcello D’Agostino, Dov M. Gabbay, Reiner Hähnle, and Joachim Posegga, editors, Handbook of Tableau Methods, pages 297–396. Springer Netherlands, Dordrecht, 1999. doi:10.1007/978-94-017-1754-0_6 . 17 Alberto Griggio, Marco Roveri, and Stefano Tonetta. Certifying Proofs for LTL Model Checking. In Formal Methods in Computer-Aided Design, FMCAD 2018, Austin, USA, pages 1–9, October 2018. doi:10.23919/FMCAD.2018.8603022. 18 IEC. IEC 61508 Functional safety of electrical/electronic/programmable electronic safetyrelated systems, 2010. 19 ISO. Road vehicles – Functional safety, 2011. 20 Henry Kautz and Bart Selman. Pushing the Envelope: Planning, Propositional Logic, and Stochastic Search. In Proceedings of the Thirteenth National Conference on Artificial Intelligence - Volume 2, AAAI’96, pages 1194–1201. AAAI Press, 1996. URL: http://dl.acm. org/citation.cfm?id=1864519.1864564. TIME 2019 12:18 Towards Certified Model Checking for PLTL Using One-Pass Tableaux 21 Jörg Kreiker, Andrzej Tarlecki, Moshe Y. Vardi, and Reinhard Wilhelm. Modeling, Analysis, and Verification - The Formal Methods Manifesto 2010 (Dagstuhl Perspectives Workshop 10482). Dagstuhl Manifestos, 1(1):21–40, 2011. doi:10.4230/DagMan.1.1.21. 22 Tuomas Kuismin and Keijo Heljanko. Increasing Confidence in Liveness Model Checking Results with Proofs. In Valeria Bertacco and Axel Legay, editors, Hardware and Software: Verification and Testing, pages 32–43. Springer International Publishing, 2013. 23 Orna Kupferman and Moshe Y. Vardi. From complementation to certification. Theoretical Computer Science, 345(1):83–100, 2005. doi:10.1007/978-3-540-24730-2_43. 24 Jianwen Li, Geguang Pu, Lijun Zhang, Moshe Y Vardi, and Jifeng He. Accelerating LTL satisfiability checking by SAT solvers. Journal of Logic and Computation, 28(6):1011–1030, April 2018. doi:10.1093/logcom/exy013. 25 Jianwen Li, Shufang Zhu, Geguang Pu, Lijun Zhang, and Moshe Y. Vardi. SAT-based explicit LTL reasoning and its application to satisfiability checking. Formal Methods in System Design, January 2019. doi:10.1007/s10703-018-00326-5. 26 Zohar Manna and Amir Pnueli. The Temporal Logic of Reactive and Concurrent Systems. Springer-Verlag, Berlin, Heidelberg, 1992. doi:10.1007/978-1-4612-0931-7. 27 Daniel Matichuk, Toby Murray, and Makarius Wenzel. Eisbach: A Proof Method Language for Isabelle. Journal of Automated Reasoning, 56, January 2016. doi:10.1007/ s10817-015-9360-2. 28 Alain Mebsout and Cesare Tinelli. Proof Certificates for SMT-based Model Checkers for Infinite-state Systems. In Proceedings of the 16th Conference on Formal Methods in ComputerAided Design, FMCAD ’16, pages 117–124, 2016. doi:10.1109/FMCAD.2016.7886669. 29 Kedar S. Namjoshi. Certifying Model Checkers. In Proceedings of the 13th International Conference on Computer Aided Verification, CAV ’01, pages 2–13. Springer-Verlag, 2001. doi:10.1007/3-540-44585-4_2. 30 Tobias Nipkow, Lawrence C. Paulson, and Markus Wenzel. Isabelle/HOL — A Proof Assistant for Higher-Order Logic, volume 2283 of LNCS. Springer, 2002. doi:10.1007/3-540-45949-9 . 31 Jean-Pierre Queille and Joseph Sifakis. Specification and verification of concurrent systems in CESAR. In Mariangiola Dezani-Ciancaglini and Ugo Montanari, editors, International Symposium on Programming, pages 337–351, Berlin, Heidelberg, 1982. Springer Berlin Heidelberg. doi:10.1007/3-540-11494-7_22. 32 Kristin Y. Rozier and Moshe Y. Vardi. LTL Satisfiability Checking. In Dragan Bošnački and Stefan Edelkamp, editors, Model Checking Software, pages 149–167, Berlin, Heidelberg, 2007. Springer Berlin Heidelberg. doi:10.1007/978-3-540-73370-6_11. 33 Aravinda P. Sistla and Edmund M. Clarke. The Complexity of Propositional Linear Temporal Logics. In Proceedings of the Fourteenth Annual ACM Symposium on Theory of Computing, STOC ’82, pages 159–168, New York, NY, USA, 1982. ACM. doi:10.1145/800070.802189.