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

Satisfiability Checking Algorithms of Formulas of Temporal Logics

Student: Brazhenko Andrey

Supervisor: Mikhail Rybakov

Faculty: Faculty of Mathematics

Educational Programme: Joint Bachelor's Programme with the Centre for Teaching Excellence (Bachelor)

Year of Graduation: 2024

В этой статье представлено подробное описание и анализ существующего алгоритма проверки выполнимости формул линейной временной логики (LTL), ранее представленного в работе (Pierre Wolper. “The Tableau Method for Temporal Logic: An Overview”. In: Logique Et Analyse 28.110-111 (1985), pp. 119–136.). Также в статье предложено новое усовершенствование этого алгоритма.

Student Theses at HSE must be completed in accordance with the University Rules and regulations specified by each educational programme.

Summaries of all theses must be published and made freely available on the HSE website.

The full text of a thesis can be published in open access on the HSE website only if the authoring student (copyright holder) agrees, or, if the thesis was written by a team of students, if all the co-authors (copyright holders) agree. After a thesis is published on the HSE website, it obtains the status of an online publication.

Student theses are objects of copyright and their use is subject to limitations in accordance with the Russian Federation’s law on intellectual property.

In the event that a thesis is quoted or otherwise used, reference to the author’s name and the source of quotation is required.

Search all student theses