Answer: The exact unrounded model-checking problem is in \(\mathrm P\), with running time \(O(L)\) under the explicit input encoding.
Theorem 3.12 — class: algorithmic
PDF text-layer excerpt — equations and symbol order may be approximateGiven an agent template A and an ACTLK formula φ, the following hold: 1. ˆ SA(1) |= φ implies ∀n ≫α. SA(n) |= φ. 2. ˆ SA(1) ̸|= φ implies ∃n ≫α. SA(n) ̸|= φ.
statement extracted from the paper’s text layer; consult the paper for the exact wording
Given a finite template \(A=(O,h,\alpha,t)\) with \(O=\{A,B\}\), odd \(\alpha\), a binary-rational initial distribution \(\mu_0\) over the template's local states, and a universal temporal formula \(\phi\) without epistemic operators, decide whether every path from \(\mu_0\) satisfies \(\phi\). For a distribution \(\mu\), let \(a(\mu)\) be its active mass and \(a_o(\mu)\) the active mass holding opinion \(o\). When \(a(\mu)>0\), set \(q_o=a_o(\mu)/a(\mu)\) and \(p_o(\mu)=\sum_{j=(\alpha+1)/2}^{\alpha}\binom{\alpha}{j}q_o(\mu)^j(1-q_o(\mu))^{\alpha-j}\). A transition chooses masses \(x_{\ell,o}\geq0\) with \(\sum_o x_{\ell,o}=\mu_\ell\), forces latent mass to take the action for its current opinion, and requires \(\sum_{\ell\ \mathrm{active}}x_{\ell,o}=a(\mu)p_o(\mu)\). It produces \(\mu'_{\ell'}=\sum_{\ell,o:t(\ell,o)=\ell'}x_{\ell,o}\); if \(a(\mu)=0\), only latent transitions apply. The proposition \(p(o)\) holds exactly when all mass has opinion \(o\).
A template is \(\mathcal A=(O,h,\alpha,t)\), where \(O=\{A,B\}\), \(m=|O|=2\), \(h:O\to\mathbb Z_{\geq0}\), and \(\alpha\geq1\) is odd. Put \(H=\max_o h(o)\) and \(\mathcal L=O\times\{0,\ldots,H\}\times\{0,1\}\); a state \(\ell=(o,v,b)\) has opinion \(o\) and is latent exactly when \(b=1\). The total function \(t:\mathcal L\times O\to\mathcal L\) is given explicitly: active states satisfy \(\operatorname{op}(t(\ell,o))=o\), and latent states satisfy \(\operatorname{op}(t(\ell,\operatorname{op}(\ell)))=\operatorname{op}(\ell)\).
A society is given by its support: the list of the \(\tau\) types with positive mass, each with its mass as a binary rational. Types are local states; \(\tau\) is the support size, not the number of possible types. The initial masses sum to \(1\) and are supported on \(\{(o,h(o),0):o\in O\}\). Subsequent distributions may have arbitrary nonnegative real masses summing to \(1\).
For a distribution \(\mu\), define \(a_o(\mu)=\sum_{\ell:\,b(\ell)=0,\,\operatorname{op}(\ell)=o}\mu_\ell\) and \(a(\mu)=\sum_o a_o(\mu)\). When \(a(\mu)>0\), put \(q_o=a_o(\mu)/a(\mu)\) and \(p_o(\mu)=\sum_{j=(\alpha+1)/2}^{\alpha}\binom{\alpha}{j}q_o^j(1-q_o)^{\alpha-j}\).
A synchronous transition chooses real \(x_{\ell,o}\geq0\) satisfying \(\sum_o x_{\ell,o}=\mu_\ell\); for latent \(\ell\), require \(x_{\ell,\operatorname{op}(\ell)}=\mu_\ell\). If \(a(\mu)>0\), require \(\sum_{\ell:\,b(\ell)=0}x_{\ell,o}=a(\mu)p_o(\mu)\). Set \(\mu'_{\ell'}=\sum_{\ell,o:\,t(\ell,o)=\ell'}x_{\ell,o}\). If \(a(\mu)=0\), apply only the forced latent transitions.
The input formula \(\phi\) is in ACTL, with atomic propositions \(p(o)\) for \(o\in O\), interpreted by \(\mu\models p(o)\) exactly when \(\sum_{\ell:\,\operatorname{op}(\ell)=o}\mu_\ell=1\). Use standard branching-time semantics over all infinite transition paths, without fairness restrictions; the decision problem is whether \(\mu_0\models\phi\).
Is this continuous model-checking problem in \(\mathrm P\), or is it \(\mathrm{NP}\)-hard? State running times in \(m,\tau,L,|\mathcal L|,\alpha,|\phi|\), where \(L\) is the total binary input length and the integer parameters are binary encoded.
For finite-agent systems, the [finite-abstraction result](https://www.doc.ic.ac.uk/~alessio/papers/16/AAMAS16-KL.pdf) claims a decision procedure for universal temporal-epistemic verification under a small-neighbourhood assumption; it gives no polynomial-time bound. Its abstraction uses a finite weight grid and rounding. No result settling the exact unrounded mass problem above was identified in the search.
The exact, unrounded model-checking problem is decidable in \(\mathrm P\), with running time \(O(L)\) under the explicit input encoding.
The key invariant is that the set of opinions with positive mass never changes. Consequently, every reachable distribution has the same atomic labels, and ACTL model checking reduces to evaluating the formula on a single state with a self-loop. This covers arbitrary permitted transition tables, every finite odd \(\alpha\), and mixed initial societies.
Let \(r=(\alpha+1)/2\). When \(a(\mu)>0\), write \(q=q_A\), so \(q_B=1-q\). Reindexing the sum defining \(p_B\) gives
\[
p_A+p_B
=
\sum_{j=r}^{\alpha}\binom{\alpha}{j}q^j(1-q)^{\alpha-j}
+
\sum_{j=0}^{r-1}\binom{\alpha}{j}q^j(1-q)^{\alpha-j}
=1.
\]
Here the two ranges partition all indices because \(\alpha\) is odd.
Thus a feasible allocation exists: for active \(\ell\), choose \(x_{\ell,o}=\mu_\ell p_o\); for latent \(\ell\), choose \(x_{\ell,\operatorname{op}(\ell)}=\mu_\ell\) and set the other allocation to zero. The active row sums equal \(\mu_\ell\), and the active column sums equal \(a(\mu)p_o\).
When \(a(\mu)=0\), use the prescribed latent allocations. In both cases, the resulting successor is a distribution: all masses are nonnegative, and total mass remains \(1\) because \(t\) is total.
Therefore the transition relation is serial. Repeatedly using the allocation just constructed produces an infinite path from every distribution.
Define the total and latent masses of opinion \(o\) by
\[
c_o(\mu)=\sum_{\ell:\operatorname{op}(\ell)=o}\mu_\ell,
\qquad
z_o(\mu)=\sum_{\ell:\operatorname{op}(\ell)=o,\ b(\ell)=1}\mu_\ell.
\]
Then \(c_o(\mu)=a_o(\mu)+z_o(\mu)\).
For every permitted transition \(\mu\to\mu'\) with \(a(\mu)>0\), the transition restrictions imply
\[
c_o(\mu')=z_o(\mu)+a(\mu)p_o(\mu).
\]
Indeed, latent mass keeps its opinion under its forced action. Active mass allocated to action \(o\) acquires opinion \(o\), and its prescribed total is \(a(\mu)p_o(\mu)\). This identity holds for every feasible allocation, regardless of the successor latent statuses.
Also,
\[
p_o(\mu)>0\quad\Longleftrightarrow\quad a_o(\mu)>0.
\]
To verify this, if \(a_o(\mu)=0\), then \(q_o=0\), and every term defining \(p_o\) vanishes because its exponent \(j\) is positive. If \(a_o(\mu)>0\), then \(q_o>0\), and the term with \(j=\alpha\) gives \(p_o(\mu)\geq q_o^\alpha>0\).
Since all masses are nonnegative, it follows that
\[
c_o(\mu')>0
\quad\Longleftrightarrow\quad
z_o(\mu)>0\ \text{or}\ a_o(\mu)>0
\quad\Longleftrightarrow\quad
c_o(\mu)>0.
\]
If \(a(\mu)=0\), all mass is latent and preserves its opinion, so \(c_o(\mu')=c_o(\mu)\). Hence, in every case,
\[
\{o:c_o(\mu')>0\}=\{o:c_o(\mu)>0\}.
\]
By induction, this opinion support is constant along every finite transition sequence.
Because total mass is \(1\), the proposition \(p(o)\) holds exactly when opinion support is the singleton \(\{o\}\). Therefore every distribution reachable from \(\mu_0\) has precisely the same atomic labels as \(\mu_0\).
In particular, a mixed initial society never reaches exact unanimity at any finite time.
Let \(S_0=\{o:c_o(\mu_0)>0\}\). Define a Boolean evaluator \(E\) on the standard ACTL basis by
\[
E(p(o))=[S_0=\{o\}],\qquad E(\neg p(o))=\neg E(p(o)),
\]
\[
E(\psi\land\chi)=E(\psi)\land E(\chi),\qquad
E(\psi\lor\chi)=E(\psi)\lor E(\chi),
\]
\[
E(\mathrm{AX}\,\psi)=E(\psi),
\]
\[
E(\mathrm A[\psi\,\mathrm U\,\chi])=E(\chi),\qquad
E(\mathrm A[\psi\,\mathrm R\,\chi])=E(\chi).
\]
The brackets in the atomic clause denote the Boolean truth value of the enclosed condition.
Claim. For every subformula \(\theta\) and every reachable distribution \(\mu\), we have \(\mu\models\theta\) exactly when \(E(\theta)\) is true.
Proof. Proceed by structural induction.
The atomic cases follow from opinion-support invariance. The Boolean cases follow directly from the induction hypothesis.
For \(\mathrm{AX}\,\psi\), all successors are reachable and have the same truth value \(E(\psi)\). Since every distribution has a successor and every successor extends to an infinite path, universal next has exactly that truth value.
For \(\mathrm A[\psi\,\mathrm U\,\chi]\), if \(E(\chi)\) is true, then \(\chi\) already holds at the current position, satisfying until with witness index \(0\). If \(E(\chi)\) is false, it remains false at every position of every path, so no until witness exists. Infinite paths exist, so the universal formula is false.
For \(\mathrm A[\psi\,\mathrm R\,\chi]\), if \(E(\chi)\) is true, then \(\chi\) holds forever on every path, satisfying release. If \(E(\chi)\) is false, release fails at the current position: standard release requires its right operand there, including when its left operand already holds. Again, infinite paths exist.
This completes the induction. \(\square\)
Standard abbreviations such as \(\mathrm{AF}\) and \(\mathrm{AG}\) can be handled directly by the same evaluator.
The algorithm is:
Under the stated initialization restriction, \(\tau\leq m=2\): each opinion has only one permitted initial state. Because the support list contains only positive masses, no rational arithmetic is needed to determine \(S_0\).
After parsing, the semantic computation uses \(O(m+\tau+|\phi|)\) elementary Boolean and support operations. Including an input scan, the running time is
\[
O(L+m+\tau+|\phi|)=O(L),
\]
where \(L\) is the total binary input length.
Here \(|\mathcal L|=2m(H+1)=4(H+1)\), and the explicit transition table contains \(m|\mathcal L|\) entries. Its encoding contributes to \(L\), but the algorithm need not evaluate transitions or majority polynomials. There is no additional dependence on the numerical values of \(|\mathcal L|\) or \(\alpha\). In particular, binary encoding of \(\alpha\) causes no numerical iteration up to \(\alpha\).
Thus the problem is in \(\mathrm P\). NP-hardness under polynomial-time many-one reductions would consequently imply \(\mathrm P=\mathrm{NP}\).
The referenced paper’s Definition 3.3 uses a finite weight set and replaces the updated opinion mass by a nearest weight. That is a different transition rule from exact mass evolution. [Kouvaros–Lomuscio, Definition 3.3](https://www.doc.ic.ac.uk/~alessio/papers/16/AAMAS16-KL.pdf)
The proof here depends on preserving arbitrarily small positive masses. It therefore settles the specified unrounded problem directly, without invoking that abstraction. Standard temporal “eventually” requires truth at a finite path position; asymptotic approach to unanimity does not satisfy it.
⟨structured verdict parsed — rendered above⟩
The prover resolves the stated continuous model-checking problem correctly. The support invariant holds for every permitted transition, and the ACTL reduction and linear-time bound follow from it. I found no major or minor mathematical gaps.
The calculation establishing \(p_A+p_B=1\) is correct. With \(r=(\alpha+1)/2\), reindexing the expression for \(p_B\) yields indices from \(0\) through \(\alpha-r=r-1\). Thus the two sums partition the binomial expansion. The hypotheses \(m=2\) and odd \(\alpha\) are both essential and explicitly satisfied.
The proposed active allocation \(x_{\ell,o}=\mu_\ell p_o\) satisfies nonnegativity, every row-sum constraint, and every active column-sum constraint. The latent allocations satisfy their forced-action constraints.
When \(a(\mu)=0\), nonnegativity implies that every active state has zero mass, so the prescribed latent allocations cover all positive mass. Totality of \(t\) ensures that pushing either allocation forward preserves total mass.
The transition relation is therefore serial. The explicit successor construction can be iterated to obtain an infinite path; no computational construction of that path is needed by the decision algorithm.
Assessment: Correct, including the case \(a(\mu)=0\).
The identity
\[
c_o(\mu')=z_o(\mu)+a(\mu)p_o(\mu)
\]
correctly accounts for every contribution to successor opinion \(o\):
The successor’s latent status does not affect this identity.
For \(a(\mu)>0\), the claimed equivalence \(p_o(\mu)>0\) exactly when \(a_o(\mu)>0\) is correct. If \(q_o=0\), every summand vanishes because \(j\geq r\geq1\). If \(q_o>0\), the \(j=\alpha\) term is \(q_o^\alpha>0\). This also covers \(\alpha=1\) and \(q_o=1\).
Consequently, \(c_o(\mu')>0\) exactly when \(z_o(\mu)>0\) or \(a_o(\mu)>0\), which is equivalent to \(c_o(\mu)>0\). For \(a(\mu)=0\), all positive mass is latent and preserves its opinion.
Induction over finite transition sequences therefore establishes precisely the claimed invariant. Arbitrarily small positive masses cause no exception under exact real arithmetic.
Assessment: Correct for arbitrary permitted transition tables and all distributions in the specified domain.
Because masses are nonnegative and sum to \(1\), the equality \(c_o(\mu)=1\) holds exactly when the opinion support is \(\{o\}\). Thus opinion-support invariance implies constant atomic labels throughout the reachable system.
The statement that a mixed initial society never reaches exact unanimity at any finite time follows directly. The proof does not assume that positive mass stays bounded away from zero.
Assessment: Correct.
The structural induction has the necessary uniform scope: it concerns every reachable distribution for each subformula. Every successor and every finite position on a path from a reachable distribution is itself reachable.
The temporal clauses are correct under standard, non-strict semantics:
Infinite-path existence justifies the negative universal cases. The Boolean and atomic clauses are valid, and the stated treatment of \(\mathrm{AF}\) and \(\mathrm{AG}\) follows from their standard abbreviations.
Assessment: The singleton self-loop evaluation is exact for the requested ACTL language.
The initialization restriction permits only one initial state per opinion. Hence \(\tau\leq m=2\), as claimed. Since the support lists only positive masses, determining opinion support requires no rational arithmetic.
Bottom-up formula evaluation takes \(O(|\phi|)\) Boolean operations. Including support processing and an input scan gives
\[
O(L+m+\tau+|\phi|)=O(L)
\]
under the stated explicit encoding.
The calculation \(|\mathcal L|=2m(H+1)=4(H+1)\) and the transition-table entry count \(m|\mathcal L|\) are correct. Their encoding is included in \(L\). The algorithm performs no iteration up to the numerical value of \(\alpha\), and it need not compute majority probabilities or reachable distributions.
This bound concerns inputs satisfying the task’s stated restrictions; the algorithm is not claimed to validate malformed inputs.
Assessment: The polynomial-time classification and the more specific linear-time bound are justified.
The reference check supports the distinction made in the output. Definition 3.3 specifies a finite weight set and rounds the active opinion contribution to a nearest weight, subject to normalization, before adding the latent contribution. This differs from exact unrounded evolution. [Kouvaros–Lomuscio, Definition 3.3](https://www.doc.ic.ac.uk/~alessio/papers/16/AAMAS16-KL.pdf)
The prover does not invoke the paper’s verification theorem, so no hypotheses of that theorem require verification here.
No repair or additional clarification is required. The result applies to the exact unanimity propositions and transition restrictions specified in the task.
⟨structured verdict parsed — rendered above⟩
Tier: machine-proved, adversarially reviewed by an independent model. No human has checked this proof. Generated from pipeline artifacts by tools/atlas_build.py.