Technical Report · Preprint under review · April 2026
ARIA: Accountable Real-time Intelligence Arbiter
Algorithmic governance of social benefits with formal temporal-fairness guarantees: proof that a locally correct system can still produce systematic injustice over time.
Systems Engineering · AI GovernanceFormal system modeling3 research questions — all 3 answeredEU AI Act (Article 14)
Systems Engineer & AI Ethics Researcher · Formal Methods · Algorithmic Fairness · 2026
I designed a formal AI–human architecture that mathematically proves a system can make every single decision correctly and still produce systematic injustice over time.
ΚΥΡΙΑ ΕΥΡΗΜΑΤΑ
Αποδείχθηκε επίσημα (μαθηματική επαγωγή) και επαληθεύτηκε σε n=100.000 εφαρμογές. Πλήρης αρχιτεκτονική 4 υποσυστημάτων με 30/30 unit tests και 1:1 αντιστοίχιση με EU AI Act Art. 14.
Formal Methods · Petri NetsSysML · BPMN 2.0Python · Bootstrap CISTRIDE Security AnalysisSSM / CATWOEEU AI Act Compliance
Abstract
The problem and the approach in one paragraph
Abstract
Public administrations deploy algorithmic welfare systems with no way to prove they stay fair over time: a system can satisfy every individual fairness rule and still produce systematic injustice at the population level. ARIA introduces TFAS (Temporally Fair Arbitration System — the five-condition framework this paper defines) — five independently checkable conditions — and proves the Temporal Injustice Theorem: for δ ≥ 1, decisions diverge monotonically across groups, regardless of local correctness. Verified both analytically (induction) and empirically (n=100,000, B=200 bootstrap, |G|=4 groups).
Το Πρόβλημα: Δομική Αόρατη Αδικία
Why local correctness doesn't guarantee global fairness
Post-hoc audit failure
SyRI (Netherlands), Robodebt (Australia): bias surfaced years later — thousands of harmful decisions before any correction.
Static metrics fall short
Individual Fairness, Equal Opportunity, Counterfactual Fairness all define fairness as static — none model the human–retraining feedback loop.
ARIA's answer
TFAS introduces δ as a formal system parameter. The condition δ < 1 bridges individually fair decisions with systemic temporal fairness.
Το Κενό στη Βιβλιογραφία
No other definition combines all five dimensions at once
Algorithmic-fairness research covers many dimensions individually — no single definition combines all five, until TFAS.
ΚαλύπτεταιΜερικώςΔεν καλύπτεται
Ορισμός
Temporal Stabilitytemporal drift
Bounded Feedbackδ as parameter
Human Loophuman-in-the-loop
Auditability / Auditlegal record
Demographic PrivacyG separation
Individual Fairness[Dwork et al., 2012]
Equal Opportunity[Hardt et al., 2016]
Counterfactual Fairness[Kusner et al., 2017]
G/B-Fairness (Petri)[Fröschle, 2015]
Runtime Monitoring[Henzinger et al., 2023]
TFAS — ARIADimakopoulos, 2026
No other definition covers all five dimensions. The intersection of these five is ARIA's original contribution.
Ορισμός TFAS
Temporally Fair Arbitration System — 5 independently checkable conditions
System S satisfies TFAS if and only if all five conditions are satisfied simultaneously.
(i) LF — Local Fairness
Local Fairness
P(esc | eᵢ, f(eᵢ)) ⊥ group(eᵢ)
The escalation decision is independent of group membership — enforced architecturally by SS2.
Arch: SS2 · Gate #1
(ii) TS — Temporal Stability
Temporal Stability
r(gⱼ,t)/r(gₖ,t) ∈ [1−ε, 1+ε] ∀ t
Escalation rates across groups stay within a tolerance band ε ∈ (0, 0.15] — monitored by the SS1 using SPC (Statistical Process Control — control-chart-based statistical monitoring).
Arch: SS1, W · Gate #5
(iii) BF — Bounded Feedback
Bounded Feedback
|Δθ(g,t)| ≤ δ |Δθ(g,t−1)|, δ < 1
The central innovation: the first formal parameter modelling the human reviewer's contribution to retraining. Requires geometric convergence.
Arch: Thm. 5.1 · Gate #2
(iv) AUD — Auditability
Auditability
∀eᵢ: ∃ rec(eᵢ) ∈ SS4 ∧ notify(DPA) ≤ τ
Every decision is logged in a Merkle append-only log; the DPA (Data Protection Authority — the regulator responsible for enforcing data-protection law) is notified within τ=48h. Implements EU AI Act Art. 14.
Arch: SS4 · Gate #3
(v) LS — Level Separation
Level Separation — G ∈ SS1.inputs, G ∉ SS2.inputs
Demographic data G is stored exclusively in SS1 — never linked to individual decisions
Architectural privacy separation: G is used only for monitoring, never as a model feature. Statically verified on every deployment via Gate #1.
Arch: Gate #1 (static verification at every CI/CD run)
Temporal Injustice Theorem
Proof by mathematical induction — verified at n=100,000
The central theoretical result: local correctness is not equivalent to global temporal fairness. Even if every individual decision is unbiased, retraining feedback can still lead to irreversible divergence.
Theorem 5.1 — Temporal Injustice Theorem
$$\text{If } \delta \geq 1 \text{, then } \exists\, g_j, g_k \in G : |\Pi(g_j,t) - \Pi(g_k,t)| \to \infty \text{ as } t \to \infty$$
Independently of the local correctness of any individual transition. Base case: r(gⱼ,1) = r₀(1+δβ). Induction: r(gⱼ,t)/r(gₖ,t) = (1+δβ)ᵗ. For δ≥1 and β>0, the ratio grows geometrically without bound.
TFAS(iii) δ<1 is necessary to prevent monotonic divergence: thresholds converge, giving SS1 time to intervene before TFAS(ii) is irreversibly violated.
Empirical verification — ratio r(A)/r(B) per time step (t = 0 → 20)
The multi-group extension (|G|=4: migrants β=0.04, long-term unemployed β=0.02, people with disabilities β=0.05) confirms the theorem for |G|>2 — under δ=1.2, all three protected groups diverge simultaneously.
Αρχιτεκτονική Τεσσάρων Υποσυστημάτων
Each subsystem enforces exactly one group of TFAS conditions
SS1 — Bias Monitor
Output Distribution Monitoring
SysML BDD (Block Definition Diagram) · SPC Control Chart
Monitors per-group rates r(g,t) using a sliding window W=10,000 and CUSUM k=2.0 (a statistical test for detecting gradual drift). Under δ=0.5: 6 alarms across 120,000 decisions; under δ=1.2: persistent alarms.
Enforces: TFAS(ii) Temporal Stability
SS2 — Intervention Engine
Escalation Logic & Automaton
Finite Automaton · Stateflow
4 states: MONITOR → ESCALATE → SUSPEND / OVERRIDE. G never enters as input; SUSPEND halts retraining whenever SS1 raises a TFAS alarm.
Enforces: TFAS(i) Local Fairness · TFAS(v) Level Separation
Provides XAI (Explainable AI) context and counterfactual explanations without G — addresses automation bias (~4% empirical). The only subsystem defined in SysML/BPMN without an executable implementation.
Every decision is recorded with a Merkle hash chain (a tamper-evident log: any edit breaks the chain and is detectable); every threshold change is logged with timestamp+admin_id. External notary + DPA read-only access. Implements EU AI Act Art. 14(4)(d).
Enforces: TFAS(iv) Auditability
Ερευνητικά Ερωτήματα & Απαντήσεις
Three research questions — all three answered
RQ1 ✓ Answered
Can human feedback be embedded as a formally bounded parameter?
Yes. TFAS(iii) is the first fairness definition that treats the human reviewer's retraining signal as an explicit, bounded parameter — grounded by the Theorem, estimated via proxy verification in CI/CD, and legally documentable in SS4.
TFAS(iii) — the first formal human-feedback parameter in the fairness literature
RQ2 ✓ Proven
Under what conditions does a locally correct system produce globally unjust outcomes?
The Temporal Injustice Theorem proves δ≥1 is sufficient for monotonic divergence. Important: δ<1 is necessary but not sufficient — for δ=0.9 and β≥0.07, the violation rate exceeds 50%.
δ=1.2 → 2.4× faster divergence · p<10⁻⁴⁰ · R²>0.999 · Final ratio T=20: 1.38 vs 1.19
RQ3 ✓ Verified
How can a 4-subsystem architecture implement, check and prove TFAS compliance?
1:1 TFAS ↔ SS ↔ CI/CD gate mapping. Executable Python implementations of SS1, SS2, SS4 verify that each subsystem enforces its TFAS condition in practice.
30/30 unit tests · 1:1 TFAS↔CI/CD · SS1+SS2+SS4 executable · SS3 in SysML/BPMN
CI/CD Deployment Gate
5 automated checks — 1:1 mapping to TFAS conditions
The deployment gate translates EU AI Act compliance into a verifiable engineering artefact — unlike Model Cards, Gate #5 blocks deployment without current verification.
#1
Model Feature Inspection — static check that dem_grp ∉ the model's features
TFAS(v) Level Separation · every commit
#2
Feedback Coefficient Config — fb_coef < 1.0, enforced in an externally configurable file
Demographic Smoke Test — |rA/rB −1| ≤ ε across n=1,000 synthetic applications
TFAS(ii) Temporal Stability · every deployment
Contributions
Five original contributions to the algorithmic-fairness literature
C1 · TFAS Definition
First formal definition with bounded feedback
TFAS is the first fairness definition that embeds the human reviewer's retraining contribution as an explicit parameter — rather than treating it as an exogenous disturbance.
C2 · Temporal Injustice Theorem
Proven both analytically and empirically
Mathematical induction + verification at n=100,000 (B=200 bootstrap). The first formal bridge between locally fair decisions and systemic temporal injustice.
C3 · ARIA Architecture
4 subsystems in SysML/BPMN 2.0
1:1 TFAS ↔ SS ↔ CI/CD gate mapping. Security analysis using STRIDE (a framework for identifying security threats; 13 threats identified). A verifiable engineering artefact for EU AI Act Art. 14 + GDPR (EU General Data Protection Regulation) Art. 22.
C4 · Sensitivity Analysis
15×10 grid (δ, β) space
Answers: for which combinations is runtime monitoring sufficient? Key finding: δ≤0.6 and the SUSPEND mechanism is the primary control — not just parameter choice.
C5 · Privacy-Preserving Fairness
Fairness verification without demographic exposure
Demographic data G is stored exclusively in SS1 — never linked to individual decisions. CI/CD Gate #1 architecturally verifies this separation on every deployment, resolving the privacy paradox [Veale & Binns, 2017].
Practical Implications
For public administrations, legal practitioners, and AI ethics researchers
P1
Public Administrations: append-only log → Art. 14(4)(d), CI/CD gate → Art. 9 risk management, DPA notification → Art. 14(3)(b). The first architecture to address all three at once.
P2
Citizens & Legal Practitioners: The audit log creates a legally defensible record — citizens can contest automated decisions (GDPR Art. 22), with every threshold change carrying a timestamp and admin ID.
P3
AI Ethics Researchers: The (δ,β) sensitivity analysis offers concrete guidance. The theorem generalises beyond benefits — criminal law, medical AI, hiring — anywhere human judgments feed into retraining.
P4
The "Fairness Washing" Risk: ARIA acknowledges its own risk — algorithmically satisfying the conditions while failing their spirit (e.g. gaming Gate #5). The CI/CD gate is a floor, not a ceiling.
Technical Appendix EN ONLY
Reproducibility · STRIDE security · Limitations — for technical reviewers
SSM (Soft Systems Methodology — a method for structuring complex, ill-defined problems into stages) / CATWOE (its analysis tool) — chosen because algorithmic governance is a "wicked problem" (no single correct framing); CATWOE forces an explicit worldview before technical design.
13 threats analysed under STRIDE (a standard attack-category checklist); 4 high-priority: Spoofing (mTLS+SS4), Tampering (Merkle log + notary), Information Disclosure (Gate #1), Elevation of privilege (rate limit+WORM).
Code Repository
github.com/SpiliosDimakopoulos/aria-tfas · 6 scripts · 30/30 unit tests (~5s) · MIT license · seed=42
Limitations & Future Work
L1
Petri Net scope: verified only for T=20 cycles, not an unlimited time horizon. Future work: symbolic model checking (SPIN/LTL).
L2
Synthetic β: calibrated from [Alon-Barkat & Busuioc, 2023], not measured on a live deployment — a field study with a consenting administration is needed.
L3
SS3 unverified: the only subsystem without an executable implementation. Future work: an HMI prototype with a usability study on real reviewers.
L4
Static G: TFAS assumes fixed groups — legislative change requires re-verification. Future work: dynamic G with versioned TFAS certificates.
ARIA δεν αυτοματοποιεί αποφάσεις.
Αυτοματοποιεί το ερώτημα ποιος πρέπει να τις λάβει — και αποδεικνύει επίσημα τι συμβαίνει όταν αυτό το ερώτημα απαντάται σωστά, αλλά το σύστημα λειτουργεί αρκετά καιρό.
Spilios Dimakopoulos · Systems Engineering · April 2026