Publication: Research - peer-review › Article in proceedings – Annual report year: 2012
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|
|Conference||9th International Conference on Integrated Formal Methods (iFM 2012)|
|Period||18/06/12 → 21/06/12|
|Name||Lecture Notes in Computer Science|
|Citations||Web of Science® Times Cited: No match on DOI|
Loading map data...