Adaptability Checking in Multi-Level Complex Systems
Emanuela Merelli, Nicola Paoletti, Luca Tesei

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…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsFormal Methods in Verification · Advanced Software Engineering Methodologies · Petri Nets in System Modeling
