{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,30]],"date-time":"2026-01-30T02:54:19Z","timestamp":1769741659786,"version":"3.49.0"},"reference-count":25,"publisher":"Association for Computing Machinery (ACM)","issue":"S2","license":[{"start":{"date-parts":[[2012,8,1]],"date-time":"2012-08-01T00:00:00Z","timestamp":1343779200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Embed. Comput. Syst."],"published-print":{"date-parts":[[2012,8]]},"abstract":"<jats:p>\n            This article introduces Periodically Controlled Hybrid Automata (PCHA) for modular specification of embedded control systems. In a PCHA,\n            <jats:italic>control<\/jats:italic>\n            actions that change the control input to the plant occur roughly periodically, while other actions that update the state of the controller may occur in the interim. Such actions could model, for example, sensor updates and information received from higher-level planning modules that change the set point of the controller. Based on periodicity and subtangential conditions, a new sufficient condition for verifying invariant properties of PCHAs is presented. For PCHAs with polynomial continuous vector fields, it is possible to check these conditions automatically using, for example, quantifier elimination or sum of squares decomposition. We examine the feasibility of this automatic approach on a small example. The proposed technique is also used to manually verify safety and progress properties of a fairly complex planner-controller subsystem of an autonomous ground vehicle. Geometric properties of planner-generated paths are derived which guarantee that such paths can be safely followed by the controller.\n          <\/jats:p>","DOI":"10.1145\/2331147.2331163","type":"journal-article","created":{"date-parts":[[2012,9,11]],"date-time":"2012-09-11T22:21:06Z","timestamp":1347402066000},"page":"1-24","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":16,"title":["Verification of Periodically Controlled Hybrid Systems"],"prefix":"10.1145","volume":"11","author":[{"given":"Tichakorn","family":"Wongpiromsarn","sequence":"first","affiliation":[{"name":"California Institute of Technology"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sayan","family":"Mitra","sequence":"additional","affiliation":[{"name":"University of Illinois at Urbana Champaign"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andrew","family":"Lamperski","sequence":"additional","affiliation":[{"name":"California Institute of Technology"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Richard M.","family":"Murray","sequence":"additional","affiliation":[{"name":"California Institute of Technology"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2012,8]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(94)00202-T"},{"key":"e_1_2_1_2_1","volume-title":"Lecture Notes in Mathematics","volume":"35","author":"Bhatia N. P.","unstructured":"Bhatia , N. P. and Szeg\u00f6 , G. P . 1967. Dynamical systems: Stability theory and applications . Lecture Notes in Mathematics , vol. 35 . Springer-Verlag, Berlin. Bhatia, N. P. and Szeg\u00f6, G. P. 1967. Dynamical systems: Stability theory and applications. Lecture Notes in Mathematics, vol. 35. Springer-Verlag, Berlin."},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/968708.968710"},{"key":"e_1_2_1_4_1","doi-asserted-by":"crossref","unstructured":"Burdick J. W. DuToit N. Howard A. Looman C. Ma J. Murray R. M. and Wongpiromsarn T. 2007. Sensing navigation and reasoning technologies for the DARPA Urban Challenge. Tech. rep. DARPA Urban Challenge Final Report. Burdick J. W. DuToit N. Howard A. Looman C. Ma J. Murray R. M. and Wongpiromsarn T. 2007. Sensing navigation and reasoning technologies for the DARPA Urban Challenge. Tech. rep. DARPA Urban Challenge Final Report.","DOI":"10.21236\/ADA475519"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-85778-5_16"},{"key":"e_1_2_1_6_1","volume-title":"Proceedings of the International Workshop on Intelligent Vehicle Control Systems (IVCS).","author":"DuToit N. E.","unstructured":"DuToit , N. E. , Wongpiromsarn , T. , Burdick , J. W. , and Murray , R. M . 2008. Situational reasoning for road driving in an urban environment . In Proceedings of the International Workshop on Intelligent Vehicle Control Systems (IVCS). DuToit, N. E., Wongpiromsarn, T., Burdick, J. W., and Murray, R. M. 2008. Situational reasoning for road driving in an urban environment. In Proceedings of the International Workshop on Intelligent Vehicle Control Systems (IVCS)."},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.automatica.2008.08.008"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-70545-1_18"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/225058.225162"},{"key":"e_1_2_1_10_1","doi-asserted-by":"crossref","unstructured":"Kaynar D. K. Lynch N. Segala R. and Vaandrager F. 2005. The Theory of Timed I\/O Automata. Synthesis Lectures on Computer Science. Morgan Claypool. Also available as Tech. rep. MIT-LCS-TR-917. Kaynar D. K. Lynch N. Segala R. and Vaandrager F. 2005. The Theory of Timed I\/O Automata . Synthesis Lectures on Computer Science. Morgan Claypool. Also available as Tech. rep. MIT-LCS-TR-917.","DOI":"10.1007\/978-3-031-01794-0"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/11730637_26"},{"key":"e_1_2_1_12_1","doi-asserted-by":"crossref","unstructured":"Lafferriere G. Pappas G. J. and \n      Yovine S\n  . \n  1999\n  . A new class of decidable hybrid systems. In Hybrid Systems: Computation and Control F. W. Vaandrager and J. H. van Schuppen Eds. Lecture Notes in Computer Science vol. \n  1569\n  . \n  Springer Berlin 137--151. Lafferriere G. Pappas G. J. and Yovine S. 1999. A new class of decidable hybrid systems. In Hybrid Systems: Computation and Control F. W. Vaandrager and J. H. van Schuppen Eds. Lecture Notes in Computer Science vol. 1569. Springer Berlin 137--151.","DOI":"10.1007\/3-540-48983-5_15"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0890-5401(03)00067-1"},{"key":"e_1_2_1_15_1","doi-asserted-by":"crossref","unstructured":"Mitra S. Wang Y. Lynch N. and \n      Feron E\n  . \n  2003\n  . Safety verification of model helicopter controller using hybrid Input\/Output automata. In Hybrid Systems: Computation and Control O. Maler and A. Pnueli Eds. Lecture Notes in Computer Science vol. \n  2623 Springer Berlin 343--358. Mitra S. Wang Y. Lynch N. and Feron E. 2003. Safety verification of model helicopter controller using hybrid Input\/Output automata. In Hybrid Systems: Computation and Control O. Maler and A. Pnueli Eds. Lecture Notes in Computer Science vol. 2623 Springer Berlin 343--358.","DOI":"10.1007\/3-540-36580-X_26"},{"key":"e_1_2_1_16_1","volume-title":"Proceedings of the International Conference on Computer-Aided Verification (CAV\u201996)","volume":"1102","author":"Owre S.","unstructured":"Owre , S. , Rajan , S. , Rushby , J. , Shankar , N. , and Srivas , M . 1996. PVS: Combining specification, proof checking, and model checking . In Proceedings of the International Conference on Computer-Aided Verification (CAV\u201996) . R. Alur and T. A. Henzinger Eds., Lecture Notes in Computer Science , vol. 1102 . Springer-Verlag, New Brunswick, NJ, 411--414. Owre, S., Rajan, S., Rushby, J., Shankar, N., and Srivas, M. 1996. PVS: Combining specification, proof checking, and model checking. In Proceedings of the International Conference on Computer-Aided Verification (CAV\u201996). R. Alur and T. A. Henzinger Eds., Lecture Notes in Computer Science, vol. 1102. Springer-Verlag, New Brunswick, NJ, 411--414."},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-70545-1_17"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78929-1_29"},{"key":"e_1_2_1_19_1","doi-asserted-by":"crossref","unstructured":"Prajna S.\n     and \n      Jadbabaie A\n  . \n  2004\n  . Safety verification of hybrid systems using barrier certificates. In Hybrid Systems: Computation and Control R. Alur and G. J. Pappas Eds. Lecture Notes in Computer Science vol. \n  2993\n  . \n  Springer Berlin 477--492. Prajna S. and Jadbabaie A. 2004. Safety verification of hybrid systems using barrier certificates. In Hybrid Systems: Computation and Control R. Alur and G. J. Pappas Eds. Lecture Notes in Computer Science vol. 2993. Springer Berlin 477--492.","DOI":"10.1007\/978-3-540-24743-2_32"},{"key":"e_1_2_1_20_1","volume-title":"Proceedings of the 41st IEEE Conference on Decision and Control. 741--746","author":"Prajna S.","unstructured":"Prajna , S. , Papachristodoulou , A. , and Parrilo , P. A . 2002. Introducing SOSTOOLS: A general purpose sum of squares programming solver . In Proceedings of the 41st IEEE Conference on Decision and Control. 741--746 . Prajna, S., Papachristodoulou, A., and Parrilo, P. A. 2002. Introducing SOSTOOLS: A general purpose sum of squares programming solver. In Proceedings of the 41st IEEE Conference on Decision and Control. 741--746."},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-007-0046-1"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.automatica.2008.03.010"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-70583-3_12"},{"key":"e_1_2_1_24_1","volume-title":"Proceedings of the International Workshop on Intelligent Vehicle Control Systems (IVCS).","author":"Wongpiromsarn T.","unstructured":"Wongpiromsarn , T. and Murray , R. M . 2008. Distributed mission and contingency management for the DARPA urban challenge . In Proceedings of the International Workshop on Intelligent Vehicle Control Systems (IVCS). Wongpiromsarn, T. and Murray, R. M. 2008. Distributed mission and contingency management for the DARPA urban challenge. In Proceedings of the International Workshop on Intelligent Vehicle Control Systems (IVCS)."},{"key":"e_1_2_1_25_1","unstructured":"Wongpiromsarn T. Mitra S. Murray R. and Lamperski A. 2008. Periodically controlled hybrid systems: Verifying a controller for an autonomous vehicle. Tech. rep. CaltechCDSTR:2008.003 California Institute of Technology. http:\/\/resolver.caltech.edu\/CaltechCDSTR:2008.003. Wongpiromsarn T. Mitra S. Murray R. and Lamperski A. 2008. Periodically controlled hybrid systems: Verifying a controller for an autonomous vehicle. Tech. rep. CaltechCDSTR:2008.003 California Institute of Technology. http:\/\/resolver.caltech.edu\/CaltechCDSTR:2008.003."},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-00602-9_28"}],"container-title":["ACM Transactions on Embedded Computing Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2331147.2331163","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2331147.2331163","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T08:48:50Z","timestamp":1750236530000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2331147.2331163"}},"subtitle":["Application to an Autonomous Vehicle"],"short-title":[],"issued":{"date-parts":[[2012,8]]},"references-count":25,"journal-issue":{"issue":"S2","published-print":{"date-parts":[[2012,8]]}},"alternative-id":["10.1145\/2331147.2331163"],"URL":"https:\/\/doi.org\/10.1145\/2331147.2331163","relation":{},"ISSN":["1539-9087","1558-3465"],"issn-type":[{"value":"1539-9087","type":"print"},{"value":"1558-3465","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012,8]]},"assertion":[{"value":"2009-05-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2010-06-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2012-08-01","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}