Tableau-based approaches to model-checking
Girish S. Bhat, W. R. Cleaveland · 1998
This dissertation addresses the problem of checking automatically if a finite-state system satisfies a specification given as temporal logic formula. This technique, termed as model-checking, has emerged as one of the most powerful approaches to verify reactive systems automatically. We present a framework based on semantic-tableaux that serves as the basis for model-checking many different logics like $\mu$-calculus, CTL, LTL, CTL* and PDL-$\delta .$ We develop efficient on-the-fly model-checking algorithms for different logics using this framework. In contrast to existing approaches to model-checking, this framework can be used to verify both state-based and event-based systems and in conjunction with several state-space saving techniques like symbolic model-checking and partial model-checking. We also present two case-studies involving verification of the ATM UNI 3.1 signalling protocol and the SCSI 2.0 bus protocol to illustrate the utility of our approach.