Showing 1–20 of 20 results for author: D'Argenio, P

Polytopal Stochastic Games

Authors: Pablo F. Castro, Pedro D'Argenio

Abstract: In this paper we introduce polytopal stochastic games, an extension of two-player, zero-sum, turn-based stochastic games, in which we may have uncertainty over the transition probabilities. In these games the uncertainty over the probabilities distributions is captured via linear (in)equalities whose space of solutions forms a polytope. We give a formal definition of these games and prove their ba… ▽ More In this paper we introduce polytopal stochastic games, an extension of two-player, zero-sum, turn-based stochastic games, in which we may have uncertainty over the transition probabilities. In these games the uncertainty over the probabilities distributions is captured via linear (in)equalities whose space of solutions forms a polytope. We give a formal definition of these games and prove their basic properties: determinacy and existence of optimal memoryless and deterministic strategies. We do this for reachability and different types of reward objectives and show that the solution exists in a finite representation of the game. We also state that the corresponding decision problems are in the intersection of NP and coNP. We motivate the use of polytopal stochastic games via a simple example. Finally, we report some experiments we performed with a prototype tool. △ Less

Submitted 25 February, 2025; v1 submitted 22 February, 2025; originally announced February 2025.

Digging for Decision Trees: A Case Study in Strategy Sampling and Learning

Authors: Carlos E. Budde, Pedro R. D'Argenio, Arnd Hartmanns

Abstract: 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 optimisation goal corresponds to maximising a time-bounded expected reward property. Today's model checking algorithms exacerbate the state space explosion problem by applying a discretisation approach to such properties on MA. W… ▽ More 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 optimisation goal corresponds to maximising a time-bounded expected reward property. Today's model checking algorithms exacerbate the state space explosion problem by applying a discretisation approach to such properties on MA. We show that model checking is infeasible even for small mine instances. Instead, we propose statistical model checking with lightweight strategy sampling or table-based Q-learning over untimed strategies as an alternative to approach the optimisation task, using the Modest Toolset's modes tool. We add support for partial observability to modes so that strategies can be based on carefully selected model features, and we implement a connection from modes to the dtControl tool to convert sampled or learned strategies into decision trees. We experimentally evaluate the adequacy of our new tooling on the open-pit mine case study. Our experiments demonstrate the limitations of Q-learning, the impact of feature selection, and the usefulness of decision trees as an explainable representation. △ Less

Submitted 6 December, 2024; originally announced December 2024.

ACM Class: F.4.3; I.6.5; I.6.8

Quantifying Masking Fault-Tolerance via Fair Stochastic Games

Authors: Pablo F. Castro, Pedro R. D'Argenio, Ramiro Demasi, Luciano Putruele

Abstract: 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 also take into account the possible faulty behavior of systems. When no faults are present, these games boil down to probabilistic bisimulation games. Since these games could be infinite, we propose a symbolic way of repre… ▽ More 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 also take into account the possible faulty behavior of systems. When no faults are present, these games boil down to probabilistic bisimulation games. Since these games could be infinite, we propose a symbolic way of representing them so that they can be solved in polynomial time. In particular, we use this notion of masking to quantify the level of masking fault-tolerance exhibited by almost-sure failing systems, i.e., those systems that eventually fail with probability 1. The level of masking fault-tolerance of almost-sure failing systems can be calculated by solving a collection of functional equations. We produce this metric in a setting in which one of the player behaves in a strong fair way (mimicking the idea of fair environments). △ Less

Submitted 13 September, 2023; originally announced September 2023.

Comments: In Proceedings EXPRESS/SOS2023, arXiv:2309.05788. arXiv admin note: substantial text overlap with arXiv:2207.02045

Journal ref: EPTCS 387, 2023, pp. 132-148

A Stochastic Game Approach to Masking Fault-Tolerance: Bisimulation and Quantification

Authors: Pablo F. Castro, Pedro D'Argenio, Luciano Putruele, Ramiro Demasi

Abstract: We introduce a formal notion of masking fault-tolerance between probabilistic transition systems based on a variant of probabilistic bisimulation (named masking simulation). We also provide the corresponding probabilistic game characterization. Even though these games could be infinite, we propose a symbolic way of representing them, such that it can be decided in polynomial time if there is a mas… ▽ More We introduce a formal notion of masking fault-tolerance between probabilistic transition systems based on a variant of probabilistic bisimulation (named masking simulation). We also provide the corresponding probabilistic game characterization. Even though these games could be infinite, we propose a symbolic way of representing them, such that it can be decided in polynomial time if there is a masking simulation between two probabilistic transition systems. We use this notion of masking to quantify the level of masking fault-tolerance exhibited by almost-sure failing systems, i.e., those systems that eventually fail with probability 1. The level of masking fault-tolerance of almost-sure failing systems can be calculated by solving a collection of functional equations. We produce this metric in a setting in which the minimizing player behaves in a strong fair way (mimicking the idea of fair environments), and limit our study to memoryless strategies due to the infinite nature of the game. We implemented these ideas in a prototype tool, and performed an experimental evaluation. △ Less

Submitted 5 July, 2022; originally announced July 2022.

Playing Against Fair Adversaries in Stochastic Games with Total Rewards

Authors: Pablo F. Castro, Pedro R. D'Argenio, Luciano Putruele, Ramiro Demasi

Abstract: 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 on games in which the minimizer plays in a fair way. We believe that these kinds of games enjoy interesting applications in software verification, where the maximizer plays the role of a syst… ▽ More 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 on games in which the minimizer plays in a fair way. We believe that these kinds of games enjoy interesting applications in software verification, where the maximizer plays the role of a system intending to maximize the number of "milestones" achieved, and the minimizer represents the behavior of some uncooperative but yet fair environment. Normally, to study total reward properties, games are requested to be stopping (i.e., they reach a terminal state with probability 1). We relax the property to request that the game is stopping only under a fair minimizing player. We prove that these games are determined, i.e., each state of the game has a value defined. Furthermore, we show that both players have memoryless and deterministic optimal strategies, and the game value can be computed by approximating the greatest-fixed point of a set of functional equations. We implemented our approach in a prototype tool, and evaluated it on an illustrating example and an Unmanned Aerial Vehicle case study. △ Less

Submitted 19 May, 2022; v1 submitted 17 December, 2021; originally announced December 2021.

Routing in Delay-Tolerant Networks under Uncertain Contact Plans

Authors: Fernando D. Raverta, Juan A. Fraire, Pablo G. Madoery, Ramiro A. Demasi, Jorge M. Finochietto, Pedro R. D'Argenio

Abstract: Delay-Tolerant Networks (DTN) enable store-carry-and-forward data transmission in networks challenged by frequent disruptions and high latency. Existing classification distinguishes between scheduled and probabilistic DTNs, for which specific routing solutions have been developed. In this paper, we uncover a gap in-between where uncertain contact plans can be exploited to enhance data delivery in… ▽ More Delay-Tolerant Networks (DTN) enable store-carry-and-forward data transmission in networks challenged by frequent disruptions and high latency. Existing classification distinguishes between scheduled and probabilistic DTNs, for which specific routing solutions have been developed. In this paper, we uncover a gap in-between where uncertain contact plans can be exploited to enhance data delivery in many practical scenarios described by probabilistic schedules available a priori. Routing under uncertain contact plans (RUCoP) is next formulated as a multiple-copy Markov Decision Process and then exported to local-knowledge (L-RUCoP) and Contact Graph Routing extensions (CGR-UCoP) which can be implemented in the existing DTN protocol stack. RUCoP and its derivations are evaluated in a first extensive simulation benchmark for DTNs under uncertain contact plans comprising both random and realistic scenarios. Results confirm that RUCoP and L-RUCoP closely approach the ideal delivery ratio of an oracle, while CGR-UCoP improves state-of-the-art DTN routing schemes delivery ratio up to 25%. △ Less

Submitted 16 August, 2021; originally announced August 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

A compositional semantics for Repairable Fault Trees with general distributions

Authors: Raul E. Monti, Pedro R. D'Argenio, Carlos E. Budde

Abstract: 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 introducing the possibility to describe complex dependent repairs of system components. Usual frameworks for analyzing FTs such as BDD, SBDD, and Markov chains fail to assess the desired properties over RFT complex models, eith… ▽ More 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 introducing the possibility to describe complex dependent repairs of system components. Usual frameworks for analyzing FTs such as BDD, SBDD, and Markov chains fail to assess the desired properties over RFT complex models, either because these become too large, or due to cyclic behaviour introduced by dependent repairs. Simulation is another way to carry out this kind of analysis. In this paper we review the RFT model with Repair Boxes as introduced by Daniele Codetta-Raiteri. We present compositional semantics for this model in terms of Input/Output Stochastic Automata, which allows for the modelling of events occurring according to general continuous distribution. Moreover, we prove that the semantics generates (weakly) deterministic models, hence suitable for discrete event simulation, and prominently for Rare Event Simulation using the FIG tool. △ Less

Submitted 23 October, 2019; originally announced October 2019.

Doping Tests for Cyber-Physical Systems

Authors: Sebastian Biewer, Pedro D'Argenio, Holger Hermanns

Abstract: 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 doing. Most malfunctionings of such systems are not intended by the manufacturer, but some are, which means these cannot be classified as bugs or security loopholes. The most prominent examples have become public in the die… ▽ More 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 doing. Most malfunctionings of such systems are not intended by the manufacturer, but some are, which means these cannot be classified as bugs or security loopholes. The most prominent examples have become public in the diesel emissions scandal, where millions of cars were found to be equipped with software violating the law, altogether polluting the environment and putting human health at risk. The behaviour of the software embedded in these cars was intended by the manufacturer, but it was not in the interest of society, a phenomenon that has been called software doping. Doped software is significantly different from buggy or insecure software and hence it is not possible to use classical verification and testing techniques to discover and mitigate software doping. The work presented in this paper builds on existing definitions of software doping and lays the theoretical foundations for conducting software doping tests, so as to enable attacking evil manufacturers. The complex nature of software doping makes it very hard to effectuate doping tests in practice. We explain the biggest challenges and provide efficient solutions to realise doping tests despite this complexity. △ Less

Submitted 18 April, 2019; originally announced April 2019.

Measuring Masking Fault-Tolerance

Authors: Pablo F. Castro, Pedro R. D'Argenio, Ramiro Demasi, Luciano Putruele

Abstract: 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. In practice, there are different kinds of fault-tolerance, here we restrict ourselves to the analysis of masking fault-tolerance because it is often a highly desirable goal for critical syste… ▽ More 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. In practice, there are different kinds of fault-tolerance, here we restrict ourselves to the analysis of masking fault-tolerance because it is often a highly desirable goal for critical systems. Roughly speaking, a system is masking fault-tolerant when it is able to completely mask the faults, not allowing these faults to have any observable consequences for the users. We capture masking fault-tolerance via a simulation relation, which is accompanied by a corresponding game characterization. We enrich the resulting games with quantitative objectives to define the notion of masking fault-tolerance distance. Furthermore, we investigate the basic properties of this notion of masking distance, and we prove that it is a directed pseudo metric. We have implemented our approach in a prototype tool that automatically compute the masking distance between a nominal system and a fault-tolerant version of it. We have used this tool to measure the masking tolerance of multiple instances of several case studies △ Less

Submitted 20 November, 2018; v1 submitted 13 November, 2018; originally announced November 2018.

Comments: 25 pages including an appendix

Input/Output Stochastic Automata with Urgency: Confluence and weak determinism

Authors: Pedro R. D'Argenio, Raúl E. Monti

Abstract: 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, that is, it does not contain non-deterministic choices. However, such variant is not sufficiently versatile for compositional modelling. In this article, we extend IOSA with urgent actions. Thi… ▽ More 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, that is, it does not contain non-deterministic choices. However, such variant is not sufficiently versatile for compositional modelling. In this article, we extend IOSA with urgent actions. This extension greatly increases the modularization of the models, allowing to take better advantage on compositionality than its predecessor. However, this extension introduces non-determinism even in closed models. We first show that confluent models are weakly deterministic in the sense that, regardless the resolution of the non-determinism, the stochastic behaviour is the same. In addition, we provide sufficient conditions to ensure that a network of interacting IOSAs is confluent without the need to obtain the composed IOSA. △ Less

Submitted 17 August, 2018; v1 submitted 8 August, 2018; originally announced August 2018.

Facets of Software Doping

Authors: Gilles Barthe, Pedro R. D'Argenio, Bernd Finkbeiner, Holger Hermanns

Abstract: This paper provides an informal discussion of the formal aspects of software doping. This paper provides an informal discussion of the formal aspects of software doping. △ Less

Submitted 27 March, 2018; originally announced March 2018.

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

A Hierarchy of Scheduler Classes for Stochastic Automata

Authors: Pedro R. D'Argenio, Marcus Gerhold, Arnd Hartmanns, Sean Sedwards

Abstract: Stochastic automata are a formal compositional model for concurrent stochastic timed systems, with general distributions and non-deterministic choices. Measures of interest are defined over schedulers that resolve the nondeterminism. In this paper we investigate the power of various theoretically and practically motivated classes of schedulers, considering the classic complete-information view and… ▽ More Stochastic automata are a formal compositional model for concurrent stochastic timed systems, with general distributions and non-deterministic choices. Measures of interest are defined over schedulers that resolve the nondeterminism. In this paper we investigate the power of various theoretically and practically motivated classes of schedulers, considering the classic complete-information view and a restriction to non-prophetic schedulers. We prove a hierarchy of scheduler classes w.r.t. unbounded probabilistic reachability. We find that, unlike Markovian formalisms, stochastic automata distinguish most classes even in this basic setting. Verification and strategy synthesis methods thus face a tradeoff between powerful and efficient classes. Using lightweight scheduler sampling, we explore this tradeoff and demonstrate the concept of a useful approximative verification technique for stochastic automata. △ Less

Submitted 16 October, 2017; originally announced October 2017.

Is your software on dope? Formal analysis of surreptitiously "enhanced" programs

Authors: Pedro R. D'Argenio, Gilles Barthe, Sebastian Biewer, Bernd Finkbeiner, Holger Hermanns

Abstract: 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 that economical or technological reasons might make a manufacturer become interested in the software slightly deviating from its main objective for dubious reasons. Examples include lock-in… ▽ More 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 that economical or technological reasons might make a manufacturer become interested in the software slightly deviating from its main objective for dubious reasons. Examples include lock-in strategies and the $\mathrm{NO}_x$ emission scandals in automotive industry. This phenomenon is what we call software doping. It is turning more widespread as software is embedded in ever more devices of daily use. The primary contribution of this article is to provide a hierarchy of simple but solid formal definitions that enable to distinguish whether a program is clean or doped. Moreover, we show that these characterisations provide an immediate framework for analysis by using already existing verification techniques. We exemplify this by applying self-composition on sequential programs and model checking of HyperLTL formulas on reactive models. △ Less

Submitted 15 February, 2017; originally announced February 2017.

Comments: To appear in the proceedings of ESOP 2017

SOS rule formats for convex and abstract probabilistic bisimulations

Authors: Pedro R. D'Argenio, Matias David Lee, Daniel Gebler

Abstract: Probabilistic transition system specifications (PTSSs) in the $nt μfθ/ ntμxθ$ format provide structural operational semantics for Segala-type systems that exhibit both probabilistic and nondeterministic behavior and guarantee that bisimilarity is a congruence for all operator defined in such format. Starting from the $nt μfθ/ ntμxθ$ format, we obtain restricted formats that guarantee that three co… ▽ More Probabilistic transition system specifications (PTSSs) in the $nt μfθ/ ntμxθ$ format provide structural operational semantics for Segala-type systems that exhibit both probabilistic and nondeterministic behavior and guarantee that bisimilarity is a congruence for all operator defined in such format. Starting from the $nt μfθ/ ntμxθ$ format, we obtain restricted formats that guarantee that three coarser bisimulation equivalences are congruences. We focus on (i) Segala's variant of bisimulation that considers combined transitions, which we call here "convex bisimulation"; (ii) the bisimulation equivalence resulting from considering Park & Milner's bisimulation on the usual stripped probabilistic transition system (translated into a labelled transition system), which we call here "probability obliterated bisimulation"; and (iii) a "probability abstracted bisimulation", which, like bisimulation, preserves the structure of the distributions but instead, it ignores the probability values. In addition, we compare these bisimulation equivalences and provide a logic characterization for each of them. △ Less

Submitted 26 August, 2015; originally announced August 2015.

Comments: In Proceedings EXPRESS/SOS 2015, arXiv:1508.06347

Journal ref: EPTCS 190, 2015, pp. 31-45

Smart Sampling for Lightweight Verification of Markov Decision Processes

Authors: Pedro D'Argenio, Axel Legay, Sean Sedwards, Louis-Marie Traonouez

Abstract: Markov decision processes (MDP) are useful to model optimisation problems in concurrent systems. To verify MDPs with efficient Monte Carlo techniques requires that their nondeterminism be resolved by a scheduler. Recent work has introduced the elements of lightweight techniques to sample directly from scheduler space, but finding optimal schedulers by simple sampling may be inefficient. Here we de… ▽ More Markov decision processes (MDP) are useful to model optimisation problems in concurrent systems. To verify MDPs with efficient Monte Carlo techniques requires that their nondeterminism be resolved by a scheduler. Recent work has introduced the elements of lightweight techniques to sample directly from scheduler space, but finding optimal schedulers by simple sampling may be inefficient. Here we describe "smart" sampling algorithms that can make substantial improvements in performance. △ Less

Submitted 4 February, 2015; v1 submitted 7 September, 2014; originally announced September 2014.

Comments: IEEE conference style, 11 pages, 5 algorithms, 11 figures, 1 table

Tree rules in probabilistic transition system specifications with negative and quantitative premises

Authors: Matias David Lee, Daniel Gebler, Pedro R. D'Argenio

Abstract: Probabilistic transition system specifications (PTSSs) in the ntmufnu/ntmuxnu format provide structural operational semantics for Segala-type systems that exhibit both probabilistic and nondeterministic behavior and guarantee that isimilarity is a congruence.Similar to the nondeterministic case of rule format tyft/tyxt, we show that the well-foundedness requirement is unnecessary in the probabilis… ▽ More Probabilistic transition system specifications (PTSSs) in the ntmufnu/ntmuxnu format provide structural operational semantics for Segala-type systems that exhibit both probabilistic and nondeterministic behavior and guarantee that isimilarity is a congruence.Similar to the nondeterministic case of rule format tyft/tyxt, we show that the well-foundedness requirement is unnecessary in the probabilistic setting. To achieve this, we first define an extended version of the ntmufnu/ntmuxnu format in which quantitative premises and conclusions include nested convex combinations of distributions. This format also guarantees that bisimilarity is a congruence. Then, for a given (possibly non-well-founded) PTSS in the new format, we construct an equivalent well-founded transition system consisting of only rules of the simpler (well-founded) probabilistic ntree format. Furthermore, we develop a proof-theoretic notion for these PTSSs that coincides with the existing stratification-based meaning in case the PTSS is stratifiable. This continues the line of research lifting structural operational semantic results from the nondeterministic setting to systems with both probabilistic and nondeterministic behavior. △ Less

Submitted 13 August, 2012; originally announced August 2012.

Comments: In Proceedings EXPRESS/SOS 2012, arXiv:1208.2440

Journal ref: EPTCS 89, 2012, pp. 115-130

Bisimulations for Nondeterministic Labeled Markov Processes

Authors: Pedro D'Argenio, Pedro Sánchez Terraf, Nicolás Wolovick

Abstract: 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 nondeterministic continuous probabilistic systems. We define nondeterministic labeled Markov processes (NLMP) and provide three definition of bisimulations: a bisimulation following a traditional characterization, a state based b… ▽ More 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 nondeterministic continuous probabilistic systems. We define nondeterministic labeled Markov processes (NLMP) and provide three definition of bisimulations: a bisimulation following a traditional characterization, a state based bisimulation tailored to our "measurable" non-determinism, and an event based bisimulation. We show the relation between them, including that the largest state bisimulation is also an event bisimulation. We also introduce a variation of the Hennessy-Milner logic that characterizes event bisimulation and that is sound w.r.t. the other bisimulations for arbitrary NLMP. This logic, however, is infinitary as it contains a denumerable $\lor$. We then introduce a finitary sublogic that characterize all bisimulations for image finite NLMP whose underlying measure space is also analytic. Hence, in this setting, all notions of bisimulation we deal with turn out to be equal. Finally, we show that all notions of bisimulations are different in the general case. The counterexamples that separate them turn to be non-probabilistic NLMP. △ Less

Submitted 15 November, 2010; originally announced November 2010.

MSC Class: 60Jxx ACM Class: G.3; F.4.1

Proceedings First Workshop on Quantitative Formal Methods: Theory and Applications

Authors: Suzana Andova, Annabelle McIver, Pedro D'Argenio, Pieter Cuijpers, Jasen Markovski, Caroll Morgan, Manuel Núñez

Abstract: This volume contains the papers presented at the 1st workshop on Quantitative Formal Methods: Theory and Applications, which was held in Eindhoven on 3 November 2009 as part of the International Symposium on Formal Methods 2009. This volume contains the final versions of all contributions accepted for presentation at the workshop. This volume contains the papers presented at the 1st workshop on Quantitative Formal Methods: Theory and Applications, which was held in Eindhoven on 3 November 2009 as part of the International Symposium on Formal Methods 2009. This volume contains the final versions of all contributions accepted for presentation at the workshop. △ Less

Submitted 10 December, 2009; originally announced December 2009.

ACM Class: D.2.1; D.2.4; D.3.1; F.3.1

Journal ref: EPTCS 13, 2009

Significant Diagnostic Counterexamples in Probabilistic Model Checking

Authors: Miguel E. Andres, Pedro D'Argenio, Peter van Rossum

Abstract: This paper presents a novel technique for counterexample generation in probabilistic model checking of Markov Chains and Markov Decision Processes. (Finite) paths in counterexamples are grouped together in witnesses that are likely to provide similar debugging information to the user. We list five properties that witnesses should satisfy in order to be useful as debugging aid: similarity, accura… ▽ More This paper presents a novel technique for counterexample generation in probabilistic model checking of Markov Chains and Markov Decision Processes. (Finite) paths in counterexamples are grouped together in witnesses that are likely to provide similar debugging information to the user. We list five properties that witnesses should satisfy in order to be useful as debugging aid: similarity, accuracy, originality, significance, and finiteness. Our witnesses contain paths that behave similar outside strongly connected components. This papers shows how to compute these witnesses by reducing the problem of generating counterexamples for general properties over Markov Decision Processes, in several steps, to the easy problem of generating counterexamples for reachability properties over acyclic Markov Chains. △ Less

Submitted 6 June, 2008; originally announced June 2008.

ACM Class: B.8; C.4; D.2.4; G.3