Formal modeling study demonstrates temporal classification of psychological games via finite-trace logic, highlighting structural invariants for early intervention.
We formalise a source-verified corpus of seven transactional games - six classical Berne games from Games People Play plus one contemporary corpus scenario - as finite-trace LTL properties over Karpman-projected role traces. The paper introduces the antithesis window W = t_red - t_obs as the temporal invariant separating reactive (W>0), knife-edge (W=0), pre-committed (W<0), and unresolved (W=undefined) regimes, and instantiates each regime with a corpus witness. A catalogue of eight agent-property temporal formulae is classified in the Safety / Cosafety / Liveness / Coliveness intersection algebra of Bragetti-Italiano (Zenodo 10.5281/zenodo.21099448), together with the minimum verdict-alphabet cardinality required for prefix monitoring in each cell. An optional refinement-confirmation certification layer (Bragetti, Zenodo 10.5281/zenodo.22028019) is documented for the FG-persistence entries. Core results: prop:under (role-level under-determination), prop:karpman-noninj (Karpman non-injectivity), prop:sigma-insufficient (permutation classification refutation), prop:s3 (S_3 switch group), thm:t2 (architecture-side information loss). --- SCOPE AND STATUS. This is a preprint. It has not been peer reviewed and is not under journal acceptance.
No takes yet. Share an insight, caveat, or question.
Bragetti et al. (2026) studied this question.
Synapse has enriched 5 closely related papers on similar clinical questions. Consider them for comparative context: