Perturbation analysis in verification of Discrete-time Markov Chains

Chen, T; Feng, Y; Rosenblum, DS; Su, G

Perturbation analysis in verification of Discrete-time Markov Chains

Chen, T Feng, Y

Rosenblum, DS Su, G

Permalink

Publication Type:: Conference Proceeding
Citation:: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 2014, 8704 LNCS pp. 218 - 233
Issue Date:: 2014-01-01

Open Access

Copyright Clearance Process

Recently Added
In Progress
Open Access

This item is open access.

Adobe PDF

Download Accepted Manuscript versionAdobe PDF (307.1 kB)

View on publisher's site

View statistics

Full metadata record

Field	Value	Language
dc.contributor.author	Chen, T	en_US
dc.contributor.author	Feng, Y https://orcid.org/0000-0002-3097-3896	en_US
dc.contributor.author	Rosenblum, DS	en_US
dc.contributor.author	Su, G	en_US
dc.date.issued	2014-01-01	en_US
dc.identifier.citation	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 2014, 8704 LNCS pp. 218 - 233	en_US
dc.identifier.isbn	9783662445839	en_US
dc.identifier.issn	0302-9743	en_US
dc.identifier.uri	http://hdl.handle.net/10453/33132
dc.description.abstract	Perturbation analysis in probabilistic verification addresses the robustness and sensitivity problem for verification of stochastic models against qualitative and quantitative properties. We identify two types of perturbation bounds, namely non-asymptotic bounds and asymptotic bounds. Non-asymptotic bounds are exact, pointwise bounds that quantify the upper and lower bounds of the verification result subject to a given perturbation of the model, whereas asymptotic bounds are closed-form bounds that approximate non-asymptotic bounds by assuming that the given perturbation is sufficiently small. We perform perturbation analysis in the setting of Discrete-time Markov Chains. We consider three basic matrix norms to capture the perturbation distance, and focus on the computational aspect. Our main contributions include algorithms and tight complexity bounds for calculating both non-asymptotic bounds and asymptotic bounds with respect to the three perturbation distances. © 2014 Springer-Verlag.	en_US
dc.relation.ispartof	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)	en_US
dc.relation.isbasedon	10.1007/978-3-662-44584-6_16	en_US
dc.subject.classification	Artificial Intelligence & Image Processing	en_US
dc.title	Perturbation analysis in verification of Discrete-time Markov Chains	en_US
dc.type	Conference Proceeding
utslib.citation.volume	8704 LNCS	en_US
utslib.for	080203 Computational Logic and Formal Languages	en_US
pubs.embargo.period	Not known	en_US
pubs.organisational-group	/University of Technology Sydney
pubs.organisational-group	/University of Technology Sydney/Faculty of Engineering and Information Technology
pubs.organisational-group	/University of Technology Sydney/Strength - QSI - Centre for Quantum Software and Information
utslib.copyright.status	open_access
pubs.publication-status	Published	en_US
pubs.volume	8704 LNCS	en_US

Abstract:

Perturbation analysis in probabilistic verification addresses the robustness and sensitivity problem for verification of stochastic models against qualitative and quantitative properties. We identify two types of perturbation bounds, namely non-asymptotic bounds and asymptotic bounds. Non-asymptotic bounds are exact, pointwise bounds that quantify the upper and lower bounds of the verification result subject to a given perturbation of the model, whereas asymptotic bounds are closed-form bounds that approximate non-asymptotic bounds by assuming that the given perturbation is sufficiently small. We perform perturbation analysis in the setting of Discrete-time Markov Chains. We consider three basic matrix norms to capture the perturbation distance, and focus on the computational aspect. Our main contributions include algorithms and tight complexity bounds for calculating both non-asymptotic bounds and asymptotic bounds with respect to the three perturbation distances. © 2014 Springer-Verlag.

Please use this identifier to cite or link to this item:

http://hdl.handle.net/10453/33132