Linearizer Benchmark

This repository contains benchmark reproducing experiments from our paper "Linearising Discrete Time Hybrid Systems" submitted to IEEE Transactions on Automatic Control.

To provide faithful reproduction of our experiments and easy execution on any platform we packaged benchmark as a software container. The only needed prerequisite for its execution is Docker, that can be installed using instructions from the official website.

After Docker installation you need to perform following steps to execute the benchmark:

1. Build the image:

docker build -t mclab/linearizer-benchmark .

As an alternative you can download a prebuilt image from official docker hub:

docker pull mclab/linearizer-benchmark

2. Run the container:

docker run --rm -it mclab/linearizer-benchmark

Now you are inside the shell of the benchmark container. From here you can execute different parts of the benchmark described below.

Evaluation of linearisation algorithm

This part of the benchmark evaluates performance of our linearisation algorithm implemented in linearizer library.

Linearisation of \(y \cos{x}\)

Tool lin_benchmark_1 computes linearisation of the function \(y \cos(x)\) on the interval \([0,2\pi]\times[-\alpha,\alpha]\).

        lin_benchmark_1:  --alpha=<val> --eps=<val> -m <num> -o <file>
        lin_benchmark_1:  -h|--help

--alpha=<val>             y ranges in [-alpha,alpha]
--eps=<val>               error threshold
-m <num>                  number of sampling points
-o <file>                 output file
-h, --help                print help message

Example invocation that computes linearisation of \(y \cos(x)\) on the interval \([0,2\pi]\times[-2,2]\) using \(\varepsilon=0.1\) as upper bound for linearisation error and \(m=80\) number of sampling points:

lin_benchmark_1 --alpha=2 --eps=0.1 -m 80 -o lin.txt

During the execution tool reports the current progress, number of intervals in the cover, CPU time and peak RAM usage.

Progress       n   CPU (sec)    RAM (KB)
   0.10%       5      0.0511       36648
   0.15%       7      0.0632       36648

The output is a text file with very simple format. First line contains two numbers: the number of intervals in the computer cover and the arity of the input function. The rest of the file tool fills line by line with the elements of the following matrices:

  1. matrix representing lower bounds of the cover intervals(element \((i,j)\) is the lower bound of \(i\)-th interval for \(j\)-th dimension)
  2. matrix representing upper bounds of the cover intervals (element \((i,j)\) is the upper bound of \(i\)-th interval for \(j\)-th dimension)
  3. matrix representing under-approximation
  4. matrix representing over-approximation

Source code of the tool is available in the directory linearisation/src.

Term-wise approach

Tool lin_benchmark_2 computes linearisation of the function \(\sum_{i=1}^{t} x_{i} x_{i+1}\).

This can be done

  • giving this function as it is to the linearisation algorithm (monolithic approach)
  • treating each element of the sum separately (term-wise approach)
        lin_benchmark_2:  -t <num> -w <val> --eps=<val> -m <num> -o <file> [--term-wise]
        lin_benchmark_2:  -h|--help

-t <num>                  number of terms (1..4)
-w <val>                  x_{i} ranges in [-w,w]
--eps=<val>               error threshold
-m <num>                  number of sampling points
-o <file>                 output file
--term-wise               use term-wise approach
-h, --help                print help message

Example invocation that computes linearisation of \(x_1x_2+x_2x_3+x_3x_4\) on the interval \([-2,2]^{4}\) using term-wise approach and \(\varepsilon=1.0\) as upper bound for linearisation error and \(m=10\) number of sampling points:

lin_benchmark_2 -t 3 -w 2 --eps=0.1 -m 10 -o lin.txt --term-wise

The execution log format and output format are the same as of lin_benchmark_1. The only difference is that when term-wise approach is used, \(t\) output files are produced, one for each term.

Source code of the tool is available in the directory linearisation/src.

Control software synthesis

This part of the benchmark demonstrates how our linearisation approach combined with QKS tool can be used to automatically generate control software for a non-linear Discrete Time Hybrid System.

Our workflow consists of following steps:

  1. Linearisation
  2. Replication of transition relation
  3. Controller synthesis
  4. Simulation of closed loop system

We apply this workflow to the model of inverted pendulum with different frictions.

In the paper we presented 3 experiments with following configurations (\(\varepsilon\) is the upper bound for linearisation error, \(b\) is the number of quantization bits):

  1. \(\varepsilon=0.5\) and \(b=8\)
  2. \(\varepsilon=0.5\) and \(b=9\)
  3. \(\varepsilon=1.1\) and \(b=9\)

Other parameters in all experiments were chosen as follows:

  • simulation step \(\tau=0.01\)
  • controller sampling time \(T=0.1\)
  • friction coefficient above pivot point \(\mu_1=0.01\)
  • friction coefficient below pivot point \(\mu_2=0\)
  • torquing force intensity \(F=0.5\)

For each experiment there is a directory inside control_software_synthesis/hybrid that contains input and output for each workflow step.

Below you can find detailed description of each step.


We use our tool lin4qks to computer DTLHS overapproxmating initial DTHS model. More information about it can be found here.

Example invocation:

lin4qks -i input/model.m -f input/functions.c -o output/model.m

Here lin4qks takes as input file input/model.m, reads definitions of the functions from input/functions.c and writes the output DTLHS to output/model.m.

Replication of transition relation

After obtaining DTLHS model at the previous step we continue replicating its transition relation \(k\) times in such way that \(T=k\tau\) where \(T\) is desired controller sampling time and \(\tau\) is simulation step.

Tool replicate4qks takes as input the file with the model and how many times to replicate its transition relation. It outputs model with replicated transition relation together with file containing computed bounds for new variables introduced.

Example invocation:

replicate4qks -i input/model.m -o output/model.m -b output/computed_bounds.txt -n 10

Controller synthesis

Finally QKS is used to automatically synthesize control software.

Example invocation:

qks -d input -dk output -no_compute_bounds -on_the_fly

QKS will generate control software (files ctrl.h and ctrl.c) in the output directory.

Simulation of closed loop system

For the experiment #2 (\(\varepsilon=0.5\) and \(b=9\)) in which QKS succeeded to find controller we performed also simulation of plugging generated control software into OpenModelica-based simulator.

Simulator can be found in directory control_software_synthesis/hybrid/simulator:

  • is the model of the inverted pendulum.
  • is modelica wrapper for our C control software.
  • is the model that couples together plant and controller.

Files ctrl.h and ctrl.c generated by QKS must be put into Resources/Include.

Simulation can be started by running omc run.mos

Control software synthesis for switched systems

This part of the benchmarks is aimed at comparison of our approach with the state-of-the-art tool PESSOA.

By setting \(\mu_1=\mu_2=0.01\) in our model of the inverted pendulum we get a switched system without mode jumps.

We run 1 experiment with PESSOA and 2 experiments with QKS. In all expeirments we used the same sampling time \(T=0.1\).


Experiment configuration:

  • state quantization \(0.0138\) (that corresponds to 9 bits for the angle and 10 bits for the velocity)
  • input range \([-0.5,0.5]\) and input quantization \(0.5\)

Note that this experiment cannot be reproduced inside Docker container, since we cannot redistribute MATLAB environment. To run this experiment navigate inside MATLAB to the directory with the input files and execute InvPend command.

Input and output files can be found in control_software_synthesis/switched/pessoa.

List of the input files:

  • InvPend.m
  • pss_dynamics.m
  • dynamic.m

List of the output files:

  • InvPend.bdd is the OBDD for the abstraction
  • InvPendTargetSet.bdd is the OBDD for the target set
  • InvPendController.bdd is the OBDD for the controller

Also in the same directory you can find Simulink model closed_loop.mdl that allows simulation of the closed loop system obtained with the generated controller, using S-Function block provided together with PESSOA.


We run 2 experiments with QKS with \(\tau=0.01\) and with \(\tau=0.1\). In both experiments we used linerisation computed with \(\varepsilon=0.1\) as error threshold resulting in 8 intervals. We used 9 bits for state quantization and torquing force intensity \(F=0.5\).

Input and output files for the each step of the control software synthesis flow can be found in control_software_synthesis/switched/qks.

For these experiments we also provide Simulink model for simulation: closed_loop.mdl. Before using it, first copy the needed ctrl.c and ctrl.h files (QKS controller) in the same folder as closed_loop.mdl and then compile QKS controller and S-Function into MATLAB MEX executable file:

mex ctrl_sfunction.c ctrl.c