research-article

Verifying the long-run behavior of probabilistic system models in the presence of uncertainty

Authors:

Yamilet R. Serrano Llerena,

David S. RosenblumAuthors Info & Claims

ESEC/FSE 2018: Proceedings of the 2018 26th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering

Pages 587 - 597

https://doi.org/10.1145/3236024.3236078

Published: 26 October 2018 Publication History

Abstract

Verifying that a stochastic system is in a certain state when it has reached equilibrium has important applications. For instance, the probabilistic verification of the long-run behavior of a safety-critical system enables assessors to check whether it accepts a human abort-command at any time with a probability that is sufficiently high. The stochastic system is represented as probabilistic model, a long-run property is asserted and a probabilistic verifier checks the model against the property.

However, existing probabilistic verifiers do not account for the imprecision of the probabilistic parameters in the model. Due to uncertainty, the probability of any state transition may be subject to small perturbations which can have direct consequences for the veracity of the verification result. In reality, the safety-critical system may accept the abort-command with an insufficient probability.

In this paper, we introduce the first probabilistic verification technique that accounts for uncertainty on the verification of long-run properties of a stochastic system. We present a mathematical framework for the asymptotic analysis of the stationary distribution of a discrete-time Markov chain, making no assumptions about the distribution of the perturbations. Concretely, our novel technique computes upper and lower bounds on the long-run probability, given a certain degree of uncertainty about the stochastic system.

References

[1]

Dean Michael Berris, Alistair Veitch, Nevin Heintze, Eric Anderson, and Ning Wang. 2016.

[2]

XRay: A Function Call Tracing System. Technical Report. A white paper on XRay, a function call tracing system developed at Google.

[3]

Igor V Cadez, David Heckerman, Christopher Meek, Padhraic Smyth, and Steven White. 2000. Visualization of navigation patterns on a Web site using model-based clustering. In KDD. 280.

Digital Library

[4]

Grace E. Cho and Carl D. Meyer. 2000.

[5]

Markov Chain Sensitivity Measured by Mean First Passage Times. Linear Algebra Appl. 316, 1 (2000), 21–28.

[6]

Grace E. Cho and Carl D. Meyer. 2001. Comparison of Perturbation Bounds for the Stationary Distribution of a Markov Chain. Linear Algebra Appl. 335, 1 (2001), 137–150.

[7]

Nicolas Coste. 2010.

[8]

Towards Performance Prediction of Compositional Models in GALS Designs. Ph.D. Dissertation. University of Grenoble.

[9]

Altman E., Avrachenkov K., and Núñez Queija R. 2004. Perturbation Analysis for Denumerable Markov Chains with Application to Queueing Models. Advances in Applied Probability 36 (2004), 839–853.

[10]

Seneta E. 1988. Perturbation of the Stationary Distribution Measured by Ergodicity Coefficients. Advances in Applied Probability 20, 1 (1988), 228–230.

[11]

Ernst Moritz Hahn, Holger Hermanns, and Lijun Zhang. 2009.

[12]

Probabilistic Reachability for Parametric Markov Models. In SPIN. 88–106.

Digital Library

[13]

Moshe Haviv and Ludo Van Der Heyden. 1984.

[14]

Perturbation Bounds for the Stationary Probabilities of a Finite Markov Chain. Advances in Applied Probability 16, 4 (1984), 804–818. http://www.jstor.org/stable/1427341

[15]

David Heckerman. 1999. MSNBC.com Anonymous Web Data Set. http://archive. ics.uci.edu/ml/datasets/msnbc.com+anonymous+web+data. (1999).

[16]

Accessed: 2018-02-05.

[17]

Kemeny J. and Snell J. 1960.

[18]

Finite Markov Chains. D. Van Nostrand, New York.

[19]

Schweitzer Paul J. 1968. Perturbation Theory and Finite Markov Chains. Journal of Applied Probability 5, 2 (1968), 401–413.

[20]

Stephen Kirkland, Michael Neumann, and Bryan Shader. 1998. Applications of Paz’s Inequality to Perturbation Bounds for Markov Chains. Linear Algebra Appl. 268, 1 (1998), 183–196.

[21]

Marta Z. Kwiatkowska, Gethin Norman, and David Parker. 2005. Probabilistic Model Checking in Practice: Case Studies with PRISM. SIGMETRICS Performance Evaluation Review 32, 4 (2005), 16–21.

Digital Library

[22]

Ruggero Lanotte, Andrea Maggiolo-Schettini, and Angelo Troina. 2007. Parametric Probabilistic Transition Systems for System Design and Analysis. Formal Asp. Comput. 19, 1 (2007), 93–109.

Digital Library

[23]

Yamilet R. Serrano Llerena, Guoxin Su, and David S. Rosenblum. 2017. Probabilistic Model Checking of Perturbed MDPs with Applications to Cloud Computing. In Proceedings of the 2017 11th Joint Meeting on Foundations of Software Engineering, ESEC/FSE 2017, Paderborn, Germany, September 4-8, 2017. 454–464.

Digital Library

[24]

Alan L. Montgomery, Shibo Li, Kannan Srinivasan, and John C. Liechty. 2004.

[25]

Modeling Online Browsing and Path Analysis Using Clickstream Data. Marketing Science 23, 4 (2004), 579–595.

[26]

Nicolas Privault. 2013.

[27]

Understanding Markov Chains: Examples and Applications. Springer Singapore.

[28]

Guoxin Su, Taolue Chen, Yuan Feng, and David S. Rosenblum. 2017.

[29]

ProEva: Runtime Proactive Performance Evaluation Based on Continuous-Time Markov Chains. In Proceedings of the 39th International Conference on Software Engineering, ICSE 2017, Buenos Aires, Argentina, May 20-28, 2017. 484–495. http://dl.acm.org/ citation.cfm?id=3097426

Digital Library

[30]

G. Su, Y. Feng, T. Chen, and D. S. Rosenblum. 2016.

[31]

Asymptotic Perturbation Bounds for Probabilistic Model Checking with Empirically Determined Probability Parameters. IEEE Transactions on Software Engineering 42, 7 (July 2016), 623–639.

Digital Library

[32]

Guoxin Su and David S. Rosenblum. 2013. Asymptotic Bounds for Quantitative Verification of Perturbed Probabilistic Systems. In ICFEM. 297–312.

Cited By

Xia CDutta SMisailovic SMarinov DZhang L(2023)Balancing Effectiveness and Flakiness of Non-Deterministic Machine Learning Tests2023 IEEE/ACM 45th International Conference on Software Engineering (ICSE)10.1109/ICSE48619.2023.00154(1801-1813)Online publication date: May-2023
https://doi.org/10.1109/ICSE48619.2023.00154
Dutta SArunachalam AMisailovic S(2022)To Seed or Not to Seed? An Empirical Analysis of Usage of Seeds for Testing in Machine Learning Projects2022 IEEE Conference on Software Testing, Verification and Validation (ICST)10.1109/ICST53961.2022.00026(151-161)Online publication date: Apr-2022
https://doi.org/10.1109/ICST53961.2022.00026
Alasmari NCalinescu RPaterson CMirandola R(2022)Quantitative verification with adaptive uncertainty reductionJournal of Systems and Software10.1016/j.jss.2022.111275188(111275)Online publication date: Jun-2022
https://doi.org/10.1016/j.jss.2022.111275
Show More Cited By

Index Terms

Verifying the long-run behavior of probabilistic system models in the presence of uncertainty
1. Mathematics of computing
  1. Probability and statistics
    1. Probabilistic representations
      1. Markov networks
2. Software and its engineering
  1. Software organization and properties
    1. Software functional properties
      1. Formal methods
        Model checking
        Software verification

Recommendations

Probabilistic model checking of perturbed MDPs with applications to cloud computing
ESEC/FSE 2017: Proceedings of the 2017 11th Joint Meeting on Foundations of Software Engineering

Probabilistic model checking is a formal verification technique that has been applied successfully in a variety of domains, providing identification of system errors through quantitative verification of stochastic system models. One domain that can ...
Dealing with uncertainty in verification of nondeterministic systems
FSE 2014: Proceedings of the 22nd ACM SIGSOFT International Symposium on Foundations of Software Engineering

Uncertainty complicates the formal verification of nondeterministic systems. Unpredictable changes and alterations in their environments can lead an invalid verification results and the decrease of confidence degree of these systems. However, current ...
DTMC Model Checking by SCC Reduction
QEST '10: Proceedings of the 2010 Seventh International Conference on the Quantitative Evaluation of Systems

Discrete-Time Markov Chains (DTMCs) are a widely-used formalism to model probabilistic systems. On the one hand, available tools like PRISM or MRMC offer efficient model checking algorithms and thus support the verification of DTMCs. However, these ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

ESEC/FSE 2018: Proceedings of the 2018 26th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering

October 2018

987 pages

ISBN:9781450355735

DOI:10.1145/3236024

General Chair:
Gary T. Leavens
University of Central Florida, USA
,
Program Chairs:
Alessandro Garcia
PUC-Rio, Brazil
,
Corina S. Păsăreanu
NASA Ames Research Center, USA

Copyright © 2018 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Sponsors

SIGSOFT: ACM Special Interest Group on Software Engineering

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 26 October 2018

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Conference

ESEC/FSE '18

Sponsor:

SIGSOFT

ESEC/FSE '18: 26th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering

November 4 - 9, 2018

FL, Lake Buena Vista, USA

Acceptance Rates

Overall Acceptance Rate 112 of 543 submissions, 21%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

4
Total Citations
View Citations
208
Total Downloads

Downloads (Last 12 months)10
Downloads (Last 6 weeks)0

Reflects downloads up to 25 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Xia CDutta SMisailovic SMarinov DZhang L(2023)Balancing Effectiveness and Flakiness of Non-Deterministic Machine Learning Tests2023 IEEE/ACM 45th International Conference on Software Engineering (ICSE)10.1109/ICSE48619.2023.00154(1801-1813)Online publication date: May-2023
https://doi.org/10.1109/ICSE48619.2023.00154
Dutta SArunachalam AMisailovic S(2022)To Seed or Not to Seed? An Empirical Analysis of Usage of Seeds for Testing in Machine Learning Projects2022 IEEE Conference on Software Testing, Verification and Validation (ICST)10.1109/ICST53961.2022.00026(151-161)Online publication date: Apr-2022
https://doi.org/10.1109/ICST53961.2022.00026
Alasmari NCalinescu RPaterson CMirandola R(2022)Quantitative verification with adaptive uncertainty reductionJournal of Systems and Software10.1016/j.jss.2022.111275188(111275)Online publication date: Jun-2022
https://doi.org/10.1016/j.jss.2022.111275
Badings TCubuktepe MJansen NJunges SKatoen JTopcu U(2022)Scenario-based verification of uncertain parametric MDPsInternational Journal on Software Tools for Technology Transfer10.1007/s10009-022-00673-z24:5(803-819)Online publication date: 14-Sep-2022
https://doi.org/10.1007/s10009-022-00673-z

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Table of Contents