Hybrid Systems

Hybrid systems are modeled as phase transition systems with sampling semantics. By identifying a set of important events it is ensured that all significant state changes are observed, thus correcting previous drawbacks of the sampling computations semantics. A proof rule for verifying properties of hybrid systems is presented and illustrated on several examples.

Duration Calculus is a real-time interval logic which can be used to specify and reason about timing and logical constraints on discrete states in a dynamic system. It has been used to specify and verify designs for a number of real-time systems. This paper extends the Duration Calculus with notations to capture properties of piecewise continuous states. This is useful for reasoning about hybrid systems with a mixture of continuous and discrete states. The proof theory of Duration Calculus is extended such that results proven using mathematical analysis can be used freely in the logic. This provides a flexible interface to conventional control theory.

We propose a formal framework for designing hybrid systems by stepwise refinement. Starting with a specification in hybrid temporal logic, we make successively more transitions explicit until we obtain an executable system.

TLA⁺ is a general purpose, formal specification language based on the Temporal Logic of Actions, with no built-in primitives for specifying real-time properties. Here, we use TLA⁺ to define operators for specifying the temporal behavior of physical components obeying integral equations of evolution. These operators, together with previously defined operators for describing timing constraints, are used to specify a toy gas burner introduced by Ravn, Rischel, and Hansen. The burner is specified at three levels of abstraction, each of the two lower-level specifications implementing the next higher-level one. Correctness proofs are sketched.

Explicit clocks provide a well-known possibility to introduce time into non-real-time theories of reactive systems. This technique is applied here to an approach where distributed systems are modeled with temporal logic of actions as the formal basis, and fairness as the basic force that makes events take place. The focus of the paper is on the formalization and practical proof of hybrid properties of the form “at every moment of time t, Φ(t) holds for X,” where X is a set of objects with distributed clocks, and Φ is a predicate that depends both on the discrete states of x ε X and on time t. The approach is illustrated by a treatment of two well-known examples from the hybrid system literature.

To specify and verify distributed real-time systems, classical Hoare triples are extended with timing primitives and the interpretation is modified to be able to specify non-terminating computations. For these modified triples a compositional proof system has been formulated. Compositionality supports top-down program derivation, and by using a dense time domain also hybrid systems with continuous components can be designed. This is illustrated by a process control example of a water level monitoring system. First we prove the correctness of a control strategy in terms of a continuous interface. Next, to obtain a discrete interface, a sensor and an actuator are introduced. Using their specifications only, a suitable specification of the control unit is derived. This reduces the design of the system to the conventional problem of deriving a program according to its specification. Finally the control unit is extended, in a modular way, with error detection features.

Integration Graphs are a computational model developed in the attempt to identify simple Hybrid Systems with decidable analysis problems. We start with the class of constant slope hybrid systems (cshs), in which the right hand side of all differential equations is an integer constant. We refer to continuous variables whose right hand side constants are always 1 as timers. All other continuous variables are called integrators. The first result shown in the paper is that simple questions such as reachability of a given state are undecidable for even this simple class of systems.

To restrict the model even further, we impose the requirement that no test that refers to integrators may appear within a loop in the graph. This restricted class of cshs is called integration graphs. The main results of the paper are that the reachability problem of integration graphs is decidable for two special cases: The case of a single timer and the case of a single test involving integrators.

The expressive power of the integration graphs formalism is demonstrated by showing that some typical problems studied within the context of the Calculus of Durations and Timed Statecharts can be formulated as reachability problems for restricted integration graphs, and a high fraction of these fall into the subclasses of a single timer or a single dangerous test.

We introduce the framework of hybrid automata as a model and specification language for hybrid systems. Hybrid automata can be viewed as a generalization of timed automata, in which the behavior of variables is governed in each state by a set of differential equations. We show that many of the examples considered in the workshop can be defined by hybrid automata. While the reachability problem is undecidable even for very restricted classes of hybrid automata, we present two semidecision procedures for verifying safety properties of piecewiselinear hybrid automata, in which all variables change at constant rates. The two procedures are based, respectively, on minimizing and computing fixpoints on generally infinite state spaces. We show that if the procedures terminate, then they give correct answers. We then demonstrate that for many of the typical workshop examples, the procedures do terminate and thus provide an automatic way for verifying their properties.

Hybrid Systems are models of systems operating in real-time and handling events as well as “continuous” computations. The Signal formalism for Hybrid Systems is presented in this paper. Its expressive power is discussed, and a general method, to associate various formal systems with it, is presented with applications to Signal compilation and proof system.

This paper establishes a general framework for describing hybrid dynamical systems which is particularly suitable for numerical simulation. In this context, the data structures used to describe the sets and functions which comprise the dynamical system are crucial since they provide the link between a natural mathematical formulation of a problem and the correct application of standard numerical algorithms. We describe a partial implementation of the design methodology and use this simulation tool for a specific control problem in robotics as an illustration of the utility of the approach for practical applications.

Hybrid dynamical systems consist of two types of systems, a continuous state system called the plant and a discrete event system called the supervisor. Since the plant and supervisor are different types of systems, an interface is required to facilitate communication. An important issue in the design of hybrid control systems is the determination of this interface. Essentially, the interface associates logical symbols used by the supervisor with nonsymbolic events representative of the plant's behaviour. This chapter discusses a method for learning a hybrid system interface where symbols and events are bound in a way which is compatible with the goal of plant stabilization. The method is called event identification and provides an on-line method for adapting hybrid dynamical systems in the face of unforseen plant variations.

In this section we present a few conclusions pertaining to the suitability of our proposed architecture for implementing, designing and analyzing PSC.

The two-agent architecture has been shown to be sound and complete. Further research is needed to prove and test a network with more than two agents.

The architecture is easily extensible. Additional rules can be easily added to reflected changes in goals or constraints. This feature allows easy and flexible customization of the agent behavior and goals.

Robustness was demonstrated by showing that small variations in goals produced small variations in behavior. The architecture also responded appropriately to introduced errors, such as process shutdown and interrupted material flow, making adaptations to the goals and constraints to reflect these changes.

The simulation also demonstrated the architecture's ability to incorporate externally coded algorithms, a scheduler in this case.

By a “hybrid system” we mean a system of continuous plants, subject to disturbances, interacting with sequential automata in a network. “Hybrid Control” is the name we give to control of continuous plants by digital sequential control automata, that is, by control programs implemented on sequential automata. We associate, without using any approximations, sequential automata with continuous plants, and use this to bring sequential control automata and continuous plants into automata networks which themselves are sequential automata modelling hybrid systems. To be useful, the control automaton's ability to control plant trajectories in a hybrid system should be maintained under small changes in control laws, disturbance, trajectory, measurement, etc. We formalize this notion of controllability and observability for hybrid systems by continuity of system functions, including the input-output function of the control automaton, in non-Hausdorff subtopologies of the usual topologies on spaces of controls, sensor data, plants, disturbances, target sets, etc. These subtopologies arise from the limited ability of digital programs to discriminate between continuous inputs. These notions are appropriate for any knowledge or rule based system where automated deduction interacts in real time with the external world. This topological approach was announced in [46]. (What we call “controllability and observability” here is what we called “stability” in [46] in order to correspond somewhat more closely to usage in the literature [3].)

We consider hybrid systems as networks consisting of continuous input-output systems and discrete input-output automata. Some of the outputs may be connected to some of the inputs; the others server as the inputs and outputs of the hybrid system. We define a class of regular flows for such systems and make some remarks about them.

Hybrid control systems contain two distinct types of systems, continuous state and discrete-state, that interact with each other. Their study is essential in designing sequential supervisory controllers for continuous-state systems, and it is central in designing control systems with high degree of autonomy.

After an introduction to intelligent autonomous control and its relation to hybrid control, models for the plant, controller, and interface are introduced. The interface contains memoryless mappings between the supervisor's symbolic domain and the plant's nonsymbolic state space. The simplicity and generality afforded by the assumed interface allows us to directly confront important system theoretic issues in the design of supervisory control systems. such as determinism, quasideterminism, and the relationship of hybrid system theory to the more mature theory of logical discrete event systems.

Feedback control systems are vulnerable to faults in control loop sensors and actuators, because feedback action may cause abrupt and damaging responses when faults occur. Despite the importance of the subject, research results from analysis, design, and implementation of fault handling methods have not been widely accepted in the industry. One reason has been scarcity of realistic examples for testing of new methods against industrial systems. Another has been lack of interaction between control systems theory and computer science in this area. This paper is a contribution to help bridging these gaps.

Mathematical methods to detect and isolate faults in industrial feedback control systems are presented and analyzed, and it is shown where these methods work well and where other techniques are needed. An industrial position control loop with electro-mechanical components is used as an application example because it has several characteristics which are generic for hybrid feedback control systems. As a salient feature, the paper provides both a simple mathematical model of this system for use in the design of fault handling methods and a complete, nonlinear description for simulation and verification work. These models make it possible to make bench-mark testing of new methods including assessment of robustness against modelling uncertainty and process disturbances. These are crucial for industrial applicability but somewhat overlooked in hybrid system theory.

Key contributions are the presentation and analysis of an industrial feedback system which is suitable for bench-mark testing of new ideas in hybrid system theory, and the demonstration of state of the art in mathematical methods for fault detection and accommodation.

Drawing on practical experience in the development of dependable applications, this paper presents a number of “goals” for industrially applicable formal techniques in the specification and analysis of requirements for hybrid systems. These goals stem from domain-specific concerns such as the division between environment, plant and controller; and from the development context with its wide variety of analysis and design activities.

Motivated by some of these goals, we present a methodology, based on formal methods, for the requirements analysis of hybrid systems that are safetycritical. This methodology comprises a framework whose stages are based on levels of abstraction that follow a general structure for process control systems, a set of techniques appropriate for the issues to be analysed at each stage of the framework, and a hierarchical structure for the product of the analysis. Some aspects of the methodology are exemplified through two case studies. The extent to which this approach meets the goals espoused earlier is discussed.

This paper demonstrates how the extended duration calculus