Authors
Anuj Dawar, Erich Grädel, Stephan Kreutzer
Publication date
2004/4/1
Journal
ACM Transactions on Computational Logic (TOCL)
Volume
5
Issue
2
Pages
282-315
Publisher
ACM
Description
We consider an extension of modal logic with an operator for constructing inflationary fixed points, just as the modal μ-calculus extends basic modal logic with an operator for least fixed points. Least and inflationary fixed-point operators have been studied and compared in other contexts, particularly in finite model theory, where it is known that the logics IFP and LFP that result from adding such fixed-point operators to first-order logic have equal expressive power. As we show, the situation in modal logic is quite different, as the modal iteration calculus (MIC), we introduce has much greater expressive power than the μ-calculus. Greater expressive power comes at a cost: the calculus is algorithmically much less manageable.
Total citations
200120022003200420052006200720082009201020112012201320142015201620172018201920202021202220232336719137222222113
Scholar articles
A Dawar, E Grädel, S Kreutzer - ACM Transactions on Computational Logic (TOCL), 2004
A Dawar, E Grädel, S Kreutzer - International Workshop on Computer Science Logic, 2001