We use cookies in order to improve the quality and usability of the HSE website. More information about the use of cookies is available here, and the regulations on processing personal data can be found here. By continuing to use the site, you hereby confirm that you have been informed of the use of cookies by the HSE website and agree with our rules for processing personal data. You may disable cookies in your browser settings.

  • A
  • A
  • A
  • ABC
  • ABC
  • ABC
  • А
  • А
  • А
  • А
  • А
Regular version of the site

At the ISSA laboratory seminar Prof. Mark Reynolds gave a talk entitled: "A Faster Tableau for CTL*"

Prof. Mark Reynolds is the Head of the School of Computer Science and Software Engineering at The University of Western Australia

Title: "A Faster Tableau for CTL*"

SpeakerMark Reynolds, Head of the School of Computer Science and Software Engineering at The University of Western Australia.
Abstract :
There have been several recent suggestions for tableau systems for deciding satisfiability in the practically important branching time temporal logic known as CTL*. In this talk we present a streamlined and more traditional tableau
approach built upon the author's earlier theoretical work.
Soundness and completeness results are proved. A prototype implementation demonstrates the significantly improved performance of the new approach on a range of test formulas. We also see that it compares favourably to state of the art, game and automata based decision procedures.