Verifying Continuous-time Stochastic Hybrid Systems via Mori-Zwanzig Model Reduction
pdf
Abstract:
Stochastic hybrid systems are a class of stochastic models that incorporates both continuous- and discretestate dynamics. They have wide applications in modeling various processes, such as communication networks [4] and biochemical reactions [6]. In this work, we focus on continuous-time stochastic hybrid systems (CTSHS); specifically, we propose a framework using Metric Interval Temporal Logic (MITL) [1] to describe the systems’ behavior and verifying the MITL formulas via model reduction and sampling. MITL can be viewed as a continuous-time and decidable extension of the common Linear Temporal Logic. It a powerful tool to describe both the transient and asymptotic behaviors of various kinds of dynamical systems, and to specify design goals in synthesis and verification problems. In addition, it provides a proper interface for automated verification using computers. However, checking MITL formulas on the CTSHS directly is beyond the computational capacity of computers since the system has infinitely many possible configurations. To circumvent this problem, we propose an approach of using the Mori-Zwanzig model reduction method [2], [3] to reduce the continuous-time stochastic hybrid systems to continuous-time Markov chains (CTMC) of finite states. This can be viewed as the hybrid and continuous-time extension of our previous works [7], [8]. Specifically, we divide the continuous state space into a finite number of partitions and treat each partition as a state of the CTMC. The transition rate between the states is determined by using the MoriZwanig method. We prove that, for systems that satisfy a contractivity condition, checking an MITL formula on the CTSHS can be achieved by check a slightingly stronger MITL formula on the CTMC. And the amount of strengthening required converges to zero as we refine the partitions. Generally, there are two approaches to verify MITL formulas on a CTMC: symbolic and sampling-based, among which the latter is more efficient in handling large-scale systems [5]. Considering that a large CTMC may be needed to approximate the CTSHS properly, we develop a sampling-based algorithm. The algorithm takes as input the MITL formula, the CTMC with its initial condition, and parameters describing the confidence level and the size of the indifference region. It returns “Yes/No” with high confidence when the evaluation of the MITL formula is outside the indifference region, and “Unknown” otherwise. The confidence level can be set arbitrarily close to 1 and the size of the indifference arbitrarily close to 0, at the expense of increasing the number of samples. Finally, we implement in a Billiard problem this framework for verifying MITL formulas on the CTSHS using the Mori-Zwanzig model reduction method and the sampling-based algorithm. The results show that it can handle a relatively complex problem in a reasonable amount of time. In the future, we will implement this method to more real-world applications, such as powertrain systems.
REFERENCES:
[1] R. Alur, T. Feder, and T. A. Henzinger. The benefits of relaxing punctuality. J. ACM, 43(1):116–146, Jan. 1996.
[2] C. Beck, S. Lall, T. Liang, and M. West. Model reduction, optimal prediction, and the mori-zwanzig representation of markov chains. In Proceedings of the 48th IEEE Conference on Decision and Control, 2009 held jointly with the 2009 28th Chinese Control Conference. CDC/CCC 2009, pages 3282–3287, Dec. 2009.
[3] A. J. Chorin, O. H. Hald, and R. Kupferman. Optimal prediction and the mori-zwanzig representation of irreversible processes. Proceedings of the National Academy of Sciences, 97(7):2968–2973, Mar. 2000.
[4] J. P. Hespanha. Stochastic hybrid systems: Application to communication networks. In Hybrid systems: computation and control, pages 387–401. Springer, 2004.
[5] K. Sen, M. Viswanathan, and G. Agha. On statistical model checking of stochastic systems. In K. Etessami and S. K. Rajamani, editors, Computer Aided Verification, number 3576 in Lecture Notes in Computer Science, pages 266–280. Springer Berlin Heidelberg, Jan. 2005.
[6] A. Singh and J. P. Hespanha. Stochastic hybrid systems for studying biochemical processes. Philosophical Transactions of the Royal Society of London A: Mathematical, Physical and Engineering Sciences, 368(1930):4995–5011, 2010.
[7] Y. Wang, N. Roohi, M. West, M. Viswanathan, and G. E. Dullerud. A mori-zwanzig and mitl based approach to statistical verification of continuous-time dynamical systems (to appear). In Proceedings of the 5th IFAC Workshop on Analysis and Design of Hybrid Systems, ADHS ’15, Atlanta, GA, USA, 2015.
[8] Y. Wang, N. Roohi, M. West, M. Viswanathan, and G. E. Dullerud. Statistical verification of dynamical systems using set oriented methods. In Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control, HSCC ’15, pages 169–178, New York, NY, USA, 2015. ACM.
Yu Wang and Geir E. Dullerud are with Coordinate Science Laboratory and the Department of Mechanical Science and Engineering, University of Illinois at Urbana-Champaign, Urbana, IL 61801 USA. Email: yuwang8@illinois.edu, dullerud@illinois.edu Nima Roohi and Mahesh Viswanathan are with the Department of Computer Science, University of Illinois at Urbana-Champaign, Urbana, IL 61801 USA. Email: roohi2@illinois.edu, vmahesh@illinois.edu Matthew West is with the Department of Mechanical Science and Engineering, University of Illinois at Urbana-Champaign, Urbana, IL 61801 USA. Email: mwest@illinois.edu The authors acknowledge support for this work from NSF CPS grant 1329991. Program Manager: Dr. David Corman.
Submitted by Geir Dullerud
on
Abstract:
Stochastic hybrid systems are a class of stochastic models that incorporates both continuous- and discretestate dynamics. They have wide applications in modeling various processes, such as communication networks [4] and biochemical reactions [6]. In this work, we focus on continuous-time stochastic hybrid systems (CTSHS); specifically, we propose a framework using Metric Interval Temporal Logic (MITL) [1] to describe the systems’ behavior and verifying the MITL formulas via model reduction and sampling. MITL can be viewed as a continuous-time and decidable extension of the common Linear Temporal Logic. It a powerful tool to describe both the transient and asymptotic behaviors of various kinds of dynamical systems, and to specify design goals in synthesis and verification problems. In addition, it provides a proper interface for automated verification using computers. However, checking MITL formulas on the CTSHS directly is beyond the computational capacity of computers since the system has infinitely many possible configurations. To circumvent this problem, we propose an approach of using the Mori-Zwanzig model reduction method [2], [3] to reduce the continuous-time stochastic hybrid systems to continuous-time Markov chains (CTMC) of finite states. This can be viewed as the hybrid and continuous-time extension of our previous works [7], [8]. Specifically, we divide the continuous state space into a finite number of partitions and treat each partition as a state of the CTMC. The transition rate between the states is determined by using the MoriZwanig method. We prove that, for systems that satisfy a contractivity condition, checking an MITL formula on the CTSHS can be achieved by check a slightingly stronger MITL formula on the CTMC. And the amount of strengthening required converges to zero as we refine the partitions. Generally, there are two approaches to verify MITL formulas on a CTMC: symbolic and sampling-based, among which the latter is more efficient in handling large-scale systems [5]. Considering that a large CTMC may be needed to approximate the CTSHS properly, we develop a sampling-based algorithm. The algorithm takes as input the MITL formula, the CTMC with its initial condition, and parameters describing the confidence level and the size of the indifference region. It returns “Yes/No” with high confidence when the evaluation of the MITL formula is outside the indifference region, and “Unknown” otherwise. The confidence level can be set arbitrarily close to 1 and the size of the indifference arbitrarily close to 0, at the expense of increasing the number of samples. Finally, we implement in a Billiard problem this framework for verifying MITL formulas on the CTSHS using the Mori-Zwanzig model reduction method and the sampling-based algorithm. The results show that it can handle a relatively complex problem in a reasonable amount of time. In the future, we will implement this method to more real-world applications, such as powertrain systems.
REFERENCES:
[1] R. Alur, T. Feder, and T. A. Henzinger. The benefits of relaxing punctuality. J. ACM, 43(1):116–146, Jan. 1996.
[2] C. Beck, S. Lall, T. Liang, and M. West. Model reduction, optimal prediction, and the mori-zwanzig representation of markov chains. In Proceedings of the 48th IEEE Conference on Decision and Control, 2009 held jointly with the 2009 28th Chinese Control Conference. CDC/CCC 2009, pages 3282–3287, Dec. 2009.
[3] A. J. Chorin, O. H. Hald, and R. Kupferman. Optimal prediction and the mori-zwanzig representation of irreversible processes. Proceedings of the National Academy of Sciences, 97(7):2968–2973, Mar. 2000.
[4] J. P. Hespanha. Stochastic hybrid systems: Application to communication networks. In Hybrid systems: computation and control, pages 387–401. Springer, 2004.
[5] K. Sen, M. Viswanathan, and G. Agha. On statistical model checking of stochastic systems. In K. Etessami and S. K. Rajamani, editors, Computer Aided Verification, number 3576 in Lecture Notes in Computer Science, pages 266–280. Springer Berlin Heidelberg, Jan. 2005.
[6] A. Singh and J. P. Hespanha. Stochastic hybrid systems for studying biochemical processes. Philosophical Transactions of the Royal Society of London A: Mathematical, Physical and Engineering Sciences, 368(1930):4995–5011, 2010.
[7] Y. Wang, N. Roohi, M. West, M. Viswanathan, and G. E. Dullerud. A mori-zwanzig and mitl based approach to statistical verification of continuous-time dynamical systems (to appear). In Proceedings of the 5th IFAC Workshop on Analysis and Design of Hybrid Systems, ADHS ’15, Atlanta, GA, USA, 2015.
[8] Y. Wang, N. Roohi, M. West, M. Viswanathan, and G. E. Dullerud. Statistical verification of dynamical systems using set oriented methods. In Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control, HSCC ’15, pages 169–178, New York, NY, USA, 2015. ACM.
Yu Wang and Geir E. Dullerud are with Coordinate Science Laboratory and the Department of Mechanical Science and Engineering, University of Illinois at Urbana-Champaign, Urbana, IL 61801 USA. Email: yuwang8@illinois.edu, dullerud@illinois.edu Nima Roohi and Mahesh Viswanathan are with the Department of Computer Science, University of Illinois at Urbana-Champaign, Urbana, IL 61801 USA. Email: roohi2@illinois.edu, vmahesh@illinois.edu Matthew West is with the Department of Mechanical Science and Engineering, University of Illinois at Urbana-Champaign, Urbana, IL 61801 USA. Email: mwest@illinois.edu The authors acknowledge support for this work from NSF CPS grant 1329991. Program Manager: Dr. David Corman.