Weryfikacja temporalnych własności algorytmów niedeterministycznych

W pracy zaprezentowany został system dowodowy dla logiki temporalnej czasu rozgałęzionego, nazwany Temporalną Logiką Procesów. Pozwala on na badanie statycznych i dynamicznych własności programów wyrażonych jako formuły temporalne rozważanego języka. Udowodniono mocne twierdzenie o pełności dla przedstawionego systemu formalnego.

---

This paper provides one of the versions of prepositional, branching time temporal logic, called Process Temporal Logic. It allows to verify static and dynamic properties of programs, which are expressed as temporal formulas. PTL system is presented with the infinitary axiomatic system and the proof of the completeness theorem. The majority of temporal logics treats a program as a separate object and not as a language element. The system shown in this article is different. Program is a part of expression which describes its quality just as in dynamic and algorithmic logic.