A Caltech Library Service

Verification of Periodically Controlled Hybrid Systems: Application to an Autonomous Vehicle

Wongpiromsarn, Tichakorn and Mitra, Sayan and Lamperski, Andrew and Murray, Richard M. (2012) Verification of Periodically Controlled Hybrid Systems: Application to an Autonomous Vehicle. ACM Transactions in Embedded Computing Systems, 11 (S2). Art. No. 53. ISSN 1539-9087. doi:10.1145/2331147.2331163.

Full text is not posted in this repository. Consult Related URLs below.

Use this Persistent URL to link to this item:


This article introduces Periodically Controlled Hybrid Automata (PCHA) for modular specification of embedded control systems. In a PCHA, control 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.

Item Type:Article
Related URLs:
URLURL TypeDescription ItemTechnical Report
Murray, Richard M.0000-0002-5785-7481
Additional Information:© 2012 ACM. Received May 2009; January 2010; accepted June 2010. This work is partially supported by AFOSR through the MURI program. The authors gratefully acknowledge Sumit Gulwani and Ashish Tiwari for letting them use their nonlinear solver for solving ∃∀ problems.
Funding AgencyGrant Number
Air Force Office of Scientific Research (AFOSR)UNSPECIFIED
Subject Keywords:Verification; Embedded systems; invariants
Issue or Number:S2
Record Number:CaltechAUTHORS:20121026-084418812
Persistent URL:
Official Citation:Wongpiromsarn, T., Mitra, S., Lamperski, A., and Murray, R. M. 2012. Verification of periodically controlled hybrid systems: Application to an autonomous vehicle. ACM Trans. Embed. Comput. Syst. 11, S2, Article 53 (August 2012), 24 pages
Usage Policy:No commercial reproduction, distribution, display or performance rights in this work are provided.
ID Code:35114
Deposited By: Tony Diaz
Deposited On:01 Nov 2012 23:36
Last Modified:09 Nov 2021 23:12

Repository Staff Only: item control page