SENSE Documentation

The internal structure and work flow in SENSE: From specifications to code generation.

General information about the structure of SENSE is presented here. However, we suggest referring to the manual for further details. The C++ part of SENSE provides the algorithms to compute the symbolic model of Networked Control Systems (NCS) and to synthesize controllers based on the computed model.

The input is supposed to be a BDD that represnts the transition relation of the plant within the NCS. Such BDD can be generated by constructing a symbolic model using the library SCOTS inside SENSE. Then the file should be safed in a file. The tool should then be provided with details about the NCS itself.

The output is a BDD that represents the transition relation of the NCS. Users can further continue and synthesize symbolic controllers for the NCS. We provide fixed-point operations to synthesize controllers that enforce any of the following specifications: 

  • Reachabilitly
  • Safety
  • Persistence
  • Recurrence

The tool contains a Matlab interface to simulate the generated controller in the closed loop system and to visualize the abstract state space together with the atomic propositions. The tool allows for generating C/C++ or VHDL/Verilog codes to cover hardware and software implementations of the synthesized controllers. The figure to the right presents the internal structure and the work flow inside SENSE.


The SENSE tool contain several examples for the NCS symbolic model abstraction as well as controller the synthesis of symbolic controllers. Examples are found in the 'examples' folder within the root folder of the package. We encourage users to read the instructions document on how to repeat such experiments with SENSE.


The manual of SENSE can be downloaded from here. This document is the main source of information regarding the installation and operation of the SENSE tool.