Loop reduction techniques for reachability analysis of linear hybrid automata
详细信息 查看全文
- 作者：MinXue Pan (1)
You Li (1)
Lei Bu (1)
XuanDong Li (1) - 关键词：real ; time and hybrid systems ; linear hybrid automata ; reachability analysis
- 刊名：SCIENCE CHINA Information Sciences
- 出版年：2012
- 出版时间：December 2012
- 年：2012
- 卷：55
- 期：12
- 页码：2663-2674
- 全文大小：382KB
- 参考文献：1. Henzinger T A. The theory of hybrid automata. In: Proceedings of the 11th Annual IEEE Symposium on Logic in Computer Science, New Brunswick, 1996. 278鈥?92
2. Asarin E, Maler O, Pnueli A. Reachability analysis of dynamical systems having piecewise-constant derivatives. Theor Comput Sci, 1995, 138: 35鈥?5 CrossRef
3. Alur R, Courcoubetis C, Halbwachs N, et al. The algorithmic analysis of hybrid systems. Theor Comput Sci, 1995, 138: 3鈥?4 CrossRef
4. Alur R, Henzinger T A, Ho P H. Automatic symbolic verification of embedded systems. IEEE Trans Softw Eng, 1996, 22: 181鈥?01 CrossRef
5. Silva B I, Richeson K, Krogh B, et al. Modeling and verification of hybrid dynamical system using checkmate. In: Proceedings of the 4th International Conference on Automation of Mixed Processes: Hybrid Dynamic Systems. Dortmund, 2000. 323鈥?28
6. Asarin E, Dang T, Maler O. The d/dt tool for verification of hybrid systems. In: Brinksma E, Larsen K, eds. Computer Aided Verification. Lecture Notes in Computer Science, Vol 2404. Berlin: Springer, 2002. 746鈥?70
7. Henzinger T A, Ho P H, Wong-Toi H. HyTech: A model checker for hybrid systems. Int J Softw Tools Technol Transf, 1997, 1: 110鈥?22 CrossRef
8. Frehse G. Phaver: algorithmic verification of hybrid systems past HyTech. Int J Softw Tools Technol Transf, 2008, 10: 263鈥?79 CrossRef
9. Asarin E, Dang T, Frehse G, et al. Recent progress in continuous and hybrid reachability analysis. In: IEEE International Symposium on Computer Aided Control System Design. Washington, DC: IEEE, 2006. 1582鈥?587
10. Fr盲nzle M, Herde C. HySat: An efficient proof engine for bounded model checking of hybrid systems. Form Methods Syst Des, 2007, 30: 179鈥?98 CrossRef
11. Audemard G, Bozzano M, Cimatti A, et al. Verifying industrial hybrid systems with MathSAT. Electron Notes Theor Comput Sci, 2005, 119: 17鈥?2 CrossRef
12. Bu L, Li Y, Wang L, et al. BACH: Bounded reachability checker for linear hybrid automata. In: 8th International Conference on Formal Methods in Computer Aided Design, Portland, 2008. 65鈥?8
13. Bu L, Li X. Path-oriented bounded reachability analysis of composed linear hybrid systems. Int J Softw Tools Technol Transf, 2011, 13: 307鈥?17 CrossRef
14. Henzinger T A, Ho P H, and Wong-Toi H. HyTech: the next generation. In: 16th IEEE Real-Time Systems Symposium. Washington, DC: IEEE, 1995. 56鈥?5 CrossRef
15. Henzinger T A, Horowitz B, Majumdar R, et al. Beyond HyTech: Hybrid systems analysis using interval numerical methods. In: Lynch N, Krogh B, eds. Hybrid Systems: Computation and Control. Lecture Notes in Computer Science, Vol 1790. Berlin: Springer, 2000, 130鈥?44 CrossRef
16. Bagnara R, Ricci E, Zaffanella E, et al. Possibly not closed convex polyhedra and the parma polyhedra library. In: Hermenegildo M and Puebla G, eds. Static Analysis. Lecture Notes in Computer Science, Vol 2477. Berlin: Springer, 2002, 213鈥?29 CrossRef
17. Stursberg O, Krogh H. Efficient representation and computation of reachable sets for hybrid systems. In: Maler O, Pnueli A, eds. Hybrid Systems: Computation and Control. Lecture Notes in Computer Science, Vol 2623. Berlin: Springer, 2003. 482鈥?97 CrossRef
18. Halbwachs N, Proy Y, Raymond P. Verification of linear hybrid systems by means of convex approximations. In: Le Charlier B, ed. Static Analysis. Lecture Notes in Computer Science, Vol 864. Berlin: Springer, 1994. 223鈥?37 CrossRef
19. Henzinger T A, Ho P H. A note on abstract interpretation strategies for hybrid automata. In: Antsaklis P, Kohn W, Nerode A, eds. Hybrid Systems II. Lecture Notes in Computer Science, Vol 999. Berlin: Springer, 1995. 252鈥?64 CrossRef
20. Asarin E, Dang T, Maler O, et al. Approximate reachability analysis of piecewise-linear dynamical systems. In: Lynch N, Krogh B, eds. Hybrid Systems: Computation and Control. Lecture Notes in Computer Science, Vol 1790. Berlin: Springer, 2000. 20鈥?1 CrossRef
21. Chinneck J W, Dravnieks E W. Locating minimal infeasible constraint sets in linear programs. ORSA J Comput, 1991, 3: 157鈥?68 CrossRef
22. Kesten Y, Pnueli A, Sifakis J, et al. Decidable integration graphs. Inf Comput, 1999, 150: 209鈥?43 CrossRef
23. Alur R, Courcoubetis C, Henzinger T A. Computing accumulated delays in real-time systems. Form Methods Syst Des, 1997, 11: 137鈥?55 CrossRef
24. Henzinger T A, Kopke P W, Puri A, et al. What鈥檚 decidable about hybrid automata? J Comput Syst Sci, 1998, 57: 94鈥?24 CrossRef
25. Li X, Zhao J, Yu P, et al. Positive loop-closed automata: a decidable class of hybrid systems. J Logic Algebr Program, 2002: 79鈥?08
26. Damm W, Ihlemann C, Sofronie-Stokkermans V. Decidability and complexity for the verification of safety properties of reasonable linear hybrid automata. In: Proceedings of the 14th International Conference on Hybrid Systems: Computation and Control. New York: ACM, 2011. 73鈥?2 - 作者单位：MinXue Pan (1)
You Li (1)
Lei Bu (1)
XuanDong Li (1)
1. State Key Laboratory for Novel Software Technology, Department of Computer Science and Technology, Nanjing University, Nanjing, 210093, China - ISSN：1869-1919
文摘
The problem of reachability analysis of linear hybrid automata (LHA) is very difficult. This paper considers to improve the efficiency of the reachability analysis by optimizing the structures of LHA. We identify two types of loops called the flexible loops and the zero loops, and present the techniques to replace the repetitions of those loops in the behavior of LHA with finite sequences of locations and in the meantime simplify the associated constraints. The techniques work not only for the polyhedral computing based algorithms but also for the bounded model checkers.