UPPAAL Meets Cognitive Science and Learning: Synthesizing Shared Control for Human-Cyber-Physical Systems

Kurzfassung

Human–Cyber–Physical Systems (HCPS) require automation that can share control with human operators while preserving safety. A key challenge is enabling automation to recognise when and how to intervene or defer control to the human operator, which requires predictive models of human cognitive dynamics. Although cognitive architectures such as ACT-R provide detailed, executable models of human behaviour, their complexity makes them difficult to integrate with formal reactive synthesis techniques. The presented approach bridges this gap by combining automata learning of cognitive models with game-theoretic controller synthesis in UPPAAL-Tiga. ACT-R simulations of human perceptual, cognitive, and motor processes are abstracted into finite-state Mealy automata via active automata learning, yielding a learned Human Model that captures admissible human behaviour. This model is embedded into a timed game automaton in which different automation levels correspond to distinct sets of controllable actions. Reactive synthesis is then used to determine, for each design variant, whether safety and performance objectives can be guaranteed while accommodating human behaviour. The resulting controllers are correct-by-construction, ensuring safety, progress, and minimal unnecessary overrides. By integrating model learning, formal synthesis, and verification, the framework provides a systematic, tool-supported methodology for designing adaptive shared-control automation and supports reasoning about partial observability by tailoring the learned model’s observable alphabet.