logo

SCIENTIA SINICA Informationis, Volume 47 , Issue 3 : 288-309(2017) https://doi.org/10.1360/N112016-00042

Composed IIS path locating based optimization for bounded \\reachability analysis of compositional linear hybrid systems}{Composed IIS path locating based optimization for bounded reachability analysis of compositional linear hybrid systems

More info
  • ReceivedMar 2, 2016
  • AcceptedMay 31, 2016
  • PublishedSep 14, 2016

Abstract


Funded by

国家重点基础研究发展计划(973)

(2014CB340703)

国家自然科学基金(61561146394)

国家自然科学基金(61572249)

国家自然科学基金(61321491)


References

[1] Clarke E, Grumberg O, Peled D. Model Checking. Cambridge: MIT Press, 1999. Google Scholar

[2] Henzinger T A. The theory of hybrid automata. In: Proceedings of the 11st Annual IEEE Symposium on Logic in Computer Science, New Brunswick, 1996. 278-292. Google Scholar

[3] Henzinger T A, Kopke P W, Puri A, et al. What's decidable about hybrid automata? J Comput Syst Sci, 1998, 57: 94-124. Google Scholar

[4] Henzinger T A, Ho P H, Wong-Toi H. HYTECH: a model checker for hybrid systems. Softw Tools Techn Transfer, 1997, 1: 110-122. Google Scholar

[5] Frehse G. PHAVer: algorithmic verification of hybrid systems past HyTech. In: Hybrid Systems: Computation and Control. Berlin: Springer, 2005. 258-273. Google Scholar

[6] Frehse G, Guernic C L, Donzé A, et al. SpaceEx: scalable verification of hybrid systems. In: Computer Aided Verification. Berlin: Springer, 2011. 379-395. Google Scholar

[7] Biere A, Cimatti A, Clarke E, et al. Bounded model checking. Advance Comput, 2003, 58: 118-149. Google Scholar

[8] Barrett C W, Sebastiani R, Seshia S, et al. Satisifiability modulo theories. Handbook of Satisfiability, 2009, 185: 825-885. Google Scholar

[9] Audemard G, Bozzano M, Cimatti A, et al. Verifying industrial hybrid systems with MathSAT. Electron Notes Theor Comput Sci, 2005, 119: 17-32 CrossRef Google Scholar

[10] de Moura L, Bj{\o}rner N. Z3: an efficient SMT solver. In: Tools and Algorithms for the Construction and Analysis of Systems. Berlin: Springer, 2008. 337-340. Google Scholar

[11] Li X D, Jha S K, Bu L. Towards an efficient path-oriented tool for bounded reachability analysis of linear hybrid systems using linear programming. Electron Notes Theor Comput Sci, 2007, 174: 57-70. Google Scholar

[12] Bu L, Li Y, Wang L Z, et al. BACH 2: bounded reach ability checker for compositional linear hybrid systems. In: Proceedings of the 13th Design Automation & Test in Europe Conference, Leuven, 2010. 1512-1517. Google Scholar

[13] Xie D B, Bu L, Zhao J H, et al. SAT-LP-IIS joint-directed path-oriented bounded reachability analysis of linear hybrid automata. Formal Methods Syst Design, 2014, 45: 42-62 CrossRef Google Scholar

[14] Bu L, Yang Y, Li X D. IIS-guided DFS for efficient bounded reachability analysis of linear hybrid automata. In: Proceedings of the 7th International Haifa Verification Conference, Haifa, 2011. 35-49. Google Scholar

[15] Mark L, Ammar M. Enumerating infeasibility: finding multiple MUSes quickly. In: Proceedings of the 10th International Conference on Integration of Artificial Intelligence and Operations Research Techniques in Constraint Programming, Yorktown Heights, 2013. 160-175. Google Scholar

[16] Bu L, Li Y, Wang L Z, et al. BACH: bounded reachability checker for linear hybrid automata. In: Proceedings of the 8th International Conference on Formal Methods in Computer Aided Design, Portland, 2008. 65-68. Google Scholar

[17] Cimatti A, Griggio A, Mover S, et al. HyComp: an SMT-based model checker for hybrid systems. In: Tools and Algorithms for the Construction and Analysis of Systems. Berlin: Springer, 2015. 52-67. Google Scholar

[18] Bu L, Li X D. Path-oriented bounded reachability analysis of composed linear hybrid systems. Int J Softw Tools Tech Transfer, 2011, 13: 307-317 CrossRef Google Scholar

[19] Chinneck J, Dravnieks E. Locating minimal infeasible constraint sets in linear programs. ORSA J Comput, 1991, 3: 157-168 CrossRef Google Scholar

[20] Biere A, Clarke E, Zhu Y S. Symbolic model checking without BDDs. In: Tools and Algorithms for the Construction and Analysis of Systems. Berlin: Springer, 1999. 193-207. Google Scholar

[21] Xie D B, Bu L, Li X D. Deriving unbounded proof of linear hybrid automata from bounded verification. In: Proceedings of Real-Time Systems Symposium (RTSS), Rome, 2014. 128-137. Google Scholar

[22] Zhao J H, Li X D, Zheng T, et al. Removing irrelevant atomic formulas for checking timed automata efficiently.\linebreak In: Formal Modeling and Analysis of Timed Systems. Berlin: Springer, 2004. 34-45. Google Scholar

[23] Jha S, Krogh B H, Weimer J E, et al. Reachability for linear hybrid automata using iterative relaxation abstraction. In: Hybrid Systems: Computation and Control. Berlin: Springer, 2007. 287-300. Google Scholar

[24] Wang F. Symbolic parametric safety analysis of linear hybrid systems with BDD-like data structures. IEEE Trans Softw Eng, 2005, 31: 38-51 CrossRef Google Scholar

[25] Bu L, Cimatti A, Li X D, et al. Model checking of hybrid systems using shallow synchronzation. In: Formal Techniques for Distributed Systems. Berlin: Springer, 2010. 155-169. Google Scholar

[26] Heljabko K, Niemala I. Bounded LTL model checking with stable models. In: Theory and Practice of Logic Programming. Cambridge: Cambridge University Press, 2003. 519-550. Google Scholar