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 language | English |
|---|---|
| Title of host publication | Proceedings of SOFSEM 2011 |
| Number of pages | 12 |
| Publication date | 2012 |
| Publication status | Published - 2012 |
| Event | 38th International Conference on Current Trends in Theory and Practice of Computer Science : Student Research Forum - Špindlerův Mlýn, Czech Republic Duration: 21 Jan 2012 → 27 Jan 2012 http://www.sofsem.cz/sofsem12/ |
Conference
| Conference | 38th International Conference on Current Trends in Theory and Practice of Computer Science : Student Research Forum |
|---|---|
| Country/Territory | Czech Republic |
| City | Špindlerův Mlýn |
| Period | 21/01/2012 → 27/01/2012 |
| Internet address |