Showing 1–35 of 35 results for author: Stoelinga, M

Fuzzy Fault Trees Formalized

Authors: Thi Kim Nhung Dang, Milan Lopuhaä-Zwakenberg, Mariëlle Stoelinga

Abstract: Fault tree analysis is a vital method of assessing safety risks. It helps to identify potential causes of accidents, assess their likelihood and severity, and suggest preventive measures. Quantitative analysis of fault trees is often done via the dependability metrics that compute the system's failure behaviour over time. However, the lack of precise data is a major obstacle to quantitative analys… ▽ More Fault tree analysis is a vital method of assessing safety risks. It helps to identify potential causes of accidents, assess their likelihood and severity, and suggest preventive measures. Quantitative analysis of fault trees is often done via the dependability metrics that compute the system's failure behaviour over time. However, the lack of precise data is a major obstacle to quantitative analysis, and so to reliability analysis. Fuzzy logic is a popular framework for dealing with ambiguous values and has applications in many domains. A number of fuzzy approaches have been proposed to fault tree analysis, but -- to the best of our knowledge -- none of them provide rigorous definitions or algorithms for computing fuzzy unreliability values. In this paper, we define a rigorous framework for fuzzy unreliability values. In addition, we provide a bottom-up algorithm to efficiently calculate fuzzy reliability for a system. The algorithm incorporates the concept of $α$-cuts method. That is, performing binary algebraic operations on intervals on horizontally discretised $α$-cut representations of fuzzy numbers. The method preserves the nonlinearity of fuzzy unreliability. Finally, we illustrate the results obtained from two case studies. △ Less

Submitted 13 March, 2024; originally announced March 2024.

Comments: 14 pages

Querying Fault and Attack Trees: Property Specification on a Water Network

Authors: Stefano M. Nicoletti, Milan Lopuhaä-Zwakenberg, E. Moritz Hahn, Mariëlle Stoelinga

Abstract: We provide an overview of three different query languages whose objective is to specify properties on the highly popular formalisms of fault trees (FTs) and attack trees (ATs). These are BFL, a Boolean Logic for FTs, PFL, a probabilistic extension of BFL and ATM, a logic for security metrics on ATs. We validate the framework composed by these three logics by applying them to the case study of a wa… ▽ More We provide an overview of three different query languages whose objective is to specify properties on the highly popular formalisms of fault trees (FTs) and attack trees (ATs). These are BFL, a Boolean Logic for FTs, PFL, a probabilistic extension of BFL and ATM, a logic for security metrics on ATs. We validate the framework composed by these three logics by applying them to the case study of a water distribution network. We extend the FT for this network - found in the literature - and we propose to model the system under analysis with the Fault Trees/Attack Trees (FT/ATs) formalism, combining both FTs and ATs in a unique model. Furthermore, we propose a novel combination of the showcased logics to account for queries that jointly consider both the FT and the AT of the model, integrating influences of attacks on failure probabilities of different components. Finally, we extend the domain specific language for PFL with novel constructs to capture the interplay between metrics of attacks - e.g., "cost", success probabilities - and failure probabilities in the system. △ Less

Submitted 29 January, 2024; originally announced January 2024.

Fuzzy quantitative attack tree analysis

Authors: Thi Kim Nhung Dang, Milan Lopuhaä-Zwakenberg, Mariëlle Stoelinga

Abstract: Attack trees are important for security, as they help to identify weaknesses and vulnerabilities in a system. Quantitative attack tree analysis supports a number security metrics, which formulate important KPIs such as the shortest, most likely and cheapest attacks. A key bottleneck in quantitative analysis is that the values are usually not known exactly, due to insufficient data and/or lack of… ▽ More Attack trees are important for security, as they help to identify weaknesses and vulnerabilities in a system. Quantitative attack tree analysis supports a number security metrics, which formulate important KPIs such as the shortest, most likely and cheapest attacks. A key bottleneck in quantitative analysis is that the values are usually not known exactly, due to insufficient data and/or lack of knowledge. Fuzzy logic is a prominent framework to handle such uncertain values, with applications in numerous domains. While several studies proposed fuzzy approaches to attack tree analysis, none of them provided a firm definition of fuzzy metric values or generic algorithms for computation of fuzzy metrics. In this work, we define a generic formulation for fuzzy metric values that applies to most quantitative metrics. The resulting metric value is a fuzzy number obtained by following Zadeh's extension principle, obtained when we equip the basis attack steps, i.e., the leaves of the attack trees, with fuzzy numbers. In addition, we prove a modular decomposition theorem that yields a bottom-up algorithm to efficiently calculate the top fuzzy metric value. △ Less

Submitted 22 January, 2024; originally announced January 2024.

Comments: 23 pages, 6 figures, FASE2024

CTMCs with Imprecisely Timed Observations

Authors: Thom Badings, Matthias Volk, Sebastian Junges, Marielle Stoelinga, Nils Jansen

Abstract: Labeled continuous-time Markov chains (CTMCs) describe processes subject to random timing and partial observability. In applications such as runtime monitoring, we must incorporate past observations. The timing of these observations matters but may be uncertain. Thus, we consider a setting in which we are given a sequence of imprecisely timed labels called the evidence. The problem is to compute r… ▽ More Labeled continuous-time Markov chains (CTMCs) describe processes subject to random timing and partial observability. In applications such as runtime monitoring, we must incorporate past observations. The timing of these observations matters but may be uncertain. Thus, we consider a setting in which we are given a sequence of imprecisely timed labels called the evidence. The problem is to compute reachability probabilities, which we condition on this evidence. Our key contribution is a method that solves this problem by unfolding the CTMC states over all possible timings for the evidence. We formalize this unfolding as a Markov decision process (MDP) in which each timing for the evidence is reflected by a scheduler. This MDP has infinitely many states and actions in general, making a direct analysis infeasible. Thus, we abstract the continuous MDP into a finite interval MDP (iMDP) and develop an iterative refinement scheme to upper-bound conditional probabilities in the CTMC. We show the feasibility of our method on several numerical benchmarks and discuss key challenges to further enhance the performance. △ Less

Submitted 29 January, 2024; v1 submitted 12 January, 2024; originally announced January 2024.

Comments: Extended version (with appendix) of the paper accepted at TACAS 2024

Fault Trees, Decision Trees, And Binary Decision Diagrams: A Systematic Comparison

Authors: L. A. Jimenez-Roa, T. Heskes, M. Stoelinga

Abstract: In reliability engineering, we need to understand system dependencies, cause-effect relations, identify critical components, and analyze how they trigger failures. Three prominent graph models commonly used for these purposes are fault trees (FTs), decision trees (DTs), and binary decision diagrams (BDDs). These models are popular because they are easy to interpret, serve as a communication tool b… ▽ More In reliability engineering, we need to understand system dependencies, cause-effect relations, identify critical components, and analyze how they trigger failures. Three prominent graph models commonly used for these purposes are fault trees (FTs), decision trees (DTs), and binary decision diagrams (BDDs). These models are popular because they are easy to interpret, serve as a communication tool between stakeholders of various backgrounds, and support decision-making processes. Moreover, these models help to understand real-world problems by computing reliability metrics, minimum cut sets, logic rules, and displaying dependencies. Nevertheless, it is unclear how these graph models compare. Thus, the goal of this paper is to understand the similarities and differences through a systematic comparison based on their (i) purpose and application, (ii) structural representation, (iii) analysis methods, (iv) construction, and (v) benefits & limitations. Furthermore, we use a running example based on a Container Seal Design to showcase the models in practice. Our results show that, given that FTs, DTs and BDDs have different purposes and application domains, they adopt different structural representations and analysis methodologies that entail a variety of benefits and limitations, the latter can be addressed via conversion methods or extensions. Specific remarks are that BDDs can be considered as a compact representation of binary DTs, since the former allows sub-node sharing, which makes BDDs more efficient at representing logical rules than binary DTs. It is possible to obtain cut sets from BDDs and DTs and construct a FT using the (con/dis)junctive normal form, although this may result in a sub-optimal FT structure. △ Less

Submitted 3 October, 2023; originally announced October 2023.

Deterioration modeling of sewer pipes via discrete-time Markov chains: A large-scale case study in the Netherlands

Authors: L. A. Jimenez-Roa, T. Heskes, T. Tinga, H. Molegraaf, M. Stoelinga

Abstract: Sewer pipe network systems are an important part of civil infrastructure, and in order to find a good trade-off between maintenance costs and system performance, reliable sewer pipe degradation models are essential. In this paper, we present a large-scale case study in the city of Breda in the Netherlands. Our dataset has information on sewer pipes built since the 1920s and contains information on… ▽ More Sewer pipe network systems are an important part of civil infrastructure, and in order to find a good trade-off between maintenance costs and system performance, reliable sewer pipe degradation models are essential. In this paper, we present a large-scale case study in the city of Breda in the Netherlands. Our dataset has information on sewer pipes built since the 1920s and contains information on different covariates. We also have several types of damage, but we focus our attention on infiltrations, surface damage, and cracks. Each damage has an associated severity index ranging from 1 to 5. To account for the characteristics of sewer pipes, we defined 6 cohorts of interest. Two types of discrete-time Markov chains (DTMC), which we called Chain `Multi' and `Single' (where Chain `Multi' contains additional transitions compared to Chain `Single'), are commonly used to model sewer pipe degradation at the pipeline level, and we want to evaluate which suits better our case study. To calibrate the DTMCs, we define an optimization process using Sequential Least-Squares Programming to find the DTMC parameter that best minimizes the root mean weighted square error. Our results show that for our case study, there is no substantial difference between Chain `Multi' and `Single', but the latter has fewer parameters and can be easily trained. Our DTMCs are useful to compare the cohorts via the expected values, e.g., concrete pipes carrying mixed and waste content reach severe levels of surface damage more quickly compared to concrete pipes carrying rainwater, which is a phenomenon typically identified in practice. △ Less

Submitted 3 October, 2023; originally announced October 2023.

ATM: a Logic for Quantitative Security Properties on Attack Trees

Authors: Stefano M. Nicoletti, Milan Lopuhaä-Zwakenberg, E. Moritz Hahn, Mariëlle Stoelinga

Abstract: Critical infrastructure systems - for which high reliability and availability are paramount - must operate securely. Attack trees (ATs) are hierarchical diagrams that offer a flexible modelling language used to assess how systems can be attacked. ATs are widely employed both in industry and academia but - in spite of their popularity - little work has been done to give practitioners instruments to… ▽ More Critical infrastructure systems - for which high reliability and availability are paramount - must operate securely. Attack trees (ATs) are hierarchical diagrams that offer a flexible modelling language used to assess how systems can be attacked. ATs are widely employed both in industry and academia but - in spite of their popularity - little work has been done to give practitioners instruments to formulate queries on ATs in an understandable yet powerful way. In this paper we fill this gap by presenting ATM, a logic to express quantitative security properties on ATs. ATM allows for the specification of properties involved with security metrics that include "cost", "probability" and "skill" and permits the formulation of insightful what-if scenarios. To showcase its potential, we apply ATM to the case study of a CubeSAT, presenting three different ways in which an attacker can compromise its availability. We showcase property specification on the corresponding attack tree and we present theory and algorithms - based on binary decision diagrams - to check properties and compute metrics of ATM-formulae. △ Less

Submitted 17 May, 2024; v1 submitted 17 September, 2023; originally announced September 2023.

With a little help from your friends: semi-cooperative games via Joker moves

Authors: Petra van den Bos, Marielle Stoelinga

Abstract: This paper coins the notion of Joker games where Player 2 is not strictly adversarial: Player 1 gets help from Player 2 by playing a Joker. We formalize these games as cost games, and study their theoretical properties. Finally, we illustrate their use in model-based testing. This paper coins the notion of Joker games where Player 2 is not strictly adversarial: Player 1 gets help from Player 2 by playing a Joker. We formalize these games as cost games, and study their theoretical properties. Finally, we illustrate their use in model-based testing. △ Less

Submitted 25 January, 2024; v1 submitted 26 April, 2023; originally announced April 2023.

Comments: Journal version for LMCS issue

Cost-damage analysis of attack trees

Authors: Milan Lopuhaä-Zwakenberg, Mariëlle Stoelinga

Abstract: Attack trees (ATs) are a widely deployed modelling technique to categorize potential attacks on a system. An attacker of such a system aims at doing as much damage as possible, but might be limited by a cost budget. The maximum possible damage for a given cost budget is an important security metric of a system. In this paper, we find the maximum damage given a cost budget by modelling this problem… ▽ More Attack trees (ATs) are a widely deployed modelling technique to categorize potential attacks on a system. An attacker of such a system aims at doing as much damage as possible, but might be limited by a cost budget. The maximum possible damage for a given cost budget is an important security metric of a system. In this paper, we find the maximum damage given a cost budget by modelling this problem with ATs, both in deterministic and probabilistic settings. We show that the general problem is NP-complete, and provide heuristics to solve it. For general ATs these are based on integer linear programming. However when the AT is tree-structured, then one can instead use a faster bottom-up approach. We also extend these methods to other problems related to the cost-damage tradeoff, such as the cost-damage Pareto front. △ Less

Submitted 12 April, 2023; originally announced April 2023.

PFL: a Probabilistic Logic for Fault Trees

Authors: Stefano M. Nicoletti, Milan Lopuhaä-Zwakenberg, E. Moritz Hahn, Mariëlle Stoelinga

Abstract: Safety-critical infrastructures must operate in a safe and reliable way. Fault tree analysis is a widespread method used for risk assessment of these systems: fault trees (FTs) are required by, e.g., the Federal Aviation Administration and the Nuclear Regulatory Commission. In spite of their popularity, little work has been done on formulating structural queries about FT and analyzing these, e.g.,… ▽ More Safety-critical infrastructures must operate in a safe and reliable way. Fault tree analysis is a widespread method used for risk assessment of these systems: fault trees (FTs) are required by, e.g., the Federal Aviation Administration and the Nuclear Regulatory Commission. In spite of their popularity, little work has been done on formulating structural queries about FT and analyzing these, e.g., when evaluating potential scenarios, and to give practitioners instruments to formulate queries on FTs in an understandable yet powerful way. In this paper, we aim to fill this gap by extending BFL [32], a logic that reasons about Boolean FTs. To do so, we introduce a Probabilistic Fault tree Logic (PFL). PFL is a simple, yet expressive logic that supports easier formulation of complex scenarios and specification of FT properties that comprise probabilities. Alongside PFL, we present LangPFL, a domain specific language to further ease property specification. We showcase PFL and LangPFL by applying them to a COVID-19 related FT and to a FT for an oil/gas pipeline. Finally, we present theory and model checking algorithms based on binary decision diagrams (BDDs). △ Less

Submitted 1 June, 2024; v1 submitted 30 March, 2023; originally announced March 2023.

Comments: arXiv admin note: text overlap with arXiv:2208.13424

Journal ref: In: Chechik, M., Katoen, JP., Leucker, M. (eds) Formal Methods. FM 2023. Lecture Notes in Computer Science, vol 14000. Springer, Cham

Robust Control for Dynamical Systems With Non-Gaussian Noise via Formal Abstractions

Authors: Thom Badings, Licio Romao, Alessandro Abate, David Parker, Hasan A. Poonawala, Marielle Stoelinga, Nils Jansen

Abstract: Controllers for dynamical systems that operate in safety-critical settings must account for stochastic disturbances. Such disturbances are often modeled as process noise in a dynamical system, and common assumptions are that the underlying distributions are known and/or Gaussian. In practice, however, these assumptions may be unrealistic and can lead to poor approximations of the true noise distri… ▽ More Controllers for dynamical systems that operate in safety-critical settings must account for stochastic disturbances. Such disturbances are often modeled as process noise in a dynamical system, and common assumptions are that the underlying distributions are known and/or Gaussian. In practice, however, these assumptions may be unrealistic and can lead to poor approximations of the true noise distribution. We present a novel controller synthesis method that does not rely on any explicit representation of the noise distributions. In particular, we address the problem of computing a controller that provides probabilistic guarantees on safely reaching a target, while also avoiding unsafe regions of the state space. First, we abstract the continuous control system into a finite-state model that captures noise by probabilistic transitions between discrete states. As a key contribution, we adapt tools from the scenario approach to compute probably approximately correct (PAC) bounds on these transition probabilities, based on a finite number of samples of the noise. We capture these bounds in the transition probability intervals of a so-called interval Markov decision process (iMDP). This iMDP is, with a user-specified confidence probability, robust against uncertainty in the transition probabilities, and the tightness of the probability intervals can be controlled through the number of samples. We use state-of-the-art verification techniques to provide guarantees on the iMDP and compute a controller for which these guarantees carry over to the original control system. In addition, we develop a tailored computational scheme that reduces the complexity of the synthesis of these guarantees on the iMDP. Benchmarks on realistic control systems show the practical applicability of our method, even when the iMDP has hundreds of millions of transitions. △ Less

Submitted 4 January, 2023; originally announced January 2023.

Comments: To appear in the Journal of Artificial Intelligence Research (JAIR). arXiv admin note: text overlap with arXiv:2110.12662

Journal ref: Journal of Artificial Intelligence Research (JAIR) 76 (2023) 341-391

Efficient and Generic Algorithms for Quantitative Attack Tree Analysis

Authors: Milan Lopuhaä-Zwakenberg, Carlos E. Budde, Mariëlle Stoelinga

Abstract: Numerous analysis methods for quantitative attack tree analysis have been proposed. These algorithms compute relevant security metrics, i.e. performance indicators that quantify how good the security of a system is; typical metrics being the most likely attack, the cheapest, or the most damaging one. However, existing methods are only geared towards specific metrics or do not work on general attac… ▽ More Numerous analysis methods for quantitative attack tree analysis have been proposed. These algorithms compute relevant security metrics, i.e. performance indicators that quantify how good the security of a system is; typical metrics being the most likely attack, the cheapest, or the most damaging one. However, existing methods are only geared towards specific metrics or do not work on general attack trees. This paper classifies attack trees in two dimensions: proper trees vs. directed acyclic graphs (i.e. with shared subtrees); and static vs. dynamic gates. For three out of these four classes, we propose novel algorithms that work over a generic attribute domain, encompassing a large number of concrete security metrics defined on the attack tree semantics; dynamic attack trees with directed acyclic graph structure are left as an open problem. We also analyse the computational complexity of our methods. △ Less

Submitted 10 December, 2022; originally announced December 2022.

Comments: Funding: ERC Consolidator (Grant Number: 864075), and European Union (Grant Number: 101067199-ProSVED), in IEEE Transactions on Dependable and Secure Computing, 2022. arXiv admin note: substantial text overlap with arXiv:2105.07511

ACM Class: F.1.0; F.2.2; G.2.3

BFL: a Logic to Reason about Fault Trees

Authors: Stefano M. Nicoletti, E. Moritz Hahn, Marielle Stoelinga

Abstract: Safety-critical infrastructures must operate safely and reliably. Fault tree analysis is a widespread method used to assess risks in these systems: fault trees (FTs) are required - among others - by the Federal Aviation Authority, the Nuclear Regulatory Commission, in the ISO26262 standard for autonomous driving and for software development in aerospace systems. Although popular both in industry a… ▽ More Safety-critical infrastructures must operate safely and reliably. Fault tree analysis is a widespread method used to assess risks in these systems: fault trees (FTs) are required - among others - by the Federal Aviation Authority, the Nuclear Regulatory Commission, in the ISO26262 standard for autonomous driving and for software development in aerospace systems. Although popular both in industry and academia, FTs lack a systematic way to formulate powerful and understandable analysis queries. In this paper, we aim to fill this gap and introduce Boolean Fault tree Logic (BFL), a logic to reason about FTs. BFL is a simple, yet expressive logic that supports easier formulation of complex scenarios and specification of FT properties. Alongside BFL, we present model checking algorithms based on binary decision diagrams (BDDs) to analyse specified properties in BFL, patterns and an algorithm to construct counterexamples. Finally, we propose a case-study application of BFL by analysing a COVID19-related FT. △ Less

Submitted 1 June, 2024; v1 submitted 29 August, 2022; originally announced August 2022.

Sampling-Based Verification of CTMCs with Uncertain Rates

Authors: Thom S. Badings, Nils Jansen, Sebastian Junges, Marielle Stoelinga, Matthias Volk

Abstract: We employ uncertain parametric CTMCs with parametric transition rates and a prior on the parameter values. The prior encodes uncertainty about the actual transition rates, while the parameters allow dependencies between transition rates. Sampling the parameter values from the prior distribution then yields a standard CTMC, for which we may compute relevant reachability probabilities. We provide a… ▽ More We employ uncertain parametric CTMCs with parametric transition rates and a prior on the parameter values. The prior encodes uncertainty about the actual transition rates, while the parameters allow dependencies between transition rates. Sampling the parameter values from the prior distribution then yields a standard CTMC, for which we may compute relevant reachability probabilities. We provide a principled solution, based on a technique called scenario-optimization, to the following problem: From a finite set of parameter samples and a user-specified confidence level, compute prediction regions on the reachability probabilities. The prediction regions should (with high probability) contain the reachability probabilities of a CTMC induced by any additional sample. To boost the scalability of the approach, we employ standard abstraction techniques and adapt our methodology to support approximate reachability probabilities. Experiments with various well-known benchmarks show the applicability of the approach. △ Less

Submitted 21 June, 2022; v1 submitted 17 May, 2022; originally announced May 2022.

Journal ref: Computed Aided Verification (CAV) 2022

Automatic inference of fault tree models via multi-objective evolutionary algorithms

Authors: Lisandro A. Jimenez-Roa, Tom Heskes, Tiedo Tinga, Marielle Stoelinga

Abstract: Fault tree analysis is a well-known technique in reliability engineering and risk assessment, which supports decision-making processes and the management of complex systems. Traditionally, fault tree (FT) models are built manually together with domain experts, considered a time-consuming process prone to human errors. With Industry 4.0, there is an increasing availability of inspection and monitor… ▽ More Fault tree analysis is a well-known technique in reliability engineering and risk assessment, which supports decision-making processes and the management of complex systems. Traditionally, fault tree (FT) models are built manually together with domain experts, considered a time-consuming process prone to human errors. With Industry 4.0, there is an increasing availability of inspection and monitoring data, making techniques that enable knowledge extraction from large data sets relevant. Thus, our goal with this work is to propose a data-driven approach to infer efficient FT structures that achieve a complete representation of the failure mechanisms contained in the failure data set without human intervention. Our algorithm, the FT-MOEA, based on multi-objective evolutionary algorithms, enables the simultaneous optimization of different relevant metrics such as the FT size, the error computed based on the failure data set and the Minimal Cut Sets. Our results show that, for six case studies from the literature, our approach successfully achieved automatic, efficient, and consistent inference of the associated FT models. We also present the results of a parametric analysis that tests our algorithm for different relevant conditions that influence its performance, as well as an overview of the data-driven methods used to automatically infer FT models. △ Less

Submitted 6 April, 2022; originally announced April 2022.

BDDs Strike Back: Efficient Analysis of Static and Dynamic Fault Trees

Authors: Daniel Basgöze, Matthias Volk, Joost-Pieter Katoen, Shahid Khan, Marielle Stoelinga

Abstract: Fault trees are a key model in reliability analysis. Classical static fault trees (SFT) can best be analysed using binary decision diagrams (BDD). State-based techniques are favorable for the more expressive dynamic fault trees (DFT). This paper combines the best of both worlds by following Dugan's approach: dynamic sub-trees are analysed via model checking Markov models and replaced by basic even… ▽ More Fault trees are a key model in reliability analysis. Classical static fault trees (SFT) can best be analysed using binary decision diagrams (BDD). State-based techniques are favorable for the more expressive dynamic fault trees (DFT). This paper combines the best of both worlds by following Dugan's approach: dynamic sub-trees are analysed via model checking Markov models and replaced by basic events capturing the obtained failure probabilities. The resulting SFT is then analysed via BDDs. We implemented this approach in the Storm model checker. Extensive experiments (a) compare our pure BDD-based analysis of SFTs to various existing SFT analysis tools, (b) indicate the benefits of our efficient calculations for multiple time points and the assessment of the mean-time-to-failure, and (c) show that our implementation of Dugan's approach significantly outperforms pure Markovian analysis of DFTs. Our implementation Storm-dft is currently the only tool supporting efficient analysis for both SFTs and DFTs. △ Less

Submitted 28 March, 2022; v1 submitted 6 February, 2022; originally announced February 2022.

Comments: Extended version of NFM'22 paper

Attack time analysis in dynamic attack trees via integer linear programming

Authors: Milan Lopuhaä-Zwakenberg, Mariëlle Stoelinga

Abstract: Attack trees (ATs) are an important tool in security analysis, and an important part of AT analysis is computing metrics. However, metric computation is NP-complete in general. In this paper, we showcase the use of mixed integer linear programming (MILP) as a tool for quantitative analysis. Specifically, we use MILP to solve the open problem of calculating the min time metric of dynamic ATs, i.e.,… ▽ More Attack trees (ATs) are an important tool in security analysis, and an important part of AT analysis is computing metrics. However, metric computation is NP-complete in general. In this paper, we showcase the use of mixed integer linear programming (MILP) as a tool for quantitative analysis. Specifically, we use MILP to solve the open problem of calculating the min time metric of dynamic ATs, i.e., the minimal time to attack a system. We also present two other tools to further improve our MILP method: First, we show how the computation can be sped up by identifying the modules of an AT, i.e. subtrees connected to the rest of the AT via only one node. Second, we define a general semantics for dynamic ATs that significantly relaxes the restrictions on attack trees compared to earlier work, allowing us to apply our methods to a wide variety of ATs. Experiments on a synthetic testing set of large ATs verify that both the integer linear programming approach and modular analysis considerably decrease the computation time of attack time analysis. △ Less

Submitted 9 September, 2023; v1 submitted 9 November, 2021; originally announced November 2021.

Sampling-Based Robust Control of Autonomous Systems with Non-Gaussian Noise

Authors: Thom S. Badings, Alessandro Abate, Nils Jansen, David Parker, Hasan A. Poonawala, Marielle Stoelinga

Abstract: Controllers for autonomous systems that operate in safety-critical settings must account for stochastic disturbances. Such disturbances are often modelled as process noise, and common assumptions are that the underlying distributions are known and/or Gaussian. In practice, however, these assumptions may be unrealistic and can lead to poor approximations of the true noise distribution. We present a… ▽ More Controllers for autonomous systems that operate in safety-critical settings must account for stochastic disturbances. Such disturbances are often modelled as process noise, and common assumptions are that the underlying distributions are known and/or Gaussian. In practice, however, these assumptions may be unrealistic and can lead to poor approximations of the true noise distribution. We present a novel planning method that does not rely on any explicit representation of the noise distributions. In particular, we address the problem of computing a controller that provides probabilistic guarantees on safely reaching a target. First, we abstract the continuous system into a discrete-state model that captures noise by probabilistic transitions between states. As a key contribution, we adapt tools from the scenario approach to compute probably approximately correct (PAC) bounds on these transition probabilities, based on a finite number of samples of the noise. We capture these bounds in the transition probability intervals of a so-called interval Markov decision process (iMDP). This iMDP is robust against uncertainty in the transition probabilities, and the tightness of the probability intervals can be controlled through the number of samples. We use state-of-the-art verification techniques to provide guarantees on the iMDP, and compute a controller for which these guarantees carry over to the autonomous system. Realistic benchmarks show the practical applicability of our method, even when the iMDP has millions of states or transitions. △ Less

Submitted 13 December, 2021; v1 submitted 25 October, 2021; originally announced October 2021.

Journal ref: AAAI 2022 (distinguished paper)

Model-based Joint Analysis of Safety and Security: Survey and Identification of Gaps

Authors: Stefano M. Nicoletti, Marijn Peppelman, Christina Kolb, Mariëlle Stoelinga

Abstract: We survey the state-of-the-art on model-based formalisms for safety and security joint analysis, where safety refers to the absence of unintended failures, and security to absence of malicious attacks. We conduct a thorough literature review and - as a result - we consider fourteen model-based formalisms and compare them with respect to several criteria: (1) Modelling capabilities and Expressivene… ▽ More We survey the state-of-the-art on model-based formalisms for safety and security joint analysis, where safety refers to the absence of unintended failures, and security to absence of malicious attacks. We conduct a thorough literature review and - as a result - we consider fourteen model-based formalisms and compare them with respect to several criteria: (1) Modelling capabilities and Expressiveness: which phenomena can be expressed in these formalisms? To which extent can they capture safety-security interactions? (2) Analytical capabilities: which analysis types are supported? (3) Practical applicability: to what extent have the formalisms been used to analyze small or larger case studies? Furthermore, (1) we present more precise definitions for safety-security dependencies in tree-like formalisms; (2) we showcase the potential of each formalism by modelling the same toy example from the literature and (3) we present our findings and reflect on possible ways to narrow highlighted gaps. In summary, our key findings are the following: (1) the majority of approaches combine tree-like formal models; (2) the exact nature of safety-security interaction is still ill-understood and (3) diverse formalisms can capture different interactions; (4) analyzed formalisms merge modelling constructs from existing safety- and security-specific formalisms, without introducing ad hoc constructs to model safety-security interactions, or (5) metrics to analyze trade offs. Moreover, (6) large case studies representing safety-security interactions are still missing. △ Less

Submitted 23 October, 2023; v1 submitted 11 June, 2021; originally announced June 2021.

Efficient Algorithms for Quantitative Attack Tree Analysis

Authors: Carlos E. Budde, Mariëlle Stoelinga

Abstract: Numerous analysis methods for quantitative attack tree analysis have been proposed. These algorithms compute relevant security metrics, i.e. performance indicators that quantify how good the security of a system is, such as the most likely attack, the cheapest, or the most damaging one. This paper classifies attack trees in two dimensions: proper trees vs. directed acyclic graphs (i.e. with shared… ▽ More Numerous analysis methods for quantitative attack tree analysis have been proposed. These algorithms compute relevant security metrics, i.e. performance indicators that quantify how good the security of a system is, such as the most likely attack, the cheapest, or the most damaging one. This paper classifies attack trees in two dimensions: proper trees vs. directed acyclic graphs (i.e. with shared subtrees); and static vs. dynamic gates. For each class, we propose novel algorithms that work over a generic attribute domain, encompassing a large number of concrete security metrics defined on the attack tree semantics. We also analyse the computational complexity of our methods. △ Less

Submitted 22 May, 2021; v1 submitted 16 May, 2021; originally announced May 2021.

Comments: Public version of CSF'21 paper, including an appendix with all proofs of lemmas and theorems

ACM Class: F.1.0; F.2.2; G.2.3

Correct-by-construction reach-avoid control of partially observable linear stochastic systems

Authors: Thom Badings, Hasan A. Poonawala, Marielle Stoelinga, Nils Jansen

Abstract: We study feedback controller synthesis for reach-avoid control of discrete-time, linear time-invariant (LTI) systems with Gaussian process and measurement noise. The problem is to compute a controller such that, with at least some required probability, the system reaches a desired goal state in finite time while avoiding unsafe states. Due to stochasticity and nonconvexity, this problem does not a… ▽ More We study feedback controller synthesis for reach-avoid control of discrete-time, linear time-invariant (LTI) systems with Gaussian process and measurement noise. The problem is to compute a controller such that, with at least some required probability, the system reaches a desired goal state in finite time while avoiding unsafe states. Due to stochasticity and nonconvexity, this problem does not admit exact algorithmic or closed-form solutions in general. Our key contribution is a correct-by-construction controller synthesis scheme based on a finite-state abstraction of a Gaussian belief over the unmeasured state, obtained using a Kalman filter. We formalize this abstraction as a Markov decision process (MDP). To be robust against numerical imprecision in approximating transition probabilities, we use MDPs with intervals of transition probabilities. By construction, any policy on the abstraction can be refined into a piecewise linear feedback controller for the LTI system. We prove that the closed-loop LTI system under this controller satisfies the reach-avoid problem with at least the required probability. The numerical experiments show that our method is able to solve reach-avoid problems for systems with up to 6D state spaces, and with control input constraints that cannot be handled by methods such as the rapidly-exploring random belief trees (RRBT). △ Less

Submitted 12 September, 2023; v1 submitted 3 March, 2021; originally announced March 2021.

Rare Event Simulation for non-Markovian repairable Fault Trees

Authors: Carlos E. Budde, Marco Biagi, Raúl E. Monti, Pedro R. D'Argenio, Mariëlle Stoelinga

Abstract: Dynamic Fault Trees (DFT) are widely adopted in industry to assess the dependability of safety-critical equipment. Since many systems are too large to be studied numerically, DFTs dependability is often analysed using Monte Carlo simulation. A bottleneck here is that many simulation samples are required in the case of rare events, e.g. in highly reliable systems where components fail seldomly. Rar… ▽ More Dynamic Fault Trees (DFT) are widely adopted in industry to assess the dependability of safety-critical equipment. Since many systems are too large to be studied numerically, DFTs dependability is often analysed using Monte Carlo simulation. A bottleneck here is that many simulation samples are required in the case of rare events, e.g. in highly reliable systems where components fail seldomly. Rare Event Simulation (RES) provides techniques to reduce the number of samples in the case of rare events. We present a RES technique based on importance splitting, to study failures in highly reliable DFTs. Whereas RES usually requires meta-information from an expert, our method is fully automatic: by cleverly exploiting the fault tree structure we extract the so-called importance function. We handle DFTs with Markovian and non-Markovian failure and repair distributions (for which no numerical methods exist) and show the efficiency of our approach on several case studies. △ Less

Submitted 28 October, 2019; v1 submitted 23 October, 2019; originally announced October 2019.

ACM Class: D.2.4; I.6.1; I.6.8

Fault Trees from Data: Efficient Learning with an Evolutionary Algorithm

Authors: Alexis Linard, Doina Bucur, Marielle Stoelinga

Abstract: Cyber-physical systems come with increasingly complex architectures and failure modes, which complicates the task of obtaining accurate system reliability models. At the same time, with the emergence of the (industrial) Internet-of-Things, systems are more and more often being monitored via advanced sensor systems. These sensors produce large amounts of data about the components' failure behaviour… ▽ More Cyber-physical systems come with increasingly complex architectures and failure modes, which complicates the task of obtaining accurate system reliability models. At the same time, with the emergence of the (industrial) Internet-of-Things, systems are more and more often being monitored via advanced sensor systems. These sensors produce large amounts of data about the components' failure behaviour, and can, therefore, be fruitfully exploited to learn reliability models automatically. This paper presents an effective algorithm for learning a prominent class of reliability models, namely fault trees, from observational data. Our algorithm is evolutionary in nature; i.e., is an iterative, population-based, randomized search method among fault-tree structures that are increasingly more consistent with the observational data. We have evaluated our method on a large number of case studies, both on synthetic data, and industrial data. Our experiments show that our algorithm outperforms other methods and provides near-optimal results. △ Less

Submitted 13 September, 2019; originally announced September 2019.

Comments: This paper is an extended version of the SETTA 2019 paper, Springer-Verlag

Hackers vs. Security: Attack-Defence Trees as Asynchronous Multi-Agent Systems

Authors: Jaime Arias, Carlos E. Budde, Wojciech Penczek, Laure Petrucci, Mariëlle Stoelinga

Abstract: Attack-Defence Trees (ADTs) are well-suited to assess possible attacks to systems and the efficiency of counter-measures. In this paper, we first enrich the available constructs with reactive patterns that cover further security scenarios, and equip all constructs with attributes such as time and cost to allow quantitative analyses. Then, ADTs are modelled as (an extension of) Asynchronous Multi-A… ▽ More Attack-Defence Trees (ADTs) are well-suited to assess possible attacks to systems and the efficiency of counter-measures. In this paper, we first enrich the available constructs with reactive patterns that cover further security scenarios, and equip all constructs with attributes such as time and cost to allow quantitative analyses. Then, ADTs are modelled as (an extension of) Asynchronous Multi-Agents Systems--EAMAS. The ADT-EAMAS transformation is performed in a systematic manner that ensures correctness. The transformation allows us to quantify the impact of different agents configurations on metrics such as attack time. Using EAMAS also permits parametric verification: we derive constraints for property satisfaction. Our approach is exercised on several case studies using the Uppaal and IMITATOR tools. △ Less

Submitted 12 June, 2019; originally announced June 2019.

Comments: This work was partially funded by the NWO project SEQUOIA (grant 15474), EU project SUCCESS (102112) and the PHC van Gogh PAMPAS. The work of Arias and Petrucci has been supported by the BQR project AMoJAS

Parametric analyses of attack-fault trees

Authors: Étienne André, Didier Lime, Mathias Ramparison, Mariëlle Stoelinga

Abstract: Risk assessment of cyber-physical systems, such as power plants, connected devices and IT-infrastructures has always been challenging: safety (i.e. absence of unintentional failures) and security (i.e. no disruptions due to attackers) are conditions that must be guaranteed. One of the traditional tools used to help considering these problems is attack trees, a tree-based formalism inspired by faul… ▽ More Risk assessment of cyber-physical systems, such as power plants, connected devices and IT-infrastructures has always been challenging: safety (i.e. absence of unintentional failures) and security (i.e. no disruptions due to attackers) are conditions that must be guaranteed. One of the traditional tools used to help considering these problems is attack trees, a tree-based formalism inspired by fault trees, a well-known formalism used in safety engineering. In this paper we define and implement the translation of attack-fault trees (AFTs) to a new extension of timed automata, called parametric weighted timed automata. This allows us to parametrize constants such as time and discrete costs in an AFT and then, using the model-checker IMITATOR, to compute the set of parameter values such that a successful attack is possible. Using the different sets of parameter values computed, different attack and fault scenarios can be deduced depending on the budget, time or computation power of the attacker, providing helpful data to select the most efficient counter-measure. △ Less

Submitted 8 May, 2019; v1 submitted 12 February, 2019; originally announced February 2019.

Comments: This is the extended version of the manuscript of the same name published in ACSD 2019. This work is supported by ANR PACS (ANR-14-CE28-0002), the PHC Van Gogh project PAMPAS, by STW under the project 15474 SEQUOIA, KIA KIEM project 628.010.006 StepUp, the EU under the project 102112 SUCCESS and ERATO HASUO Metamathematics for Systems Design Project (No. JPMJER1603), JST

Tester versus Bug: A Generic Framework for Model-Based Testing via Games

Authors: Petra van den Bos, Marielle Stoelinga

Abstract: We propose a generic game-based approach for test case generation. We set up a game between the tester and the System Under Test, in such a way that test cases correspond to game strategies, and the conformance relation ioco corresponds to alternating refinement. We show that different test assumptions from the literature can be easily incorporated, by slightly varying the moves in the games an… ▽ More We propose a generic game-based approach for test case generation. We set up a game between the tester and the System Under Test, in such a way that test cases correspond to game strategies, and the conformance relation ioco corresponds to alternating refinement. We show that different test assumptions from the literature can be easily incorporated, by slightly varying the moves in the games and their outcomes. In this way, our framework allows a wide plethora of game-theoretic techniques to be deployed for model based testing. △ Less

Submitted 9 September, 2018; originally announced September 2018.

Comments: In Proceedings GandALF 2018, arXiv:1809.02416

Journal ref: EPTCS 277, 2018, pp. 118-132

Maintenance of Smart Buildings using Fault Trees

Authors: Nathalie Cauchi, Khaza Anuarul Hoque, Marielle Stoelinga, Alessandro Abate

Abstract: Timely maintenance is an important means of increasing system dependability and life span. Fault Maintenance trees (FMTs) are an innovative framework incorporating both maintenance strategies and degradation models and serve as a good planning platform for balancing total costs (operational and maintenance) with dependability of a system. In this work, we apply the FMT formalism to a {Smart Buildi… ▽ More Timely maintenance is an important means of increasing system dependability and life span. Fault Maintenance trees (FMTs) are an innovative framework incorporating both maintenance strategies and degradation models and serve as a good planning platform for balancing total costs (operational and maintenance) with dependability of a system. In this work, we apply the FMT formalism to a {Smart Building} application and propose a framework that efficiently encodes the FMT into Continuous Time Markov Chains. This allows us to obtain system dependability metrics such as system reliability and mean time to failure, as well as costs of maintenance and failures over time, for different maintenance policies. We illustrate the pertinence of our approach by evaluating various dependability metrics and maintenance strategies of a Heating, Ventilation and Air-Conditioning system. △ Less

Submitted 22 June, 2018; v1 submitted 13 June, 2018; originally announced June 2018.

Comments: arXiv admin note: substantial text overlap with arXiv:1801.04263

One Net Fits All: A unifying semantics of Dynamic Fault Trees using GSPNs

Authors: Sebastian Junges, Joost-Pieter Katoen, Marielle Stoelinga, Matthias Volk

Abstract: Dynamic Fault Trees (DFTs) are a prominent model in reliability engineering. They are strictly more expressive than static fault trees, but this comes at a price: their interpretation is non-trivial and leaves quite some freedom. This paper presents a GSPN semantics for DFTs. This semantics is rather simple and compositional. The key feature is that this GSPN semantics unifies all existing DFT sem… ▽ More Dynamic Fault Trees (DFTs) are a prominent model in reliability engineering. They are strictly more expressive than static fault trees, but this comes at a price: their interpretation is non-trivial and leaves quite some freedom. This paper presents a GSPN semantics for DFTs. This semantics is rather simple and compositional. The key feature is that this GSPN semantics unifies all existing DFT semantics from the literature. All semantic variants can be obtained by choosing appropriate priorities and treatment of non-determinism. △ Less

Submitted 14 March, 2018; originally announced March 2018.

Comments: Accepted at Petri Nets 2018

Efficient Probabilistic Model Checking of Smart Building Maintenance using Fault Maintenance Trees

Authors: Nathalie Cauchi, Khaza Anuarul Hoque, Alessandro Abate, Marielle Stoelinga

Abstract: Cyber-physical systems, like Smart Buildings and power plants, have to meet high standards, both in terms of reliability and availability. Such metrics are typically evaluated using Fault trees (FTs) and do not consider maintenance strategies which can significantly improve lifespan and reliability. Fault Maintenance trees (FMTs) -- an extension of FTs that also incorporate maintenance and degrada… ▽ More Cyber-physical systems, like Smart Buildings and power plants, have to meet high standards, both in terms of reliability and availability. Such metrics are typically evaluated using Fault trees (FTs) and do not consider maintenance strategies which can significantly improve lifespan and reliability. Fault Maintenance trees (FMTs) -- an extension of FTs that also incorporate maintenance and degradation models, are a novel technique that serve as a good planning platform for balancing total costs and dependability of a system. In this work, we apply the FMT formalism to a Smart Building application. We propose a framework for modelling FMTs using probabilistic model checking and present an algorithm for performing abstraction of the FMT in order to reduce the size of its equivalent Continuous Time Markov Chain. This allows us to apply the probabilistic model checking more efficiently. We demonstrate the applicability of our proposed approach by evaluating various dependability metrics and maintenance strategies of a Heating, Ventilation and Air-Conditioning system's FMT. △ Less

Submitted 12 January, 2018; originally announced January 2018.

Comments: conference

Modeling and Verification of the Bitcoin Protocol

Authors: Kaylash Chaudhary, Ansgar Fehnker, Jaco van de Pol, Marielle Stoelinga

Abstract: Bitcoin is a popular digital currency for online payments, realized as a decentralized peer-to-peer electronic cash system. Bitcoin keeps a ledger of all transactions; the majority of the participants decides on the correct ledger. Since there is no trusted third party to guard against double spending, and inspired by its popularity, we would like to investigate the correctness of the Bitcoin prot… ▽ More Bitcoin is a popular digital currency for online payments, realized as a decentralized peer-to-peer electronic cash system. Bitcoin keeps a ledger of all transactions; the majority of the participants decides on the correct ledger. Since there is no trusted third party to guard against double spending, and inspired by its popularity, we would like to investigate the correctness of the Bitcoin protocol. Double spending is an important threat to electronic payment systems. Double spending would happen if one user could force a majority to believe that a ledger without his previous payment is the correct one. We are interested in the probability of success of such a double spending attack, which is linked to the computational power of the attacker. This paper examines the Bitcoin protocol and provides its formalization as an UPPAAL model. The model will be used to show how double spending can be done if the parties in the Bitcoin protocol behave maliciously, and with what probability double spending occurs. △ Less

Submitted 13 November, 2015; originally announced November 2015.

Comments: In Proceedings MARS 2015, arXiv:1511.02528

Journal ref: EPTCS 196, 2015, pp. 46-60

Time Dependent Analysis with Dynamic Counter Measure Trees

Authors: Rajesh Kumar, Dennis Guck, Marielle Stoelinga

Abstract: The success of a security attack crucially depends on time: the more time available to the attacker, the higher the probability of a successful attack. Formalisms such as Reliability block diagrams, Reliability graphs and Attack Countermeasure trees provide quantitative information about attack scenarios, but they are provably insufficient to model dependent actions which involve costs, skills, an… ▽ More The success of a security attack crucially depends on time: the more time available to the attacker, the higher the probability of a successful attack. Formalisms such as Reliability block diagrams, Reliability graphs and Attack Countermeasure trees provide quantitative information about attack scenarios, but they are provably insufficient to model dependent actions which involve costs, skills, and time. In this presentation, we extend the Attack Countermeasure trees with a notion of time; inspired by the fact that there is a strong correlation between the amount of resources in which the attacker invests (in this case time) and probability that an attacker succeeds. This allows for an effective selection of countermeasures and rank them according to their resource consumption in terms of costs/skills of installing them and effectiveness in preventing an attack △ Less

Submitted 30 September, 2015; originally announced October 2015.

Comments: 5 pages, 2 Figures, Workshop paper(QAPL 2015)-Extended abstract

Ioco Theory for Probabilistic Automata

Authors: Marcus Gerhold, Mariëlle Stoelinga

Abstract: Model-based testing (MBT) is a well-known technology, which allows for automatic test case generation, execution and evaluation. To test non-functional properties, a number of test MBT frameworks have been developed to test systems with real-time, continuous behaviour, symbolic data and quantitative system aspects. Notably, a lot of these frameworks are based on Tretmans' classical input/output co… ▽ More Model-based testing (MBT) is a well-known technology, which allows for automatic test case generation, execution and evaluation. To test non-functional properties, a number of test MBT frameworks have been developed to test systems with real-time, continuous behaviour, symbolic data and quantitative system aspects. Notably, a lot of these frameworks are based on Tretmans' classical input/output conformance (ioco) framework. However, a model-based test theory handling probabilistic behaviour does not exist yet. Probability plays a role in many different systems: unreliable communication channels, randomized algorithms and communication protocols, service level agreements pinning down up-time percentages, etc. Therefore, a probabilistic test theory is of great practical importance. We present the ingredients for a probabilistic variant of ioco and define the πoco relation, show that it conservatively extends ioco and define the concepts of test case, execution and evaluation. △ Less

Submitted 9 April, 2015; originally announced April 2015.

Comments: In Proceedings MBT 2015, arXiv:1504.01928

Journal ref: EPTCS 180, 2015, pp. 23-40

Talking quiescence: a rigorous theory that supports parallel composition, action hiding and determinisation

Authors: Gerjan Stokkink, Mark Timmer, Mariëlle Stoelinga

Abstract: The notion of quiescence - the absence of outputs - is vital in both behavioural modelling and testing theory. Although the need for quiescence was already recognised in the 90s, it has only been treated as a second-class citizen thus far. This paper moves quiescence into the foreground and introduces the notion of quiescent transition systems (QTSs): an extension of regular input-output transitio… ▽ More The notion of quiescence - the absence of outputs - is vital in both behavioural modelling and testing theory. Although the need for quiescence was already recognised in the 90s, it has only been treated as a second-class citizen thus far. This paper moves quiescence into the foreground and introduces the notion of quiescent transition systems (QTSs): an extension of regular input-output transition systems (IOTSs) in which quiescence is represented explicitly, via quiescent transitions. Four carefully crafted rules on the use of quiescent transitions ensure that our QTSs naturally capture quiescent behaviour. We present the building blocks for a comprehensive theory on QTSs supporting parallel composition, action hiding and determinisation. In particular, we prove that these operations preserve all the aforementioned rules. Additionally, we provide a way to transform existing IOTSs into QTSs, allowing even IOTSs as input that already contain some quiescent transitions. As an important application, we show how our QTS framework simplifies the fundamental model-based testing theory formalised around ioco. △ Less

Submitted 28 February, 2012; originally announced February 2012.

Comments: In Proceedings MBT 2012, arXiv:1202.5826

Journal ref: EPTCS 80, 2012, pp. 73-87

Confluence Reduction for Probabilistic Systems (extended version)

Authors: Mark Timmer, Mariëlle Stoelinga, Jaco van de Pol

Abstract: This paper presents a novel technique for state space reduction of probabilistic specifications, based on a newly developed notion of confluence for probabilistic automata. We prove that this reduction preserves branching probabilistic bisimulation and can be applied on-the-fly. To support the technique, we introduce a method for detecting confluent transitions in the context of a probabilistic pr… ▽ More This paper presents a novel technique for state space reduction of probabilistic specifications, based on a newly developed notion of confluence for probabilistic automata. We prove that this reduction preserves branching probabilistic bisimulation and can be applied on-the-fly. To support the technique, we introduce a method for detecting confluent transitions in the context of a probabilistic process algebra with data, facilitated by an earlier defined linear format. A case study demonstrates that significant reductions can be obtained. △ Less

Submitted 10 November, 2010; originally announced November 2010.

Game Refinement Relations and Metrics

Authors: Luca de Alfaro, Rupak Majumdar, Vishwanath Raman, Mariëlle Stoelinga

Abstract: We consider two-player games played over finite state spaces for an infinite number of rounds. At each state, the players simultaneously choose moves; the moves determine a successor state. It is often advantageous for players to choose probability distributions over moves, rather than single moves. Given a goal, for example, reach a target state, the question of winning is thus a probabilistic… ▽ More We consider two-player games played over finite state spaces for an infinite number of rounds. At each state, the players simultaneously choose moves; the moves determine a successor state. It is often advantageous for players to choose probability distributions over moves, rather than single moves. Given a goal, for example, reach a target state, the question of winning is thus a probabilistic one: what is the maximal probability of winning from a given state? On these game structures, two fundamental notions are those of equivalences and metrics. Given a set of winning conditions, two states are equivalent if the players can win the same games with the same probability from both states. Metrics provide a bound on the difference in the probabilities of winning across states, capturing a quantitative notion of state similarity. We introduce equivalences and metrics for two-player game structures, and we show that they characterize the difference in probability of winning games whose goals are expressed in the quantitative mu-calculus. The quantitative mu-calculus can express a large set of goals, including reachability, safety, and omega-regular properties. Thus, we claim that our relations and metrics provide the canonical extensions to games, of the classical notion of bisimulation for transition systems. We develop our results both for equivalences and metrics, which generalize bisimulation, and for asymmetrical versions, which generalize simulation. △ Less

Submitted 10 September, 2008; v1 submitted 30 June, 2008; originally announced June 2008.

ACM Class: F.4.1; F.1.1

Journal ref: Logical Methods in Computer Science, Volume 4, Issue 3 (September 11, 2008) lmcs:781