research-article

On approximation metrics for linear temporal model-checking of stochastic systems

Authors:

Alessandro AbateAuthors Info & Claims

HSCC '14: Proceedings of the 17th international conference on Hybrid systems: computation and control

Pages 193 - 202

https://doi.org/10.1145/2562059.2562118

Published: 15 April 2014 Publication History

Abstract

This paper proposes criteria for metrics between stochastic systems with a focus on the task of linear temporal model-checking. It explicitly puts forward two metrics which partially satisfy those criteria, and discusses their connection with other metrics studied in the literature. In particular, the notion of coupling between stochastic processes is shown to be crucial: omitting the explicit choice of coupling may lead to conservative results. The theoretical claims in the paper are supported by numerical examples.

References

[1]

MoVeS website. http://www.movesproject.eu.

[2]

A. Abate. A contractivity approach for probabilistic bisimulations of diffusion processes. In Proceedings of the 48th IEEE Conference on Decision and Control and 28th Chinese Control Conference, pages 2230--2235, 2009.

[3]

A. Abate. Approximation metrics based on probabilistic bisimulations for general state-space markov processes: a survey. Electronic Notes in Theoretical Computer Sciences, 2013. In Print.

Digital Library

[4]

A. Abate, J.-P. Katoen, J. Lygeros, and M. Prandini. Approximate model checking of stochastic hybrid systems. European Journal of Control, 16:624--641, 2010.

[5]

A. Abate, J.-P. Katoen, and A. Mereacre. Quantitative automata model checking of autonomous stochastic hybrid systems. In Proceedings of the 14th international conference on Hybrid Systems: Computation and Control, HSCC '11, pages 83--92, New York, NY, USA, 2011. ACM.

Digital Library

[6]

A. Abate and M. Prandini. Approximate abstractions of stochastic systems: A randomized method. In Proceedings of the 50th IEEE Conference on Decision and Control and European Control Conference, pages 4861--4866, 2011.

[7]

A. Abate, F. Redig, and I. Tkachev. On the effect of perturbation of conditional probabilities in total variation. Statistics & Probability Letters, 2014. In Press.

[8]

C. Baier and J.-P. Katoen. Principles of model checking. The MIT Press, 2008.

Digital Library

[9]

A. Dembo and O. Zeitouni. Large deviations techniques and applications. Springer-Verlag, Berlin, 2010.

[10]

J. Desharnais, A. Edalat, and P. Panangaden. Bisimulation for Labelled Markov Processes. Information and Computation, 179(2):163--193, 2002.

Digital Library

[11]

J. Desharnais, V. Gupta, R. Jagadeesan, and P. Panangaden. Metrics for Labeled Markov Systems. In Proceedings of the 10th International Conference on Concurrency Theory, CONCUR '99, pages 258--273, London, UK, 1999. Springer-Verlag.

Digital Library

[12]

J. Desharnais, V. Gupta, R. Jagadeesan, and P. Panangaden. Metrics for labelled Markov processes. Theoretical Computer Science, 318(3):323--354, 2004.

Digital Library

[13]

S. N. Ethier and T. G. Kurtz. Markov processes: characterization and convergence. Wiley Series in Probability and Mathematical Statistics: Probability and Mathematical Statistics. John Wiley & Sons Inc., New York, 1986.

[14]

N. Ferns, P. Panangaden, and D. Precup. Bisimulation metrics for continuous Markov decision processes. SIAM Journal on Computing, 40(6):1662--1714, 2011.

Digital Library

[15]

A. L. Gibbs and F. E. Su. On choosing and bounding probability metrics. International Statistical Review, 70(3):419--435, 2002.

[16]

A. Girard and G. J. Pappas. Approximation metrics for discrete and continuous systems. IEEE Transactions on Automatic Control, 52(5):782--798, 2007.

[17]

A. Girard and G. J. Pappas. Approximate bisimulation: A bridge between computer science and control theory. European Journal of Control, 17(5-6):568--578, 2011.

[18]

A. Hinton, M. Kwiatkowska, G. Norman, and D. Parker. PRISM: A tool for automatic verification of probabilistic systems. In H. Hermanns and J. Palsberg, editors, Tools and Algorithms for the Construction and Analysis of Systems, volume 3920 of Lecture Notes in Computer Science, pages 441--444. Springer Verlag, 2006.

Digital Library

[19]

A. A. Julius and G. J. Pappas. Approximations of stochastic hybrid systems. IEEE Transactions on Automatic Control, 54(6):1193--1203, 2009.

[20]

O. Kallenberg. Foundations of modern probability. Probability and its Applications. Springer-Verlag, New York, 1997.

[21]

J.-P. Katoen, M. Khattri, and I. S. Zapreev. A Markov reward model checker. In Proceedings of the Second International Conference on the Quantitative Evaluation of Systems, QEST '05, pages 243--244, Washington, DC, USA, 2005. IEEE Computer Society.

Digital Library

[22]

K. G. Larsen and A. Skou. Bisimulation through probabilistic testing. Information and Computation, 94(1):1--28, 1991.

Digital Library

[23]

T. Lindvall. Lectures on the coupling method. Wiley Series in Probability and Mathematical Statistics: Probability and Mathematical Statistics. John Wiley & Sons Inc., New York, 1992.

[24]

B. Øksendal. Stochastic differential equations: an introduction with applications. Universitext. Springer-Verlag, Berlin, sixth edition, 2003.

[25]

K. R. Parthasarathy. Probability measures on metric spaces. Probability and Mathematical Statistics, No. 3. Academic Press Inc., New York, 1967.

[26]

D. Revuz. Markov chains. North-Holland Publishing, Amsterdam, second edition, 1984.

[27]

R. Segala. A compositional trace-based semantics for probabilistic automata. In I. Lee and S. A. Smolka, editors, CONCUR '95: Concurrency Theory, volume 962 of Lecture Notes in Computer Science, pages 234--248. Springer Berlin Heidelberg, 1995.

Digital Library

[28]

B. K. Sriperumbudur, K. Fukumizu, A. Gretton, B. Schölkopf, and G. Lanckriet. On the empirical estimation of integral probability metrics. Electronic Journal of Statistics, 6:1550--1599, 2012.

[29]

P. Tabuada. Verification and control of hybrid systems: A symbolic approach. Springer Verlag, New York, 2009.

Digital Library

[30]

D. Thorsley and E. Klavins. Approximating stochastic biochemical processes with Wasserstein pseudometrics. Systems Biology, IET, 4(3):193--211, May 2010.

[31]

I. Tkachev and A. Abate. Formula-free finite abstractions for linear temporal verification of stochastic hybrid systems. In Proceedings of the 16th international conference on Hybrid Systems: Computation and Control, HSCC '13, pages 283--292, New York, NY, USA, 2013. ACM.

Digital Library

[32]

I. Tkachev, A. Mereacre, J.-P. Katoen, and A. Abate. Quantitative automata-based controller synthesis for non-autonomous stochastic hybrid systems. In Proceedings of the 16th international conference on Hybrid Systems: Computation and Control, HSCC '13, pages 293--302, New York, NY, USA, 2013. ACM.

Digital Library

[33]

Ilya Tkachev and Alessandro Abate. Characterization and computation of infinite-horizon specifications over markov processes. Theoretical Computer Science, 515(0):1--18, 2014.

Digital Library

[34]

F. van Breugel, S. Shalit, and J. Worrell. Testing labelled Markov processes. In Proceedings of the 29th International Colloquium on Automata, Languages and Programming, ICALP '02, pages 537--548, London, UK, 2002. Springer-Verlag.

Digital Library

[35]

F. van Breugel and J. Worrell. Towards quantitative verification of probabilistic transition systems. In Proceedings of the 28th International Colloquium on Automata, Languages and Programming, ICALP '01, pages 421--432, London, UK, 2001. Springer-Verlag.

Digital Library

[36]

M.Y. Vardi. Automatic verification of probabilistic concurrent finite state programs. In 26th Annual Symposium on Foundations of Computer Science, pages 327--338, 1985.

Digital Library

Cited By

Du ZBalzano LOzay N(2022)Mode Reduction for Markov Jump SystemsIEEE Open Journal of Control Systems10.1109/OJCSYS.2022.32126131(335-353)Online publication date: 2022
https://doi.org/10.1109/OJCSYS.2022.3212613
van Huijgevoort BHaesaert S(2022)Similarity quantification for linear stochastic systems: A coupling compensator approachAutomatica10.1016/j.automatica.2022.110476144(110476)Online publication date: Oct-2022
https://doi.org/10.1016/j.automatica.2022.110476
Abate ABrim LČeška MKwiatkowska M(2015)Adaptive Aggregation of Markov Chains: Quantitative Analysis of Chemical Reaction NetworksComputer Aided Verification10.1007/978-3-319-21690-4_12(195-213)Online publication date: 16-Jul-2015
https://doi.org/10.1007/978-3-319-21690-4_12
Show More Cited By

Index Terms

On approximation metrics for linear temporal model-checking of stochastic systems
1. Mathematics of computing
  1. Probability and statistics
    1. Probabilistic representations
      1. Markov networks
    2. Stochastic processes
      1. Markov processes
2. Theory of computation
  1. Theory and algorithms for application domains
    1. Machine learning theory
      1. Markov decision processes

Recommendations

Formula-free finite abstractions for linear temporal verification of stochastic hybrid systems
HSCC '13: Proceedings of the 16th international conference on Hybrid systems: computation and control

Results on approximate model-checking of Stochastic Hybrid Systems (SHS) against general temporal specifications lead to abstractions that structurally depend on the given specification or with a state cardinality that crucially depends on the size of ...
Verifying Stochastic Hybrid Systems with Temporal Logic Specifications via Model Reduction
We present a scalable methodology to verify stochastic hybrid systems for inequality linear temporal logic (iLTL) or inequality metric interval temporal logic (iMITL). Using the Mori–Zwanzig reduction method, we construct a finite-state Markov chain ...
Limit behavior of the hybrid approximation of stochastic process algebras
ASMTA'10: Proceedings of the 17th international conference on Analytical and stochastic modeling techniques and applications

We investigate the limit behavior of a class of stochastic hybrid systems obtained by hybrid approximation of Stochastic Concurrent Constraint Programming (sCCP). We prove that a sequence of Continuous Time Markov Chain (CTMC), constructed from sCCP ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

HSCC '14: Proceedings of the 17th international conference on Hybrid systems: computation and control

April 2014

328 pages

ISBN:9781450327329

DOI:10.1145/2562059

Program Chairs:
Martin Fráänzle
Carl von Ossietziky Universität Oldenburg, Germany
,
John Lygeros
ETH Zurich, Switzerland

Copyright © 2014 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 the author(s) 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

SIGBED: ACM Special Interest Group on Embedded Systems

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 15 April 2014

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Funding Sources

Conference

HSCC'14

Sponsor:

SIGBED

HSCC'14: 17th International Conference on Hybrid Systems: Computation and Control

April 15 - 17, 2014

Berlin, Germany

Acceptance Rates

HSCC '14 Paper Acceptance Rate 29 of 69 submissions, 42%;

Overall Acceptance Rate 153 of 373 submissions, 41%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

4
Total Citations
View Citations
112
Total Downloads

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

Reflects downloads up to 24 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Du ZBalzano LOzay N(2022)Mode Reduction for Markov Jump SystemsIEEE Open Journal of Control Systems10.1109/OJCSYS.2022.32126131(335-353)Online publication date: 2022
https://doi.org/10.1109/OJCSYS.2022.3212613
van Huijgevoort BHaesaert S(2022)Similarity quantification for linear stochastic systems: A coupling compensator approachAutomatica10.1016/j.automatica.2022.110476144(110476)Online publication date: Oct-2022
https://doi.org/10.1016/j.automatica.2022.110476
Abate ABrim LČeška MKwiatkowska M(2015)Adaptive Aggregation of Markov Chains: Quantitative Analysis of Chemical Reaction NetworksComputer Aided Verification10.1007/978-3-319-21690-4_12(195-213)Online publication date: 16-Jul-2015
https://doi.org/10.1007/978-3-319-21690-4_12
Abate AKwiatkowska MNorman GParker D(2014)Probabilistic Model Checking of Labelled Markov Processes via Finite Approximate BisimulationsHorizons of the Mind. A Tribute to Prakash Panangaden10.1007/978-3-319-06880-0_2(40-58)Online publication date: 2014
https://doi.org/10.1007/978-3-319-06880-0_2

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