Equivalence of finitary and infinitary semantics of concurrent programs

Question

The following claim is stated on p. 155 of Manna and Pnueli's The Temporal Logic of Reactive and Concurrent Systems: Specification.

Let $P_1$ and $P_2$ be two finitely branching transition systems whose justice and compassion sets are empty, i.e., $\mathcal{J} = \mathcal{C} = \emptyset$. Then $\mathcal{R}(P_1)=\mathcal{R}(P_2)$ iff $\mathcal{F}(P_1)=\mathcal{F}(P_2)$.

Here $\mathcal{R}(P)$ is the inifinitary semantics of $P$, and $\mathcal{F}(P)$ - its finitary semantics.

The claim is stated without proof. How can it be proved? Alternatively, where can I find a proof? (I suspect the claim is taken from some paper, but no citation is given in the textbook.)

Answer 1

For such $P_i$ we have that $\mathcal{R}(P_i)$ is the limit-closure of $\mathcal{F}(P_i)$. That the $P_i$ in general need to be finitely-branching for this claim is due to the fact that infinite branching can be used to encode liveness properties.