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


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


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.