| Abstract: | The model-checking games associated with fixed-point logicsare parity games, and it is currently not known whetherthe strategy problem for parity games can besolved in polynomial time.We study Solitaire-LFP, a fragment of least fixed-point logic, whose evaluation games are nestedsoltaire games. This means that on each strongly connected component of the game, only one player can make nontrivial moves.Winning sets of nested solitaire gamescan be computed efficiently.The model-checking problem for Solitaire-LFP isPspace-complete in general andPtime-complete for formulae of bounded width.On finite structures (but not on infinite ones), Solitaire-LFP isequivalent to transitive closure logic.We also consider the solitaire fragment of guarded fixed-point logics. Due to the restricted quantification pattern of these logics, the associated games are small and therefore admit more efficient model-checking algorithms. |
