Efficient probabilistic model checking of systems with ranged probabilities

Khalil Ghorbal; Parasara Sridhar Duggirala; Vineet Kahlon; Franjo Ivančić; Aarti Gupta

doi:10.1007/978-3-642-33512-9_10

Efficient probabilistic model checking of systems with ranged probabilities

Khalil Ghorbal, Parasara Sridhar Duggirala, Vineet Kahlon, Franjo Ivančić, Aarti Gupta

Computer Science

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

4 Scopus citations

Abstract

We introduce a new technique to model check reachability properties on Interval Discrete-Time Markov Chains (IDTMC). We compute a sound over-approximation of the probabilities of satisfying a given property where the accuracy is characterized in terms of error bounds. We leverage affine arithmetic to propagate the first-order error terms. Higher-order error terms are bounded using interval arithmetic.

Original language	English (US)
Title of host publication	Reachability Problems - 6th International Workshop, RP 2012, Proceedings
Pages	107-120
Number of pages	14
DOIs	https://doi.org/10.1007/978-3-642-33512-9_10
State	Published - 2012
Event	6th International Workshop on Reachability Problems, RP 2012 - Bordeaux, France Duration: Sep 17 2012 → Sep 19 2012

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	7550 LNCS
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Other

Other	6th International Workshop on Reachability Problems, RP 2012
Country/Territory	France
City	Bordeaux
Period	9/17/12 → 9/19/12

All Science Journal Classification (ASJC) codes

Theoretical Computer Science
General Computer Science

Access to Document

10.1007/978-3-642-33512-9_10

Cite this

Ghorbal, K., Duggirala, P. S., Kahlon, V., Ivančić, F., & Gupta, A. (2012). Efficient probabilistic model checking of systems with ranged probabilities. In Reachability Problems - 6th International Workshop, RP 2012, Proceedings (pp. 107-120). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 7550 LNCS). https://doi.org/10.1007/978-3-642-33512-9_10

Ghorbal, Khalil ; Duggirala, Parasara Sridhar ; Kahlon, Vineet et al. / Efficient probabilistic model checking of systems with ranged probabilities. Reachability Problems - 6th International Workshop, RP 2012, Proceedings. 2012. pp. 107-120 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{509133ef10c94fd586ed29b5315686a4,

title = "Efficient probabilistic model checking of systems with ranged probabilities",

abstract = "We introduce a new technique to model check reachability properties on Interval Discrete-Time Markov Chains (IDTMC). We compute a sound over-approximation of the probabilities of satisfying a given property where the accuracy is characterized in terms of error bounds. We leverage affine arithmetic to propagate the first-order error terms. Higher-order error terms are bounded using interval arithmetic.",

author = "Khalil Ghorbal and Duggirala, {Parasara Sridhar} and Vineet Kahlon and Franjo Ivan{\v c}i{\'c} and Aarti Gupta",

year = "2012",

doi = "10.1007/978-3-642-33512-9_10",

language = "English (US)",

isbn = "9783642335112",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

pages = "107--120",

booktitle = "Reachability Problems - 6th International Workshop, RP 2012, Proceedings",

note = "6th International Workshop on Reachability Problems, RP 2012 ; Conference date: 17-09-2012 Through 19-09-2012",

}

Ghorbal, K, Duggirala, PS, Kahlon, V, Ivančić, F & Gupta, A 2012, Efficient probabilistic model checking of systems with ranged probabilities. in Reachability Problems - 6th International Workshop, RP 2012, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 7550 LNCS, pp. 107-120, 6th International Workshop on Reachability Problems, RP 2012, Bordeaux, France, 9/17/12. https://doi.org/10.1007/978-3-642-33512-9_10

Efficient probabilistic model checking of systems with ranged probabilities. / Ghorbal, Khalil; Duggirala, Parasara Sridhar; Kahlon, Vineet et al.
Reachability Problems - 6th International Workshop, RP 2012, Proceedings. 2012. p. 107-120 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 7550 LNCS).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

TY - GEN

T1 - Efficient probabilistic model checking of systems with ranged probabilities

AU - Ghorbal, Khalil

AU - Duggirala, Parasara Sridhar

AU - Kahlon, Vineet

AU - Ivančić, Franjo

AU - Gupta, Aarti

PY - 2012

Y1 - 2012

N2 - We introduce a new technique to model check reachability properties on Interval Discrete-Time Markov Chains (IDTMC). We compute a sound over-approximation of the probabilities of satisfying a given property where the accuracy is characterized in terms of error bounds. We leverage affine arithmetic to propagate the first-order error terms. Higher-order error terms are bounded using interval arithmetic.

AB - We introduce a new technique to model check reachability properties on Interval Discrete-Time Markov Chains (IDTMC). We compute a sound over-approximation of the probabilities of satisfying a given property where the accuracy is characterized in terms of error bounds. We leverage affine arithmetic to propagate the first-order error terms. Higher-order error terms are bounded using interval arithmetic.

UR - http://www.scopus.com/inward/record.url?scp=84866719547&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=84866719547&partnerID=8YFLogxK

U2 - 10.1007/978-3-642-33512-9_10

DO - 10.1007/978-3-642-33512-9_10

M3 - Conference contribution

AN - SCOPUS:84866719547

SN - 9783642335112

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 107

EP - 120

BT - Reachability Problems - 6th International Workshop, RP 2012, Proceedings

T2 - 6th International Workshop on Reachability Problems, RP 2012

Y2 - 17 September 2012 through 19 September 2012

ER -

Ghorbal K, Duggirala PS, Kahlon V, Ivančić F, Gupta A. Efficient probabilistic model checking of systems with ranged probabilities. In Reachability Problems - 6th International Workshop, RP 2012, Proceedings. 2012. p. 107-120. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-642-33512-9_10

Efficient probabilistic model checking of systems with ranged probabilities

Abstract

Publication series

Other

All Science Journal Classification (ASJC) codes

Access to Document

Other files and links

Fingerprint

Cite this