1 Introduction↩︎

Many verification questions concern not only the behavior of a system, but also what can be inferred from a partial observation of its execution. This perspective is standard in discrete-event systems. Diagnosability asks whether an observer can detect an unobservable fault after a bounded delay [1]. Decentralized diagnosis considers several local observers with different projections of the same execution [2]. Opacity imposes the dual confidentiality requirement: the observations should not reveal that a secret event has occurred. Representative works include [3], [4]. See also the survey [5].

A related pattern appears in runtime verification [6], [7]. A monitor reads a finite observation prefix and produces a verdict only when it is justified by every execution compatible with the observations. This quantification over indistinguishable histories is captured by knowledge under perfect recall [8]. Temporal operators describe the execution, while a knowledge operator quantifies over executions with the same observation history.

This gives a common logical formulation of diagnosis and opacity. A diagnosis requirement states that the observer eventually knows that a fault occurred. An opacity requirement states that it never knows that a secret occurred. For a given system, both become model-checking questions for epistemic temporal formulas. Monitorability is related but not identical: it quantifies over possible continuations of every observation prefix and is therefore a property of the observation tree rather than the truth of one formula at the initial position [9]. We use runtime verification as additional motivation, but the formal applications developed below are diagnosis and opacity.

Past operators are essential for these applications. A diagnoser need not know that a fault holds at the current position. It must know that a fault occurred at some earlier position. Likewise, opacity commonly protects the occurrence of a past secret. Metric constraints (encoded in binary) express timing requirements, such as diagnosis within \(D \in \mathbb{N}\) steps or secrecy for a prescribed window. We work in discrete time, with distances counted in steps. This restriction is important: in dense time, opacity is already undecidable [10], by reduction from universality of timed automata [11]. Our logic therefore combines future and past temporal operators with strict first-time semantics, integer metric bounds, and synchronous perfect-recall knowledge. Under strict first-time semantics, a metric operator constrains the distance to the first position satisfying its argument, rather than to an arbitrary such position. We adopt it because the knowledge-free metric fragment is then only \(\mathsf{PSPACE}\) [12], whereas standard metric operators already make it \(\mathsf{EXPSPACE}\)-complete [13], so that the complexity we prove arises only from past and knowledge rather than from the metric.

Existing results do not determine the complexity of this combination. For epistemic LTL with future operators and no metric constraints, perfect-recall model checking is nonelementary in general and \(\mathsf{PSPACE}\)-complete at knowledge-alternation depth one [14]. The pure past fragment under synchronous perfect recall, without future or metric operators, has been studied in [15]. For the future-only metric logic with strict first-time semantics, satisfiability is \(\mathsf{PSPACE}\)-complete [12]. Metric temporal logic with knowledge over timed interpreted systems has been studied via bounded model checking, with a different, state-based epistemic semantics and no past operators [16], [17]. The logic KLTL, with future and past operators under synchronous perfect recall, forms the basis of a richer counterfactual logic [18] that is decidable over finite-state systems but whose exact complexity is left open. Temporal epistemic logic has been applied to fault diagnosis: the FDI framework of [19] specifies bounded-delay alarm requirements in temporal epistemic logic with past, using finite unfoldings rather than primitive binary metric operators, and without a complexity analysis for the logic considered here.

We prove that model checking is \(\mathsf{EXPSPACE}\)-complete at alternation depth one. The lower bound uses only the unbounded interval \(\mathbb{N}\). Thus \(\mathsf{EXPSPACE}\)-hardness already appears when past is added to the \(\mathsf{PSPACE}\)-complete metric-free future epistemic fragment, without positive metric constants. A related succinctness phenomenon is known without knowledge: the work [20] shows that adding a forgettable-past operator to LTL with past yields \(\mathsf{EXPSPACE}\)-complete satisfiability and model checking. Our lower bound adapts its tiling reduction.

The paper makes four contributions.

(1) We define the logic \(\mathrm{KMTL}\), with future and past operators, binary-encoded metric intervals, strict first-time semantics, and synchronous perfect-recall knowledge, together with its agent-alternation-free fragment \(\mathrm{KMTL}_1\).

(2) We express centralized diagnosis, decentralized diagnosis, and opacity in \(\mathrm{KMTL}_1\).

(3) We give an \(\mathsf{EXPSPACE}\) lower bound by reduction from exponential-width corridor tiling. The formula has one occurrence of a knowledge operator and only the interval \(\mathbb{N}\).

(4) We give a matching upper bound. The observer records sets of pairs of a system state and a temporal automaton state, distinguishing histories that end in the same system state but disagree on past formulas.

Outline

2 introduces the logic \(\mathrm{KMTL}\) and its fragment \(\mathrm{KMTL}_1\). 3 relates it to diagnosability and opacity. 4 proves the \(\mathsf{EXPSPACE}\) lower bound and 5 the matching upper bound. We conclude in 6.

Acknowledgments

This work was partly supported by the “France 2030” government investment plan managed by ANR, under the reference ANR-23-PEIA-0006.

2 The Logic \(\mathrm{KMTL}\) and its Fragment \(\mathrm{KMTL}_1\)↩︎

The syntax and semantics are parameterized by finite sets \(\mathsf{AP}\) of atomic propositions and \(\mathsf{Ag}\) of agents. Both are part of the model-checking instance (Definition 6). We write \(\Sigma=2^{\mathsf{AP}}\), viewing a letter \(\sigma\in\Sigma\) as the set of propositions true at one position. Positions are numbered from \(1\). Thus an infinite word is written \(w=\sigma_1\sigma_2\ldots\in\Sigma^\omega\). For \(i\in\mathbb{N}\), let \(w_{\le i}=\sigma_1\ldots\sigma_i\in\Sigma^*\), with \(w_{\le 0}\) the empty word. A pointed word is a pair \((w,i)\) with \(i\ge1\). Temporal operators move the distinguished position along \(w\), while knowledge compares \((w,i)\) with pointed words having the same observation history.

Formulas are interpreted over the language of a Büchi automaton:

A standard round-robin construction turns a generalized Büchi automaton into an ordinary one with at most \(m\cdot |S|\) states.

A model is a Büchi automaton over \(\Sigma=2^{\mathsf{AP}}\). We write it as \(\mathcal{M}=(Q,Q_0,\Delta,F_\mathcal{M})\) and reserve \(S,S_0,\delta,F\) for automata constructed in the proofs, which use the same definition over alphabets of the form \(2^{\mathsf{AP}'}\). Formulas are interpreted over \(L(\mathcal{M})\subseteq\Sigma^\omega\), and the finite transition structure of \(\mathcal{M}\) is the input representation used by the algorithms.

Metric constraints use nonempty intervals \(I\subseteq\mathbb{N}\) of the form \([\ell,h]=\{n\in\mathbb{N}\mid \ell\le n\le h\}\) or \([\ell,\infty)=\{n\in\mathbb{N}\mid \ell\le n\}\). Finite bounds are encoded in binary. Note that our lower-bound proof uses only the unbounded interval \(\mathbb{N}=[0,\infty)\).

Following [12], the superscript \(1\) denotes strict first-time semantics. The formula \(\varphi\,U^1_I\,\psi\) requires the first \(\psi\)-position at or after the current position to occur at a distance in \(I\), with \(\varphi\) holding before it. Dually, \(\varphi\,S^1_I\,\psi\) refers to the most recent \(\psi\)-position. In terms of classical metric until, \(\varphi\,U^1_I\,\psi\) is equivalent to \((\varphi\wedge\neg\psi)\,U_I\,\psi\). The formal semantics is as follows.

We also use the following abbreviations, for any interval \(I\): \[\begin{array}{rclcrclcrcl} \Diamond_I\varphi &:=& \top\,U^1_I\,\varphi, && \Diamond\varphi &:=& \Diamond_{\mathbb{N}}\varphi, && \Box\varphi &:=& \neg\Diamond\neg\varphi,\\[2mm] \Diamond^{-}_I\varphi &:=& \top\,S^1_I\,\varphi, && \Diamond^{-}\varphi &:=& \Diamond^{-}_{\mathbb{N}}\varphi, && \Box^{-}\varphi &:=& \neg\Diamond^{-}\neg\varphi. \end{array}\] Note that \(\Diamond_I\varphi\) says that the first position satisfying \(\varphi\) lies in the window \(I\). For \(I=\mathbb{N}\) this is the usual eventuality, and \(\Box\) and \(\Box^{-}\) are the usual universal modalities. For \(k\in\mathbb{N}\), \(X^k\varphi\) denotes \(k\) iterated applications of \(X\), with \(X^0\varphi=\varphi\).

We restrict alternation between knowledge operators of different agents.

Equivalently, no \(K_b\) with \(b\ne a\) may occur in the scope of \(K_a\). Same-agent nesting is allowed, and non-nested knowledge subformulas may refer to different agents. This is knowledge-alternation depth at most one in the sense of [14]. The subscript in \(\mathrm{KMTL}_1\) records this depth. By contrast, the subscript in the metric logic \(\mathrm{MTL}_1\) of [12] refers to first-time semantics, which we mark directly on the temporal operators.

3 Motivating Examples from Diagnosis and Opacity↩︎

Diagnosis and opacity are defined through partial observations. At a given position, an observer must consider every execution compatible with the observation prefix. Knowledge captures this quantification, while past operators describe the event to be inferred, such as an earlier fault or secret.

Classical definitions are usually phrased in terms of diagnosers and indistinguishable runs. Diagnosis has also been formalized in temporal epistemic logic, notably in the FDI framework of [19], and opacity has been expressed epistemically as \(\Box\neg K\,\mathit{sec}\) [21]. We show below that centralized diagnosis, decentralized diagnosis, and past-event opacity are all expressed by shallow epistemic temporal formulas with past. The examples account for past, metric bounds, and multiple agents while staying inside \(\mathrm{KMTL}_1\).

Bounded diagnosis

Let \(a \in \mathsf{Ag}\) be an observing agent and let \(f\in\mathsf{AP}\setminus\mathsf{AP}_a\) be an unobservable proposition marking a fault occurrence. For a trace \(w\) and a position \(i\), the formula \(\Diamond^- f\) says that a fault occurred in the prefix \(w_{\le i}\). Let \(D \in \mathbb{N}\) be a delay. In the classical sense of [1], a \(D\)-delay diagnoser for a given model \(\mathcal{M}\) is a function \[\mathsf{diag}:(2^{\mathsf{AP}_a})^+\to\{0,1\}\] from observation prefixes to alarms such that:

(i) if a finite prefix \(u\) of some \(w\in L(\mathcal{M})\) is fault-free, then \(\mathsf{diag}(\mathsf{obs}_a(u))=0\).

(ii) if \(w\in L(\mathcal{M})\) has a fault at position \(i\), then \(\mathsf{diag}(\mathsf{obs}_a(w_{\le j}))=1\) for all \(j\ge i+D\).

The first clause forbids false alarms. The second requires the alarm to stay on from \(D\) steps after every fault onward, matching the uniform-delay condition of [1].

The unbounded eventual-diagnosis formula \(\varphi_{\mathsf{diag}} := \Box\bigl(f\rightarrow \Diamond K_a\Diamond^- f\bigr)\) drops the delay bound and captures the qualitative requirement. The bound can also be written with iterated next as \(\Box(f\rightarrow X^D K_a\Diamond^- f)\). By monotonicity of \(K_a\Diamond^- f\), this is equivalent to \(\varphi_{\mathsf{diag}}^{\le D}\), but it expresses the delay \(D\) in unary, whereas the metric constant in \(\Diamond_{[0,D]}\) is binary.

Decentralized diagnosis

The translation extends to decentralized diagnosis. Suppose several agents observe different projections, \(f\notin\mathsf{AP}_a\) for every \(a\in\mathsf{Ag}\), and no fixed agent is required to diagnose every fault. Under the codiagnosability notion of [22], implemented by the disjunctive protocol of [2], a fault is detected once at least one agent can infer it from its local observations. A \(D\)-delay decentralized diagnoser is a family \((\mathsf{diag}_a)_{a\in\mathsf{Ag}}\) of local alarm functions \(\mathsf{diag}_a:(2^{\mathsf{AP}_a})^+\to\{0,1\}\), each subject to the no-false-alarm clause (i) above for its own observation alphabet, such that whenever \(w\in L(\mathcal{M})\) has a fault at position \(i\), then for every \(j\ge i+D\) at least one \(a\in\mathsf{Ag}\) has \(\mathsf{diag}_a(\mathsf{obs}_a(w_{\le j}))=1\).

This formula uses several knowledge operators, but they are not nested. Hence decentralized diagnosis remains in our fragment \(\mathrm{KMTL}_1\).

Opacity

Let \(\mathit{sec}\in\mathsf{AP}\setminus\mathsf{AP}_a\) be an unobservable secret event. The standard trace view of opacity says that every secret observation prefix must also be compatible with a non-secret prefix [3]. For past-event opacity this becomes:

for every \(w\in L(\mathcal{M})\) and position \(i\), if \(w,i\models\Diamond^-\mathit{sec}\), then there exists \(w'\in L(\mathcal{M})\) with \((w,i)\sim_a(w',i)\) and \(w',i\not\models\Diamond^-\mathit{sec}\).

The formula contains no metric operator. Recall that, over dense-time models with observable time stamps, however, the corresponding requirement is already undecidable by reduction from timed automaton universality [10], [11]. Discrete time is therefore an important restriction.

The formula \(\Box\neg K_a\Diamond^-\mathit{sec}\) prevents the observer from becoming certain that the secret occurred, but it does not prevent certainty that it did not occur. Two-sided opacity is expressed by \[\Box\neg\bigl(K_a\Diamond^-\mathit{sec}\vee K_a\neg\Diamond^-\mathit{sec}\bigr).\] For a confidential binary value encoded at the beginning of a run, this requires both values to remain compatible with the observations. Metric variants can restrict the protection requirement to a bounded window.

Alternation depth one

The formulas above contain no nesting between different agents’ knowledge. They therefore belong to \(\mathrm{KMTL}_1\). The lower bound shows that adding past to this shallow epistemic fragment already yields \(\mathsf{EXPSPACE}\)-hardness.

4 EXPSPACE Lower Bound↩︎

We reduce from exponential-width corridor tiling. An instance asks for a tiling of a grid of width \(2^m\) and arbitrary finite height, with matching horizontal and vertical colors and prescribed corner tiles. The model emits the grid in row-major order, from the bottom row upward. Each cell is represented by a block containing an \(m\)-bit column counter and a tile. After the last row, the trace enters a terminal \(\#^\omega\) loop. A single agent \(a\) observes all propositions except two auxiliary tags. See Figure 1 for an illustration.

The counter, corner constraints, and horizontal compatibility are checked on the visible trace by a polynomial-size formula. Vertical compatibility is the only condition involving cells separated by an entire row. Their distance is \(2^m\) cells, so expanding this distance with next operators would require an exponential-size formula, and a metric operator does not provide the direct comparison either (cf.Remark [rem:metric-free]).

We check vertical compatibility with one knowledge operator. Two propositions \(\mathsf{L}\) and \(\mathsf{U}\) are hidden from \(a\) and may each mark at most one cell start. A placement with \(\mathsf{L}\) on a cell and \(\mathsf{U}\) on the cell in the next row selects a vertical edge. At the first \(\#\)-position, all placements over the same visible prefix are indistinguishable to \(a\). Thus \(K_a\) quantifies over every candidate placement. A bad vertical edge yields an indistinguishable placement for which the test fails. Past operators compare the counter at the \(\mathsf{L}\)-cell with later cells: the first later occurrence of the same counter is the cell in the next row. Figure 1 shows the construction.

We state the reduction here and give the formulas and their semantic proofs in Appendix 7. The source problem is the standard exponential-width corridor-tiling problem (cf. [20]). An instance \[\mathcal{T}=(C,T,m,d_{\mathsf{init}},d_{\mathsf{final}})\] is given by a finite color set \(C\), a set \(T\subseteq C^4\) of tiles, each with a bottom, left, top, and right color, a width parameter \(m\ge 1\) in unary, and two corner dominoes \(d_{\mathsf{init}},d_{\mathsf{final}}\in T\). It asks for a height \(n\ge 1\) and a tiling of \(\{0,\ldots,2^m-1\}\times\{0,\ldots,n-1\}\) by dominoes from \(T\) so that adjacent tiles agree on the color of their shared edge, the bottom-left tile is \(d_{\mathsf{init}}\), and the top-right tile is \(d_{\mathsf{final}}\). Since \(m\) is in unary, the width \(2^m\) is exponential in the size of \(\mathcal{T}\), and the problem is \(\mathsf{EXPSPACE}\)-complete. The structure follows the tiling reduction of [20]. Their forgettable-past operator is used to compare cells in adjacent rows, whereas our reduction instead uses hidden tags quantified by knowledge.

For such an instance we build a polynomial-size tagged Büchi automaton \(\mathcal{M}_{\mathcal{T}}^{\mathsf{tag}}\) in which all states are accepting. Its visible propositions are the counter bits, the domino propositions, the terminal marker \(\#\), and a marker \(\mathsf{End}\) that flags the first \(\#\)-position. The only invisible propositions are \(\mathsf{L}\) and \(\mathsf{U}\). The system ensures that the visible trace is a sequence of complete cell blocks followed, when it stops, by \(\#^\omega\), that \(\mathsf{End}\) holds exactly at the first \(\#\), and that each hidden tag occurs at most once and only at a cell start. Apart from those regular restrictions, the tags can be assigned arbitrarily.

The reduction formula is \[\Phi_{\mathcal{T}}:= \Phi_{\mathsf{base}}\wedge\Diamond(\mathsf{End}\wedge\Phi_{\mathsf{col}}), \qquad \Phi_{\mathsf{col}}:= K_a(\mathsf{Pair}\rightarrow\mathsf{Good}).\] The visible marker \(\mathsf{End}\) occurs at the first \(\#\)-position, where \(\Phi_{\mathsf{col}}\) is evaluated. The formula \(\Phi_{\mathsf{base}}\) checks the two corners, the modulo-\(2^m\) column counter, and horizontal compatibility. The formula \(\mathsf{Pair}\) holds when \(\mathsf{L}\) marks a cell and \(\mathsf{U}\) marks the first later cell with the same counter. Under \(\Phi_{\mathsf{base}}\), these cells are vertical neighbors. The formula \(\mathsf{Good}\) checks their tile colors. All formulas have size polynomial in \(m+|T|\), and their definitions are given in Appendix 7.

The formula also satisfies the syntactic restriction stated in 2: all past operators occur inside the sole \(K_a\). The evaluation point is marked by \(\mathsf{End}\) rather than by a past modality.

5 EXPSPACE Upper Bound↩︎

The future-only strict first-time metric logic has a \(\mathsf{PSPACE}\) satisfiability procedure based on exponential-size temporal automata [12]. We extend this construction with forward-propagated counters for past operators. Since the target bound is exponential space, it is enough to obtain exponential-size pointed automata whose local predicates are testable in polynomial space.

Let \(\theta\) be knowledge-free. The automaton \(A_\theta\) stores one counter for each metric scheme, namely a metric subformula with its finite bound replaced by a placeholder (Definition 9). A scheme is future or past according to whether it comes from an until or a since operator, and upper-bound or lower-bound according to whether its interval bounds the distance to the witness from above or from below. Under strict first-time semantics, all concrete bounds for the same scheme are determined by one witness distance. Each counter uses \(O(\log B)\) bits, where \(B\) is the largest finite bound, and there are polynomially many schemes. Lower-bound and unbounded future obligations are handled by a generalized Büchi condition, which is then converted into an ordinary Büchi condition. Appendix 8 gives the construction.

After reading \(w_{\le i}\), the automaton state contains the temporal information relevant at position \(i\). A set \(C_\theta\) marks the states in which \(\theta\) holds. Since \(A_\theta\) is nondeterministic, truth at a pointed word is characterized by an accepting run whose state at the distinguished position belongs to \(C_\theta\).

Past operators

For a past scheme \(\gamma\) with arguments \(\varphi\) and \(\psi\), write \(c_i(\gamma)\) for its counter after reading position \(i\). It records the capped distance from position \(i\) back to the most recent \(\psi\)-position, provided that \(\varphi\wedge\neg\psi\) holds at every intervening position. At position \(1\), the counter is \(0\) if \(\psi\) holds and \(\bot\) otherwise. For \(i\ge 1\), \[c_{i+1}(\gamma)= \begin{cases} 0 & \text{if }\psi\text{ holds at position }i+1,\\ c_i(\gamma)\oplus_\gamma 1 & \text{if }\varphi\wedge\neg\psi\text{ holds at position }i+1,\\ \bot & \text{otherwise}, \end{cases}\] where \(z\oplus_\gamma 1\) is the increment of \(z\) capped so as never to exceed the largest finite bound \(B\), with \(\bot\oplus_\gamma 1=\bot\). For an upper-bound scheme it becomes \(\bot\) once the distance exceeds \(B\), in which case \(\bot\) represents either the absence of a witness or a witness beyond every relevant upper bound. For a lower-bound scheme it saturates at \(B\).

Unlike a future counter, a past counter is determined by the prefix already read. Its value is fixed at position \(1\) and propagated forward, so past schemes need no fairness condition. The Büchi condition is used only for future lower-bound schemes, where it rules out runs that keep an obligation active forever without reaching its witness.

Counting per scheme rather than per interval bound is the essential step in building the automaton. For future operators, this counting is due to [12]. We extend it to past operators, which the applications require and which their future-only construction does not cover. The extension keeps \(A_\theta\) exponential in size and its local tests in polynomial space, as stated in the following lemma.

The marked state alone does not ensure that the model and the test automaton have compatible accepting continuations. Fix a model \(\mathcal{M}=(Q,Q_0,\Delta,F_\mathcal{M})\) over \(2^{\mathsf{AP}}\) and a knowledge-free \(\theta\) over \(\mathsf{AP}\), so that Lemma 5 applies with \(\mathsf{AP}'=\mathsf{AP}\). Define \(\mathsf{Live}^\mathcal{M}_\theta\subseteq Q\times S_\theta\) by letting \((q,s)\in\mathsf{Live}^\mathcal{M}_\theta\) if \(s\in C_\theta\) and the product from \((q,s)\) has an infinite path that visits both acceptance components infinitely often. Its transitions are \((q,s)\to(q',s')\) whenever some \(\sigma\in2^{\mathsf{AP}}\) satisfies \((q,\sigma,q')\in\Delta\) and \((s,\sigma,s')\in\delta_\theta\). Membership is a generalized Büchi nonemptiness test in the exponential product. Each product state has polynomial size and the transition relation is polynomial-space testable, so the test runs in polynomial space.

Consequently, a run prefix \[q_0\xrightarrow{\sigma_1}q_1\cdots \xrightarrow{\sigma_i}q_i\] of \(\mathcal{M}\) extends to an accepted word satisfying \(\theta\) at position \(i\) iff \(A_\theta\) has a run on \(\sigma_1\ldots\sigma_i\) ending in some \(s\) with \((q_i,s)\in\mathsf{Live}^\mathcal{M}_\theta\). For formulas with past, the state \(s\) contains information about the prefix that cannot be recovered from \(q_i\).

Epistemic observers

First consider \(K_a\psi\) with knowledge-free \(\psi\), and put \(\chi=\neg\psi\). For a realized observation prefix \(u\in(2^{\mathsf{AP}_a})^+\), define \[O_{a,\psi}(u)\subseteq Q\times S_\chi\] as the set of pairs reachable by a run prefix of \(\mathcal{M}\) with observation \(u\) and a simultaneous run prefix of \(A_\chi\) on the same model letters (Definition 14 in the appendix). This is the perfect-recall information set over \(Q\times S_\chi\), rather than over \(Q\) alone. The temporal component distinguishes histories that reach the same model state but differ on past formulas. The set is updated incrementally by a subset construction (Lemma 14).

For \(w\in L(\mathcal{M})\), \(i\ge1\), and \(u=\mathsf{obs}_a(w_{\le i})\), the knowledge test is \[w,i\models_\mathcal{M}K_a\psi \quad\Longleftrightarrow\quad O_{a,\psi}(u)\cap\mathsf{Live}^\mathcal{M}_\chi=\emptyset\] (see Lemma 15 in the appendix). A pair in the intersection represents an indistinguishable prefix with an accepting continuation on which \(\neg\psi\) holds at position \(i\).

Same-agent blocks

Our fragment \(\mathrm{KMTL}_1\) excludes nesting between different agents, but permits repeated nesting for the same agent. For fixed \(a\), the truth of \(K_a\xi\) is invariant on an \(a\)-observation class: \[(w,i)\sim_a(w',i) \quad\Longrightarrow\quad \bigl(w,i\models_\mathcal{M}K_a\xi\iff w',i\models_\mathcal{M}K_a\xi\bigr).\] We therefore process an \(a\)-local block from the inside out. For a knowledge block \(\eta=K_a\psi\), let \(\widehat\psi\) be the formula obtained by replacing the immediate inner knowledge subformulas by fresh propositions. Their valuations depend only on the current observation prefix, and \(\widehat\psi\) is knowledge-free over the extended proposition set. The counterexample automaton for \(\eta\) is built for \(\chi_\eta:=\neg\widehat\psi\) and reads each model letter together with the values of these fresh propositions provided by the inner observers.

Relative liveness

The preceding observer handles the prefix up to the current position. If \(\widehat\psi\) contains an inner knowledge proposition below a future operator, its value is also needed along a possible counterexample continuation. That value depends on the continuation of the observation history, not only on the pair \((q,s)\).

For this reason, the liveness graph for \(\eta=K_a\psi\) uses configurations \((q,s,\mathcal{I})\), where \(\mathcal{I}\) contains the observers for every knowledge subformula strictly inside \(\psi\). All nesting levels are retained because an observer can be updated only after the observers inside its own body have provided their current truth values. A transition chooses a model letter \(\tau\), advances \(q\), and updates \(\mathcal{I}\) on \(\mathsf{obs}_a(\tau)\) from the innermost observer outward. The updated tuple \(\mathcal{I}'\) determines the valuation \(\kappa_{\mathcal{I}'}\) of the immediate inner propositions read by \(A_{\chi_\eta}\). We write \[\mathsf{Live}^\mathcal{M}_{a,\psi}(q,s,\mathcal{I})\] when the resulting graph has a continuation from \((q,s,\mathcal{I})\) that is accepting in both \(\mathcal{M}\) and \(A_{\chi_\eta}\). At every future position, the inner valuation is shared by exactly the runs with the same extended observation prefix. If \(\psi\) contains no knowledge subformula, \(\mathcal{I}\) is empty and the definition reduces to \(\mathsf{Live}^\mathcal{M}_{\chi_\eta}(q,s)\). Formal definitions and correctness are given in Appendix 8.

Global search

We refute \(\mathcal{M}\models\varphi\) by searching for a word satisfying \(\neg\varphi\). Replace every maximal knowledge subformula \(\eta\) of \(\neg\varphi\) by a fresh proposition \(p_\eta\), obtaining the knowledge-free formula \(\theta_{\mathsf{top}}\). A global configuration is \[(q,t,\mathcal{O}),\] where \(q\in Q\), \(t\in S_{\theta_{\mathsf{top}}}\), and \(\mathcal{O}\) contains the observer sets for all knowledge subformulas, including nonmaximal descendants, which are needed to evaluate the maximal blocks. The knowledge tests compute from \(\mathcal{O}\) a valuation \(\kappa_{\mathcal{O}}\) of the fresh propositions. For a block \(\eta=K_a\psi\), the proposition \(p_\eta\) is true exactly when its observer contains no pair \((q,s)\) satisfying \(\mathsf{Live}^\mathcal{M}_{a,\psi}(q,s,\mathcal{I})\), where \(\mathcal{I}\) is the tuple of strictly inner observers.

An initial configuration chooses a first model transition \((q_0,\sigma,q)\in\Delta\) with \(q_0\in Q_0\). The observers are initialized on \(\sigma\) from the innermost blocks outward, yielding \(\kappa_{\mathcal{O}}\). We then choose the first state \(t\) of the top automaton so that \[(t_0,\sigma\cup\kappa_{\mathcal{O}},t) \in\delta_{\theta_{\mathsf{top}}}\] for some \(t_0\in S_{0,\theta_{\mathsf{top}}}\), with \(t\in C_{\theta_{\mathsf{top}}}\). A successor chooses \((q,\sigma',q')\in\Delta\), updates all observers on \(\sigma'\) to \(\mathcal{O}'\), computes \(\kappa_{\mathcal{O}'}\), and takes a transition \[(t,\sigma'\cup\kappa_{\mathcal{O}'},t') \in\delta_{\theta_{\mathsf{top}}}.\] The global acceptance condition requires both the model component and the top automaton component to be accepting. Acceptance conditions of inner temporal automata are checked only inside the relative liveness predicates.

The next lemma relates the three components of a global run.

By item (iii), at every position the enriched word read by the top automaton carries the correct truth values of the knowledge subformulas that were replaced. An induction on the structure of \(\neg\varphi\) therefore shows that the enriched word satisfies \(\theta_{\mathsf{top}}\) at position \(1\) iff \(w,1\models_\mathcal{M}\neg\varphi\). Together with item (iv) and Lemma 5, this shows that the global product is nonempty exactly when some \(w\in L(\mathcal{M})\) satisfies \(w,1\models_\mathcal{M}\neg\varphi\).

Table 1 situates this result among related logics. For the knowledge-free metric fragment, satisfiability is \(\mathsf{PSPACE}\)-complete [12], and the model-checking result follows using the standard product construction.

6 Discussion and Conclusion↩︎

In diagnosis and opacity, information sets over system states are insufficient: they cannot distinguish observation-equivalent histories with different pasts. We therefore let observers range over pairs of system states and temporal automaton states.

The lower bound uses one agent, one knowledge occurrence, and only the unbounded interval \(\mathbb{N}\), so metric constants are not the source of hardness. Under standard, non-first-time metric operators the knowledge-free fragment is already \(\mathsf{EXPSPACE}\)-complete [13], and we conjecture the full problem to be \(2\)-\(\mathsf{EXPSPACE}\)-complete.

Monitorability suggests a separate, apparently harder problem: after every reachable observation prefix, is there a finite continuation forcing a definitive verdict? Over dense time it is undecidable for nondeterministic timed-automaton specifications [24], and its discrete-time complexity is open.

7 Lower-Bound Details↩︎

We give the formulas used in 4 and prove the properties claimed there. Fix a tiling instance \[\mathcal{T}=(C,T,m,d_{\mathsf{init}},d_{\mathsf{final}}),\] where \(T\subseteq C^4\) and \(m\ge 1\). For \(d\in T\), write \(d_{\mathsf{down}},d_{\mathsf{left}},d_{\mathsf{up}},d_{\mathsf{right}}\) for its four colors.

7.1 Visible Grid Encodings↩︎

Let \[\mathsf{Main}=\{b_i^+,b_i^-\mid 1\le i\le m\}\cup T\cup\{\#,\mathsf{End}\}\] be a set of propositions. The visible proposition \(\mathsf{End}\) marks the first \(\#\)-position. A cell is represented by a block of length \(m+1\): \[\{b_1^{\pm}\}\;\{b_2^{\pm}\}\;\ldots\;\{b_m^{\pm}\}\;\{d\}.\] At position \(i\) of the block, exactly one of \(b_i^+\) and \(b_i^-\) is visible, and the last position carries exactly one tile proposition \(d\in T\). The least significant bit is \(b_1\). Encoding one bit per position keeps the number of propositions, and hence the automaton constructed below, polynomial in \(m+|T|\).

The visible part of a finite grid is listed row by row, from left to right and from the bottom row upwards. It is followed by \(\#^\omega\). At a cell-start position, put \[\mathsf{Cell}:= b_1^+\vee b_1^-.\] For \(1\le r\le m\) and \(d\in T\), define \[\mathsf{Bit}_r^+ := X^{r-1}b_r^+, \qquad \mathsf{Bit}_r^- := X^{r-1}b_r^-, \qquad \mathsf{Tile}_d := X^m d.\] Evaluated at a cell start, \(\mathsf{Bit}_r^\pm\) and \(\mathsf{Tile}_d\) thus refer to the \(r\)-th counter bit and the tile of that cell. Finally, let \[\mathsf{Zero}:= \bigwedge_{r=1}^m \mathsf{Bit}_r^-, \qquad \mathsf{Max}:= \bigwedge_{r=1}^m \mathsf{Bit}_r^+.\]

7.2 The Tagged System↩︎

We now extend the set of propositions with the two hidden tags: \[\mathsf{AP}_{\mathcal{T}}=\mathsf{Main}\cup\{\mathsf{L},\mathsf{U}\}.\] There is one agent \(a\), with \[\mathsf{AP}_a=\mathsf{Main}.\] Hence \(a\) observes the complete grid encoding but not the tags.

To recognize this language, \(\mathcal{M}_{\mathcal{T}}^{\mathsf{tag}}\) needs only to record the position within a cell block, whether the terminal loop has started, and whether each tag has already occurred, so it has polynomially many states. Its transition relation is polynomial as well. Although the alphabet \(2^{\mathsf{AP}_{\mathcal{T}}}\) is exponential, the encoding of one bit per position enables at each state only the \(O(|T|)\) letters that carry a single counter bit or a single tile, together with one of the constantly many admissible tag placements. Every other letter has no outgoing transition and is rejected, so \(\delta\) is never enumerated over the full alphabet. Hence \(\mathcal{M}_{\mathcal{T}}^{\mathsf{tag}}\) has size polynomial in \(m+|T|\). Traces containing no \(\#\)-position are allowed, but cannot satisfy the eventual \(\mathsf{End}\)-requirement in \(\Phi_{\mathcal{T}}\).

7.3 The Base Formula↩︎

The base formula checks the visible constraints that do not compare adjacent rows. For \(1\le r\le m\), let \[\mathsf{Carry}_r := \bigwedge_{s<r}\mathsf{Bit}_s^+,\] where \(\mathsf{Carry}_1=\top\), and put \[\mathsf{NextCell}(\varphi):=X^{m+1}\varphi.\] Define \[\mathsf{Inc}:= \bigwedge_{r=1}^m \left( \bigl(\mathsf{Carry}_r\rightarrow (\mathsf{NextCell}(\mathsf{Bit}_r^+)\leftrightarrow \mathsf{Bit}_r^-)\bigr) \wedge \bigl(\neg\mathsf{Carry}_r\rightarrow (\mathsf{NextCell}(\mathsf{Bit}_r^+)\leftrightarrow \mathsf{Bit}_r^+)\bigr) \right).\] At a cell start, \(\mathsf{Inc}\) states that the counter in the next cell is the current counter plus one modulo \(2^m\).

Horizontal compatibility is expressed by \[\mathsf{Horiz}:= \Box\left( \mathsf{Cell}\wedge\neg\mathsf{Max} \rightarrow \bigwedge_{d\in T} \left( \mathsf{Tile}_d\rightarrow \bigvee_{\substack{d'\in T\\ d_{\mathsf{right}}=d'_{\mathsf{left}}}} \mathsf{NextCell}(\mathsf{Tile}_{d'}) \right) \right).\] Now let \[\Phi_{\mathsf{base}}:= (\mathsf{Cell}\wedge\mathsf{Zero}\wedge\mathsf{Tile}_{d_{\mathsf{init}}}) \wedge \Diamond(\mathsf{Cell}\wedge\mathsf{Max}\wedge\mathsf{Tile}_{d_{\mathsf{final}}} \wedge\mathsf{NextCell}(\mathsf{End}))\] \[\wedge\; \Box(\mathsf{Cell}\wedge\mathsf{NextCell}(\neg\#)\rightarrow\mathsf{Inc}) \wedge \mathsf{Horiz}.\]

7.4 The Hidden-Tag Column Check↩︎

The vertical test is evaluated at the first \(\#\)-position. At a cell start, the following formula compares the current counter with that of the \(\mathsf{L}\)-marked cell: \[\mathsf{SameL}:= \mathsf{Cell}\wedge \Diamond^{-}(\mathsf{L}\wedge\mathsf{Cell}) \wedge \bigwedge_{r=1}^m \left( \mathsf{Bit}_r^+ \leftrightarrow \Diamond^{-}(\mathsf{L}\wedge\mathsf{Cell}\wedge\mathsf{Bit}_r^+) \right).\] Define \[\mathsf{Pair}:= \Diamond^{-} \left( \mathsf{L}\wedge\mathsf{Cell} \wedge \mathsf{NextCell} \left( (\neg \#\wedge\neg\mathsf{SameL}) \,U^1_{\mathbb{N}}\, (\mathsf{U}\wedge\mathsf{Cell}\wedge\mathsf{SameL}) \right) \right).\] In the left-hand argument, \(\neg\mathsf{SameL}\) fails at any earlier cell that shares the counter of the \(\mathsf{L}\)-cell. Consequently, \(\mathsf{Pair}\) holds exactly when \(\mathsf{U}\) marks the first later cell whose counter agrees with that of the \(\mathsf{L}\)-cell.

Vertical color compatibility is expressed by \[\mathsf{Good}:= \Diamond^{-} \left( \mathsf{U}\wedge\mathsf{Cell} \wedge \bigvee_{\substack{d,d'\in T\\ d_{\mathsf{up}}=d'_{\mathsf{down}}}} \left( \mathsf{Tile}_{d'} \wedge \Diamond^{-}(\mathsf{L}\wedge\mathsf{Cell}\wedge\mathsf{Tile}_d) \right) \right).\] Finally, set \[\Phi_{\mathsf{col}}:= K_a(\mathsf{Pair}\rightarrow\mathsf{Good}), \qquad \Phi_{\mathcal{T}}:= \Phi_{\mathsf{base}}\wedge\Diamond(\mathsf{End}\wedge\Phi_{\mathsf{col}}).\]

8 Upper-Bound Details↩︎

We now give the temporal test automata, the observer update, and the global product used in the upper bound.

8.1 Knowledge-Free Temporal Automata↩︎

The construction below follows the future-operator temporal automata of [12], extended with forward-propagated counters for past operators.

Strict first-time semantics gives the equivalences \[\varphi\,U^1_{[\ell,h]}\,\psi \;\equiv\; \bigl(\varphi\,U^1_{[0,h]}\,\psi\bigr) \wedge \bigl(\varphi\,U^1_{[\ell,\infty)}\,\psi\bigr),\] and, symmetrically, \[\varphi\,S^1_{[\ell,h]}\,\psi \;\equiv\; \bigl(\varphi\,S^1_{[0,h]}\,\psi\bigr) \wedge \bigl(\varphi\,S^1_{[\ell,\infty)}\,\psi\bigr).\] Indeed, both conjuncts refer to the same first future, respectively most recent past, occurrence of \(\psi\). We represent the normalized formula as a directed acyclic graph and share the two arguments of each split. Normalization then adds only a constant number of nodes per metric subformula. In the notation below, \[\varphi\,U^1_{\le h}\,\psi \quad\text{and}\quad \varphi\,U^1_{\ge\ell}\,\psi\] stand for the two simple forms, and similarly for \(S^1\). Negations are not pushed to the atoms, and truth values will be defined compositionally on the closure.

All concrete instances of one scheme have the same witness distance. A single counter for the scheme therefore determines the truth of every bound occurring in \(\theta\).

The number of ordinary entries and schemes is polynomial in \(|\theta|\).

A type is represented by polynomially many bits for \(v\) and \(O(|\theta|)\) bits per counter. Hence \[|\mathsf H_\theta|\le 2^{\mathsf{poly}(|\theta|)}.\]

We next specify the intended counter values. Fix a word \(w\) and arguments \(\varphi,\psi\). The future witness distance at position \(i\) is the unique \(d\in\mathbb{N}\), if it exists, such that \[w,i+d\models\psi \quad\text{and}\quad w,k\models\varphi\wedge\neg\psi \text{ for all }i\le k<i+d.\] The past witness distance is defined by \[w,i-d\models\psi \quad\text{and}\quad w,k\models\varphi\wedge\neg\psi \text{ for all }i-d<k\le i.\] For an upper-bound scheme, its truthful counter is \(d\) when \(d\le B_\theta\), and \(\bot\) otherwise. For a lower-bound scheme it is \(\min(d,B_\theta)\). In either case it is \(\bot\) when no witness exists. These capped values preserve every comparison with a bound occurring in \(\theta\).

Here \(H\) describes the current position and \(H'\) the next one, and the label \(\sigma\) is the letter at the next position. Future counters are guessed backward from a witness, while past counters are computed forward from the initial position.

The set \(G_\gamma\) rules out runs on which a saturated lower-bound counter stays active forever while \(\psi\) never holds. Upper-bound future counters need no acceptance set: once active, they decrease along the run and reach \(0\) within \(B_\theta\) steps. Past counters are determined by the prefix already read and likewise need no acceptance set.

This proves Lemma 5 of the main text, which states the same result in the notation used there.

The live predicate

Fix the input model \(\mathcal{M}=(Q,Q_0,\Delta,F_\mathcal{M})\) over \(2^{\mathsf{AP}}\). For a knowledge-free \(\theta\) over \(\mathsf{AP}\), define \[\mathsf{Live}^\mathcal{M}_\theta\subseteq Q\times S_\theta\] as follows. The product has transitions \[(q,s)\longrightarrow(q',s')\] if some \(\sigma\in2^{\mathsf{AP}}\) satisfies \[(q,\sigma,q')\in\Delta \quad\text{and}\quad (s,\sigma,s')\in\delta_\theta.\] A pair \((q,s)\) belongs to \(\mathsf{Live}^\mathcal{M}_\theta\) if \(s\in C_\theta\) and the product has an infinite continuation from \((q,s)\) that visits \(F_\mathcal{M}\times S_\theta\) and \(Q\times F_\theta\) infinitely often. Membership is a generalized Büchi nonemptiness test in the exponential graph. Each state has polynomial size and the transition relation is polynomial-space testable, so it is decidable in polynomial space.

Let \[q_0\xrightarrow{\sigma_1}q_1\cdots \xrightarrow{\sigma_i}q_i\] be a run prefix of \(\mathcal{M}\). It extends to an accepting run whose word satisfies \(\theta\) at position \(i\) iff \(A_\theta\) has a run on \(\sigma_1\ldots\sigma_i\) ending in a state \(s\) with \((q_i,s)\in\mathsf{Live}^\mathcal{M}_\theta\). The forward implication follows from the completeness part of Lemma 12, and the reverse implication follows from soundness after joining the two prefixes to a live product continuation.

8.2 Observers and Knowledge Tests↩︎

We first set up the notation for abstracting inner knowledge. Consider an occurrence \[\eta=K_a\psi.\] Every knowledge operator nested in \(\psi\) is also indexed by \(a\), because the formula is agent-alternation-free. Let \(\mathsf{Imm}(\eta)\) be the knowledge-subformula occurrences in \(\psi\) that are not contained in another knowledge subformula of \(\psi\). Assign a fresh proposition \(p_\zeta\) to every \(\zeta\in\mathsf{Imm}(\eta)\), and let \(\widehat\psi\) be obtained by replacing each such \(\zeta\) with \(p_\zeta\). Then \(\widehat\psi\) is knowledge-free. Write \[P^{\mathsf{in}}_\eta=\{p_\zeta\mid\zeta\in\mathsf{Imm}(\eta)\}, \qquad \chi_\eta=\neg\widehat\psi,\] and let \[A_\eta=(S_\eta,S_{0,\eta},\delta_\eta,F_\eta), \qquad C_\eta\subseteq S_\eta,\] be the pointed tester for \(\chi_\eta\). Since \(\chi_\eta\) is knowledge-free over \(\mathsf{AP}\cup P^{\mathsf{in}}_\eta\), Lemma 5 applies with \(\mathsf{AP}'=\mathsf{AP}\cup P^{\mathsf{in}}_\eta\), so \(\delta_\eta\subseteq S_\eta\times2^{\mathsf{AP}\cup P^{\mathsf{in}}_\eta}\times S_\eta\) and each letter read by \(A_\eta\) has the form \(\tau\cup\kappa'\) with \(\tau\in2^{\mathsf{AP}}\) and \(\kappa'\subseteq P^{\mathsf{in}}_\eta\). All fresh propositions are chosen outside \(\mathsf{AP}\) and are distinct across knowledge-subformula occurrences. When the occurrence is clear, we also write \[P^{\mathsf{in}}_{a,\psi}=P^{\mathsf{in}}_\eta,\qquad O_{a,\psi}=O_\eta,\qquad \mathsf{Live}^\mathcal{M}_{a,\psi}=\mathsf{Live}^\mathcal{M}_\eta,\] in agreement with the notation of the main text.

Call \(u=o_1\ldots o_i\in(2^{\mathsf{AP}_a})^i\) realized if \[u=\mathsf{obs}_a(w_{\le i})\] for some \(w\in L(\mathcal{M})\). For an immediate inner block \(\zeta=K_a\psi_\zeta\), Lemma 13 makes its truth value a function of \(u\). Let \[\kappa_\eta(u)= \{p_\zeta\in P^{\mathsf{in}}_\eta\mid w,i\models_\mathcal{M}\zeta \text{ for some, equivalently every, }w \text{ with }\mathsf{obs}_a(w_{\le i})=u\}.\] These valuations are defined by induction on knowledge-nesting depth.

Thus \(O_\eta(u)\) contains the joint states reachable along all model prefixes with observation \(u\), while \(A_\eta\) reads the corresponding model letters extended by the truth values of the immediate inner blocks. The model prefixes in this set need not themselves be live, and liveness is tested separately.

For \(o\in2^{\mathsf{AP}_a}\) and \(\kappa'\subseteq P^{\mathsf{in}}_\eta\), put \[\begin{align} \mathsf{init}_\eta(o,\kappa') =\{(q,s)\mid {}& \exists q_0\in Q_0,\;\exists\tau\in2^{\mathsf{AP}},\; \exists s_0\in S_{0,\eta}:\\[-1mm] & (q_0,\tau,q)\in\Delta,\quad \mathsf{obs}_a(\tau)=o,\quad (s_0,\tau\cup\kappa',s)\in\delta_\eta\}, \\[1mm] \mathsf{post}_\eta(O,o,\kappa') =\{(q',s')\mid {}& \exists(q,s)\in O,\;\exists\tau\in2^{\mathsf{AP}}:\\[-1mm] & (q,\tau,q')\in\Delta,\quad \mathsf{obs}_a(\tau)=o,\quad (s,\tau\cup\kappa',s')\in\delta_\eta\}. \end{align}\]

Relative liveness

The observer \(O_\eta(u)\) records the prefix up to the current position. Along a future counterexample continuation, the tester \(A_\eta\) must also receive the values of the propositions in \(P^{\mathsf{in}}_\eta\). Those values depend on the continued observation history. We therefore retain the observers of all knowledge blocks properly nested in \(\eta\).

Let \(\mathsf{Desc}(\eta)\) be the set of all knowledge-subformula occurrences strictly inside \(\eta\). For a realized observation prefix \(u\), define the inner tuple \[\mathcal{I}_\eta(u)= \bigl(O_\zeta(u)\bigr)_{\zeta\in\mathsf{Desc}(\eta)}.\] Here every \(\zeta\) has agent \(a\), so all components are indexed by the same observation prefix. The definitions below proceed by induction on the knowledge depth of \(\eta\).

For an abstract inner tuple \(\mathcal{I}=(O_\zeta)_\zeta\), define the valuation of the immediate inner propositions by \[p_\zeta\in\kappa_\eta(\mathcal{I})\] iff no pair \((\tilde{q},\tilde{s})\in O_\zeta\) satisfies \[\mathsf{Live}^\mathcal{M}_\zeta (\tilde{q},\tilde{s},\mathcal{I}_\zeta),\] where \(\mathcal{I}_\zeta\) is the subtuple indexed by \(\mathsf{Desc}(\zeta)\). The predicate on the right concerns a block of strictly smaller knowledge depth.

For \(o\in2^{\mathsf{AP}_a}\), define \(\mathsf{post}(\mathcal{I},o)\) by updating its components from the deepest blocks outwards. When the component \(O_\zeta\) is updated, all components strictly inside \(\zeta\) have already been updated and determine the new valuation \(\kappa_\zeta\). The new component is then \[\mathsf{post}_\zeta(O_\zeta,o,\kappa_\zeta).\]

Define \[\mathsf{Live}^\mathcal{M}_\eta(q,s,\mathcal{I})\] on configurations \((q,s,\mathcal{I})\), where \(q\in Q\), \(s\in S_\eta\), and \(\mathcal{I}\) is an inner tuple for \(\eta\). There is a transition \[(q,s,\mathcal{I})\longrightarrow(q',s',\mathcal{I}')\] iff some \(\tau\in2^{\mathsf{AP}}\) satisfies \[(q,\tau,q')\in\Delta, \qquad \mathcal{I}'=\mathsf{post}(\mathcal{I},\mathsf{obs}_a(\tau)),\] and \[(s,\tau\cup\kappa_\eta(\mathcal{I}'),s')\in\delta_\eta.\] The predicate holds if \(s\in C_\eta\) and this graph has an infinite continuation visiting \(F_\mathcal{M}\) in the first component and \(F_\eta\) in the second component infinitely often.

If \(\eta\) has no inner knowledge block, the tuple is empty and the definition is the ordinary live predicate for \(\chi_\eta=\neg\psi\). Otherwise, successor generation invokes liveness predicates only for proper descendants. An inner tuple has an exponential-space representation, and the recursion depth is linear in the formula size, so membership in \(\mathsf{Live}^\mathcal{M}_\eta\) is decidable in exponential space.

8.3 Alternation Depth One and the Global Product↩︎

Let \(\mathsf{Know}(\varphi)\) be the set of knowledge-subformula occurrences of \(\varphi\). For each such occurrence, construct its observer and relative live predicate as above. Because \(\varphi\in\mathrm{KMTL}_1\), every descendant of a block \(K_a\psi\) has the same agent \(a\). Different agents may occur in separate, non-nested blocks.

Replace every maximal knowledge subformula of \(\neg\varphi\) by its fresh proposition, obtaining a knowledge-free formula \(\theta_{\mathsf{top}}\). The observers of all nested descendants are retained because they are needed to evaluate the maximal blocks.

A global configuration is \[(q,t,\mathcal{O}),\] where \(q\in Q\), \(t\in S_{\theta_{\mathsf{top}}}\), and \[\mathcal{O}=(O_\eta)_{\eta\in\mathsf{Know}(\varphi)}\] contains one observer set per knowledge block. The tuple determines a valuation \(\kappa_{\mathcal{O}}\) of all fresh propositions that occur in \(\theta_{\mathsf{top}}\): the proposition for \(\eta\) is true iff its observer contains no pair satisfying the relative live predicate from the corresponding descendant subtuple.

An initial configuration is obtained by choosing \[(q_0,\sigma,q)\in\Delta \quad\text{with}\quad q_0\in Q_0.\] Initialize all observer sets on \(\sigma\), from the deepest blocks outwards. Each block uses the observation \(\mathsf{obs}_a(\sigma)\) of its own agent. This yields \(\mathcal{O}\) and \(\kappa_{\mathcal{O}}\). Choose \(t_0\in S_{0,\theta_{\mathsf{top}}}\) and \(t\in C_{\theta_{\mathsf{top}}}\) such that \[(t_0,\sigma\cup\kappa_{\mathcal{O}},t) \in\delta_{\theta_{\mathsf{top}}}.\]

From \((q,t,\mathcal{O})\), choose a model transition \[(q,\sigma',q')\in\Delta.\] Update every observer on the observation of \(\sigma'\) for its agent, again from the deepest blocks outwards, to obtain \(\mathcal{O}'\). Compute \(\kappa_{\mathcal{O}'}\), and choose \(t'\) with \[(t,\sigma'\cup\kappa_{\mathcal{O}'},t') \in\delta_{\theta_{\mathsf{top}}}.\] The successor is \((q',t',\mathcal{O}')\). The acceptance condition requires the first component to visit \(F_\mathcal{M}\) infinitely often and the second to visit \(F_{\theta_{\mathsf{top}}}\) infinitely often. Acceptance conditions of the inner testers are checked within the relative live predicates and impose no additional condition on the global path.

References↩︎