Conference paper
Model Checking as Static Analysis: Revisited
Department of Informatics and Mathematical Modeling, Technical University of Denmark1
Language-Based Technology, Department of Informatics and Mathematical Modeling, Technical University of Denmark2
Computer Science and Engineering, Department of Informatics and Mathematical Modeling, Technical University of Denmark3
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.
| Language: | English |
|---|---|
| Publisher: | Springer |
| Year: | 2012 |
| Pages: | 99-112 |
| Proceedings: | 9th International Conference on Integrated Formal Methods (iFM 2012) |
| Series: | Lecture Notes in Computer Science |
| Journal subtitle: | 9th International Conference, Ifm 2012 Pisa, Italy, June 18-21, 2012 Proceedings |
| ISBN: | 3642307280 , 3642307299 , 9783642307287 and 9783642307294 |
| ISSN: | 03029743 |
| Types: | Conference paper |
| DOI: | 10.1007/978-3-642-30729-4_8 |
| ORCIDs: | Nielson, Flemming and Nielson, Hanne Riis |
