Formal Control of an Inverted Pendulum on a Cart via Stochastic Abstractions

Abstract

The use of machine learning (ML), especially neural networks, in modeling control systems has shown promise, particularly for systems with complex physics. However, applying these models in safety-critical areas requires reliable verification and control synthesis methods due to their inherent complexity. Formal methods, using stochastic finite state models like interval Markov decision processes (IMDPs), provide a way to analyze and verify these systems against detailed safety and performance specifications defined using linear temporal logic over finite traces (LTLf). Abstraction of ML models into such IMDPs, allows the deriving of formal guarantees on the IMDP that carryover to the underlying ML model.

This thesis focuses on designing a switched controller for a cart-pendulum system using neural network dynamic models (NNDM) by formal control synthesis, validating it through formal verification methods. The methodology includes modeling the system behavior under different controllers, abstracting these models into IMDPs, applying the respective formal methods, and validating the approach through experiments. The aim is to demonstrate the framework's utility in a practical context, comparing different neural network architectures and researching the applicability of formal guarantees to both the models and the actual system.

The main contributions are a practical application of the framework to a specific system, a comparison of neural network architectures for dynamic modeling, and an experiment-based validation of the framework's effectiveness. It confirms that the formal guarantees for abstracted models are relevant to the actual system, providing insights into the framework's potential for real-world applications. The findings suggest areas for further research, particularly in making such frameworks more accessible for practical deployment in safety-critical systems.