Perturbation of CTMC Trapping Probabilities with Application to Model Repair
Pages 36 - 43
Abstract
This paper studies properties of continuous-time Markov chains with one class of transient states and at least two absorbing states. We look at a perturbation of the chain that arises by uniformly decreasing all rates to absorption. For this situation, the monotonicity of the trapping probabilities is analysed, and their asymptotic limit is computed. The theoretical findings are then applied to a type of model repair problem, where a lower time-bounded and lower probability-bounded CSL until requirement needs to be satisfied. The paper presents an algorithm for this type of problem and proves its correctness.
References
[1]
C. Baier, B. Haverkort, H. Hermanns, and J.-P. Katoen. 2003. Model-Checking Algorithms for Continuous-Time Markov Chains. IEEE Transactions on Software Engineering 29, 6 (2003), 524--541.
[2]
E. Bartocci, R. Grosu, P. Katsaros, C.R. Ramakrishnan, and S.A. Smolka. 2011. Model Repair for Probabilistic Systems. In TACAS'11. Springer LNCS 6605, 326--340.
[3]
A. Berman and R.J. Plemmons. 1979. Nonnegative matrices in the mathematical sciences. Academic Press.
[4]
A. et al. Bobbio. 2005. Matching Three Moments with Minimal Acyclic Phase Type Distributions. Stochastic Models 2--3, 21 (2005), 303--326.
[5]
S. L. Campbell. 1980. Singular systems of differential equations. Pitman, London.
[6]
M. Ceska, F. Dannenberg, M. Z. Kwiatkowska, and N. Paoletti. 2014. Precise Parameter Synthesis for Stochastic Biochemical Systems. In Computational Methods in Systems Biology - 12th International Conference, CMSB. 86--98.
[7]
T. Chen, E. M. Hahn, T. Han, M. Kwiatkowska, H. Qu, and L. Zhang. 2013. Model Repair for Markov Decision Processes. In Proc. 7th Int. Symp. Theor. Aspects of Software Engineering (TASE). IEEE CS Press, 85--92.
[8]
P. Collet, S. Martinez, and J. San Martin. 2013. Quasi-Stationary Distributions -- Markov Chains, Diffusion and Dynamical Systems. Springer.
[9]
J. N. Darroch and E. Seneta. 1967. On Quasi-Stationary Distributions in Absorbing Continuous-Time Finite Markov Chains. J. Appl. Probab. 4, 1 (1967), 192--196.
[10]
N. Castro González. 2005. Additive perturbation results for the Drazin inverse. Linear Algebra Appl. 397, 0 (2005), 279--297.
[11]
T. Han, J.-P. Katoen, and A. Mereacre. 2008. Approximate Parameter Synthesis for Probabilistic Time-Bounded Reachability. In Proceedings of the 29th IEEE Real-Time Systems Symposium, RTSS. 173--182.
[12]
Robert E. Hartwig, Guorong Wang, and Yimin Wei. 2001. Some additive results on Drazin inverse. Linear Algebra Appl. 322, 1-3 (2001), 207--217.
[13]
A. Horvath and M. Telek. 2002. PhFit: A General Phase-Type Fitting Tool. In TOOLS 2002, T. Field et al. (Ed.). Springer LNCS 2324, 82--91.
[14]
G. Horvath and M. Telek. 2009. On the canonical representation of phase type distributions. Performance Evaluation 66, 8 (2009), 396--409. Selected papers of the Fourth European Performance Engineering Workshop (EPEW) 2007.
[15]
M. Kwiatkowska, G. Norman, and D. Parker. 2011. PRISM 4.0: Verification of Probabilistic Real-time Systems. In Proc. 23rd International Conference on Computer Aided Verification (CAV'11). Springer LNCS 6806, 585--591.
[16]
G. Latouche and V. Ramaswami. 1999. Introduction to Matrix Analytic Methods in Stochastic Modeling. Society for Industrial and Applied Mathematics.
[17]
C. A. et al. O'Cinneide. 1967. Characterization of Phase-Type Distributions. Communications in Statistics: Stochastic Models 1, 6 (1967), 1--57.
[18]
S. Pathak, E. Ábrahám, N. Jansen, A. Tacchella, and J.-P. Katoen. 2015. A Greedy Approach for the Efficient Repair of Stochastic Models. In NASA Formal Methods - 7th Int. Symposium. 295--309.
[19]
T. Quatmann, C. Dehnert, N. Jansen, S. Junges, and J.-P. Katoen. 2016. Parameter Synthesis for Markov Models: Faster Than Ever. In ATVA 2016. Springer LNCS 9938, 50--67.
[20]
B. Tati and M. Siegle. 2015. Parameter and Controller Synthesis for Markov Chains with Actions and State Labels. In 2nd International Workshop on Synthesis of Complex Parameters (SynCoP'15) (OpenAccess Series in Informatics (OASIcs)), É. André and G. Frehse (Eds.), Vol. 44. Dagstuhl, Germany, 63--76.
[21]
B. Tati and M. Siegle. 2016. Rate Reduction for State-labelled Markov Chains with Upper Time-bounded CSL Requirements. In Proc. Cassting Workshop on Games for the Synthesis of Complex Systems and 3rd Int. Workshop on Synthesis of Complex Parameters, Eindhoven, NL, April 2-3, 2016, T. Brihaye, B. Delahaye, L. Jezequel, N. Markey, and J. Srba (Eds.). Open Publishing Assoc, El. Proc. in Theoret. Computer Science Vol. 220, 77--89.
Index Terms
- Perturbation of CTMC Trapping Probabilities with Application to Model Repair
Recommendations
Markov chains with perturbed rates to absorption: Theory and application to model repair
AbstractThis work investigates properties of continuous-time Markov chains with absorbing states, where there is no restriction on the structure of the set of transient states. The paper studies the behaviour of the hitting probabilities, as ...
Model and Program Repair via SAT Solving
Special Issue on MEMCODE 2015 and Regular Papers (Diamonds)We consider the subtractive model repair problem: given a finite Kripke structure M and a CTL formula η, determine if M contains a substructure M′ that satisfies η. Thus, M can be “repaired” to satisfy eta by deleting some transitions and states. We map ...
Abstract model repair
NFM'12: Proceedings of the 4th international conference on NASA Formal MethodsGiven a Kripke structure M and CTL formula φ, where M ⊭ φ, the problem of Model Repair is to obtain a new model M′ such that M′⊨φ. Moreover, the changes made to M to derive M′ should be minimal with respect to all such M′. As in model checking, state ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
December 2017
268 pages
ISBN:9781450363464
DOI:10.1145/3150928
Copyright © 2017 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]
In-Cooperation
- EAI: The European Alliance for Innovation
Publisher
Association for Computing Machinery
New York, NY, United States
Publication History
Published: 05 December 2017
Check for updates
Author Tags
Qualifiers
- Research-article
- Research
- Refereed limited
Conference
VALUETOOLS 2017
VALUETOOLS 2017: 11th EAI International Conference on Performance Evaluation Methodologies and Tools
December 5 - 7, 2017
Venice, Italy
Acceptance Rates
Overall Acceptance Rate 90 of 196 submissions, 46%
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- 0Total Citations
- 34Total Downloads
- Downloads (Last 12 months)1
- Downloads (Last 6 weeks)0
Reflects downloads up to 01 Nov 2024
Other Metrics
Citations
View Options
Get Access
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in