{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,28]],"date-time":"2026-04-28T17:20:29Z","timestamp":1777396829744,"version":"3.51.4"},"reference-count":24,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2020,2,4]],"date-time":"2020-02-04T00:00:00Z","timestamp":1580774400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"European Research Council","award":["610150"],"award-info":[{"award-number":["610150"]}]},{"name":"Deutsche Forschungsgemeinschaft project","award":["389792660- TRR 248"],"award-info":[{"award-number":["389792660- TRR 248"]}]},{"name":"ERC Synergy Grant ImPACT"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Model. Perform. Eval. Comput. Syst."],"published-print":{"date-parts":[[2020,3,31]]},"abstract":"<jats:p>Time-bounded reachability is a fundamental problem in model checking continuous-time Markov chains (CTMCs) and Markov decision processes (CTMDPs) for specifications in continuous stochastic logics. It can be computed by numerically solving a characteristic linear dynamical system, but the procedure is computationally expensive. We take a control-theoretic approach and propose a reduction technique that finds another dynamical system of lower dimension (number of variables), such that numerically solving the reduced dynamical system provides an approximation to the solution of the original system with guaranteed error bounds. Our technique generalizes lumpability (or probabilistic bisimulation) to a quantitative setting. Our main result is a Lyapunov function characterization of the difference in the trajectories of the two dynamics that depends on the initial mismatch and exponentially decreases over time. In particular, the Lyapunov function enables us to compute an error bound between the two dynamics as well as a convergence rate. Finally, we show that the search for the reduced dynamics can be computed in polynomial time using a Schur decomposition of the transition matrix. This enables us to efficiently solve the reduced dynamical system by computing the exponential of an upper-triangular matrix characterizing the reduced dynamics. For CTMDPs, we generalize our approach using piecewise quadratic Lyapunov functions for switched affine dynamical systems. We synthesize a policy for the CTMDP via its reduced-order switched system that guarantees that the time-bounded reachability probability lies above a threshold. We provide error bounds that depend on the minimum dwell time of the policy. We demonstrate the technique on examples from queueing networks, for which lumpability does not produce any state space reduction, but our technique synthesizes policies using a reduced version of the model.&lt;?vsp -2pt?&gt;<\/jats:p>","DOI":"10.1145\/3371923","type":"journal-article","created":{"date-parts":[[2020,4,3]],"date-time":"2020-04-03T13:41:04Z","timestamp":1585921264000},"page":"1-29","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["A Lyapunov Approach for Time-Bounded Reachability of CTMCs and CTMDPs"],"prefix":"10.1145","volume":"5","author":[{"given":"Mahmoud","family":"Salamati","sequence":"first","affiliation":[{"name":"MPI-SWS, Kaiserslautern, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sadegh","family":"Soudjani","sequence":"additional","affiliation":[{"name":"Newcastle University, Newcastle upon Tyne, United Kingdom"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Rupak","family":"Majumdar","sequence":"additional","affiliation":[{"name":"MPI-SWS, Kaiserslautern, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2020,2,4]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/343369.343402"},{"key":"e_1_2_1_2_1","doi-asserted-by":"crossref","unstructured":"G. Bacci G. Bacci G. Larsen and R. Mardare. 2015. On the total variation distance of semi-Markov chains. In Foundations of Software Science and Computation Structures. Lecture Notes in Computer Science 9034. Springer-Verlag GBR 185--199.  G. Bacci G. Bacci G. Larsen and R. Mardare. 2015. On the total variation distance of semi-Markov chains. In Foundations of Software Science and Computation Structures. Lecture Notes in Computer Science 9034. Springer-Verlag GBR 185--199.","DOI":"10.1007\/978-3-662-46678-0_12"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2003.1205180"},{"key":"e_1_2_1_4_1","doi-asserted-by":"crossref","unstructured":"S. Boyd L. El Ghaoui E. Feron and V. Balakrishnan. 1994. Linear Matrix Inequalities in System and Control Theory. Vol. 15. SIAM.  S. Boyd L. El Ghaoui E. Feron and V. Balakrishnan. 1994. Linear Matrix Inequalities in System and Control Theory. Vol. 15. SIAM.","DOI":"10.1137\/1.9781611970777"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(98)00169-8"},{"key":"e_1_2_1_6_1","doi-asserted-by":"crossref","unstructured":"P. Buchholz E. M. Hahn H. Hermanns and L. Zhang. 2011. Model checking algorithms for CTMDPs. In Computer Aided Verification. Springer Berlin 225--242.  P. Buchholz E. M. Hahn H. Hermanns and L. Zhang. 2011. Model checking algorithms for CTMDPs. In Computer Aided Verification. Springer Berlin 225--242.","DOI":"10.1007\/978-3-642-22110-1_19"},{"key":"e_1_2_1_7_1","doi-asserted-by":"crossref","unstructured":"Y. Butkova H. Hatefi H. Hermanns and J. Kr\u010d\u00e1l. 2015. Optimal continuous time Markov decisions. In Automated Technology for Verification and Analysis. Springer International Publishing 166--182.  Y. Butkova H. Hatefi H. Hermanns and J. Kr\u010d\u00e1l. 2015. Optimal continuous time Markov decisions. In Automated Technology for Verification and Analysis. Springer International Publishing 166--182.","DOI":"10.1007\/978-3-319-24953-7_12"},{"key":"e_1_2_1_8_1","volume-title":"Applied Numerical Linear Algebra","author":"Demmel James W.","unstructured":"James W. Demmel . 1997. Applied Numerical Linear Algebra . Society for Industrial and Applied Mathematics . James W. Demmel. 1997. Applied Numerical Linear Algebra. Society for Industrial and Applied Mathematics."},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2003.09.013"},{"key":"e_1_2_1_10_1","unstructured":"J. Doyle B. Francis and A. Tannenbaum. 1990. Feedback Control Theory. Macmillan Publishing Co.  J. Doyle B. Francis and A. Tannenbaum. 1990. Feedback Control Theory. Macmillan Publishing Co."},{"key":"e_1_2_1_11_1","volume-title":"C (April","author":"Fearnley John","year":"2016","unstructured":"John Fearnley , Markus N. Rabe , Sven Schewe , and Lijun Zhang . 2016. Efficient approximation of optimal control for continuous-time Markov games. Information and Computation 247 , C (April 2016 ), 106--129. John Fearnley, Markus N. Rabe, Sven Schewe, and Lijun Zhang. 2016. Efficient approximation of optimal control for continuous-time Markov games. Information and Computation 247, C (April 2016), 106--129."},{"key":"e_1_2_1_12_1","volume-title":"An Introduction to Probability Theory and Its Applications","author":"Feller W.","unstructured":"W. Feller . 1968. An Introduction to Probability Theory and Its Applications . John Wiley ' Sons. W. Feller. 1968. An Introduction to Probability Theory and Its Applications. John Wiley ' Sons."},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1109\/TAC.2009.2034922"},{"key":"e_1_2_1_14_1","doi-asserted-by":"crossref","unstructured":"M. Grant and S. Boyd. 2008. Graph implementations for nonsmooth convex programs. In Recent Advances in Learning and Control. Springer-Verlag Limited 95--110.  M. Grant and S. Boyd. 2008. Graph implementations for nonsmooth convex programs. In Recent Advances in Learning and Control. Springer-Verlag Limited 95--110.","DOI":"10.1007\/978-1-84800-155-8_7"},{"key":"e_1_2_1_15_1","volume-title":"Proceedings of the 3rd International Workshop on the Numerical Solution of Markov Chains (NSMC\u201999)","author":"Hermanns H.","unstructured":"H. Hermanns , J. Meyer-Kayser , and M. Siegle . 1999. Multi terminal binary decision diagrams to represent and analyse continuous time Markov chains . In Proceedings of the 3rd International Workshop on the Numerical Solution of Markov Chains (NSMC\u201999) . 188--207. H. Hermanns, J. Meyer-Kayser, and M. Siegle. 1999. Multi terminal binary decision diagrams to represent and analyse continuous time Markov chains. In Proceedings of the 3rd International Workshop on the Numerical Solution of Markov Chains (NSMC\u201999). 188--207."},{"key":"e_1_2_1_16_1","doi-asserted-by":"crossref","unstructured":"R. A. Horn and C. R. Johnson. 1985. Matrix Analysis. Cambridge University Press. Cambridge.  R. A. Horn and C. R. Johnson. 1985. Matrix Analysis. Cambridge University Press. Cambridge.","DOI":"10.1017\/CBO9780511810817"},{"key":"e_1_2_1_17_1","volume-title":"\u201cGeneralization of a Fundamental Matrix","author":"Kemeny John G.","unstructured":"John G. Kemeny and J. Laurie Snell . 1976. Finite Markov Chains: With a New Appendix \u201cGeneralization of a Fundamental Matrix .\u201d Springer . John G. Kemeny and J. Laurie Snell. 1976. Finite Markov Chains: With a New Appendix \u201cGeneralization of a Fundamental Matrix.\u201d Springer."},{"key":"e_1_2_1_18_1","volume-title":"Nonlinear Systems","author":"Khalil H. K.","unstructured":"H. K. Khalil . 1996. Nonlinear Systems . Prentice Hall , Upper Saddle River, NJ. H. K. Khalil. 1996. Nonlinear Systems. Prentice Hall, Upper Saddle River, NJ."},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(91)90030-6"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1109\/CACSD.2004.1393890"},{"key":"e_1_2_1_21_1","volume-title":"2010 7th International Conference on the Quantitative Evaluation of Systems. 209--218","author":"Neuhausser M. R.","unstructured":"M. R. Neuhausser and L. Zhang . 2010. Time-bounded reachability probabilities in continuous-time Markov decision processes . In 2010 7th International Conference on the Quantitative Evaluation of Systems. 209--218 . M. R. Neuhausser and L. Zhang. 2010. Time-bounded reachability probabilities in continuous-time Markov decision processes. In 2010 7th International Conference on the Quantitative Evaluation of Systems. 209--218."},{"key":"e_1_2_1_22_1","volume-title":"Modern Control Engineering","author":"Ogata Katsuhiko","unstructured":"Katsuhiko Ogata . 2001. Modern Control Engineering ( 4 th ed.). Prentice Hall PTR , Upper Saddle River, NJ. Katsuhiko Ogata. 2001. Modern Control Engineering (4th ed.). Prentice Hall PTR, Upper Saddle River, NJ.","edition":"4"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00236-011-0140-0"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-99154-2_24"}],"container-title":["ACM Transactions on Modeling and Performance Evaluation of Computing Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3371923","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3371923","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T23:44:19Z","timestamp":1750203859000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3371923"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,2,4]]},"references-count":24,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2020,3,31]]}},"alternative-id":["10.1145\/3371923"],"URL":"https:\/\/doi.org\/10.1145\/3371923","relation":{},"ISSN":["2376-3639","2376-3647"],"issn-type":[{"value":"2376-3639","type":"print"},{"value":"2376-3647","type":"electronic"}],"subject":[],"published":{"date-parts":[[2020,2,4]]},"assertion":[{"value":"2019-01-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2019-11-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2020-02-04","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}