Browsing Comunicaciones by Author "Abuin Yepes, Alex"

Now showing items 1-2 of 2

    • Thumbnail

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

      Abuin Yepes, Alex; Bolotov, Alexander; Hermo Huguet, Montserrat; Lucio Carrasco, Francisca (Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020-09-25)
      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 ...
    • Thumbnail

      Towards Certified Model Checking for PLTL Using One-Pass Tableaux 

      Abuin Yepes, Alex; Bolotov, Alexander; Díaz de Cerio, Unai; Hermo Huguet, Montserrat; Lucio Carrasco, Francisca (Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019-10-19)
      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 ...