Computing differential invariants of hybrid systems as fixedpoints

Alur R, Pappas GJ (eds) (2004) Hybrid systems: computation and control, Proceedings of the 7th International Workshop, HSCC 2004, Philadelphia, PA, USA, March 25–27, 2004. LNCS, vol 2993. Springer, Berlin

Anai H, Weispfenning V (2001) Reach set computations using real quantifier elimination. In: Benedetto MDD, Sangiovanni-Vincentelli AL (eds) HSCC. LNCS, vol 2034. Springer, Berlin, pp 63–76. doi: 10.1007/3-540-45351-2_9

Asarin E, Dang T, Girard A (2003) Reachability analysis of nonlinear systems using conservative approximation. In: Maler O, Pnueli A (eds) HSCC. LNCS, vol 2623. Springer, Berlin, pp 20–35. doi: 10.1007/3-540-36580-X_5

Chutinan A, Krogh BH (2003) Computational techniques for hybrid system verification. IEEE Trans Autom Control 48(1):64–75. doi: 10.1109/TAC.2002.806655

Clarke EM (1979) Program invariants as fixedpoints. Computing 21(4):273–294. doi: 10.1007/BF02248730

Collins GE, Hong H (1991) Partial cylindrical algebraic decomposition for quantifier elimination. J Symb Comput 12(3):299–328. doi: 10.1016/S0747-7171(08)80152-6

Damm W, Hungar H, Olderog ER (2006) Verification of cooperating traffic agents. Int J Control 79(5):395–421

Damm W, Pinto G, Ratschan S (2005) Guaranteed termination in the verification of LTL properties of non-linear robust discrete time hybrid systems. In: Peled D, Tsay YK (eds) ATVA. LNCS, vol 3707. Springer, Berlin, pp 99–113. doi: 10.1007/11562948_10

Davoren JM, Nerode A (2000) Logics for hybrid systems. IEEE 88(7):985–1010. doi: 10.1109/5.871305

Donzé A, Maler O (2004) Systematic simulation using sensitivity analysis. In: Bemporad A et al. (eds) Hybrid systems: computation and control, Proceedings of the 10th international conference, HSCC 2007, Pisa, Italy. LNCS, vol 4416. Springer, Berlin, pp 174–189. doi: 10.1007/978-3-540-71493-4_16

Dowek G, Muñoz C, Carreño VA (2005) Provably safe coordinated strategy for distributed conflict resolution. In: Proceedings of the AIAA guidance navigation, and control conference and exhibit 2005, AIAA-2005-6047

Fränzle M (1999) Analysis of hybrid systems: an ounce of realism can save an infinity of states. In: Flum J, Rodríguez-Artalejo M (eds) CSL. LNCS, vol 1683. Springer, Berlin, pp 126–140

Frehse G (2005) PHAVer: Algorithmic verification of hybrid systems past HyTech. In: Morari M, Thiele L (eds) Hybrid systems: computation and control, Proceedings of the 8th international workshop, HSCC 2005, Zurich, Switzerland, March 9–11, 2005. LNCS, vol 3414. Springer, Berlin, pp 258–273. doi: 10.1007/b106766

Gulwani S, Tiwari A (2008) Constraint-based approach for analysis of hybrid systems. In: Gupta A, Malik S (eds) Proceedings computer aided verification, CAV 2008, Princeton, NJ, USA. LNCS, vol 5123. Springer, Berlin, pp 190–203. doi: 10.1007/978-3-540-70545-1

Harel D, Kozen D, Tiuryn J (2000) Dynamic logic. MIT Press, Cambridge

Henzinger TA (1996) The theory of hybrid automata. In: LICS. IEEE Computer Society, Los Alamitos, pp 278–292

Henzinger TA, Ho PH, Wong-Toi H (1997) HyTech: a model checker for hybrid systems. In: Grumberg O (ed) CAV. LNCS, vol 1254. Springer, Berlin, pp 460–463

Hwang I, Kim J, Tomlin C (2007) Protocol-based conflict resolution for air traffic control. Air Traffic Control Q 15(1):1–34

Lanotte R, Tini S (2005) Taylor approximation for hybrid systems. In: Morari M, Thiele L (eds) Hybrid systems: computation and control, Proceedings of the 8th international workshop, HSCC 2005, Zurich, Switzerland, March 9–11, 2005. LNCS, vol 3414. Springer, Berlin, pp 402–416. doi: 10.1007/b106766

Mansfield EL (1991) Differential Gröbner bases. PhD thesis, University of Sydney

Massink M, Francesco ND (2001) Modelling free flight with collision avoidance. In: Andler SF, Offutt J (eds) ICECCS. IEEE Computer Society, Los Alamitos, pp 270–280. doi: 10.1109/ICECCS.2001.930186

Parrilo PA (2003) Semidefinite programming relaxations for semialgebraic problems. Math Program 96(2):293–320. doi: 10.1007/s10107-003-0387-5

Piazza C, Antoniotti M, Mysore V, Policriti A, Winkler F, Mishra B (2005) Algorithmic algebraic model checking, I: challenges from systems biology. In: Etessami K, Rajamani SK (eds) CAV. LNCS, vol 3576. Springer, Berlin, pp 5–19. doi: 10.1007/11513988_3

Platzer A (2008) Differential-algebraic dynamic logic for differential-algebraic programs. J Log Comput. doi: 10.1093/logcom/exn070

Platzer A (2008) Differential dynamic logic for hybrid systems. J Autom Reas 41(2):143–189. doi: 10.1007/s10817-008-9103-8

Platzer A, Clarke EM (2007) The image computation problem in hybrid systems model checking. In: Bemporad A et al. (eds) Hybrid systems: computation and control, Proceedings of the 10th international conference, HSCC 2007, Pisa, Italy. LNCS, vol 4416. Springer, Berlin, pp 473–486. doi: 10.1007/978-3-540-71493-4_37

Platzer A, Clarke EM (2008) Computing differential invariants of hybrid systems as fixedpoints. In: Gupta A, Malik S (eds) Proceedings computer aided verification, CAV 2008, Princeton, NJ, USA. LNCS, vol 5123. Springer, Berlin, pp 176–189. doi: 10.1007/978-3-540-70545-1_17

Platzer A, Clarke EM (2008) Computing differential invariants of hybrid systems as fixedpoints. Tech Rep CMU-CS-08-103, School of Computer Science, Carnegie Mellon University, Pittsburgh, PA

Platzer A, Quesel JD (2008) KeYmaera: A hybrid theorem prover for hybrid systems. In: Armando A, Baumgartner P, Dowek G (eds) IJCAR. LNCS, vol 5195. Springer, Berlin, pp 171–178. doi: 10.1007/978-3-540-71070-7_15

Platzer A, Quesel JD (2008) Logical verification and systematic parametric analysis in train control. In: Egerstedt M, Mishra B (eds) HSCC. LNCS, vol 4981. Springer, Berlin, pp 646–649. doi: 10.1007/978-3-540-78929-1_55

Prajna S, Jadbabaie A (2004) Safety verification of hybrid systems using barrier certificates. In: Alur R, Pappas GJ (eds) Hybrid systems: computation and control, Proceedings of the 7th international workshop, HSCC 2004, Philadelphia, PA, USA, March 25–27, 2004. LNCS, vol 2993. Springer, Berlin, pp 477–492. doi: 10.1007/b96398

Prajna S, Jadbabaie A, Pappas GJ (2007) A framework for worst-case and stochastic safety verification using barrier certificates. IEEE Trans Autom Control 52(8):1415–1429. doi: 10.1109/TAC.2007.902736

Rodríguez-Carbonell E, Tiwari A (2005) Generating polynomial invariants for hybrid systems. In: Morari M, Thiele L (eds) Hybrid systems: computation and control, Proceedings of the 8th international workshop, HSCC 2005, Zurich, Switzerland, March 9–11, 2005. LNCS, vol 3414. Springer, Berlin, pp 590–605. doi: 10.1007/b106766

Sankaranarayanan S, Sipma H, Manna Z (2004) Constructing invariants for hybrid systems. In: Alur R, Pappas GJ (eds) Hybrid systems: computation and control, Proceedings of the 7th international workshop, HSCC 2004, Philadelphia, PA, USA, March 25–27, 2004. LNCS, vol 2993. Springer, Berlin, pp 539–554. doi: 10.1007/b96398

Tomlin C, Pappas GJ, Sastry S (1998) Conflict resolution for air traffic management: a study in multi-agent hybrid systems. IEEE Trans Autom Control 43(4):509–521. doi: 10.1109/9.664154