6 papers · 1 filter
Causal Past Logic for Runtime Verification of Distributed LLM Agent Workflows
Benedikt Bollig
Distributed LLM agent workflows should not be monitored as if they produced a single sequential log. In an asynchronous execution, a decision can only depend on events that are cau…
Runtime Verification: Monitoring, Knowledge, and Uncertainty (Lecture Notes)
Benedikt Bollig
Runtime verification is a lightweight verification technique that complements model checking by analyzing system executions at runtime rather than exploring a complete system model…
Verification of Neural Networks (Lecture Notes)
Benedikt Bollig
These lecture notes provide an introduction to the verification of neural networks from a theoretical perspective. We discuss feed-forward neural networks, recurrent neural network…
High-Level Message Sequence Charts: Satisfiability and Realizability Revisited
Benedikt Bollig, Marie Fortin, Paul Gastin
Message sequence charts (MSCs) visually represent interactions in distributed systems that communicate through FIFO channels. High-level MSCs (HMSCs) extend MSCs with choice, conca…
On the Satisfiability of Local First-Order Logics with Data
Benedikt Bollig, Arnaud Sangnier, Olivier Stietel
We study first-order logic over unordered structures whose elements carry a finite number of data values from an infinite domain. Data values can be compared wrt.\ equality. As the…
Branch-Well-Structured Transition Systems and Extensions
Benedikt Bollig, Alain Finkel, Amrita Suresh
We propose a relaxation to the definition of well-structured transition systems (\WSTS) while retaining the decidability of boundedness and non-termination. In this class, the well…