Fixpoints vs Moore Families

Publication: Research - peer-reviewArticle in proceedings – Annual report year: 2012

Standard

Fixpoints vs Moore Families. / Zhang, Fuyuan; Nielson, Flemming; Nielson, Hanne Riis.

Proceedings of SOFSEM 2011. 2012.

Publication: Research - peer-reviewArticle in proceedings – Annual report year: 2012

Harvard

Zhang, F, Nielson, F & Nielson, HR 2012, 'Fixpoints vs Moore Families'. in Proceedings of SOFSEM 2011.

APA

CBE

Zhang F, Nielson F, Nielson HR. 2012. Fixpoints vs Moore Families. In Proceedings of SOFSEM 2011.

MLA

Vancouver

Zhang F, Nielson F, Nielson HR. Fixpoints vs Moore Families. In Proceedings of SOFSEM 2011. 2012.

Author

Zhang, Fuyuan; Nielson, Flemming; Nielson, Hanne Riis / Fixpoints vs Moore Families.

Proceedings of SOFSEM 2011. 2012.

Publication: Research - peer-reviewArticle in proceedings – Annual report year: 2012

Bibtex

@inbook{2b32148c735a44c3827176922e61196d,
title = "Fixpoints vs Moore Families",
author = "Fuyuan Zhang and Flemming Nielson and Nielson, {Hanne Riis}",
year = "2012",
booktitle = "Proceedings of SOFSEM 2011",

}

RIS

TY - GEN

T1 - Fixpoints vs Moore Families

A1 - Zhang,Fuyuan

A1 - Nielson,Flemming

A1 - Nielson,Hanne Riis

AU - Zhang,Fuyuan

AU - Nielson,Flemming

AU - Nielson,Hanne Riis

PY - 2012

Y1 - 2012

N2 - 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.

AB - 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.

BT - Proceedings of SOFSEM 2011

T2 - Proceedings of SOFSEM 2011

ER -