Approximation de l'accessibilité garantie et sûre via la décomposition basée sur les dépendances d'états.

Résumé

L'accessibilité Hamilton Jacobi (HJ) est un outil de vérification formelle largement utilisé dans l'analyse de la sécurité robotique. Compte tenu d'un ensemble d'états non sûrs, un système dynamique est assuré de ne pas entrer dans la cible dans le pire des cas s'il évite le tube d'accessibilité en arrière (BRT). Cependant, le calcul des BRT souffre d'une complexité exponentielle en temps de calcul et en espace par rapport à la dimension de l'état. Auparavant, des techniques de décomposition et de projection de systèmes ont été étudiées, mais le compromis entre l'applicabilité à une classe plus large de dynamiques et le degré de conservatisme a été difficile à trouver. Dans cet article, nous proposons un graphe de dépendance d'état pour représenter la dynamique du système, et nous décomposons le système complet où seuls les états dépendants sont inclus dans chaque sous-système, et les états "manquants" sont traités comme des perturbations limitées. Ainsi, pour une grande variété de dynamiques en robotique, les BRTs peuvent être rapidement approximés en sous-systèmes enchaînés de dimension inférieure avec la propriété de sécurité garantie préservée. Nous démontrons notre méthode par des expériences numériques sur l'intégrateur quadruple 4D, et la bicyclette 6D, un modèle de voiture important qui était auparavant intraitable.