Model Learning for Adjusting the Level of Automation in HCPS

TL;DR

This paper introduces a model-based framework combining automata learning and game-theoretic synthesis to design and verify safe shared-control strategies in human-automation systems, especially for safety-critical applications.

Contribution

It presents a novel approach that integrates active automata learning with reactive synthesis to analyze and refine shared-control strategies in human-automation interactions.

Findings

Framework successfully derives human behavior models from simulations.

It verifies safety guarantees through reactive synthesis.

Case study demonstrates practical applicability in driving scenarios.

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.