Temporal logics for reasoning under fairness assumptions (mechanical verification, decision procedures)
Chin‐Laung Lei · 1986
In this dissertation, we consider the problem of whether the branching time or linear time framework is more appropriate for reasoning about concurrent programs in light of the criteria of expressiveness and complexity. We pay special attention to the problem of temporal reasoning under (various) fairness assumptions. In particular, we focus on the following: (1) The Model Checking Problem--Given a formula p and a finite structure M, does M define a model of p? (2) The Satisfiability Problem--Given a formula p, does there exist a structure M which defines a model of p? Algorithms for the model checking problem are useful in mechanical verification of finite state concurrent systems. Algorithms for testing satisfiability have applications not only to the automation of verification of (possibly infinite state) concurrent programs, but also in mechanical synthesis of concurrent programs where the decision procedure is used to construct a model of the specification formula from which a concurrent program is extracted.