-
Chapter and Conference Paper
Optimal Route Synthesis in Space DTN Using Markov Decision Processes
Delay-tolerant networks (DTN) are time evolving networks which do not provide continuous and instantaneous end-to-end communication [5, 9]. Instead, the topological configuration of DTN changes continuously: conn...
-
Article
Open AccessAnalysis of non-Markovian repairable fault trees through rare event simulation
Dynamic fault trees (DFTs) 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 analy...
-
Chapter and Conference Paper
MaskD: A Tool for Measuring Masking Fault-Tolerance
We present MaskD, an automated tool designed to measure the level of fault-tolerance provided by software components. The tool focuses on measuring masking fault-tolerance, that is, the kind of fault-tolerance th...
-
Chapter and Conference Paper
Playing Against Fair Adversaries in Stochastic Games with Total Rewards
We investigate zero-sum turn-based two-player stochastic games in which the objective of one player is to maximize the amount of rewards obtained during a play, while the other aims at minimizing it. We focus ...
-
Chapter and Conference Paper
Comparing Statistical and Analytical Routing Approaches for Delay-Tolerant Networks
In delay-tolerant networks (DTNs) with uncertain contact plans, the communication episodes and their reliabilities are known a priori. To maximize the end-to-end delivery probability, a bounded network-wide nu...
-
Article
Open AccessAn efficient statistical model checker for nondeterminism and rare events
Statistical model checking avoids the state space explosion problem in verification and naturally supports complex non-Markovian formalisms. Yet as a simulation-based approach, its runtime becomes excessive in...
-
Article
On the probabilistic bisimulation spectrum with silent moves
In this paper we look at one of the seminal works of Rob van Glabbeek from a probabilistic angle. We develop the bisimulation spectrum with silent moves for probabilistic models, namely Markov decision process...
-
Chapter and Conference Paper
Sampling Distributed Schedulers for Resilient Space Communication
We consider routing in delay-tolerant networks like satellite constellations with known but intermittent contacts, random message loss, and resource-constrained nodes. Using a Markov decision process model, we...
-
Chapter and Conference Paper
Rare Event Simulation for Non-Markovian Repairable Fault Trees
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 analys...
-
Chapter and Conference Paper
Measuring Masking Fault-Tolerance
In this paper we introduce a notion of fault-tolerance distance between labeled transition systems. Intuitively, this notion of distance measures the degree of fault-tolerance exhibited by a candidate system. ...
-
Chapter and Conference Paper
A Hierarchy of Scheduler Classes for Stochastic Automata
Stochastic automata are a formal compositional model for concurrent stochastic timed systems, with general distributions and nondeterministic choices. Measures of interest are defined over schedulers that resolve...
-
Chapter and Conference Paper
Input/Output Stochastic Automata with Urgency: Confluence and Weak Determinism
In a previous work, we introduced an input/output variant of stochastic automata (IOSA) that, once the model is closed (i.e., all synchronizations are resolved), the resulting automaton is fully stochastic, th...
-
Chapter and Conference Paper
A Statistical Model Checker for Nondeterminism and Rare Events
Statistical model checking avoids the state space explosion problem in verification and naturally supports complex non-Markovian formalisms. Yet as a simulation-based approach, its runtime becomes excessive in...
-
Chapter and Conference Paper
Lightweight Statistical Model Checking in Nondeterministic Continuous Time
Lightweight scheduler sampling brings statistical model checking to nondeterministic formalisms with undiscounted properties, in constant memory. Its direct application to continuous-time models is rendered in...
-
Chapter and Conference Paper
Is Your Software on Dope?
Usually, it is the software manufacturer who employs verification or testing to ensure that the software embedded in a device meets its main objectives. However, these days we are confronted with the situation...
-
Chapter
The Road from Stochastic Automata to the Simulation of Rare Events
We report in the advances on stochastic automata and its use on rare event simulation. We review and introduce an extension of IOSA, an input/output variant of stochastic automata that under mild constraints c...
-
Chapter and Conference Paper
Better Automated Importance Splitting for Transient Rare Events
Statistical model checking uses simulation to overcome the state space explosion problem in formal verification. Yet its runtime explodes when faced with rare events, unless a rare event simulation method like...
-
Chapter and Conference Paper
Facets of Software Do**
This paper provides an informal discussion of the formal aspects of software do**.
-
Chapter and Conference Paper
Input/Output Stochastic Automata
Stochastic automata provide a way to symbolically model systems in which the occurrence time of events may respond to any continuous random variable. We introduce here an input/output variant of stochastic aut...
-
Chapter and Conference Paper
Statistical Approximation of Optimal Schedulers for Probabilistic Timed Automata
The verification of probabilistic timed automata involves finding schedulers that optimise their nondeterministic choices with respect to the probability of a property. In practice, approaches based on model c...
