^{1} Department of Computer Science, Faculty of Science, Aarhus University, Aarhus University^{2} Department of Computer Science, ETH Zürich^{3} Institut für Informatik, LMU München

DOI:

10.1007/11944836_26

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 nondeterministic Büchi 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.

ISBN:

3540499946

Type:

Conference paper

Language:

English

Published in:

Fsttcs '06: Foundations of Software Technology and Theoretical Computer Science, 26th International Conference, 2006, p. 273-284

Main Research Area:

Science/technology

Publication Status:

Published

Series:

Lecture Notes in Computer Science

Review type:

Peer Review

Conference:

A Proof System for the Linear Time <em>μ</em>-Calculus, 2006