Synthesis of Switching Rules for Ensuring Reachability Properties of Sampled Linear Systems

Laurent Fribourg
(Laboratoire Specification et Verification)
Bertrand Revol
Romain Soulat
(Laboratoire Specification et Verification)

We consider here systems with piecewise linear dynamics that are periodically sampled with a given period τ . At each sampling time, the mode of the system, i.e., the parameters of the linear dynamics, can be switched, according to a switching rule. Such systems can be modelled as a special form of hybrid automata, called "switched systems", that are automata with an infinite real state space. The problem is to find a switching rule that guarantees the system to still be in a given area V at the next sampling time, and so on indefinitely. In this paper, we will consider two approaches: the indirect one that abstracts the system under the form of a finite discrete event system, and the direct one that works on the continuous state space.

Our methods rely on previous works, but we specialize them to a simplified context (linearity, periodic switching instants, absence of control input), which is motivated by the features of a focused case study: a DC-DC boost converter built by electronics laboratory SATIE (ENS Cachan). Our enhanced methods allow us to treat successfully this real-life example.

In Fang Yu and Chao Wang: Proceedings 13th International Workshop on Verification of Infinite-State Systems (INFINITY 2011), Taipei, Taiwan, 10th October 2011, Electronic Proceedings in Theoretical Computer Science 73, pp. 35–48.
Published: 11th November 2011.

ArXived at: bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to:
For website issues: