Adaptability Checking in Multi-Level Complex Systems

TL;DR

This paper presents a hierarchical model for multi-level adaptive systems, defining adaptability concepts and reducing adaptability checking to CTL model checking, demonstrated through autonomous vehicle motion control.

Contribution

It introduces a formal hierarchical framework with weak and strong adaptability notions, and reduces adaptability verification to a model checking problem.

Findings

Adaptability checking can be reduced to CTL model checking.

The framework effectively models motion control in autonomous vehicles.

Defines weak and strong adaptability for multi-level systems.

Abstract

A hierarchical model for multi-level adaptive systems is built on two basic levels: a lower behavioural level B accounting for the actual behaviour of the system and an upper structural level S describing the adaptation dynamics of the system. The behavioural level is modelled as a state machine and the structural level as a higher-order system whose states have associated logical formulas (constraints) over observables of the behavioural level. S is used to capture the global and stable features of B, by a defining set of allowed behaviours. The adaptation semantics is such that the upper S level imposes constraints on the lower B level, which has to adapt whenever it no longer can satisfy them. In this context, we introduce weak and strong adaptabil- ity, i.e. the ability of a system to adapt for some evolution paths or for all possible evolutions, respectively. We provide a relational characterisation for these two notions and we show that adaptability checking, i.e. deciding if a system is weak or strong adaptable, can be reduced to a CTL model checking problem. We apply the model and the theoretical results to the case study of motion control of autonomous transport vehicles.