Name
Abstract | ||
|---|---|---|
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. |
Year | DOI | Venue |
|---|---|---|
2012 | 10.1007/978-3-642-30729-4_8 | IFM |
Keywords | Field | DocType |
succinct fixed point logic,weak stratification,new logic,intended model,moore family result,weakly stratified clause sequence,logical approach,fixed logic,model checking problem,static analysis | Computation tree logic,Kripke structure,Logical approach,Model checking,Programming language,Computer science,Static analysis,Theoretical computer science,Fixed point,Logic programming,Semantics | Conference |
Citations | PageRank | References |
1 | 0.36 | 18 |
Authors | ||
3 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Fuyuan Zhang | 1 | 8 | 1.88 |
| flemming nielson | 2 | 1769 | 172.05 |
| Hanne Riis Nielson | 3 | 1719 | 153.77 |