# Monitor-Based Runtime Assurance for Temporal Logic Specifications

## TL;DR

This paper presents a runtime safety assurance architecture for systems with specifications in Linear Temporal Logic, utilizing monitors and backup strategies to ensure safety in real-time applications.

## Contribution

It introduces a novel safety controller architecture combining performance, backup, and assurance components with FSM-based monitors for LTL specifications.

## Key findings

- Successfully implemented on a cyber-physical system
- Guarantees safety by detecting and preventing bad system trajectories
- Demonstrates effectiveness through a detailed case study

## Abstract

This paper introduces the safety controller architecture as a runtime assurance mechanism for system specifications expressed as safety properties in Linear Temporal Logic (LTL). The safety controller has three fundamental components: a performance controller, a backup controller, and an assurance mechanism. The assurance mechanism uses a monitor, constructed as a finite state machine (FSM), to analyze a suggested performance control input and search for system trajectories that are bad prefixes of the system specification. A fault flag from the assurance mechanism denotes a potentially dangerous future system state and triggers a sequence of inputs that is guaranteed to keep the system safe for all time. A case study is presented which details the construction and implementation of a safety controller on a non-deterministic cyber-physical system.