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.

Direct parameter extraction in feedthrough-embedded capacitive MEMS resonators

This paper presents a method for fast and accurate determination of parameters relevant to the characterization of capacitive MEMS resonators like quality factor (Q), resonant frequency (fn), and equivalent circuit parameters such as the motional capacitance (Cm). In the presence of a parasitic feedthrough capacitor (CF) appearing across the input and output ports, the transmission characteristic is marked by two resonances: series (S) and parallel (P). Close approximations of these circuit parameters are obtained without having to first de-embed the resonator motional current typically buried in feedthrough by using the series and parallel resonances. While previous methods with the same objective are well known, we show that these are limited to the condition where CF ≪ CmQ. In contrast, this work focuses on moderate capacitive feedthrough levels where CF > CmQ, which are more common in MEMS resonators. The method is applied to data obtained from the measured electrical transmission of fabricated SOI MEMS resonators. Parameter values deduced via direct extraction are then compared against those obtained by a full extraction procedure where de-embedding is first performed and followed by a Lorentzian fit to the data based on the classical transfer function associated with a generic LRC series resonant circuit. © 2011 Elsevier B.V. All rights reserved.

Scaling the iHMM: Parallelization versus Hadoop

This paper compares parallel and distributed implementations of an iterative, Gibbs sampling, machine learning algorithm. Distributed implementations run under Hadoop on facility computing clouds. The probabilistic model under study is the infinite HMM [1], in which parameters are learnt using an instance blocked Gibbs sampling, with a step consisting of a dynamic program. We apply this model to learn part-of-speech tags from newswire text in an unsupervised fashion. However our focus here is on runtime performance, as opposed to NLP-relevant scores, embodied by iteration duration, ease of development, deployment and debugging. © 2010 IEEE.