Runtime Verification under Split Past and Future

Abstract

Runtime assurance for autonomous systems increasingly requires reasoning not only about observed executions but also about anticipated future behaviors. Traditional runtime verification, however, primarily evaluates the execution observed so far and does not directly account for predicted continuations. We propose a formal framework for runtime assurance that combines monitoring of the observed execution with analysis of multiple predicted continuations. To support this integration, we introduce Split Linear Temporal Logic (SplitLTL), a linear-time temporal logic that assigns complementary roles to past and future temporal specifications within a single specification. The past component uses the observed history to determine the assurance requirements applicable at the current point of execution, while the future component evaluates predicted continuations against those requirements. The framework therefore filters predicted continuations according to the requirements induced by the observed history, identifying admissible continuations that can support subsequent decision making. We formally define the syntax and semantics of SplitLTL and present an online monitoring architecture for evaluating observed executions together with predicted continuations.