Browsing Comunicaciones by Author "Bolotov, Alexander"

Now showing items 1-3 of 3

    • Thumbnail

      Extending Fairness Expressibility of ECTL+: A Tree-Style One-Pass Tableau Approach 

      Bolotov, Alexander; Hermo Huguet, Montserrat; Lucio Carrasco, Francisca (Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2018-10-08)
      Temporal logic has become essential for various areas in computer science, most notably for the specification and verification of hardware and software systems. For specification purposes rich temporal languages are required ...
    • 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 ...