R. Axelsson & M. Lange (2007):
Model Checking the First-Order Fragment of Higher-Order Fixpoint Logic.
In: Proc. 14th Int. Conf. on Logic for Programming, Artificial Intelligence, and Reasoning, LPAR'07,
LNCS 4790.
Springer,
pp. 62–76,
doi:10.1007/978-3-540-75560-9_7.
J. R. Burch, E. M. Clarke, K. L. McMillan, D. L. Dill & L. J. Hwang (1992):
Symbolic Model Checking: 10^20 States and Beyond.
Information and Computation 98(2),
pp. 142–170,
doi:10.1016/0890-5401(92)90017-A.
E. Grädel, P. G. Kolaitis, L. Libkin, M. Marx, J. Spencer, M. Y. Vardi, Y. Venema & S. Weinstein (2007):
Finite Model Theory and its Applications.
Springer-Verlag,
doi:10.1007/3-540-68804-8.
D. Janin & I. Walukiewicz (1996):
On the Expressive Completeness of the Propositional μ-Calculus with Respect to Monadic Second Order Logic.
In: CONCUR,
pp. 263–277,
doi:10.1007/3-540-61604-7_60.
M. Jurdziński (1998):
Deciding the winner in parity games is in UPco-UP.
Inf. Process. Lett. 68(3),
pp. 119–124,
doi:10.1016/S0020-0190(98)00150-1.
D. Kozen (1983):
Results on the Propositional μ-calculus.
TCS 27,
pp. 333–354,
doi:10.1007/BFb0012782.
M. Otto (1999):
Bisimulation-invariant PTIME and higher-dimensional μ-calculus.
Theor. Comput. Sci. 224(1-2),
pp. 237–265,
doi:10.1016/S0304-3975(98)00314-4.
C. Stirling (1995):
Local Model Checking Games.
In: Proc. 6th Conf. on Concurrency Theory, CONCUR'95,
LNCS 962.
Springer,
pp. 1–11,
doi:10.1007/3-540-60218-6_1.
J. Vöge & M. Jurdziński (2000):
A Discrete Strategy Improvement Algorithm for Solving Parity Games.
In: CAV,
pp. 202–215,
doi:10.1007/10722167_18.
Igor Walukiewicz (1996):
Pushdown Processes: Games and Model Checking.
In: CAV,
pp. 62–74,
doi:10.1007/3-540-61474-5_58.
eptcs@eptcs.org