Handbook of Automated Reasoning

This lemma is important for model checking of μ TL on finite Kripke models. Moreover, it allows to prove the following result.

5.5. Theorem

Finite models are monotonie μ TL-equivalent iff they are bisimilar: if ${\mathcal{M}}_1$ and ${\mathcal{M}}_2$ are finite, then ${ℳ}_1\underset{\_}{\leftrightarrow }{ℳ}_2$ iff ${ℳ}_1{\equiv }_{\mu TL}{ℳ}_2$

Proof

Trivially, ...