Relational Abstractions for Hybrid Systems

Timed Relational Abstractions for

Sampled Data Control Systems

 

What are Sampled Data Control Systems?

Sampled data control systems consist of a plant, modeled as a hybrid system and a synchronous controller, modeled as a discrete transition system. The controller periodically observes the plant states and exercises control actions in order to achieve the desired performance. The correctness of the system depends on the controller design as well as an appropriate choice of  its sampling period.

The sampling period is important because usually a controller is designed in the continuous domain, i.e., it is designed considering the interaction between the controller and the plant to be continuous. However, controllers these days are usually always implemented digitally and the they can only periodically sense and actuate the plant. The sampling period then becomes an important aspect of the system and can affect the stability and performance of the system.

The

The Plant Model

plant is a physical system with continuous dynamics and can be defined using a set of ODEs. We use Hybrid Automata to model the plant’s dynamics. Informally a hybrid automaton is a set of locations and transitions between these locations; where each location defines the flow of the continuous variables. One can think of the plant as a Hybrid Automaton with the locations defining the mode of operation of the plant between which it can switch under controller actions and environmental changes. We call these transitions Controlled and Autonomous respectively.

The

The Controller Model

rollers regulate the behavior of the plant in a desired way. These days they are digital implementations, interfaced with the physical world and the plant through sensors and actuators. According to our simplistic(but not overly so) definition, the controller running on a micro-controller polls the plant and its environment every sampling period through its sensors, computes control actions and actuates the plant. Controllers are usually implemented in imperative software languages like C and it seems a good choice to model them by an infinite state discrete transition system with an associated sampling time.

What ar

What are Relational and Timed Relational Abstractions?

text-align: justify;">We construct a timed relational abstraction of the hybrid plant by replacing the continuous plant dynamics by relations. These relations map a state of the plant to states reachable within the sampling time period. i.e., we try to capture the states of the plant as seen by the controller at the sample times while abstracting away the intersample behavior conservatively.

Why do we

Why do we need abstractions?

a method to discretize the plant dynamics into an infinite state transition system, and because this discretization may contain more behaviors than the original plant we term it as an abstraction(in other words an over-approximation). Being discrete, infinite-state transition systems these abstractions can be verified using conventional verification tools. We use k-induction to prove safety properties and bounded model checking (BMC) to find potential falsifications.

ResourcesResources

lign: justify;">For Additional details please refer to the CAV 2012 publication (final version).

The SAL and HSAL files of the benchmarks can be found here (updated).

A high level presentation given at MVD 2012.

People

T

People

rried out by a team consisting of

  • Aditya Zutshi, PhD candidate (ECEE), University of Colorado, Boulder.
  • Sriram Sankaranarayanan, Asst. Professor (CSCI), University of Colorado, Boulder.
  • Ashish Tiwari, SRI international, Menlo Park, CA.

Support

Support

ranarayanan’s work supported by NSF Career grant CNS-0953941. Tiwari’s work supported in part by DARPA under Contract No. FA8650-10-C-7078, NSF grants CSR-0917398 and SHF:CSR-1017483. All opinions expressed are those of the authors and not necessarily of the US NSF or DARPA.