# Equivalence of finitary and infinitary semantics of concurrent programs

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.)

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.