Thomas Sturm
Ashish Tiwari
ABSTRACT
We present the application of real quantifier elimination to formal verification and synthesis of continuous and switched dynamical systems. Through a series of case studies, we show how first-order formulas over the reals arise when formally analyzing models of complex control systems. Existing off-the-shelf quantifier elimination procedures are not successful in eliminating quantifiers from many of our benchmarks. We therefore automatically combine three established software components: virtual subtitution based quantifier elimination in Reduce/Redlog, cylindrical algebraic decomposition implemented in Qepcad, and the simplifier Slfq implemented on top of Qepcad. We use this combination to successfully analyze various models of systems including adaptive cruise control in automobiles, adaptive flight control system, and the classical inverted pendulum problem studied in control theory.
- H. Anai. A symbolic-numeric approach to nonlinear dynamical system analysis, 2010. SIAM/MSRI workshop on hybrid method. for symb.-numeric comp.Google Scholar
- D. S. Arnon, G. E. Collins, and S. McCallum. Cylindrical algebraic decomposition I: The basic algorithm. SIAM J. Computing, 13(4):865--877, 1984. Google ScholarDigital Library
- S. Basu, R. Pollack, and M.-F. Roy. On the combinatorial and algebraic complexity of quantifier elimination. J. of the ACM, 43(6):1002--1045, 1996. Google ScholarDigital Library
- California PATH: Partners for advanced transit and highways. http://www.path.berkeley.edu/.Google Scholar
- S. Boyd, L. El Ghaoui, E. Feron, and V. Balakrishnan. Linear matrix inequalities in system and control theory. SIAM, 1994.Google Scholar
- C. W. Brown. QEPCAD B: a program for computing with semi-algebraic sets using CADs. ACM SIGSAM Bulletin, 37(4):97--108, 2003. Google ScholarDigital Library
- C. W. Brown and C. Gross. Efficient preprocessing methods for quantifier elimination. In CASC, volume 4194 of LNCS, pages 89--100. Springer-Verlag, 2006. Google Scholar
- G. E. Collins. Quantifier elimination for real closed fields by cylindrical algebraic decomposition -- preliminary report. ACM SIGSAM Bulletin, 8(3):80--90, Aug. 1974. Google ScholarDigital Library
- G. E. Collins and H. Hong. Partial cylindrical algebraic decomposition for quantifier elimination. J. Symbolic Computation, 12(3):299--328, Sept. 1991. Google ScholarDigital Library
- J. H. Davenport and J. Heintz. Real quantifier elimination is doubly exponential. J. of Symbolic Computation, 5(1-2):29--35, Feb.-Apr. 1988. Google ScholarDigital Library
- W. Decker et al. Singular 3-1-2 -- A computer algebra system for polynomial computations, 2010. http://www.singular.uni-kl.de.Google Scholar
- A. Dolzmann and T. Sturm. Redlog: Computer algebra meets computer logic. ACM SIGSAM Bulletin, 31(2):2--9, June 1997. Google ScholarDigital Library
- A. Dolzmann and T. Sturm. Simplification of quantifier-free formulae over ordered fields. J. of Symbolic Computation, 24(2):209--231, Aug. 1997. Google ScholarDigital Library
- A. Dolzmann, T. Sturm, and V. Weispfenning. A new approach for automatic theorem proving in real geometry. J. Automated Reasoning, 21(3), 1998. Google ScholarDigital Library
- D. Gayme, M. Fazel, and J. C. Doyle. Complexity in automation of SOS proofs: An illustrative example. In 45th IEEE Conf. on Decision and Control, 2006.Google ScholarCross Ref
- D. Godbole and J. Lygeros. Longitudinal control of the lead car of a platoon. IEEE Transactions on Vehicular Technology, 43(4):1125--35, 1994.Google ScholarCross Ref
- D. Grigoriev. Complexity of deciding Tarski algebra. Journal of Symbolic Computation, 5(1-2):65--108, 1988. Google ScholarDigital Library
- S. Gulwani and A. Tiwari. Constraint-based approach for analysis of hybrid systems. In Proc. 20th CAV, volume 5123 of LNCS, pages 190--203. Springer, 2008. Google Scholar
- H. Hong and M. Safey El Din. Variant real quantifier elimination: algorithm and application. In ISSAC, pages 183--190. ACM, 2009. Google ScholarDigital Library
- M. Jirstrand. Nonlinear control system design by quantifier elimination. J. Symb. Comput., 24(2):137--152, 1997. Google ScholarDigital Library
- G. Lafferriere, G. J. Pappas, and S. Yovine. Symbolic reachability computations for families of linear vector fields. J. Symbolic Computation, 32(3):231--253, 2001. Google ScholarDigital Library
- P. A. Parrilo. SOS methods for semi-algebraic games and optimization. In HSCC 2005, volume 3414 of LNCS, page 54. Springer, 2005. Google Scholar
- S. Prajna, A. Jadbabaie, and G. J. Pappas. A framework for worst-case and stochastic safety verification using barrier certificates. IEEE Trans. on Automatic Control, 52(8):1415--1428, 2007.Google ScholarCross Ref
- A. Puri and P. Varaiya. Driving safely in smart cars. In Proc. 1995 American Control Conference, 1995.Google ScholarCross Ref
- J. Renegar. On the computational complexity and geometry of the first-order theory of the reals. Journal of Symbolic Computation, 13(3):255--352, Mar. 1992.Google ScholarDigital Library
- S. Sankaranarayanan, H. Sipma, and Z. Manna. Constructing invariants for hybrid systems. In HSCC, volume 2993 of LNCS, pages 539--554. Springer, 2004.Google Scholar
- A. Taly, S. Gulwani, and A. Tiwari. Synthesizing switching logic using constraint solving. In VMCAI, volume 5403 of LNCS, pages 305--319. Springer, 2009. Google Scholar
- A. Taly and A. Tiwari. Deductive verification of continuous dynamical systems. In FSTTCS, volume 4 of LIPIcs, pages 383--394, 2009.Google Scholar
- A. Taly and A. Tiwari. Switching logic synthesis for reachability. In EMSOFT, 2010. Google ScholarDigital Library
- A. Tiwari. Approximate reachability for linear systems. In Proc. 6th HSCC, volume 2623 of LNCS, pages 514--525. Springer, 2003. Google Scholar
- A. Tiwari. Bounded verification of adaptive flight control systems. In Proc. AIAA Infotech@Aerospace, 2010. AIAA-2010-3362.Google ScholarCross Ref
- A. Tiwari. Certificate-based verification: Tools and benchmarks, 2011. http://www.csl.sri.com/ tiwari/existsforall/.Google Scholar
- A. Tiwari and G. Khanna. Series of abstractions for hybrid automata. In HSCC, volume 2289 of LNCS, pages 465--478. Springer, 2002. Google ScholarDigital Library
- C. J. Tomlin, I. Mitchell, A. M. Bayen, and M. Oishi. Computational techniques for the verification of hybrid systems. Proc. of the IEEE, 91(7), 2003.Google ScholarCross Ref
- V. Weispfenning. The complexity of linear problems in fields. J. of Symbolic Computation, 5(1&2):3--27, 1988. Google ScholarDigital Library
- V. Weispfenning. Quantifier elimination for real algebra-the cubic case. In Proc. ISSAC, pages 258--263. ACM Press, New York, 1994. Google ScholarDigital Library
- V. Weispfenning. Quantifier elimination for real algebra-the quadratic case and beyond. Applicable Alg. in Eng. Comm. Comp., 8(2):85--101, 1997.Google ScholarCross Ref
Index Terms
- Verification and synthesis using real quantifier elimination
Recommendations
Formal verification of ASMs using MDGs
We present a framework for the formal verification of abstract state machine (ASM) designs using the multiway decision graphs (MDG) tool. ASM is a state based language for describing transition systems. MDG provides symbolic representation of transition ...
Paxos made EPR: decidable reasoning about distributed protocols
Distributed protocols such as Paxos play an important role in many computer systems. Therefore, a bug in a distributed protocol may have tremendous effects. Accordingly, a lot of effort has been invested in verifying such protocols. However, checking ...
Comments