We study the monitorability of properties specified in Distribution Temporal Logic (DisTL), a quantitative temporal logic for expressing robustness properties of dynamic systems operating under uncertainty. We define monitors for DisTL and for its extension with unbounded temporal operators, and study their monotonicity and convergence to their semantics. Our monitors provide quantitative verdicts corresponding to the robustness of the observed behaviour with respect to the given requirement. Moreover, verdicts are provided starting from the first evaluable step of the monitored property, i.e., the first moment in time at which an approximate evaluation of robustness can be provided. We implement the proposed monitoring framework in our tool Stark and demonstrate its applicability by monitoring an AI-driven vehicle on a highway.
In this tutorial paper we provide an introduction to Stark, the Software Tool for the Analysis of Robustness in the unKnown environment. Stark is a Java-based tool that has been introduced to model and analyse the behaviour of dynamical, autonomous systems interacting with an unpredictable environment. Specifically, the tool uses an original behavioural model, namely the evolution sequence model, to represent systems behaviour, and offers two temporal logics, Robustness Temporal Logic (RobTL) and Distribution Temporal Logic (DisTL), to specify and verify requirements on such behaviour. We discuss the main components of Stark and showcase its range of applications by means of case studies from autonomous driving and system biology.
Large Language Models (LLMs) are increasingly used in settings where safe behavior depends not only on the conversational history, but also on the objects mentioned across turns, such as accounts, documents, tickets, or products. Existing guardrail mechanisms lack a formal, declarative framework for online monitoring of temporal policies that relate specific entities mentioned across different turns of an open-ended LLM conversation. We present a runtime monitoring approach for LLM conversations based on past-time temporal logic, where policies are checked incrementally as the dialogue unfolds. To support policies that refer to concrete entities mentioned across messages, the monitor also tracks objects and preserves their identities over time. Our approach treats a conversation as a trace of user messages and LLM-generated assistant responses. It grounds each message into predicates with associated objects, and monitors the resulting trace online. It uses a modified version of DejaVu, a runtime monitoring framework for quantified temporal logic. This rich specification language makes it possible to express policies that depend on object identity and numeric relations across turns. A central challenge is grounding: extracting the relevant predicates and objects from natural-language messages efficiently and accurately. To address this, we propose a lightweight grounding approach with two variations. We evaluate our method through grounding experiments and end-to-end monitoring experiments, and implement it in a tool called DejaVuGuard. Our results demonstrate the feasibility of object-aware temporal monitoring as a practical guardrail layer for conversational AI.
With the increasing complexity of modern hardware designs comes a growing need for robust pre-silicon hardware verification. We propose Periscope, a novel framework for automatic assertion mining with a hybrid approach for simulation, formal verification, and runtime verification. By combining simulation with dynamic assertion mining, rigorous guarantees of Formal Verification, and the performance of Runtime Verification with FPGA emulation, we rapidly generate new pre-silicon assertions that previous work has forgone. We evaluate Periscope with a case study on the CVA6 open-source RISC-V processor core. We extend previous work and generate a new class of assertions that are runtime-consistent, providing new insights into the design as well as formal and runtime verification limitations.
