In this paper, we present a mechanism for building hybrid system observers to differentiate between specific positions of the hybrid system. The mechanism is designed through inferring metric temporal logic (MTL) formulae from simulated trajectories from the hybrid system. We first approximate the system behavior by simulating finitely many trajectories with timerobust tube segments around them. These time-robust tube segments account for both spatial and temporal uncertainties that exist in the hybrid system with initial state variations. The inferred MTL formulae classify different time-robust tube segments and thus can be used for classifying the hybrid system behaviors in a provably correct fashion. We implement our approach on a model of a smart building testbed to distinguish two cases of room occupancy.
In this work we formulate the satisfaction of a (syntactically co-safe) linear temporal logic specification on a physical plant through a recent hybrid dynamical systems formalism. In order to solve this problem, we introduce an extension to such a hybrid system framework of the so-called eventuality property, which matches suitably the condition for the satisfaction of such a temporal logic specification. The eventuality property can be established through barrier certificates, which we derive for the considered hybrid system framework. Using a hybrid barrier certificate, we propose a solutio…
We present a scalable methodology to verify stochastic hybrid systems. Using the Mori-Zwanzig reduction method, we construct a finite state Markov chain reduction of a given stochastic hybrid system and prove that this reduced Markov chain is approximately equivalent to the original system in a distributional sense. Approximate equivalence of the stochastic hybrid system and its Markov chain reduction means that analyzing the Markov chain with respect to a suitably strengthened property, allows us to conclude whether the original stochastic hybrid system meets its temporal logic specifications…
In this work we formulate the problem of satisfying a linear temporal logic formula on a linear plant with output feedback, through a recent hybrid systems formalism. We relate this problem to the notion of recurrence introduced for the considered formalism, and we then extend Lyapunov-like conditions for recurrence of an open, unbounded set. One of the proposed relaxed conditions allows certifying recurrence of a suitable set, and this guarantees that the high-level evolution of the plant satisfies the formula, without relying on discretizations of the plant. Simulations illustrate the propos…
This paper presents an intelligent autonomous parking system with Hybrid Fuzzy Controllers (HFCs). The system enables intelligent vehicles to perform slot detection, parallel and vertical parking in a completely unmanned environment. The HFC, constituting of a Base Fuzzy Controller (BFC) and a Supervisory Fuzzy Controller (SFC), optimizes the control logic to counteract external disturbances in parking process by implementing additional fuzzy rule base. Customized HFCs are designed for critical steps in parking, namely turning control and posture stabilization. As a result, more accurate and e…
This paper introduces operators, semantics, characterizations, and solution-independent conditions to guarantee temporal logic specifications for hybrid dynamical systems. Hybrid dynamical systems are given in terms of differential inclusions -- capturing the continuous dynamics -- and difference inclusions -- capturing the discrete dynamics or events -- with constraints. State trajectories (or solutions) to such systems are parameterized by a hybrid notion of time. For such broad class of solutions, the operators and semantics needed to reason about temporal logic are introduced. Characteriza…
Synergistic hybrid feedback refers to a collection of feedback laws that allow for global asymptotic stabilization of a compact set through the following switching logic: given a collection of Lyapunov functions that are indexed by a logic variable, whenever the currently selected Lyapunov function exceeds the value of another function in the collection by a given margin, then a switch to the corresponding feedback law is triggered. This kind of feedback has been under development over the past decade and it has led to multiple solutions for global asymptotic stabilization on compact manifolds…
This paper investigates a collaborative rover-copter path planning and exploration with temporal logic specifications under uncertain environments. The objective of the rover is to complete a mission expressed by a syntactically co-safe linear temporal logic (scLTL) formula, while the objective of the copter is to actively explore the environment and reduce its uncertainties, aiming at assisting the rover and enhancing the efficiency of the mission completion. To formalize our approach, we first capture the environmental uncertainties by environmental beliefs of the atomic propositions, under …
Hybrid control strategy for a semi active suspension system using fuzzy logic and bio-inspired chaotic fruit fly algorithm
Carnegie Mellon University（卡内基梅隆大学）；Jadavpur University（贾达普大学）；Sun Yat-sen University-Carnegie Mellon University (SYSU-CMU) Joint Institute of Engineering（中山大学-卡内基梅隆大学（SYSU-CMU）联合工程学院）
This paper proposes a robust design of Hybrid Fuzzy Controller for speed and steering angle control in an Intelligent Autonomous Parking System (IAPS). The Hybrid Fuzzy Controller consists of a Base Fuzzy Controller (BFC) and a Supervisory Fuzzy Decision Tree Controller (SFDTC). The BFC evolves from previous work on fuzzy logic control for unmanned parking and it ensures that optimal parking trajectory is achieved with minimal computational cost. SFDTC further increases the system robustness when there is noise in the operating environment. The design of SFDTC combines Decision Tree theory and…
