SENSE Documentation

The work flow in SENSE to compute a symbolic model of the NCS and to synthesize a controller to enforce specification.

General information about the structure of SCOTS are presented here. However, we suggest refering 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 tool SCOTS. 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 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.