Fixpoints vs Moore Families

    Research output: Chapter in Book/Report/Conference proceedingArticle in proceedingsResearchpeer-review

    71 Downloads (Pure)

    Abstract

    Model checking and static analysis are both successful approaches to the analysis of IT systems and it has been shown that many static analyses can be reduced to model checking. Recent results show that CTL model checking can be reduced to static analysis and that the set of satisfying states of a CTL formula can be described as the least element in a Moore family of acceptable sets of states for the static analysis. Turning the attention to the μ-calculus we are able to generalise this result to the alternation-free fragment whereas even for the fragment of alternation depth 2 we show that the fixed point characterisation cannot be recast as a Moore family property.
    Original languageEnglish
    Title of host publicationProceedings of SOFSEM 2011
    Number of pages12
    Publication date2012
    Publication statusPublished - 2012
    Event38th International Conference on Current Trends in Theory and Practice of Computer Science : Student Research Forum - Špindlerův Mlýn, Czech Republic
    Duration: 21 Jan 201227 Jan 2012
    http://www.sofsem.cz/sofsem12/

    Conference

    Conference38th International Conference on Current Trends in Theory and Practice of Computer Science : Student Research Forum
    CountryCzech Republic
    CityŠpindlerův Mlýn
    Period21/01/201227/01/2012
    Internet address

    Cite this

    Zhang, F., Nielson, F., & Nielson, H. R. (2012). Fixpoints vs Moore Families. In Proceedings of SOFSEM 2011