Verification of periodically controlled hybrid systems: Application to an autonomous vehicle

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. © 2012 ACM.

Periodically controlled hybrid systems verifying a controller for an autonomous vehicle

This paper introduces Periodically Controlled Hybrid Automata (PCHA) for describing a class of hybrid control systems. In a PCHA, control actions occur roughly periodically while internal and input actions may occur in the interim changing the discrete-state or the setpoint. Based on periodicity and subtangential conditions, a new sufficient condition for verifying invariance of PCHAs is presented. This technique is used in verifying safety of the planner-controller subsystem of an autonomous ground vehicle, and in deriving geometric properties of planner generated paths that can be followed safely by the controller under environmental uncertainties.

The role of human orbitofrontal cortex in value comparison for incommensurable objects.

The human orbitofrontal cortex is strongly implicated in appetitive valuation. Whether its role extends to support comparative valuation necessary to explain probabilistic choice patterns for incommensurable goods is unknown. Using a binary choice paradigm, we derived the subjective values of different bundles of goods, under conditions of both gain and loss. We demonstrate that orbitofrontal activation reflects the difference in subjective value between available options, an effect evident across valuation for both gains and losses. In contrast, activation in dorsal striatum and supplementary motor areas reflects subjects' choice probabilities. These findings indicate that orbitofrontal cortex plays a pivotal role in valuation for incommensurable goods, a critical component process in human decision making.

Autonomous rigid body attitude synchronization

Control laws to synchronize attitudes in a swarm of fully actuated rigid bodies, in the absence of a common reference attitude or hierarchy in the swarm, are proposed in [Smith, T. R., Hanssmann, H., & Leonard, N.E. (2001). Orientation control of multiple underwater vehicles with symmetry-breaking potentials. In Proc. 40th IEEE conf. decision and control (pp. 4598-4603); Nair, S., Leonard, N. E. (2007). Stable synchronization of rigid body networks. Networks and Heterogeneous Media, 2(4), 595-624]. The present paper studies two separate extensions with the same energy shaping approach: (i) locally synchronizing the rigid bodies' attitudes, but without restricting their final motion and (ii) relaxing the communication topology from undirected, fixed and connected to directed, varying and uniformly connected. The specific strategies that must be developed for these extensions illustrate the limitations of attitude control with reduced information. © 2008 Elsevier Ltd.

Autonomous rigid body attitude synchronization

This paper studies some extensions to the decentralized attitude synchronization of identical rigid bodies. Considering fully actuated Euler equations, the communication links between the rigid bodies are limited and the available information is restricted to relative orientations and angular velocities. In particular, no leader nor external reference dictates the swarm's behavior. The control laws are derived using two classical approaches of nonlinear control - tracking and energy shaping. This leads to a comparison of two corresponding methods which are currently considered for distributed synchronization - consensus and stabilization of mechanical systems with symmetries. © 2007 IEEE.