Abstract
In this paper is introduced a proof system for branching time temporal logic, called PTL. It allows to verify static and dynamic properties of nondeterministic programs, which are expressed as a temporal formulas of PTL language. The strong completeness theorem of this system is presented.
Get full access to this article
View all access options for this article.