liu.seSearch for publications in DiVA
Change search
ReferencesLink to record
Permanent link

Direct link
Model Checking Methods for Mode Switching Systems
Linköping University, Department of Electrical Engineering, Automatic Control. Linköping University, The Institute of Technology.
2000 (English)Doctoral thesis, monograph (Other academic)
Abstract [en]

This thesis deals with modeling and analysis of a special class of hybrid systems, i.e., systems displaying behavior of both continuous and discrete nature.

We focus on the class of systems which are naturally modeled as having continuous trajectories, but where the trajectories evolve according to a system of first order differential equations with piecewise continuous right hand side. We further restrict our attention to models where the right hand side is piecewise affine in the continuous state variables. Systems which are naturally modeled in this fashion are called piecewise affine switched systems.

The modeling is packaged into a modeling framework where the right hand side of the differential equations consists of both continuous and discrete valued variables. The equations then run in combination with a finite state machine, and their interatcion is specified via an interface. This framework allows a compact decription of a potentially large number of affine models, as well as a modular approach to modeling of complex systems.

The analysis consists of verifying if a swithced system fulfills specifications given either in terms of sets of good or bad discrete states, or as formulas in temporal logic specifying sesired or undesired behavior. This kind of analysis is often applied to purely discrete systems. We therefore take the approach to discretize the switched system using conservative approximations. This is done using two different automated procedures devised in this thesis. Both methods can be seen as special instances of using invariant sets and Lyapunov theory to guarantee either that bad states are avoided and/or that goal states are reached in finite time.

The former discretization method results in two different approximations, named acceptor and exceptor, which together can be utilized to obtain bounds on behavior which can be certified. We also introduce a discrete device, called reflector, which allows us to reduce the non-determinism resulting from the approximations. Furthermore, implementations of the procedure suggested, using either linear programming or quantifier elimination as computational tools, are discussed.

The second method utilized invariant sets of a special type called power cones, of which quadratic sets such as cones and paraboloids are special instances. This approach results in thighter approximations while still allowing for efficient implementation using Linear Matrix Inequalities and convex optimization.

Together, the discrete approximations, obtained automatically from a model of a switched system, can be used to verify properties of interest. This is illustrated as we apply one of our methods to two examples, a chemical reactor model and a model of the landing gear of a fighter aircraft.

Place, publisher, year, edition, pages
Linköping: Linköping University , 2000. , 168 p.
Linköping Studies in Science and Technology. Dissertations, ISSN 0345-7524 ; 652
National Category
Control Engineering
URN: urn:nbn:se:liu:diva-98137ISBN: 91-7219-836-2OAI: diva2:652269
Available from: 2013-10-09 Created: 2013-09-30 Last updated: 2013-10-09Bibliographically approved

Open Access in DiVA

No full text

By organisation
Automatic ControlThe Institute of Technology
Control Engineering

Search outside of DiVA

GoogleGoogle Scholar
The number of downloads is the sum of all downloads of full texts. It may include eg previous versions that are now no longer available

Total: 51 hits
ReferencesLink to record
Permanent link

Direct link