Taolue Chen
Skip Abstract Section
Abstract
Stochastic modelling and algorithmic verification techniques have been proved useful in analysing and detecting unusual trends in performance and energy usage of systems such as power management controllers and wireless sensor devices. Many important properties are dependent on the cumulated time that the device spends in certain states, possibly intermittently. We study the problem of verifying continuous-time Markov Chains (CTMCs) against Linear Duration Properties (LDP), that is, properties stated as conjunctions of linear constraints over the total duration of time spent in states that satisfy a given property. We identify two classes of LDP properties, Eventuality Duration Properties (EDP) and Invariance Duration Properties (IDP), respectively referring to the reachability of a set of goal states, within a time bound; and the continuous satisfaction of a duration property over an execution path. The central question that we address is how to compute the probability of the set of infinite timed paths of the CTMC that satisfy a given LDP. We present algorithms to approximate these probabilities up to a given precision, stating their complexity and error bounds. The algorithms mainly employ an adaptation of uniformisation and the computation of volumes of multidimensional integrals under systems of linear constraints, together with different mechanisms to bound the errors.
- Alur, R., Courcoubetis, C., and Henzinger, T. A. 1997. Computing accumulated delays in real-time systems. Formal Methods Syst. Des. 11, 2, 137--155. Google Scholar
Digital Library
- Aziz, A., Sanwal, K., Singhal, V., and Brayton, R. K. 2000. Model-checking continous-time markov chains. ACM Trans. Comput. Log. 1, 1, 162--170. Google ScholarDigital Library
- Baier, C., Haverkort, B. R., Hermanns, H., and Katoen, J.-P. 2000. On the logical characterization of performability properties. In Proceedings of the 27th International Colloquium on Automata, Languages and Programming (ICALP'00). U. Montanari, J. D. P. Rolim, and E. Welzl, Eds., Lecture Notes in Computer Science, vol. 1853, Springer, 780--792. Google ScholarDigital Library
- Baier, C., Haverkort, B. R., Hermanns, H., and Katoen, J.-P. 2003. Model-checking algorithms for continuous-time Markov chains. IEEE Trans. Softw. Engin. 29, 6, 524--541. Google ScholarDigital Library
- Baier, C., Haverkort, B. R., Hermanns, H., and Katoen, J.-P. 2010. Performance evaluation and model checking join forces. Comm. ACM 53, 9, 76--85. Google ScholarDigital Library
- Baier, C. and Katoen, J.-P. 2008. Principles of Model Checking. MIT Press. Google ScholarDigital Library
- Barbot, B., Chen, T., Han, T., Katoen, J.-P., and Mereacre, A. 2011. Efficient CTMC model checking of linear real-time objectives. In Proceedings of the 17th International Conference on Tools and Algorithms for the Construction and Analysis of Systems: Part of the Joint European Conferences on Theory and Practice of Software (TACAS/ETAP'11). P. A. Abdulla and K. R. M. Leino, Eds., Lecture Notes in Computer Science, vol. 6605, Springer, 128--142. Google ScholarDigital Library
- Boker, U., Chatterjee, K., Henzinger, T. A., and Kupferman, O. 2011. Temporal specifications with accumulative values. In Proceedings of the 26th Annual IEEE Symposium on Logic in Computer Science (LICS'11). IEEE Computer Society, Los Alamitos, CA, 43--52. Google ScholarDigital Library
- Bouajjani, A., Echahed, R., and Sifakis, J. 1993. On model checking for real-time properties with durations. In Proceedings of the Annual IEEE Symposium on Logic in Computer Science (LICS'93). IEEE Computer Society, Los Alamitos, CA, 147--159.Google Scholar
- Bouyer, P., Fahrenberg, U., Larsen, K. G., and Markey, N. 2010. Timed automata with observers under energy constraints. In Proceedings of the 13th ACM International Conference on Hybrid Systems: Computation and Control (HSCC'10). K. H. Johansson and W. Yi, Eds., ACM Press, New York, 61--70. Google ScholarDigital Library
- Bouyer, P., Fahrenberg, U., Larsen, K. G., Markey, N., and Srba, J. 2008. Infinite runs in weighted timed automata with energy constraints. In Proceedings of the 6th International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS'08). F. Cassez and C. Jard, Eds., Lecture Notes in Computer Science, vol. 5215, Springer, 33--47. Google ScholarDigital Library
- Chen, T., Diciolla, M., Kwiatkowska, M. Z., and Mereacre, A. 2011a. Time-bounded verification of ctmcs against real-time specifications. In Proceedings of the 9th International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS'11). U. Fahrenberg and S. Tripakis, Eds., Lecture Notes in Computer Science, vol. 6919, Springer, 26--42. Google ScholarDigital Library
- Chen, T., Diciolla, M., Kwiatkowska, M. Z., and Mereacre, A. 2012. Verification of linear duration properties over continuous-time markov chains. In Proceedings of the 6th International Conference on Formal Modeling and Analysis of Timed Systems (HSCC'12). T. Dang and I. M. Mitchell, Eds., ACM Press, New York, 265--274. Google ScholarDigital Library
- Chen, T., Han, T., Katoen, J.-P., and Mereacre, A. 2009. Quantitative model checking of continuous time Markov chains against timed automata specifications. In Proceedings of the Annual IEEE Symposium on Logic in Computer Science (LICS'09). IEEE Computer Society, Los Alamitos, CA, 309--318. Google ScholarDigital Library
- Chen, T., Han, T., Katoen, J.-P., and Mereacre, A. 2011b. Model checking of continuous-time Markov chains against timed automata specifications. Logical Methods Comput. Sci. 7, 1--2, 1--34.Google ScholarCross Ref
- Cloth, L. 2006. Model checking algorithms for Markov reward models. Ph.D. thesis, University of Twente, The Netherlands.Google Scholar
- Courcoubetis, C. and Yannakakis, M. 1995. The complexity of probabilistic verification. J. ACM 42, 4, 857--907. Google ScholarDigital Library
- Dahlquist, G. 1958. Stability and error bounds in the numerical integration of ordinary differential equations. Ph.D. thesis, Stockholm College.Google Scholar
- Davis, M. H. A. 1993. Markov Models and Optimization. Chapman and Hall.Google Scholar
- Etessami, K., Stewart, A., and Yannakakis, M. 2012. Polynomial time algorithms for branching markov decision processes and probabilistic min(max) polynomial bellman equations. In Proceedings of the 39th International Colloquium on Automata, Languages, and Programming (ICLAP'12). 314--326. Google ScholarDigital Library
- Gribaudo, M. and Telek, M. 2007. Fluid models in performance analysis. In Proceedings of the 7th International Conference on Formal Methods for Performance Evaluation (SFM'07). M. Bernardo and J. Hillston, Eds., Lecture Notes in Computer Science, vol. 4486, Springer, 271--317. Google ScholarDigital Library
- Guelev, D. P. and Hung, D. V. 2010. Reasoning about qos contracts in the probabilistic duration calculus. Electron. Not. Theor. Comput. Sci. 238, 6, 41--62. Google ScholarDigital Library
- Haverkort, B. R., Cloth, L., Hermanns, H., Katoen, J.-P., and Baier, C. 2002. Model checking performability properties. In Proceedings of the International Conference on Dependable Systems and Networks (DSN'02). IEEE Computer Society, Los Alamitos, CA, 103--112. Google ScholarDigital Library
- Higham, N. J. 2002. Accuracy and Stability of Numerical Algorithms. 2nd ed. Society for Industrial and Applied Mathematics, Philadelphia, PA. Google ScholarDigital Library
- Horn, R. A. and Johnson, C. R. 1990. Matrix Analysis. Cambridge University Press. Google ScholarDigital Library
- Horton, G., Kulkarni, V. G., Nicol, D. M., and Trivedi, K. S. 1998. Fluid stochastic petri nets: Theory, applications, and solution techniques. Euro. J. Oper. Res. 105, 1, 184--201.Google ScholarCross Ref
- Hung, D. V. and Zhang, M. 2007. On verification of probabilistic timed automata against probabilistic duration properties. In Proceedings of the 13th IEEE International Conference on Embedded and Real-Time Computing Systems and Applications (RTCSA'07). IEEE Computer Society, Los Alamitos, CA, 165--172. Google ScholarDigital Library
- Hung, D. V. and Zhou, C. 1999. Probabilistic duration calculus for continuous time. Formal Aspects Comput. 11, 1, 21--44.Google ScholarCross Ref
- Jensen, A. 1953. Markoff chains as an aid in the study of markoff processes. Skand. Aktuarietidskrift 36, 87--91.Google Scholar
- Kesten, Y., Pnueli, A., Sifakis, J., and Yovine, S. 1999. Decidable integration graphs. Inf. Comput. 150, 2, 209--243. Google ScholarDigital Library
- Kwiatkowska, M., Norman, G., and Parker, D. 2007. Stochastic model checking. In Proceedings of the 7th International Conference on Formal Methods for Performance Evaluation (SFM'07). M. Bernardo and J. Hillston, Eds., Lecture Notes in Computer Science, vol. 4486, Springer, 220--270. Google ScholarDigital Library
- Kwiatkowska, M., Norman, G., and Parker, D. 2011. PRISM 4.0: Verification of probabilistic real-time systems. In Proceedings of the 23rd International Conference on Computer Aided Verification (CAV'11). G. Gopalakrishnan and S. Qadeer, Eds., Lecture Notes in Computer Science, vol. 6806, Springer, 585--591. Google ScholarDigital Library
- Lasserre, J. B. and Zeron, E. S. 2001. A laplace transform algorithm for the volume of a convex polytope. J. ACM 48, 6, 1126--1140. Google ScholarDigital Library
- Li, X., Hung, D. V., and Zheng, T. 1997. Checking hybrid automata for linear duration invariants. In Proceedings of the 3rd Asian Computing Science Conference on Advances in Computing Science (ASIAN'97). R. K. Shyamasundar and K. Ueda, Eds., Lecture Notes in Computer Science, vol. 1345, Springer, 166--180. Google ScholarDigital Library
- Meyn, S. P. and Tweedie, R. L. 1996. Markov Chains and Stochastic Stability. Springer.Google Scholar
- Neuts, M. 1981. Matrix-Geometric Solutions in Stochastic Models: An Algorithmic Approach. John Hopkins University Press.Google Scholar
- Nielsen, B. F., Nielson, F., and Nielson, H. R. 2010. Model checking multivariate state rewards. In Proceedings of the 7th International Conference on the Quantitative Evaluation of Systems (QEST'10). IEEE Computer Society, Los Alamitos, CA, 7--16. Google ScholarDigital Library
- Norman, G., Parker, D., Kwiatkowska, M., Shukla, S., and Gupta, R. 2005. Using probabilistic model checking for dynamic power management. Formal Aspects Comput. 17, 2, 160--176. Google ScholarCross Ref
- Pattipati, K. R., Mallubhatla, R., Gopalakrishna, V., and Viswanatham, N. 1993. Markov-reward models and hyperbolic systems. In 2nd International Workshop on Performability Modeling of Computer and Communication Systems.Google Scholar
- Qiu, Q., Qu, Q., and Pedram, M. 2001. Stochastic modeling of a power-managed system-construction and optimization. IEEE Trans. Comput.-Aid. Des. Integr. Circ. Syst. 20, 10, 1200--1217. Google ScholarDigital Library
- Qureshi, M. A. and Sanders, W. H. 1994. Reward model solution methods with impulse and rate rewards: An algorithm and numerical results. Perform. Eval. 20, 4, 413--436. Google ScholarDigital Library
- Thai, P. H. and Hung, D. V. 2004. Verifying linear duration constraints of timed automata. In Proceedings of the 1st International Colloquium on Theoretical Aspects of Computing (ICTAC'04). Z. Liu and K. Araki, Eds., Lecture Notes in Computer Science, vol. 3407, Springer, 295--309. Google ScholarDigital Library
- Zhang, L., Jansen, D. N., Nielson, F., and Hermanns, H. 2012. Efficient csl model checking using stratification. Logical Methods Comput. Sci. 8, 2.Google ScholarCross Ref
- Zhang, M., Hung, D. V., and Liu, Z. 2008. Verification of linear duration invariants by model checking ctl properties. In Proceedings of the 5th International Colloquium on Theoretical Aspects of Computing (ICTAC'08). J. S. Fitzgerald, A. E. Haxthausen, and H. Yenigun, Eds., Lecture Notes in Computer Science, vol. 5160, Springer, 395--409. Google ScholarDigital Library
- Zhou, C., Hoare, C. A. R., and Ravn, A. P. 1991. A calculus of durations. Inf. Process. Lett. 40, 5, 269--276.Google ScholarCross Ref
- Zhou, C., Zhang, J., Yang, L., and Li, X. 1994. Linear duration invariants. In Proceedings of the 3rd International Symposium Organized Jointly with the Working Group Provably Correct Systems on Formal Techniques in Real-Time and Fault-Tolerant Systems (FTRTFT'94). H. Langmaack, W. P. de Roever, and J. Vytopil, Eds., Lecture Notes in Computer Science, vol. 863, Springer, 86--109. Google ScholarDigital Library
Index Terms
- Verification of linear duration properties over continuous-time markov chains
Recommendations
Verification of linear duration properties over continuous-time markov chains
HSCC '12: Proceedings of the 15th ACM international conference on Hybrid Systems: Computation and ControlStochastic modeling and algorithmic verification techniques have been proved useful in analyzing and detecting unusual trends in performance and energy usage of systems such as power management controllers and wireless sensor devices. Many important ...
On-the-fly verification and optimization of DTA-properties for large Markov chains
We consider continuous-time Markov chains (CTMC) with very large or infinite state spaces which are, for instance, used to model biological processes or to evaluate the performance of computer and communication networks. We propose a numerical ...
Uniformization for nonhomogeneous Markov chains
The discrete Poissonian representation for transition probabilities of homogeneous continuous-time Markov chains, known as uniformization or randomization, is extended to time-inhomogeneous chains. For computational purposes a discrete-time ...
Comments