56 citations · 87 across the 18 of their papers we have counts for
20 papers
Effective Stochastic Automata Model Checking by Interval Abstraction (extended version)
Pedro R. D'Argenio, Arnd Hartmanns, Annabell Petri
Stochastic automata (SA) are a formal stochastic continuous-time model based on countdown timers whose expiration times follow general probability distributions. SA are particularl…
Multi-Objective Statistical Model Checking using Lightweight Strategy Sampling (extended version)
Pedro R. D'Argenio, Arnd Hartmanns, Patrick Wienhöft +1
Statistical model checking delivers quantitative verification results with statistical guarantees. It scales to model sizes and model types that are out of reach for exhaustive, an…
Digging for Decision Trees: A Case Study in Strategy Sampling and Learning
Carlos E. Budde, Pedro R. D'Argenio, Arnd Hartmanns
We introduce a formal model of transportation in an open-pit mine for the purpose of optimising the mine's operations. The model is a network of Markov automata (MA); the optimisat…
Quantifying Masking Fault-Tolerance via Fair Stochastic Games
Pablo F. Castro, Pedro R. D'Argenio, Ramiro Demasi +1
We introduce a formal notion of masking fault-tolerance between probabilistic transition systems using stochastic games. These games are inspired in bisimulation games, but they al…
A Stochastic Game Approach to Masking Fault-Tolerance: Bisimulation and Quantification
Pablo F. Castro, Pedro D'Argenio, Luciano Putruele +1
We introduce a formal notion of masking fault-tolerance between probabilistic transition systems based on a variant of probabilistic bisimulation (named masking simulation). We als…
Playing Against Fair Adversaries in Stochastic Games with Total Rewards
Pablo F. Castro, Pedro R. D'Argenio, Luciano Putruele +1
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 aim…
Routing in Delay-Tolerant Networks under Uncertain Contact Plans
Fernando D. Raverta, Juan A. Fraire, Pablo G. Madoery +3
Delay-Tolerant Networks (DTN) enable store-carry-and-forward data transmission in networks challenged by frequent disruptions and high latency. Existing classification distinguishe…
Rare Event Simulation for non-Markovian repairable Fault Trees
Carlos E. Budde, Marco Biagi, Raúl E. Monti +2
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…
A compositional semantics for Repairable Fault Trees with general distributions
Raul E. Monti, Pedro R. D'Argenio, Carlos E. Budde
Fault Tree Analysis (FTA) is a prominent technique in industrial and scientific risk assessment. Repairable Fault Trees (RFT) enhance the classical Fault Tree (FT) model by introdu…
Doping Tests for Cyber-Physical Systems
Sebastian Biewer, Pedro D'Argenio, Holger Hermanns
The software running in embedded or cyber-physical systems (CPS) is typically of proprietary nature, so users do not know precisely what the systems they own are (in)capable of doi…
Measuring Masking Fault-Tolerance
Pablo F. Castro, Pedro R. D'Argenio, Ramiro Demasi +1
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 exhi…
Input/Output Stochastic Automata with Urgency: Confluence and weak determinism
Pedro R. D'Argenio, Raúl E. Monti
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 auto…
Facets of Software Doping
Gilles Barthe, Pedro R. D'Argenio, Bernd Finkbeiner +1
This paper provides an informal discussion of the formal aspects of software doping.
A Hierarchy of Scheduler Classes for Stochastic Automata
Pedro R. D'Argenio, Marcus Gerhold, Arnd Hartmanns +1
Stochastic automata are a formal compositional model for concurrent stochastic timed systems, with general distributions and non-deterministic choices. Measures of interest are def…
Is your software on dope? Formal analysis of surreptitiously "enhanced" programs
Pedro R. D'Argenio, Gilles Barthe, Sebastian Biewer +2
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…
SOS rule formats for convex and abstract probabilistic bisimulations
Pedro R. D'Argenio, Matias David Lee, Daniel Gebler
Probabilistic transition system specifications (PTSSs) in the format provide structural operational semantics for Segala-type systems that exhibit both probabilisti…
Smart Sampling for Lightweight Verification of Markov Decision Processes
Pedro D'Argenio, Axel Legay, Sean Sedwards +1
Markov decision processes (MDP) are useful to model optimisation problems in concurrent systems. To verify MDPs with efficient Monte Carlo techniques requires that their nondetermi…
Tree rules in probabilistic transition system specifications with negative and quantitative premises
Matias David Lee, Daniel Gebler, Pedro R. D'Argenio
Probabilistic transition system specifications (PTSSs) in the ntmufnu/ntmuxnu format provide structural operational semantics for Segala-type systems that exhibit both probabilisti…
Bisimulations for Nondeterministic Labeled Markov Processes
Pedro D'Argenio, Pedro Sánchez Terraf, Nicolás Wolovick
We extend the theory of labeled Markov processes with internal nondeterminism, a fundamental concept for the further development of a process theory with abstraction on nondetermin…
Significant Diagnostic Counterexamples in Probabilistic Model Checking
Miguel E. Andres, Pedro D'Argenio, Peter van Rossum
This paper presents a novel technique for counterexample generation in probabilistic model checking of Markov Chains and Markov Decision Processes. (Finite) paths in counterexample…