Abstract | ||
---|---|---|
The linear time μ-calculus extends LTL with arbitrary least and greatest fixpoint operators. This gives it the power to express all ω-regular languages, i.e. strictly more than LTL. The validity problem is PSPACE-complete for both LTL and the linear time μ-calculus. In practice it is more difficult for the latter because of nestings of fixpoint operators and variables with several occurrences. We present a simple sound and complete infinitary proof system for the linear time μ-calculus and then present two decision procedures for provability in the system, hence validity of formulas. One uses nondeter- ministic Buchi automata, the other one a generalisation of size-change termination analysis (SCT) known from functional programming. The main novelties of this paper are the connection with SCT and the fact that both decision procedures have a better asymptotic complexity than earlier ones and have been implemented. |
Year | DOI | Venue |
---|---|---|
2006 | 10.1007/11944836_26 | FSTTCS |
DocType | Citations | PageRank |
Conference | 7 | 0.51 |
References | Authors | |
9 | 3 |
Name | Order | Citations | PageRank |
---|---|---|---|
Christian Dax | 1 | 42 | 3.86 |
Martin Hofmann | 2 | 188 | 12.61 |
Martin Lange | 3 | 44 | 4.03 |