Alex Abuin Yepes: "Certificates for decision problems in temporal logic using context- based tableaux and sequent calculi“.

Zuzendariak_Directores: Montserrat Hermo Huguet /Jorge Parra Molina.

2023_03_03, 10:00 Sala Ada Lovelace aretoa.

Abstract:

"We introduce a context-based tableau method to solve the problem of satis-fiability and model checking for temporal logic. In particular, we apply the method to the propositional linear-time temporal logic (PLTL), the com-putation tree logic (CTL) and to one of its extensions (ECTL). The main feature of our method is that it does not require auxiliary constructions or extra-logic rules, which allow us to maintain the classical duality between tableaux and sequent calculi. Context-based tableaux work as follows: for any input formula, ϕ, a closed tableau represents a formal sequent proof that certifies the unsatisfiability of ϕ, whereas an open tableau provides at least one model that certifies the satisfiability of ϕ. Therefore, in this framework satisfiability and model-checking tests can be performed and complemented by two types of certificates: proofs and models.
In this thesis, we specialise the general method when apply to PLTL (symbolic) model checking. Concretely, we propose the use of a SAT solver to deal with those formulae that specify transitions systems. In this scenario, we also explore the use of the interactive theorem prover, called Isabelle, to perform two certification-related tasks. The first is to certify the method itself. As an example of this, an automated proof that our method is sound (performed in Isabelle) is presented. The second is the possibility offered by Isabelle to re-verify the certificates produced by the tableaux. We provide an example where the output of a closed tableau is a refutational proof with a syntax that Isabelle understands and then, invoking Isabelle the proof can be replicated.
The proposed specialization in addressing PLTL model checking applies immediately to PLTL satisfiability, since the latter problem can be reduced to the problem of PLTL model checking. As a result, the same mechanism is suitable for certifying both PLTL model checking and PLTL satisfiabil-ity. However, in the context of branching-time temporal logics, the satisfi-ability problem cannot be reduced to the model-checking problem. Hence, model-checking algorithms for these logics cannot be adapted for testing satisfiability.

In this dissertation, we study in depth the satisfiability for (CTL) and (ECTL) and propose two context-based tableau methods to solve both prob-lems. The proof of the correctness (soundness, completeness and termi-nation) of the methods are provided. We define algorithms for obtaining tableaux which produce models and formal proofs depending on whether the input formula is satisfiable or not. Our proposal is again suitable for certifying the model checking for branching-time temporal logics. This is due to the fact that model checking always reduces to satisfiability.
Finally, we describe in detail the algorithm for CTL, present a real imple-mentation, and provide experimental results. The prototype has been done using the Dafny language, which is a verification-ready programming lan-guage that constantly flags any errors and gives the go-ahead when the code matches its specification. Dafny can compile the final code to C#, Java, JavaScript or Go. We have generated Java code, but also and more impor-tantly, Dafny has allowed us to prove critical properties that give confidence in the validity and accuracy of the prototype".