Assurance arguments provide a clear and structured way to explain why stakeholders should trust that a system satisfies certain properties, yet widely used notations, e.g.Goal Structuring Notation (GSN), typically lack an operational semantics for deriving assurance confidence. Existing approaches address structure and soundness but largely reason over truth values, not over confidence in the justification of claims. Subjective Logic (SL) offers a calculus of belief, disbelief, and uncertainty with operators for combining opinions, enabling confidence propagation under incomplete, conflicting, or subjective evidence. However, existing SL-based approaches do not provide a uniform, compositional semantics that covers all argument elements and relations to enable overall confidence assessment. We propose a confidence semantics that represents argument elements as SL opinions and maps relations between elements to SL operators modelling how confidence flows, effectively turning the argument into an analyzable confidence network. The approach provides explicit warrants, principled handling of context, preserved provenance, and compatibility with GSN, along with practical guidance using an exemplary assurance confidence assessment.

We present a method for dynamic quantitative assurance that enhances static safety cases with continuous, runtime-driven confidence updates. The method quantifies and propagates confidence across the development lifecycle by integrating design-time evidence and windowed runtime Safety Performance Indicators (SPIs) within a single Subjective Logic (SL)-based assurance case. At runtime, SPI evidence is continuously evaluated, and targeted claims are updated using a rule that increases confidence in the absence of violations and imposes prompt penalties when violations occur. This design prioritizes safety-relevant responsiveness over exact classical Bayesian posterior updates. We demonstrate the method using a simulation-based construction zone assist function, focusing on an ML-based construction cone detection component, and show how confidence evolves as SPI evidence is observed in operation.

Machine learning (ML) is a key technology driving innovation today, but ensuring ML safety remains a major challenge for safety-related applications. A promising idea is to build proven-in-use arguments from field data, e.g. by running ML components (MLCs) in shadow mode or within safety envelopes so that their outputs can be monitored as 'safe probes' without affecting safety. These probes can then be used to build a statistical argument about field performance in a Bayesian way. However, many Bayesian field-data approaches in safety engineering model failures as a simple Bernoulli (or binomial) process with a single global failure probability and i.i.d. trials, which is rarely adequate for MLCs whose performance depends strongly on context. Statistical evidence is also about coverage of relevant situations, including edge cases, and building a single integrated statistical model for the entire system is usually not feasible. To address these challenges, this paper introduces CUBICS, a context-modular framework for per-component, situation-aware performance estimation of safety-relevant ML components. CUBICS partitions the operational design domain into situations and, for each safety-relevant component, defines a set of situation-specific assumptions and probabilistic guarantees that are represented and updated in a Bayesian manner using Subjective Logic (SL). By combining these guarantees with beliefs about how often each situation occurs, CUBICS derives an overall risk estimate for each component without requiring a monolithic system-level statistical model, and thus provides a building block for modular, field-data based safety assurance.

ML-based agents acting in open environments must form and revise beliefs under pervasive perceptual and epistemic uncertainty. Verifying such agents over time therefore requires reasoning about how their uncertain beliefs evolve. However, existing temporal verification and monitoring frameworks -- including probabilistic and multi-valued logics -- typically reason about Boolean or graded truth of propositions along system runs, rather than about an agent’s internal belief state. We propose Subjective LTL (SLTL), a temporal specification language whose atomic propositions are Subjective Logic opinions, i.e., tuples of belief, disbelief, and uncertainty about predicates in an agent’s symbolic knowledge model. Under an evidential semantics, temporal operators aggregate evidence over time about persistent hypotheses, so SLTL formulas constrain how the agent’s belief state should evolve. This supports temporal verification and monitoring directly over the dynamics of knowledge-grounded, uncertainty-aware agents, and can equally be used to equip such agents with introspective monitors over their own evolving beliefs, which we illustrate on a simple example.

This paper introduces the concept of Fuzzy Cause Trees (FCT) as a novel approach to Safety of the Intended Functionality (SOTIF) analysis in the automotive industry. Traditional methods like fault tree analysis and Bayesian Networks face limitations when dealing with the complex, interrelated conditions that affect system performance, particularly in perception systems. FCT leverages fuzzy logic to more accurately model and analyze the causal relationships between triggering conditions and system insufficiencies under uncertainty. This method not only offers a quantitative understanding of cause-effect chains but also identifies critical paths for intervention, guiding engineers in mitigating significant risks and enhancing the overall SOTIF of automotive systems. The paper presents the theoretical framework of FCT, its advantages over existing methods, and a practical application through a running example, highlighting its potential to advance SOTIF analyses in the automotive industry. We present several quantitative analysis techniques to derive insights from the model, which can be used to reveal a path towards the mitigation of functional insufficiencies.

A safety assurance argument is a structured reasoning process used to demonstrate that a system meets certain desired safety properties. The argument typically includes claims about the system, evidence supporting those claims, and a clear, logical connection between the evidence and the claims. A critical step in this process is the evaluation of confidence in the argument. To address this step, a range of qualitative and quantitative methods have been proposed. In the qualitative case, defeaters have been used as a dialectical means to challenge nodes in an argument. The presence of defeaters in an assurance argument may highlight reasoning or knowledge gaps, significantly undermining confidence in the argument's validity. However, it is not clear how defeaters can be incorporated into quantitative methods. In this paper, we formalize the notion of defeaters and demonstrate how Subjective Logic can be used to propagate belief, disbelief, and uncertainty within a quantitative assurance argument when these defeaters are present. As a result, this approach enhances the reliability of the argument, allowing for a more rigorous evaluation of safety in complex systems.

Deep Reinforcement Learning (RL) has the potential to revolutionize the automation of complex sequential decision-making problems. Although it has been successfully applied to a wide range of tasks, deployment to real-world settings remains challenging and is often limited. One of the main reasons for this is the lack of safety guarantees for conventional RL algorithms, especially in situations that substantially differ from the learning environment. In such situations, state-of-the-art systems will fail silently, producing action sequences without signalizing any uncertainty regarding the current input. Recent works have suggested Out-of-Distribution (OOD) detection as an additional reliability measure when deploying RL in the real world. How these mechanisms benefit the safety of the entire system, however, is not yet fully understood. In this work, we study how OOD detection contributes to the safety of RL systems by describing the challenges involved with detecting unknown situations. We derive several definitions for unknown events and explore potential avenues for a successful safety argumentation, building on recent work for safety assurance of Machine Learning components. In a series of experiments, we compare different OOD detectors and show how difficult it is to distinguish harmless from potentially unsafe OOD events in practice, and how standard evaluation schemes can lead to deceptive conclusions, depending on which definition of unknown is applied.

Various quantitative methods and associated metrics for evaluating safety-related properties of ML functions have been proposed. However, it is often not clear how these metrics relate to safety requirements, how suitable target values can be selected to demonstrate that the safety requirements are met, and with which confidence can the results be used to reason about safety. This paper presents an uncertainty-aware method for using quantitative evidence to evaluate safety requirements of an ML-based function. To achieve this, we make use of Subjective Logic to describe opinions related to properties of the ML function and its associated evidence. We then show how combining these opinions can allow us to reason about our confidence in the statements we make based on this evidence. The approach is illustrated with a practical example and leads to some general observations related to the confidence that can be achieved in safety arguments for ML-based systems based on such evidence.

Metrics such as accuracy, precision, recall, F1 score, etc. are generally used to assess the performance of machine learning (ML) models. From a safety perspective, relying on such single point estimates to evaluate safety requirements is problematic since they only provide a partial and indirect evaluation of the true safety risk associated with the model and its potential errors. In order to obtain a better understanding of the performance insufficiencies in the model, factors that could influence the quantitative evaluation of safety requirements such as test sample size, dataset size and model calibration need to be taken into account. In safety assurance, arguments typically combine complementary and diverse evidence to strengthen confidence in the safety claims. In this paper, we make a first step towards a more formal treatment of uncertainty in ML metrics by proposing a framework based on Subjective Logic that allows for modelling the relationship between primary and secondary pieces of evidence and the quantification of resulting uncertainty. Based on experiments, we show that single point estimates for common ML metrics tend to overestimate model performance and that a probabilistic treatment using the proposed framework can help to evaluate the probable bounds of the actual performance.

The increasing adoption of autonomous systems in safety-critical applications raises severe concerns regarding safety and reliability. Due to the distinctive characteristics of these systems, conventional approaches to safety assurance are not directly transferable and novel approaches are required. One of the main challenges is the ability to deal with significant uncertainty resulting from (1) the inherent complexity of autonomous system models, (2) potential insufficiencies of data and/or rules, and (3) the open nature of the operational environment. The validity of assumptions made about these three layers greatly impact the confidence in the guarantees provided by a safety argument. In this paper we view the problem of safety assurance as the satisfaction of a safety contract, more specifically as a conditional deduction operation from assumptions to guarantees. We formalise this idea using Subjective Logic and derive from this formalisation an argument structure in GSN that allows for automated reasoning about the uncertainty in the guarantees given the assumptions and any further available evidence. We illustrate the idea using a simple ML-based traffic sign classification example.

There is increasing interest in the application of machine learning (ML) technologies to safety-critical cyber-physical systems, with the promise of increased levels of autonomy due to their potential for solving complex perception and planning tasks. However, demonstrating the safety of ML is seen as one of the most challenging hurdles to their widespread deployment for such applications. In this paper we explore the factors which make the safety assurance of ML such a challenging task. In particular we address the impact of uncertainty on the confidence in ML safety assurance arguments. We show how this uncertainty is related to complexity in the ML models as well as the inherent complexity of the tasks that they are designed to implement. Based on definitions of uncertainty as well as an exemplary assurance argument structure, we examine typical weaknesses in the argument and how these can be addressed. The analysis combines an understanding of causes of insufficiencies in ML models with a systematic analysis of the types of asserted context, asserted evidence and asserted inference within the assurance argument. This leads to a systematic identification of requirements on the assurance argument structure as well as supporting evidence. We conclude that a combination of qualitative arguments combined with quantitative evidence are required to build a robust argument for safety-related properties of ML functions that is continuously refined to reduce residual and emerging uncertainties in the arguments after the function has been deployed into the target environment.

Smart contracts allow for exchange of coins according to program rules. While it is well known that so called bribery contracts can influence the incentive mechanism of a Nakamotostyle consensus, we present a more fine-grained bribery attack incentivizing a temporary censorship against a specific account. To this end, we introduce three different bribery contracts on the blockchain where each uniquely manipulates the rewards that a rational miner would receive. Additionally, we formalize the established bribery mechanisms as a Markov game and show for each game the existence of equilibria leading to successful censorships. Finally, we compare the bribery mechanisms with respect to the scalability of the attack costs and the strategic dominance. Our work is motivated by off-chain protocols including payment and state channels which require to publish transactions within a certain amount of time. In such off-chain protocols a temporary censorship attack can result into significant financial damage.

Central to explanatory simulation models is their capability to not just show that but also why particular things happen. Explanation is closely related with the detection of causal relationships and is, in a simulation context, typically done by means of controlled experiments. However, for complex simulation models, conventional “blackbox” experiments may be too coarse-grained to cope with spurious relationships. We present an intervention-based causal analysis methodology that exploits the manipulability of computational models, and detects and circumvents spurious effects. The core of the methodology is a formal model that maps basic causal assumptions to causal observations and allows for the identification of combinations of assumptions that have a negative impact on observability. First, experiments indicate that the methodology can successfully deal with notoriously tricky situations involving asymmetric and symmetric overdetermination and detect fine-grained causal relationships between events in the simulation. As illustrated in the article, the methodology can be easily integrated into an existing simulation environment.

Due to their immense complexity, large-scale multi-agent systems are often not amenable to exhaustive formal verification. Statistical approaches that focus on the verification of individual traces can provide an interesting alternative that circumvents combinatorial explosion. However, due to its focus on finite execution paths, trace-based verification is inherently limited to certain types of correctness properties. We show how, by combining sampling with the idea of trace fragmentation, statistical verification can be used to answer interesting quantitative correctness questions about multi-agent systems at different observational levels. The usefulness of the verification approach is illustrated with a simple case study from the area of swarm robotics.

Agent-based simulation has shown great success for the study of complex adaptive systems and could in many areas show advantages over traditional analytical methods. Due to their internal complexity, however, agent-based simulations are notoriously difficult to verify and validate. This paper presents ^ , a Monte Carlo Model Checker for Multiagent-Based Simulations. It incorporates the idea of statistical runtime verification, a combination of statistical model checking and runtime verification, and is tailored to the approximate verification of complex agent-based simulations. We provide a description of the underlying theory together with design decisions, an architectural overview, and implementation details. The performance of ^ in terms of both runtime consumption and memory allocation is evaluated against a set of example properties.

Agent-based simulation (ABS) has shown great success for the study of complex adaptive systems which are hard or even impossible to analyse using conventional analytical techniques. For reasons of performance and flexibility, non-trivial ABS models are often implemented in general purpose programming languages like Java or C++. As a consequence of the generality of those languages, simulation-based agents are traditionally rule-based and thus rather ‘myopic’ in nature which critically limits their level of behavioural sophistication. In the more general area of multiagent systems, agent-oriented programming (AOP) has emerged as a powerful paradigm for the implementation of intelligent, practically reasoning agents. However, current AOP languages tend to prioritise expressivity over performance which critically limits their application in a time-critical simulation context. The goal of this work is to address this problem and to bridge the gap between the world of C++-based simulation and the world of practically reasoning agents. We present a first version of an efficient and customisable C++-based BDI framework, equipped with a declarative AOP interface that allows for the implementation of BDI-based agents on a high level of abstraction without compromising on performance. The balance between efficiency and convenience of development is achieved by utilising advanced template metaprogramming techniques.

Due to their internal complexity, agent-based simulations are rarely amenable to conventional formal verification. With its focus on individual traces, runtime verification represents an interesting alternative for correctness assessment. Here, execution traces produced by the running system are observed by a monitor and checked for correctness on-the-fly. If the truth or falsity of a given property cannot be determined at time t, then the monitor creates an obligation that the current trace needs to satisfy at time t + 1 in order for the whole property to become true.With different observational levels, traces produced by agentbased simulations have an inherently hierarchical nature which complicates the structure and manipulation of obligations significantly. However, it turns out that this problem is general enough to be dealt with in an abstract, language-independent way.In this paper, we provide a general framework for the monitoring of hierarchical traces. It introduces different types of obligations and appropriate manipulation procedures along with minimal requirements that a property specification language needs to satisfy in order to be monitorable. We provide a full formalisation of the framework and an example implementation of a subset in Haskell.

As a consequence of the growing adoption of agent-based simulations as decision making tools in various (potentially also critical) areas, questions of veracity and validity become increasingly important. In general software and hardware development, formal verification – particularly model checking – has been applied successfully to a wide range of problems; due to their immense complexity, however, agent-based simulations lend themselves to conventional formal verification only in very simple cases and at a disproportionately high cost. The purpose of this work is to address this problem and present a statistical runtime verification approach which focusses on the analysis of the temporal behaviour of large-scale probabilistic agent-based simulations. The approach is tailored to the particular mix of characteristics that agent-based simulations typically exhibit: large populations, randomness, heterogeneity, temporal boundedness and the existence of multiple observational levels. It combines the ideas of runtime verification and statistical model checking and allows for the temporal verification of simulations with hundreds or thousands of constituents and probabilistic state transitions. Instead of requiring a formal model, verification is performed upon traces of the original simulation obtained through repeated execution. Properties are checked on-the-fly, i.e. during the execution of the simulation, which is achieved by interleaving simulation and verification. Evaluation is lazy, i.e. a simulation step is performed only if the property has not already been satisfied or refuted. This reduces the amount of simulation to a minimum and restricts state space exploration to the smallest fragment necessary for finding a definite answer to the given property. Verification results are approximate, but the precision is clearly quantifiable and adjustable by varying the number of simulation runs.