SENSE: Abstraction-Based Synthesis of Networked Control Systems

TL;DR

SENSE is a tool that constructs finite abstractions of networked control systems and synthesizes controllers to meet complex specifications, considering communication non-idealities, with code generation capabilities.

Contribution

The paper introduces SENSE, a novel tool for abstraction-based synthesis of controllers for NCS with complex specifications and communication imperfections.

Findings

Efficient construction of symbolic models using BDDs.

Automated synthesis of controllers satisfying complex temporal logic specifications.

Generation of implementation-ready code from synthesized controllers.

Abstract

While many studies and tools target the basic stabilizability problem of networked control systems (NCS), nowadays modern systems require more sophisticated objectives such as those expressed as formulae in linear temporal logic or as automata on infinite strings. One general technique to achieve this is based on so-called symbolic models, where complex systems are approximated by finite abstractions, and then, correct-by-construction controllers are automatically synthesized for them. We present tool SENSE for the construction of finite abstractions for NCS and the automated synthesis of controllers. Constructed controllers enforce complex specifications over plants in NCS by taking into account several non-idealities of the communication channels. Given a symbolic model of the plant and network parameters, SENSE can efficiently construct a symbolic model of the NCS, by employing operations on binary decision diagrams (BDDs). Then, it synthesizes symbolic controllers satisfying a class of specifications. It has interfaces for the simulation and the visualization of the resulting closed-loop systems using OMNETPP and MATLAB. Additionally, SENSE can generate ready-to-implement VHDL/Verilog or C/C++ codes from the synthesized controllers.