Verifying Temporal Properties
A very rich temporal logic, modal mu-calculus, has been described. Formulas of the logic can express liveness, safety, cyclic and other properties of processes. The next step is to provide techniques for verification, for showing when processes have, or fail to have, these features. In this chapter, we show that game theoretic ideas provide a general framework for verification.
KeywordsModel Check Temporal Property Transition Graph Winning Strategy Infinite Length
Unable to display preview. Download preview PDF.