Skip to content

torchmodal.systems

torchmodal.systems

torchmodal.systems ~~~~~~~~~~~~~~~~~~

Higher-level modal logic systems built on top of the core operators.

Provides ready-to-use modules for specific modal logics:

  • Epistemic Logic (K_a): Agent a knows ϕ iff ϕ is true in all worlds accessible to a.
  • Doxastic Logic (B_a): Agent a believes ϕ, where beliefs may differ from reality.
  • Temporal Logic (G, F): Globally ϕ (necessity over future states) and Finally ϕ (possibility of eventual truth).
  • Composite Operators (K∘G, K∘F): Nested modal operators for complex multi-agent temporal reasoning.

EpistemicOperator

Bases: Module

Epistemic knowledge operator K_a.

K_a(ϕ) asserts "agent a knows ϕ" — ϕ is true in all worlds accessible to agent a.

This is equivalent to □ restricted to agent a's accessibility row in the relation matrix.

Parameters:

Name Type Description Default
tau float

Temperature. Default 0.1.

 0.1
top_k Optional[int]

Top-k aggregation for the underlying □ (see :class:torchmodal.nn.Necessity). Default None.

 None

Example::

>>> K = EpistemicOperator()
>>> # agent_accessibility: (|W|,) row for agent a
>>> knowledge = K(prop_bounds, agent_accessibility)
Source code in torchmodal/systems.py 
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
class EpistemicOperator(nn.Module):
    r"""Epistemic knowledge operator K_a.

    ``K_a(ϕ)`` asserts "agent *a* knows ϕ" — ϕ is true in all worlds
    accessible to agent *a*.

    This is equivalent to □ restricted to agent *a*'s accessibility
    row in the relation matrix.

    Args:
        tau: Temperature. Default 0.1.
        top_k: Top-k aggregation for the underlying □ (see
            :class:`torchmodal.nn.Necessity`). Default ``None``.

    Example::

        >>> K = EpistemicOperator()
        >>> # agent_accessibility: (|W|,) row for agent a
        >>> knowledge = K(prop_bounds, agent_accessibility)
    """

    def __init__(self, tau: float = 0.1, top_k: Optional[int] = None) -> None:
        super().__init__()
        self.box = Necessity(tau=tau, top_k=top_k)

    def forward(
        self,
        prop_bounds: Tensor,
        agent_accessibility: Tensor,
    ) -> Tensor:
        """Evaluate K_a(ϕ) for a single agent.

        Args:
            prop_bounds: ``(|W|, 2)`` or ``(|W|,)`` truth bounds for ϕ.
            agent_accessibility: ``(|W|,)`` accessibility weights from
                agent *a* to all worlds.

        Returns:
            Scalar or ``(2,)`` bounds for K_a(ϕ).
        """
        # Reshape agent accessibility to (1, |W|) for single-source eval
        A_row = agent_accessibility.unsqueeze(0)  # (1, |W|)
        result = self.box(prop_bounds, A_row)       # (1, 2) or (1,)
        return cast(Tensor, result.squeeze(0))
forward 
forward(prop_bounds: Tensor, agent_accessibility: Tensor) -> Tensor

Evaluate K_a(ϕ) for a single agent.

Parameters:

Name Type Description Default
prop_bounds Tensor

(|W|, 2) or (|W|,) truth bounds for ϕ.

 required
agent_accessibility Tensor

(|W|,) accessibility weights from agent a to all worlds.

 required

Returns:

Type Description
Tensor

Scalar or (2,) bounds for K_a(ϕ).
Source code in torchmodal/systems.py 
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
def forward(
    self,
    prop_bounds: Tensor,
    agent_accessibility: Tensor,
) -> Tensor:
    """Evaluate K_a(ϕ) for a single agent.

    Args:
        prop_bounds: ``(|W|, 2)`` or ``(|W|,)`` truth bounds for ϕ.
        agent_accessibility: ``(|W|,)`` accessibility weights from
            agent *a* to all worlds.

    Returns:
        Scalar or ``(2,)`` bounds for K_a(ϕ).
    """
    # Reshape agent accessibility to (1, |W|) for single-source eval
    A_row = agent_accessibility.unsqueeze(0)  # (1, |W|)
    result = self.box(prop_bounds, A_row)       # (1, 2) or (1,)
    return cast(Tensor, result.squeeze(0))

DoxasticOperator

Bases: Module

Doxastic belief operator B_a.

B_a(ϕ) asserts "agent a believes ϕ" — ϕ is true in all worlds compatible with a's beliefs, which may differ from reality.

Structurally identical to :class:EpistemicOperator, but semantically distinct: epistemic accessibility requires veridical knowledge (ϕ must actually hold), while doxastic accessibility permits false beliefs.

This distinction is captured by the accessibility relation: epistemic relations are typically reflexive (T axiom: K_a(ϕ) → ϕ), while doxastic relations may not be.

Parameters:

Name Type Description Default
tau float

Temperature. Default 0.1.

 0.1
top_k Optional[int]

Top-k aggregation for the underlying □ (see :class:torchmodal.nn.Necessity). Default None.

 None
Source code in torchmodal/systems.py 
 89
 90
 91
 92
 93
 94
 95
 96
 97
 98
 99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
class DoxasticOperator(nn.Module):
    r"""Doxastic belief operator B_a.

    ``B_a(ϕ)`` asserts "agent *a* believes ϕ" — ϕ is true in all
    worlds compatible with *a*'s beliefs, which may differ from reality.

    Structurally identical to :class:`EpistemicOperator`, but
    semantically distinct: epistemic accessibility requires *veridical*
    knowledge (ϕ must actually hold), while doxastic accessibility
    permits *false beliefs*.

    This distinction is captured by the accessibility relation:
    epistemic relations are typically reflexive (T axiom: K_a(ϕ) → ϕ),
    while doxastic relations may not be.

    Args:
        tau: Temperature. Default 0.1.
        top_k: Top-k aggregation for the underlying □ (see
            :class:`torchmodal.nn.Necessity`). Default ``None``.
    """

    def __init__(self, tau: float = 0.1, top_k: Optional[int] = None) -> None:
        super().__init__()
        self.box = Necessity(tau=tau, top_k=top_k)

    def forward(
        self,
        prop_bounds: Tensor,
        agent_accessibility: Tensor,
    ) -> Tensor:
        """Evaluate B_a(ϕ) for a single agent.

        Args:
            prop_bounds: ``(|W|, 2)`` or ``(|W|,)`` truth bounds.
            agent_accessibility: ``(|W|,)`` accessibility row for agent *a*.

        Returns:
            Bounds for B_a(ϕ).
        """
        A_row = agent_accessibility.unsqueeze(0)
        result = self.box(prop_bounds, A_row)
        return cast(Tensor, result.squeeze(0))
forward 
forward(prop_bounds: Tensor, agent_accessibility: Tensor) -> Tensor

Evaluate B_a(ϕ) for a single agent.

Parameters:

Name Type Description Default
prop_bounds Tensor

(|W|, 2) or (|W|,) truth bounds.

 required
agent_accessibility Tensor

(|W|,) accessibility row for agent a.

 required

Returns:

Type Description
Tensor

Bounds for B_a(ϕ).
Source code in torchmodal/systems.py 
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
def forward(
    self,
    prop_bounds: Tensor,
    agent_accessibility: Tensor,
) -> Tensor:
    """Evaluate B_a(ϕ) for a single agent.

    Args:
        prop_bounds: ``(|W|, 2)`` or ``(|W|,)`` truth bounds.
        agent_accessibility: ``(|W|,)`` accessibility row for agent *a*.

    Returns:
        Bounds for B_a(ϕ).
    """
    A_row = agent_accessibility.unsqueeze(0)
    result = self.box(prop_bounds, A_row)
    return cast(Tensor, result.squeeze(0))

TemporalOperator

Bases: Module

Temporal logic operators G (Globally), F (Finally), and U (Until).

  • G(ϕ) ≡ □ϕ over temporal accessibility: ϕ holds at all future time steps. Uses necessity over forward-reachable states.
  • F(ϕ) ≡ ♢ϕ over temporal accessibility: ϕ holds at some future time step. Uses possibility over forward-reachable states.
  • U(ϕ, ψ): ϕ holds continuously until ψ becomes true. Implemented via a backward dynamic-programming sweep using Łukasiewicz connectives for differentiability.

The Until operator closes the expressiveness gap with STLCG (Leung et al., IJRR 2023), which supports the full fragment of signal temporal logic including Until.

Parameters:

Name Type Description Default
num_steps int

Number of discrete time steps.

 required
tau float

Temperature. Default 0.1.

 0.1
top_k Optional[int]

Top-k aggregation for G / F (see :class:torchmodal.nn.Necessity). Until does not aggregate over the accessibility relation and is unaffected. Default None.

 None

Example::

>>> temporal = TemporalOperator(num_steps=5)
>>> A_temporal = temporal.build_forward_accessibility()
>>> globally_phi = temporal.globally(prop_bounds, A_temporal)
>>> finally_phi = temporal.finally_(prop_bounds, A_temporal)
>>> until_result = temporal.until(phi_bounds, psi_bounds, A_temporal)
Source code in torchmodal/systems.py 
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
class TemporalOperator(nn.Module):
    r"""Temporal logic operators G (Globally), F (Finally), and U (Until).

    - **G(ϕ)** ≡ □ϕ over temporal accessibility: ϕ holds at all future
      time steps. Uses necessity over forward-reachable states.
    - **F(ϕ)** ≡ ♢ϕ over temporal accessibility: ϕ holds at some
      future time step. Uses possibility over forward-reachable states.
    - **U(ϕ, ψ)**: ϕ holds continuously until ψ becomes true.
      Implemented via a backward dynamic-programming sweep using
      Łukasiewicz connectives for differentiability.

    The Until operator closes the expressiveness gap with STLCG
    (Leung et al., IJRR 2023), which supports the full fragment of
    signal temporal logic including Until.

    Args:
        num_steps: Number of discrete time steps.
        tau: Temperature. Default 0.1.
        top_k: Top-k aggregation for G / F (see
            :class:`torchmodal.nn.Necessity`). Until does not aggregate
            over the accessibility relation and is unaffected. Default
            ``None``.

    Example::

        >>> temporal = TemporalOperator(num_steps=5)
        >>> A_temporal = temporal.build_forward_accessibility()
        >>> globally_phi = temporal.globally(prop_bounds, A_temporal)
        >>> finally_phi = temporal.finally_(prop_bounds, A_temporal)
        >>> until_result = temporal.until(phi_bounds, psi_bounds, A_temporal)
    """

    def __init__(
        self, num_steps: int, tau: float = 0.1, top_k: Optional[int] = None
    ) -> None:
        super().__init__()
        self.num_steps = num_steps
        self.box = Necessity(tau=tau, top_k=top_k)
        self.diamond = Possibility(tau=tau, top_k=top_k)

    def build_forward_accessibility(
        self,
        device: torch.device = torch.device("cpu"),
    ) -> Tensor:
        """Build a forward-time accessibility matrix.

        Creates a lower-triangular-inverted matrix where each time step
        can access all current and future steps.

        Returns:
            ``(num_steps, num_steps)`` binary accessibility matrix.
        """
        # i can access j if j >= i (forward-time) → upper triangular
        return torch.triu(torch.ones(self.num_steps, self.num_steps, device=device))

    def globally(
        self, prop_bounds: Tensor, temporal_accessibility: Tensor
    ) -> Tensor:
        """G(ϕ) — globally, ϕ holds at all accessible future states.

        Args:
            prop_bounds: ``(num_steps, 2)`` or ``(num_steps,)``.
            temporal_accessibility: ``(num_steps, num_steps)``.

        Returns:
            Bounds for G(ϕ).
        """
        return cast(Tensor, self.box(prop_bounds, temporal_accessibility))

    def finally_(
        self, prop_bounds: Tensor, temporal_accessibility: Tensor
    ) -> Tensor:
        """F(ϕ) — finally, ϕ holds at some accessible future state.

        Args:
            prop_bounds: ``(num_steps, 2)`` or ``(num_steps,)``.
            temporal_accessibility: ``(num_steps, num_steps)``.

        Returns:
            Bounds for F(ϕ).
        """
        return cast(Tensor, self.diamond(prop_bounds, temporal_accessibility))

    def until(
        self,
        phi_bounds: Tensor,
        psi_bounds: Tensor,
        temporal_accessibility: Tensor,
    ) -> Tensor:
        r"""U(ϕ, ψ) — ϕ holds continuously until ψ becomes true.

        Computes the Until operator using a backward dynamic-programming
        sweep:  ``U_t = ψ_t ∨ (ϕ_t ∧ U_{t+1})``.

        This operator is essential for expressing liveness and
        safety-with-guarantee properties that cannot be captured by
        G (globally) and F (finally) alone.

        Args:
            phi_bounds: ``(num_steps, 2)`` or ``(num_steps,)`` — the
                "hold" condition.
            psi_bounds: ``(num_steps, 2)`` or ``(num_steps,)`` — the
                "goal" condition.
            temporal_accessibility: ``(num_steps, num_steps)``.

        Returns:
            Bounds for ϕ U ψ.
        """
        return F.until(phi_bounds, psi_bounds, temporal_accessibility)
build_forward_accessibility 
build_forward_accessibility(device: device = torch.device('cpu')) -> Tensor

Build a forward-time accessibility matrix.

Creates a lower-triangular-inverted matrix where each time step can access all current and future steps.

Returns:

Type Description
Tensor

(num_steps, num_steps) binary accessibility matrix.
Source code in torchmodal/systems.py 
173
174
175
176
177
178
179
180
181
182
183
184
185
186
def build_forward_accessibility(
    self,
    device: torch.device = torch.device("cpu"),
) -> Tensor:
    """Build a forward-time accessibility matrix.

    Creates a lower-triangular-inverted matrix where each time step
    can access all current and future steps.

    Returns:
        ``(num_steps, num_steps)`` binary accessibility matrix.
    """
    # i can access j if j >= i (forward-time) → upper triangular
    return torch.triu(torch.ones(self.num_steps, self.num_steps, device=device))
globally 
globally(prop_bounds: Tensor, temporal_accessibility: Tensor) -> Tensor

G(ϕ) — globally, ϕ holds at all accessible future states.

Parameters:

Name Type Description Default
prop_bounds Tensor

(num_steps, 2) or (num_steps,).

 required
temporal_accessibility Tensor

(num_steps, num_steps).

 required

Returns:

Type Description
Tensor

Bounds for G(ϕ).
Source code in torchmodal/systems.py 
188
189
190
191
192
193
194
195
196
197
198
199
200
def globally(
    self, prop_bounds: Tensor, temporal_accessibility: Tensor
) -> Tensor:
    """G(ϕ) — globally, ϕ holds at all accessible future states.

    Args:
        prop_bounds: ``(num_steps, 2)`` or ``(num_steps,)``.
        temporal_accessibility: ``(num_steps, num_steps)``.

    Returns:
        Bounds for G(ϕ).
    """
    return cast(Tensor, self.box(prop_bounds, temporal_accessibility))
finally_ 
finally_(prop_bounds: Tensor, temporal_accessibility: Tensor) -> Tensor

F(ϕ) — finally, ϕ holds at some accessible future state.

Parameters:

Name Type Description Default
prop_bounds Tensor

(num_steps, 2) or (num_steps,).

 required
temporal_accessibility Tensor

(num_steps, num_steps).

 required

Returns:

Type Description
Tensor

Bounds for F(ϕ).
Source code in torchmodal/systems.py 
202
203
204
205
206
207
208
209
210
211
212
213
214
def finally_(
    self, prop_bounds: Tensor, temporal_accessibility: Tensor
) -> Tensor:
    """F(ϕ) — finally, ϕ holds at some accessible future state.

    Args:
        prop_bounds: ``(num_steps, 2)`` or ``(num_steps,)``.
        temporal_accessibility: ``(num_steps, num_steps)``.

    Returns:
        Bounds for F(ϕ).
    """
    return cast(Tensor, self.diamond(prop_bounds, temporal_accessibility))
until 
until(phi_bounds: Tensor, psi_bounds: Tensor, temporal_accessibility: Tensor) -> Tensor

U(ϕ, ψ) — ϕ holds continuously until ψ becomes true.

Computes the Until operator using a backward dynamic-programming sweep: U_t = ψ_t ∨ (ϕ_t ∧ U_{t+1}).

This operator is essential for expressing liveness and safety-with-guarantee properties that cannot be captured by G (globally) and F (finally) alone.

Parameters:

Name Type Description Default
phi_bounds Tensor

(num_steps, 2) or (num_steps,) — the "hold" condition.

 required
psi_bounds Tensor

(num_steps, 2) or (num_steps,) — the "goal" condition.

 required
temporal_accessibility Tensor

(num_steps, num_steps).

 required

Returns:

Type Description
Tensor

Bounds for ϕ U ψ.
Source code in torchmodal/systems.py 
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
def until(
    self,
    phi_bounds: Tensor,
    psi_bounds: Tensor,
    temporal_accessibility: Tensor,
) -> Tensor:
    r"""U(ϕ, ψ) — ϕ holds continuously until ψ becomes true.

    Computes the Until operator using a backward dynamic-programming
    sweep:  ``U_t = ψ_t ∨ (ϕ_t ∧ U_{t+1})``.

    This operator is essential for expressing liveness and
    safety-with-guarantee properties that cannot be captured by
    G (globally) and F (finally) alone.

    Args:
        phi_bounds: ``(num_steps, 2)`` or ``(num_steps,)`` — the
            "hold" condition.
        psi_bounds: ``(num_steps, 2)`` or ``(num_steps,)`` — the
            "goal" condition.
        temporal_accessibility: ``(num_steps, num_steps)``.

    Returns:
        Bounds for ϕ U ψ.
    """
    return F.until(phi_bounds, psi_bounds, temporal_accessibility)

MultiAgentKripke

Bases: Module

Multi-agent Kripke structure with temporal and epistemic dimensions.

Creates a spacetime state space S = W × T where: - W is a set of agent worlds - T is a set of time steps

Supports composite modal operators like K∘G (epistemic-temporal knowledge) and K∘F (epistemic-temporal possibility).

This mirrors the architecture used in the Diplomacy and CaSiNo experiments from the paper.

Parameters:

Name Type Description Default
num_agents int

Number of agents |W|.

 required
num_steps int

Number of time steps |T|.

 1
tau float

Temperature. Default 0.1.

 0.1
learnable_epistemic bool

If True, the epistemic accessibility is learnable. Default True.

 True
init_bias float

Initial bias for learnable epistemic logits. Default -2.0 ("prior of distrust").

 -2.0
top_k Optional[int]

Top-k aggregation for every □ / ♢ in this structure (K, G, F and the composites), see :class:torchmodal.nn.Necessity. This replaces the deprecated top_k of the accessibility modules. Default None.

 None
Source code in torchmodal/systems.py 
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
class MultiAgentKripke(nn.Module):
    r"""Multi-agent Kripke structure with temporal and epistemic dimensions.

    Creates a spacetime state space S = W × T where:
    - W is a set of agent worlds
    - T is a set of time steps

    Supports composite modal operators like K∘G (epistemic-temporal
    knowledge) and K∘F (epistemic-temporal possibility).

    This mirrors the architecture used in the Diplomacy and CaSiNo
    experiments from the paper.

    Args:
        num_agents: Number of agents |W|.
        num_steps: Number of time steps |T|.
        tau: Temperature. Default 0.1.
        learnable_epistemic: If ``True``, the epistemic accessibility is
            learnable. Default ``True``.
        init_bias: Initial bias for learnable epistemic logits.
            Default -2.0 ("prior of distrust").
        top_k: Top-k aggregation for every □ / ♢ in this structure (K, G,
            F and the composites), see :class:`torchmodal.nn.Necessity`.
            This replaces the deprecated ``top_k`` of the accessibility
            modules. Default ``None``.
    """

    def __init__(
        self,
        num_agents: int,
        num_steps: int = 1,
        tau: float = 0.1,
        learnable_epistemic: bool = True,
        init_bias: float = -2.0,
        top_k: Optional[int] = None,
    ) -> None:
        super().__init__()
        self.num_agents = num_agents
        self.num_steps = num_steps
        self.tau = tau
        self.top_k = top_k
        self.num_states = num_agents * num_steps

        # Temporal accessibility (fixed: forward-time flow)
        self.temporal = TemporalOperator(num_steps, tau=tau, top_k=top_k)
        A_temporal = self._build_spacetime_temporal()
        self.register_buffer("A_temporal", A_temporal)

        # Epistemic accessibility: learnable, or a fixed identity. Annotated
        # as the union so mypy accepts both branches; both satisfy the same
        # call signature.
        self.epistemic_access: Union[
            LearnableAccessibility, FixedAccessibility
        ]
        if learnable_epistemic:
            self.epistemic_access = LearnableAccessibility(
                num_agents,
                init_bias=init_bias,
                reflexive=True,
            )
        else:
            # Identity: each agent only sees itself
            eye = torch.eye(num_agents)
            self.epistemic_access = FixedAccessibility(eye)

        # Modal operators
        self.box = Necessity(tau=tau, top_k=top_k)
        self.diamond = Possibility(tau=tau, top_k=top_k)

    def _build_spacetime_temporal(self) -> Tensor:
        """Build temporal accessibility over the full spacetime grid.

        State (a, t) can access state (a, t') for t' >= t.

        This is a block-diagonal matrix with one upper-triangular block
        per agent: ``kron(I_agents, triu(1_T))``.
        """
        # Each agent has an independent upper-triangular temporal flow
        triu_T = torch.triu(torch.ones(self.num_steps, self.num_steps))
        return torch.kron(torch.eye(self.num_agents), triu_T)

    def get_epistemic_accessibility(
        self, features: Optional[Tensor] = None
    ) -> Tensor:
        """Get the epistemic (agent-to-agent) accessibility matrix.

        Returns:
            ``(num_agents, num_agents)`` matrix in [0, 1].
        """
        if isinstance(self.epistemic_access, MetricAccessibility):
            return cast(Tensor, self.epistemic_access(features))
        return cast(Tensor, self.epistemic_access())

    def get_full_accessibility(
        self, features: Optional[Tensor] = None
    ) -> Tensor:
        """Get the combined spacetime accessibility matrix.

        Combines temporal accessibility (within-agent time flow)
        with epistemic accessibility (between-agent trust).

        The result is ``kron(A_epi, triu(1_T))``: agent trust scaled
        by forward-time flow.

        Returns:
            ``(num_states, num_states)`` matrix in [0, 1].
        """
        A_epi = self.get_epistemic_accessibility(features)
        # Forward-time upper-triangular mask
        triu_T = torch.triu(
            torch.ones(self.num_steps, self.num_steps, device=A_epi.device)
        )
        # Kronecker product: A_full[a*T+t, b*T+t2] = A_epi[a,b] * triu[t,t2]
        return torch.kron(A_epi, triu_T)

    def K(
        self,
        prop_bounds: Tensor,
        features: Optional[Tensor] = None,
    ) -> Tensor:
        """Epistemic knowledge operator over agents.

        Args:
            prop_bounds: ``(num_agents, 2)`` bounds per agent.
            features: Optional features for metric accessibility.

        Returns:
            ``(num_agents, 2)`` bounds for K(ϕ).
        """
        A_epi = self.get_epistemic_accessibility(features)
        return cast(Tensor, self.box(prop_bounds, A_epi))

    def G(self, prop_bounds: Tensor) -> Tensor:
        """Temporal globally operator.

        Args:
            prop_bounds: ``(num_states, 2)`` bounds over spacetime.

        Returns:
            ``(num_states, 2)`` bounds for G(ϕ).
        """
        return cast(Tensor, self.box(prop_bounds, self.A_temporal))

    def F(self, prop_bounds: Tensor) -> Tensor:
        """Temporal finally operator.

        Args:
            prop_bounds: ``(num_states, 2)`` bounds over spacetime.

        Returns:
            ``(num_states, 2)`` bounds for F(ϕ).
        """
        return cast(Tensor, self.diamond(prop_bounds, self.A_temporal))

    def K_G(
        self,
        prop_bounds: Tensor,
        features: Optional[Tensor] = None,
    ) -> Tensor:
        r"""Composite K∘G: agent knows ϕ holds globally.

        First applies G (temporal necessity), then K (epistemic).

        .. warning::
           **This is two □ levels, so it carries twice the slack.** Both G
           and K are :func:`~torchmodal.functional.necessity` neurons, so
           the returned interval is widened by
           :math:`\tau H_G(w) + \tau H_K(w)` — the sum of the two levels'
           box widths, each bounded by :math:`\tau \log n` — rather than
           by one. Measured with 3 agents, 4 steps, ``tau=0.1``,
           ``phi=[1,1]``: ``G`` alone gives ``L = 0.861`` while ``K_G``
           gives ``L = 0.770``, the two
           :func:`~torchmodal.functional.box_width_entropy` levels
           contributing 0.1387 each. Budget accordingly: the faithful
           nesting depth :math:`k^* = 1/(\tau\bar{H})` is consumed twice
           as fast by this composite as by a bare ``K``. See
           :func:`torchmodal.functional.necessity` for the per-level
           table.

        Args:
            prop_bounds: ``(num_states, 2)`` bounds.
            features: Optional features for metric accessibility.

        Returns:
            ``(num_states, 2)`` bounds for K(G(ϕ)).
        """
        g_bounds = self.G(prop_bounds)
        A_full = self.get_full_accessibility(features)
        return cast(Tensor, self.box(g_bounds, A_full))

    def K_F(
        self,
        prop_bounds: Tensor,
        features: Optional[Tensor] = None,
    ) -> Tensor:
        r"""Composite K∘F: agent knows ϕ holds eventually.

        First applies F (temporal possibility), then K (epistemic).

        .. warning::
           **This is two modal levels, so it carries twice the slack** —
           a ♢ (F) followed by a □ (K). Each widens the interval by its
           own :func:`~torchmodal.functional.box_width_entropy`,
           :math:`\tau H(w) \le \tau \log n`, and the two accumulate.
           See :meth:`K_G` for the measured figures and
           :func:`torchmodal.functional.necessity` for the per-level
           table.

        Args:
            prop_bounds: ``(num_states, 2)`` bounds.
            features: Optional features for metric accessibility.

        Returns:
            ``(num_states, 2)`` bounds for K(F(ϕ)).
        """
        f_bounds = self.F(prop_bounds)
        A_full = self.get_full_accessibility(features)
        return cast(Tensor, self.box(f_bounds, A_full))

    def forward(
        self,
        prop_bounds: Tensor,
        operator: str = "K",
        features: Optional[Tensor] = None,
    ) -> Tensor:
        """Apply a named modal operator.

        Args:
            prop_bounds: Truth bounds tensor.
            operator: One of ``"K"``, ``"G"``, ``"F"``, ``"K_G"``, ``"K_F"``.
            features: Optional features for metric accessibility.

        Returns:
            Transformed truth bounds.
        """
        ops = {
            "K": lambda b: self.K(b, features),
            "G": self.G,
            "F": self.F,
            "K_G": lambda b: self.K_G(b, features),
            "K_F": lambda b: self.K_F(b, features),
        }
        if operator not in ops:
            raise ValueError(
                f"Unknown operator '{operator}'. "
                f"Choose from: {list(ops.keys())}"
            )
        return ops[operator](prop_bounds)

    def extra_repr(self) -> str:
        return (
            f"num_agents={self.num_agents}, "
            f"num_steps={self.num_steps}, "
            f"num_states={self.num_states}, "
            f"tau={self.tau}, "
            f"top_k={self.top_k}"
        )
get_epistemic_accessibility 
get_epistemic_accessibility(features: Optional[Tensor] = None) -> Tensor

Get the epistemic (agent-to-agent) accessibility matrix.

Returns:

Type Description
Tensor

(num_agents, num_agents) matrix in [0, 1].
Source code in torchmodal/systems.py 
325
326
327
328
329
330
331
332
333
334
335
def get_epistemic_accessibility(
    self, features: Optional[Tensor] = None
) -> Tensor:
    """Get the epistemic (agent-to-agent) accessibility matrix.

    Returns:
        ``(num_agents, num_agents)`` matrix in [0, 1].
    """
    if isinstance(self.epistemic_access, MetricAccessibility):
        return cast(Tensor, self.epistemic_access(features))
    return cast(Tensor, self.epistemic_access())
get_full_accessibility 
get_full_accessibility(features: Optional[Tensor] = None) -> Tensor

Get the combined spacetime accessibility matrix.

Combines temporal accessibility (within-agent time flow) with epistemic accessibility (between-agent trust).

The result is kron(A_epi, triu(1_T)): agent trust scaled by forward-time flow.

Returns:

Type Description
Tensor

(num_states, num_states) matrix in [0, 1].
Source code in torchmodal/systems.py 
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
def get_full_accessibility(
    self, features: Optional[Tensor] = None
) -> Tensor:
    """Get the combined spacetime accessibility matrix.

    Combines temporal accessibility (within-agent time flow)
    with epistemic accessibility (between-agent trust).

    The result is ``kron(A_epi, triu(1_T))``: agent trust scaled
    by forward-time flow.

    Returns:
        ``(num_states, num_states)`` matrix in [0, 1].
    """
    A_epi = self.get_epistemic_accessibility(features)
    # Forward-time upper-triangular mask
    triu_T = torch.triu(
        torch.ones(self.num_steps, self.num_steps, device=A_epi.device)
    )
    # Kronecker product: A_full[a*T+t, b*T+t2] = A_epi[a,b] * triu[t,t2]
    return torch.kron(A_epi, triu_T)
K 
K(prop_bounds: Tensor, features: Optional[Tensor] = None) -> Tensor

Epistemic knowledge operator over agents.

Parameters:

Name Type Description Default
prop_bounds Tensor

(num_agents, 2) bounds per agent.

 required
features Optional[Tensor]

Optional features for metric accessibility.

 None

Returns:

Type Description
Tensor

(num_agents, 2) bounds for K(ϕ).
Source code in torchmodal/systems.py 
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
def K(
    self,
    prop_bounds: Tensor,
    features: Optional[Tensor] = None,
) -> Tensor:
    """Epistemic knowledge operator over agents.

    Args:
        prop_bounds: ``(num_agents, 2)`` bounds per agent.
        features: Optional features for metric accessibility.

    Returns:
        ``(num_agents, 2)`` bounds for K(ϕ).
    """
    A_epi = self.get_epistemic_accessibility(features)
    return cast(Tensor, self.box(prop_bounds, A_epi))
G 
G(prop_bounds: Tensor) -> Tensor

Temporal globally operator.

Parameters:

Name Type Description Default
prop_bounds Tensor

(num_states, 2) bounds over spacetime.

 required

Returns:

Type Description
Tensor

(num_states, 2) bounds for G(ϕ).
Source code in torchmodal/systems.py 
376
377
378
379
380
381
382
383
384
385
def G(self, prop_bounds: Tensor) -> Tensor:
    """Temporal globally operator.

    Args:
        prop_bounds: ``(num_states, 2)`` bounds over spacetime.

    Returns:
        ``(num_states, 2)`` bounds for G(ϕ).
    """
    return cast(Tensor, self.box(prop_bounds, self.A_temporal))
F 
F(prop_bounds: Tensor) -> Tensor

Temporal finally operator.

Parameters:

Name Type Description Default
prop_bounds Tensor

(num_states, 2) bounds over spacetime.

 required

Returns:

Type Description
Tensor

(num_states, 2) bounds for F(ϕ).
Source code in torchmodal/systems.py 
387
388
389
390
391
392
393
394
395
396
def F(self, prop_bounds: Tensor) -> Tensor:
    """Temporal finally operator.

    Args:
        prop_bounds: ``(num_states, 2)`` bounds over spacetime.

    Returns:
        ``(num_states, 2)`` bounds for F(ϕ).
    """
    return cast(Tensor, self.diamond(prop_bounds, self.A_temporal))
K_G 
K_G(prop_bounds: Tensor, features: Optional[Tensor] = None) -> Tensor

Composite K∘G: agent knows ϕ holds globally.

First applies G (temporal necessity), then K (epistemic).

.. warning:: This is two □ levels, so it carries twice the slack. Both G and K are :func:~torchmodal.functional.necessity neurons, so the returned interval is widened by :math:\tau H_G(w) + \tau H_K(w) — the sum of the two levels' box widths, each bounded by :math:\tau \log n — rather than by one. Measured with 3 agents, 4 steps, tau=0.1, phi=[1,1]: G alone gives L = 0.861 while K_G gives L = 0.770, the two :func:~torchmodal.functional.box_width_entropy levels contributing 0.1387 each. Budget accordingly: the faithful nesting depth :math:k^* = 1/(\tau\bar{H}) is consumed twice as fast by this composite as by a bare K. See :func:torchmodal.functional.necessity for the per-level table.

Parameters:

Name Type Description Default
prop_bounds Tensor

(num_states, 2) bounds.

 required
features Optional[Tensor]

Optional features for metric accessibility.

 None

Returns:

Type Description
Tensor

(num_states, 2) bounds for K(G(ϕ)).
Source code in torchmodal/systems.py 
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
def K_G(
    self,
    prop_bounds: Tensor,
    features: Optional[Tensor] = None,
) -> Tensor:
    r"""Composite K∘G: agent knows ϕ holds globally.

    First applies G (temporal necessity), then K (epistemic).

    .. warning::
       **This is two □ levels, so it carries twice the slack.** Both G
       and K are :func:`~torchmodal.functional.necessity` neurons, so
       the returned interval is widened by
       :math:`\tau H_G(w) + \tau H_K(w)` — the sum of the two levels'
       box widths, each bounded by :math:`\tau \log n` — rather than
       by one. Measured with 3 agents, 4 steps, ``tau=0.1``,
       ``phi=[1,1]``: ``G`` alone gives ``L = 0.861`` while ``K_G``
       gives ``L = 0.770``, the two
       :func:`~torchmodal.functional.box_width_entropy` levels
       contributing 0.1387 each. Budget accordingly: the faithful
       nesting depth :math:`k^* = 1/(\tau\bar{H})` is consumed twice
       as fast by this composite as by a bare ``K``. See
       :func:`torchmodal.functional.necessity` for the per-level
       table.

    Args:
        prop_bounds: ``(num_states, 2)`` bounds.
        features: Optional features for metric accessibility.

    Returns:
        ``(num_states, 2)`` bounds for K(G(ϕ)).
    """
    g_bounds = self.G(prop_bounds)
    A_full = self.get_full_accessibility(features)
    return cast(Tensor, self.box(g_bounds, A_full))
K_F 
K_F(prop_bounds: Tensor, features: Optional[Tensor] = None) -> Tensor

Composite K∘F: agent knows ϕ holds eventually.

First applies F (temporal possibility), then K (epistemic).

.. warning:: This is two modal levels, so it carries twice the slack — a ♢ (F) followed by a □ (K). Each widens the interval by its own :func:~torchmodal.functional.box_width_entropy, :math:\tau H(w) \le \tau \log n, and the two accumulate. See :meth:K_G for the measured figures and :func:torchmodal.functional.necessity for the per-level table.

Parameters:

Name Type Description Default
prop_bounds Tensor

(num_states, 2) bounds.

 required
features Optional[Tensor]

Optional features for metric accessibility.

 None

Returns:

Type Description
Tensor

(num_states, 2) bounds for K(F(ϕ)).
Source code in torchmodal/systems.py 
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
def K_F(
    self,
    prop_bounds: Tensor,
    features: Optional[Tensor] = None,
) -> Tensor:
    r"""Composite K∘F: agent knows ϕ holds eventually.

    First applies F (temporal possibility), then K (epistemic).

    .. warning::
       **This is two modal levels, so it carries twice the slack** —
       a ♢ (F) followed by a □ (K). Each widens the interval by its
       own :func:`~torchmodal.functional.box_width_entropy`,
       :math:`\tau H(w) \le \tau \log n`, and the two accumulate.
       See :meth:`K_G` for the measured figures and
       :func:`torchmodal.functional.necessity` for the per-level
       table.

    Args:
        prop_bounds: ``(num_states, 2)`` bounds.
        features: Optional features for metric accessibility.

    Returns:
        ``(num_states, 2)`` bounds for K(F(ϕ)).
    """
    f_bounds = self.F(prop_bounds)
    A_full = self.get_full_accessibility(features)
    return cast(Tensor, self.box(f_bounds, A_full))
forward 
forward(prop_bounds: Tensor, operator: str = 'K', features: Optional[Tensor] = None) -> Tensor

Apply a named modal operator.

Parameters:

Name Type Description Default
prop_bounds Tensor

Truth bounds tensor.

 required
operator str

One of "K", "G", "F", "K_G", "K_F".

 'K'
features Optional[Tensor]

Optional features for metric accessibility.

 None

Returns:

Type Description
Tensor

Transformed truth bounds.
Source code in torchmodal/systems.py 
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
def forward(
    self,
    prop_bounds: Tensor,
    operator: str = "K",
    features: Optional[Tensor] = None,
) -> Tensor:
    """Apply a named modal operator.

    Args:
        prop_bounds: Truth bounds tensor.
        operator: One of ``"K"``, ``"G"``, ``"F"``, ``"K_G"``, ``"K_F"``.
        features: Optional features for metric accessibility.

    Returns:
        Transformed truth bounds.
    """
    ops = {
        "K": lambda b: self.K(b, features),
        "G": self.G,
        "F": self.F,
        "K_G": lambda b: self.K_G(b, features),
        "K_F": lambda b: self.K_F(b, features),
    }
    if operator not in ops:
        raise ValueError(
            f"Unknown operator '{operator}'. "
            f"Choose from: {list(ops.keys())}"
        )
    return ops[operator](prop_bounds)