Three notes on the complexity of model checking fixpoint logic with chop
Martin Lange · RAIRO - Theoretical Informatics and Applications · 2007
This paper provides lower complexity bounds of deterministic exponential time for the combined, data and expression complexity of Fixpoint Logic with Chop. This matches the previously known upper bound showing that its model checking problem is EXPTIME-complete, even when the transition system or the formula is fixed. All results already hold for the alternation-free fragment of Fixpoint Logic with Chop.