Model Learning for Adjusting the Level of Automation in HCPS

AI summary

Overview

Research area: Human-centred cyber-physical systems (HCPS), shared control, formal methods — specifically the combination of active automata learning with game-theoretic reactive synthesis.

Technical level: Advanced. The paper assumes familiarity with finite automata, active learning (Angluin's L* algorithm), timed game automata, temporal logics (LTL/TCTL), and cognitive architectures.

Scope: The paper proposes a design-time framework that learns a finite-state abstraction of human behaviour from a cognitive simulation and uses reactive synthesis to determine whether an automation design can guarantee safety while sharing control with that human, illustrated on a simplified driving scenario implemented in Uppaal.

What This Paper Is About

As automation takes on more control in safety-critical systems, designers need rigorous ways to reason about how humans and automated components interact — but human behaviour is variable, context-dependent, and only partially observable, which makes formal verification hard. The authors ask two coupled questions: what must the automation know about the human to interact appropriately, and what must the automation be able to do in order to interact appropriately. Their goal is a method that derives a finite-state model of the human from simulated behaviour, then synthesises an automation strategy that provably preserves safety against that model, and iterates when it cannot.

Key Contributions

1. A design-time framework that integrates model learning and reactive synthesis for analysing shared control in human-centred cyber-physical systems.

2. A method for deriving finite-state human abstractions through interaction with a cognitive simulation (using ACT-R), producing a Mealy machine that represents the automation's operational view of admissible human input–output behaviour.

3. A preliminary evaluation in a driving scenario demonstrating the feasibility of synthesising safety-preserving automation strategies, combining active automata learning in AALpy with reactive synthesis in Uppaal.

4. The framework additionally supports iterative refinement of the learned human model from violation-inducing traces and adaptation of the automation design variant (by expanding the controllable action set) when no winning strategy exists.

Main Findings

• Learned model size: For a configuration with four discretised time-headway levels, the learned human model (HM) comprised 13 states and 52 transitions, represented as a deterministic Mealy machine.

• Learner configuration: Active learning used AALpy with a deterministic L* learner combined with a RandomWalkEqOracle to approximate equivalence queries; the oracle's reset probability controlled how often simulations were restarted.

• Cognitive-cycle timing: A fixed cognitive-cycle delay of 50 ms was adopted, corresponding to the standard temporal resolution in cognitive modelling.

• Exact learning is infeasible: Cognitive models generally have greater expressive power than regular languages, so the learned automaton is an approximation of the cognitive model's behavioural language; adequacy for synthesis tasks is to be assessed empirically.

• Synthesis succeeded: The Uppaal model checker (v5.0.0) solved the game and produced a memoryless strategy mapping each reachable state to a controllable action, instantiating a three-mode policy.

• Three-mode policy details: In Nominal mode the driver's acceleration is accepted unmodified; in Advisory mode the controller issues a hint! message prompting the driver to re-evaluate the time headway; in Intervention mode the controller enforces acc_floor = -3 and acc_cap = -1.

• Safety thresholds used: The controller monitors time headway (thw) and time to collision (ttc), required to remain above thresholds of thw ≥ 1.5 s and ttc ≥ 2 s.

• Formal objective: The objectives were combined into a weak-until condition requiring that the follower never overtakes the leader until the destination is reached, written as A[¬(follow_pos ≥ lead_pos) W (follow_pos ≥ DEST)].

• Trace-level evidence: Simulation trace segments confirm the strategy satisfied the weak-until property, maintained safe distance, ensured progress to the destination, and minimised unnecessary overrides — for example, entries where the driver selected an acceleration of 2 while thw was 3 or 0 resulted in a clamped applied acceleration of –1 via brake override.

• Refinement loop not yet exercised: The iterative refinement mechanism that feeds violation-inducing traces back into learning to produce an updated model HM_{i+1} and strategy CS_{i+1} was not applied in the present study, and convergence of this loop is not formally guaranteed.

Methodology in Plain English

The authors treat the interaction between a human and automation as a two-player game. Rather than modelling the human by hand, they let a cognitive architecture (ACT-R, using the pyactr implementation) simulate a human performing a task — in this case a driver adjusting acceleration to maintain a safe headway behind a lead vehicle whose speed varies. Crucially, they use active automata learning: instead of passively observing logs, the learner actively queries the simulator, builds a hypothesis automaton, tests it against the simulator, and refines it whenever a counterexample is found. This matters because rare but safety-critical human actions may never appear in ordinary observational logs.

The result is a small finite-state machine — the abstract human model, abbreviated HM — that captures what the automation "expects" the human to do. The authors compose this model with automata describing the environment and the automation in a synchronous product, forming a timed game automaton in which actions are split into controllable actions (the automation's) and uncontrollable ones (the human's and the environment's). They express the goals in a fragment of TCTL — safety (never overtake the lead vehicle), reachability (eventually reach the destination), and minimal intervention (stay in Nominal or Advisory unless there is a hazard) — and let Uppaal compute whether a winning strategy exists. If it does, that strategy is a correct-by-construction controller; if it does not, the designer either refines the human model or expands what the automation is allowed to do, and tries again. Because the human model is coarse, synthesised strategies are then validated by co-simulation against the full cognitive model.

Why This Matters

Formal verification for automated systems is mature, but human-centred shared control has largely relied on static or normative human models, which limits applicability in dynamic or adaptive contexts. This work shows one route to grounding formal synthesis in behaviourally derived human abstractions, and it frames "level of automation" not as a fixed setting but as a design variant defined by the automation's controllable action set — something that can be evaluated systematically inside a single formal framework.

Real-world applications:

• Advanced driver-assistance systems, where the intervention decision (alert versus emergency braking) must be justified against uncertain driver behaviour.
• Flight-control systems, where authority is dynamically shared between pilots and automation.
• Robot-assisted surgery, where control is shared between surgeon and robot and errors are safety-critical.
• More generally, any human-centred cyber-physical system operating under a shared-control paradigm where the automation must know when to intervene and when to defer.

Industry relevance: The framework targets design-time analysis rather than runtime deployment, which fits the certification-oriented practices of safety-critical industries. The outputs specify the level of human state observability and automation capability required for implementation, giving engineering teams a principled answer to how much sensing and how much authority the automation actually needs.

Future Directions

• Formulating formal termination conditions for the iterative refinement loop and integrating the full loop into case study evaluations, since this mechanism was not yet applied in the present study.

• Empirical validation across multiple cognitive architectures — the framework is not restricted to ACT-R, and architectures such as MAMID emphasise different aspects of cognition; combining or comparing architectures could cross-validate learned abstractions and improve robustness.

• Parameter adaptation using empirical behavioural data as it becomes available, to improve generalisability of the learned model across operator profiles.

• Broader design-variant exploration and adoption of more query-efficient learning algorithms such as TTT and NL*, which can be substituted within the same framework without conceptual modification.

Target Audience

Researchers and practitioners working at the intersection of formal methods and human factors: verification and synthesis specialists interested in human-in-the-loop systems, HCI and human-factors researchers who use cognitive architectures, and safety engineers in automotive, aerospace, and medical robotics who need to justify shared-control designs. The paper is most valuable to readers already comfortable with automata learning and reactive synthesis, as it assumes that background rather than building it up.

Authors’ abstract

The steadily increasing level of automation in human-centred systems demands rigorous design methods for analysing and controlling interactions between humans and automated components, especially in safety-critical applications. The variability of human behaviour poses particular challenges for formal verification and synthesis. We present a model-based framework that enables design-time exploration of safe shared-control strategies in human-automation systems. The approach combines active automata learning -- to derive coarse, finite-state abstractions of human behaviour from simulations -- with game-theoretic reactive synthesis to determine whether a controller can guarantee safety when interacting with these models. If no such strategy exists, the framework supports iterative refinement of the human model or adjustment of the automation's controllable actions. A driving case study, integrating automata learning with reactive synthesis in UPPAAL, illustrates the applicability of the framework on a simplified driving scenario and its potential for analysing shared-control strategies in human-centred cyber-physical systems.