Advertisement

IIS-Guided DFS for Efficient Bounded Reachability Analysis of Linear Hybrid Automata

  • Lei Bu
  • Yang Yang
  • Xuandong Li
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 7261)

Abstract

In the authors’ previous work, we proposed a linear programming (LP) based approach to check the reachability specification along one abstract path in a linear hybrid automaton (LHA) at a time by translating the reachability problem into the satisfiability problem of a linear constraint set. Then a depth-first-search (DFS) is deployed on the graph structure of the LHA to check all the paths with length in the threshold to answer the question of bounded reachability.

In this DFS-style bounded model checking (BMC) algorithm, once a path is found to be infeasible by the underlying LP solver, a backtracking on the graph structure will be conducted. Clearly, the efficiency of the algorithm depends on the accuracy of the backtracking. If the DFS can backtrack to the most reasonable location, the state space need to search and verify can be reduced significantly.

Fortunately, once a linear constraint set is judged to be unsatisfiable, the irreducible infeasible set (IIS) technique can be deployed on the unsatisfiable constraint set to give a quick analysis and find a small set of constraints which makes the whole program unsatisfiable. In this paper, we adopt this technique into our DFS-style BMC of LHA to locate the nodes and transitions which make the path under verification infeasible to guide the backtracking and answer the bounded reachability of LHA more efficiently.

Keywords

Path Segment Symbolic Model Check Reachability Problem Candidate Path Bound Model Check 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    Henzinger, T.A.: The theory of hybrid automata. In: Proceedings of LICS 1996, pp. 278–292. IEEE Computer Society (1996)Google Scholar
  2. 2.
    Henzinger, T.A., Kopke, P.W., Puri, A., Varaiya, P.: What’s Decidable About Hybrid Automata? Journal of Computer and System Sciences 57, 94–124 (1998)MathSciNetzbMATHCrossRefGoogle Scholar
  3. 3.
    Henzinger, T.A., Ho, P.-H., Wong-Toi, H.: Algorithmic Analysis of Nonlinear Hybrid Systems. IEEE Transactions on Automatic Control, 540–554 (1998)Google Scholar
  4. 4.
    Alur, R., Courcoubetis, C., Halbwachs, N., Henzinger, T.A., Ho, P.-H., Nicollin, X., Olivero, A., Sifakis, J., Yovine, S.: The algorithmic analysis of hybrid systems. Theoretical Computer Science 138, 3–34 (1995)MathSciNetzbMATHCrossRefGoogle Scholar
  5. 5.
    Biere, A., Cimatti, A., Clarke, E., Strichman, O., Zhu, Y.: Bounded Model Checking. In: Advance in Computers, vol. 58, pp. 118–149. Academic Press (2003)Google Scholar
  6. 6.
    Fränzle, M., Herde, C., Ratschan, S., Schubert, T., Teige, T.: Efficient solving of large non-linear arithmetic constraint systems with complex boolean structure. Journal on Satisfiability, Boolean Modeling and Computation 1, 209–236 (2007)Google Scholar
  7. 7.
    Audemard, G., Bozzano, M., Cimatti, A., Sebastiani, R.: Verifying Industrial Hybrid Systems with MathSAT. In: Proceedings of BMC 2004, ENTCS, vol. 119(2), pp. 17–32. Elsevier Science (2005)Google Scholar
  8. 8.
    Li, X., Jha, S.K., Bu, L.: Towards an Efficient Path-Oriented Tool for Bounded Reachability Analysis of Linear Hybrid Systems using Linear Programming. In: Proceedings of BMC 2006, ENTCS, vol. 174(3), pp. 57–70. Elsevier Science, 07 (2006)Google Scholar
  9. 9.
    Bu, L., Li, Y., Wang, L., Li, X.: BACH: Bounded Reachability Checker for Linear Hybrid Automata. In: Proceedings of the 8th International Conference on Formal Methods in Computer Aided Design, pp. 65–68. IEEE Computer Society (2008)Google Scholar
  10. 10.
    Henzinger, T.A., Ho, P.-H., Wong-Toi, H.: HYTECH: a model checker for hybrid systems. Software Tools for Technology Transfer 1, 110–122 (1997)zbMATHCrossRefGoogle Scholar
  11. 11.
    Frehse, G.: PHAVer: Algorithmic Verification of Hybrid Systems Past HyTech. In: Morari, M., Thiele, L. (eds.) HSCC 2005. LNCS, vol. 3414, pp. 258–273. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  12. 12.
    Chinneck, J., Dravnieks, E.: Locating minimal infeasible constraint sets in linear programs. ORSA Journal on Computing 3, 157–168 (1991)zbMATHCrossRefGoogle Scholar
  13. 13.
    Bu, L., Li, X.: Path-Oriented Bounded Reachability Analysis of Composed Linear Hybrid Systems. Software Tools Technology Transfer 13(4), 307–317 (2011)MathSciNetCrossRefGoogle Scholar
  14. 14.
    Bu, L., Li, Y., Wang, L., Chen, X., Li, X.: BACH 2: Bounded ReachAbility CHecker for Compositional Linear Hybrid Systems. In: Proceedings of the 13th Design Automation & Test in Europe Conference, Dresden, Germany, pp. 1512–1517 (2010)Google Scholar
  15. 15.
  16. 16.
    Chinneck, J.: MINOS(IIS): Infeasibility analysis using MINOS. Computers and Operations Research 21(1), 1–9 (1994)zbMATHCrossRefGoogle Scholar
  17. 17.
  18. 18.
  19. 19.
    Jha, S., Krogh, B.H., Weimer, J.E., Clarke, E.M.: Reachability for Linear Hybrid Automata Using Iterative Relaxation Abstraction. In: Bemporad, A., Bicchi, A., Buttazzo, G. (eds.) HSCC 2007. LNCS, vol. 4416, pp. 287–300. Springer, Heidelberg (2007)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2012

Authors and Affiliations

  • Lei Bu
    • 1
  • Yang Yang
    • 1
  • Xuandong Li
    • 1
  1. 1.State Key Laboratory for Novel Software TechnologyNanjing UniversityNanjingP.R. China

Personalised recommendations