Hybrid Systems: Computation and Control: 4th International Workshop, HSCC 2001 Rome, Italy, March 28-30, 2001 Proceedings (Lecture Notes in Computer Science, 2034)

Hybrid Systems: Computation and Control
Preface
Organization
Table of Contents
Control as an Embedded Technology
Optimisation of Hybrid Processes and Hybrid Controllers
Embedded Software and Systems: Challenges and Approaches
Hybrid Systems Applications: An Oxymoron?
Design of Luenberger Observers for a Class of Hybrid Linear Systems
	Introduction
	Switching Observers for Discrete-Time Linear Systems
	An Enhanced Projection-Based Luenberger Observer
	Simulation Results
	Conclusions
	References
Hybrid Modeling and Simulation of Biomolecular Networks
	Introduction
	Modeling
	A Repressilator Network
		The Basic Phenomena
		Approaches to Modeling
		{sc Charon} Model
	Quorum Sensing in Bacteria
		The Basic Phenomena
		Mathematical Model
		{sc Charon} Model
	Conclusions
	References
Compositional Refinement for Hierarchical Hybrid Systems
	Introduction
	Motivational Example
	Modes
		Syntax
		Semantics
		Trace Semantics
	Agents
		Syntax
		Semantics
		Operations on Agents
	Compositionality Results
		Compositionality of Modes
		Compositionality of Agents
	Conclusions
	References
Optimal Paths in Weighted Timed Automata
	Introduction
	Preliminaries
	The Graph Construction
	Optimal-Runs in in Weighted Timed Automata
		Single-Source Case
		The Algorithm for the General Case
	References
Reach Set Computations Using Real Quantifier Elimination
	Introduction
	Reach Sets and Transcendental Implicitization Problem
		Problem Statement
		Reduction to Implicitization Problems
	Exact Transcendental Implicitization
	Semialgebraic Implicitization for Simple Elementary Functions
	Approximate Solutions
	Complexity
	Computational Example in {sc redlog} and {sc qepcad}
	Conclusions
	References
On Hybrid Control of Under-Actuated Mechanical Systems
	Introduction
	Control of Under-Actuated Mechanical Systems
		Under-Actuated Mechanical Systems
		Zero Dynamics
		Handling the Periodic Orbits
	The Case of the Double Pendulum
	Results
	Conclusion
	References
On the Decidability of the Reachability Problem for Planar Differential Inclusions
	Introduction
	Simple Planar Differential Inclusions
	Properties of Trajectories
	Properties of Edge Signatures
	Affine Operators
	Computing the Successor Function
	Reachability Analysis
	Concluding Remarks
	References
The Substratum of Impulse and Hybrid Control Systems
	Introduction
	Impulse Differential Inclusions
	The Substratum and the Initialization and Impulse Maps
	Some Prerequisite from Viability Theory
	The Graph of the Substratum
	Hamilton-Jacobi Characterization of the Substratum
	References
Path-Dependent Impulse and Hybrid Systems
	Impulse Path-Dependent Differential Inclusions
		History Spaces
		Histories or Paths
		Path-Dependent Differential Inclusions
		Runs of Impulse Path-Dependent Differential Inclusions
	Introduction
	Statement of The Impulse Path-Dependent Viability Theorem
		Marchaud Maps
		Contingent Directions
		The Impulse Path-Dependent Viability Theorem
		Examples
		Path-Dependent Hybrid Systems
	Impulse Evolutionary Systems
		Impulse Evolutionary Systems
		Characterization of Impulse Evolutionary Systems Viability
		Prerequisites of Viability Theory
		Proof of the Characterization of Impulse Evolutionary Systems Viability
	The Path-Dependent Viability Theorem
	References
Hybrid Feedback Control for Path Tracking by a Bounded-Curvature Vehicle
	Introduction
	Hybrid Path Tracking Modeling Using Switching Frenet\'s Frames
	Hybrid Path--Tracking Feedback Controller
		Optimal Feedback Control for Line Tracking
		Feedback Tracking Control for Generic Path
	Verification of the Hybrid Path--Tracking Controller
	Conclusions
	References
Minimum-Cost Reachability for Priced Timed Automata
	Introduction
	Linearly Priced Timed Automata
	Priced Clock Regions
	Symbolic Semantics and Algorithm
	Conclusion
	References
A Hybrid Approach to Traction Control
	Introduction
	Vehicle Model
		Discrete-Time Hybrid Model
	Optimal Control
	Controller Design
		Simulations
		Explicit Controller
	Conclusion
	Appendix
	References
Optimal Control Using Bisimulations: Implementation
	Introduction
	Optimal Control Problem
	From Hybrid Automata to Finite Automata
	Dynamic Programming
	Non-deterministic Dijkstra Algorithm
	Example
	Conclusion
	References
A Generalized Approach for Analysis and Control of Discrete-Time Piecewise Affine and Hybrid Systems
	Introduction
	Stability and State-Feedback Stabilization of PWA Systems
	Synthesis of a Stabilizing State Feedback
	$H_{infty }$ Performance of Piecewise Affine Systems
		$H_infty $ Analysis and Synthesis for PWA Systems without Displacement Terms
		Extension to PWA Systems with Displacement Terms
	Numerical Example: The Tank Case
	Conclusions
	References
Accurate Event Detection for Simulating Hybrid Systems
	Motivation and Previous Work
	Key Concepts
		Review: Numerical Integration with Linear Multistep Methods
		Feedback Linearization Analogy in Continuous Time
	Simulation Algorithm
		Symbolic Inverse
		Exact Linearization
		Approximate Linearization
		Computation of Step Sizes
		Boolean Combinations of Guards
		Final Selection
		Termination Criteria
		Algorithm
	Examples and Discussion
	Conclusions and Future Work
	References
A Clustering Technique for the Identification of Piecewise Affine Systems
	Introduction
	Problem Statement
	The Main Algorithm
	Discussion and Concluding Remarks
	References
Lateral Inhibition through Delta-Notch Signaling: A Piecewise Affine Hybrid Model
	Introduction
		Lateral Inhibition and Developmental Biology
		Previous Work: Mathematical Models
		Motivation for Hybrid Model
	Model
		Model of a Single Cell, Two Cell and $Ntimes N$ Cell Network
	Simulation Results
	Analysis
		Single Cell Hybrid Automaton
		Two Cell Hybrid Automaton
		$Ntimes N$ Cell Hybrid Automaton
	Comparison with Nonlinear Model
	Conclusion
	References
Supervision of Event-Driven Hybrid Systems: Modeling and Synthesis
	Introduction
	Problem Formulation
	DES Approach
	Finite State Approximations for the HS DES Plant
	Example
	Discussion
	References
Control of Piecewise-Linear Hybrid Systems on Simplices and Rectangles
	Introduction
	Problem Formulation
	Reachability of Hybrid Systems
	Reaching Departure Sets Using Feedback Control
	Conclusions
	References
Assume-Guarantee Reasoning for Hierarchical Hybrid Systems
	Introduction
	The Masaccio Model for Embedded Components
	Assume-Guarantee Refinement between Components
	A Two-Robot Example
	References
	Appendix: Formal De
Hybrid Modeling of TCP Congestion Control
	Introduction
	Hybrid Model for Congestion Control
	Dynamics in Normalized Time
	Steady-State Behavior
	Conclusion
	Appendix
	References
Hybrid Geodesics as Optimal Solutions to the Collision-Free Motion Planning Problem
	Introduction and Background
	Problem Formulation
		A Geometric Interpretation
		Geodesics in u-Convex Manifolds
	Hybrid System Solution
		Necessary Conditions for Optimality
		Two Agents Case
		Three Agents Case
	Conclusions
	References
Nonlinear Adaptive Backstepping with Estimator Resetting Using Multiple Observers
	Introduction
	Nonlinear Adaptive Backstepping
	Stability Analysis of Parameter Resetting
		Sufficient Conditions for Stability
		Reference Trajectory Resetting
		Application to a First Order System
		Application to a Second Order System
	Multiple Model Observer (MMO)
		Construction of the Individual Observers in the First Order Case
	First Order System
	Conclusions
	References
Mode Switching Synthesis for Reachability Specifications
	Introduction
	Problem Formulation
	A Mode Switching Condition
	Mode Sequence Synthesis
	Reachability Computations
	Conclusion
	References
Characterization of Stabilizing Switching Sequences in Switched Linear Systems Using Piecewise Linear Lyapunov Functions
	Introduction
	Problem Statement
	Piecewise Linear Lyapunov Functions
		Computation of Piecewise Linear Lyapunov Functions
	Stabilizing Switching Sequences
	Continuous-Time Switched Linear Systems
		Background Material
		Stabilizing Switching Sequences
	Conclusions
	References
On a Novel Class of Bifurcations in Hybrid Dynamical Systems
	Overview
	Background
		Sliding Motion
		Self Oscillations and Poincar{accent 19 e} Maps
	Bifurcation Scenarios Involving Sliding Section
		Analytical Conditions for Sliding Bifurcations
	Numerical Analysis of a Third Order Representative Example
		Sliding Bifurcation
		Multisliding Bifurcation
		Grazing while Sliding Bifurcation
		Switching Sliding Bifurcation, Sliding Type B
		Chaos
	Conclusions and Future Work
	References
Global Controllability of Hybrid Systems with Controlled and Autonomous Switchings
	Introduction
	Regular Control Hybrid Systems: Standing Assumptions
	Controlled Hybrifold
	The Global Controllability of Hybrid Systems
	Hybrid Fountains
	References
Modeling of Continuous-Discrete Processes
	Introduction
	Background
		Discontinuity Locking
		Review of Existing Algorithms
	Hierarchical Approach to Discontinuity Handling in Event-Driven Processes
		Event Detection
		Event Location
		Step Completion
	Advanced Issues in Hybrid Simulation
		Multiple/Simultaneous Discontinuities in Integration Step
		Step Size Selection after a Discontinuity
		Selection of Tolerances
	Application and Results
		A Rectifier Circuit - Carvers Example 3
		Discussion of the Performance Results
	Conclusions
	References
Hybrid I/O Automata Revisited
	Introduction
	Describing Hybrid Behavior
		Static and Dynamic Types
		Trajectories
		Hybrid Sequences
	Hybrid Automata
		Definition of Hybrid Automata
		Executions and Traces
		Simulation Relations
		Composition
	Hybrid I/O Automata
		Definition of Hybrid I/O Automata
		Composition
	Receptive Hybrid I/O Automata
	Sufficient Conditions for Strong Compatibility
		HIOAs with Restrictions on Input Variables
		Lipschitz HIOAs
	References
Validating a Hamilton-Jacobi Approximation to Hybrid System Reachable Sets
	Introduction
	Reachability for Hybrid Systems
	Continuous Reachability with Level Sets
		The Hamilton-Jacobi Partial Differential Equation
		Solving the Hamilton-Jacobi PDE
		Localizing Computation
		Numerical Validation of Aircraft Collision Avoidance
	Aircraft Landing Example
	References
Robust Controller Synthesis for Hybrid Systems Using Modal Logic
	Introduction
	Hybrid Automata
	Control Problem Statement
	Modal Logics for Hybrid Systems
	Abstract Algorithm of Synthesis Procedure
	Correctness and Robustness of Synthesis Procedure
	Discussion and Conclusion
	References
Diagnosis of Physical Systems with Hybrid Models Using Parametrized Causality
	Introduction
	Preliminaries
	Hybrid Models for FDI
	A Case Study
	Conclusions
	References
Addressing Multiobjective Control: Safety and Performance through Constrained Optimization
	Introduction
	Problem Description
		Collision Avoidance
		VSTOL FMS
	Safety Analysis
		Collision Avoidance
		VSTOL FMS Model
	Nonlinear Constrained Optimization
		Collision Avoidance
		VSTOL FMS
	Results
		Collision Avoidance
		VSTOL FMS
	Conclusion
	References
Representation of Quantised Systems by the Frobenius-Perron Operator
	Introduction
	Evolution of Probability Densities in the State--Space
		Results from Measure Theory
		Problem Statement
		The Frobenius-Perron Operator
		Representation of the Autonomous Quantised Systems
		Extension to Non-autonomous Systems
	Approximate Representation of Quantised Systems
		Approximation of the FPO
		Extension to Non-autonomous Systems
	Qualitative Modelling
		Modelling Aim
		Qualitative Model of the Quantised System
	Sound Abstraction of Qualitative Models
		Point-Based Cell-to-Cell Mapping
		Hyperbox Cell-to-Cell Mapping
	Conclusions
	References
Semi-decidable Synthesis for Triangular Hybrid Systems
	Introduction
	Controller Synthesis for Nonlinear Hybrid Systems
	Computing Safe Sets for Triangular Nonlinear Systems
		Computation of Optimal Control
		Construction of Hybrid System
		Reach Set Computation
		Triangular Systems
	Controller Synthesis for Triangular Hybrid Systems
	Conflict Resolution Example
	Conclusion
	References
Hybrid Abstractions that Preserve Timed Languages
	Introduction
	Abstractions of Continuous Systems
		Abstractions of Control Systems
		Controllability Equivalence
	Hybrid Control Abstractions
		Timed Language Generated by a Hybrid System
		Propagating Guards and Invariants
		Hybrid Abstractions
	Example
	Conclusions
	References
Author Index