<p>For such <span class="math-container">$P_i$</span> we have that <span class="math-container">$\mathcal{R}(P_i)$</span> is the limit-closure of <span class="math-container">$\mathcal{F}(P_i)$</span>. That the <span class="math-container">$P_i$</span> 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.</p>

CC BY-SA 4.0
2023-02-27T05:29:20.137Z
2023-02-27T05:29:20.137Z
Kai
<p>The following claim is stated on p. 155 of Manna and Pnueli's <em>The Temporal Logic of Reactive and Concurrent Systems: Specification</em>.</p>
<blockquote>
<p>Let <span class="math-container">$P_1$</span> and <span class="math-container">$P_2$</span> be two finitely branching transition systems whose justice and compassion sets are empty, i.e., <span class="math-container">$\mathcal{J} = \mathcal{C} = \emptyset$</span>. Then <span class="math-container">$\mathcal{R}(P_1)=\mathcal{R}(P_2)$</span> iff <span class="math-container">$\mathcal{F}(P_1)=\mathcal{F}(P_2)$</span>.</p>
</blockquote>
<p>Here <span class="math-container">$\mathcal{R}(P)$</span> is the inifinitary semantics of <span class="math-container">$P$</span>, and <span class="math-container">$\mathcal{F}(P)$</span> - its finitary semantics.</p>
<p>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.)</p>

<semantics><concurrency><formal-methods>
Equivalence of finitary and infinitary semantics of concurrent programs
Evan Aad
# Equivalence of finitary and infinitary semantics of concurrent programs

(Asked by: username_0 on 2023-02-26)

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

**Tags:** semantics, concurrency, formal-methods


---

## 1 answers

### Answer by username_1 on 2023-02-27. Score: 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.


---

