We show that the model checking problem of the μ-calculus can be viewed as an instance of static analysis. We propose Succinct Fixed Point Logic (SFP) within our logical approach to static analysis as an extension of Alternation-free Least Fixed Logic (ALFP). We generalize the notion of stratification to weak stratification and establish a Moore Family result for the new logic as well. The semantics of the μ-calculus is encoded as the intended model of weakly stratified clause sequences in SFP.
|Title of host publication||Integrated Formal Methods : 9th International Conference, IFM 2012 Pisa, Italy, June 18-21, 2012 Proceedings|
|Publication status||Published - 2012|
|Event||9th International Conference on Integrated Formal Methods (iFM 2012) - Pisa, Italy|
Duration: 18 Jun 2012 → 21 Jun 2012
|Conference||9th International Conference on Integrated Formal Methods (iFM 2012)|
|Period||18/06/2012 → 21/06/2012|
|Series||Lecture Notes in Computer Science|