Main contributors of the tool are Georgios Fainekos and Sriram Sankaranarayanan

This tool searches for trajectories of minimal robustness in Simulink/Stateflow. It uses randomized testing based on stochastic optimalization techniques (Monte-Carlo, Ant-Colony optimalization, etc.). It is modular and new stochaistic optimalization algorithms can be easily implemented and integrated.

S-Taliro searches for counterexamples to Metric Temporal Logic (MTL) [1] properties for non-linear hybrid systems. This goal is achieved by previously noted minimization of a robustness metric. To achieve this goal S-Taliro uses either m-functions in Matlab which would describe the system, but preferably Simulink/Stateflow models that can S-Taliro use for simulation under given circumstances.

In it's core S-Taliro uses combination of stochastic sampling together with Simulink simulation runs and a little bit of optimalization. Using this approach, tool finds the smallest robustness which is desirable, because traces with lower robustness value are closer in distance to falsifying traces. If the tool detect a negative robustness we acquire a trace which falsify temporal logic properties. Robustness is calculated by Taliro module, but the computation is based on the results of convex optimalization problems used to compute signed distances. The structure of the tool and it's architecture is describe on this picture: [2]

S-Taliro core

S-TaLiRo Installation

Installation of S-Taliro is easy, just download the software from Source and run function in file setup_staliro.m in MATLAB. There may be a problem with paths, at least I have faced it on both environments; Linux and Windows. As a hotfix solution I just overwritten the relative paths to absolute path form and marked a note to find more elegant solution (TODO!) in future for my virtual environment which is still under construction.

Another possible problem can be compilation of C++ files, because on Linux I had pre-installed gcc version 7.something.something and recommended gcc version for the files is 4.4.*. Naturally GCC couldn't compile the source code due to some issues with comments or whatsoever. I have also noticed that there is an old version of Matlab 2013, so I switched to Windows where 2017 version of MATLAB is installed. For compilation MATLAB used default MinGW and compilation ran without problems.

After successful installation of S-Taliro tools I started to examine demos.

How to use S-TaLiRo

Prerequisite: Input signals must be provided to the Simulink model through input ports

Georgios Fainekos has written S-Taliro quick guide. It explains how should be S-Taliro used, what it can do and how it works. S-Taliro takes a system model (such as Simulink model) and also a set of MTL specifications and calculate different trajectories, experiment on a certain surrounding around the simulation to be able detect robustness. Based on the robustness calculate stochastic optimizations and creates new parameters specification.

Using this approach S-Taliro tries many different runs of the simulation, but with reasonable parameters which are altered in order to enclose as much as possible to real world situations. Robustness is calculated and in case that constraints are violated, witness trajectory is generated.

S-Taliro has a certain requirements on the model, for example input signals has to have a form of input ports. To define specifications authors recommend using output ports. This way S-Taliro treats model as black-box.

There are mentioned two algorithms in the quick guide:

Room heating benchmark HEAT30

This benchmark model was introduced by Ansgar Fehnker and Franjo Ivančić in paper Benchmarks for Hybrid Systems Verification [5]. Sadly our library has no available copy of this document, though I have requested that library should borrow one.

This model represent 10 rooms and 4 heaters which result in 3 360 discrete locations. The goal for veryfication is to verify that for rooms x_0 up to xn no room temperature drops below [14.50; 14.50; 13.50; 14.00; 13.00; 14.00; 14.00; 13.00; 13.50; 14.00]. The initial conditions are temperatures in range of [17,18]. The input signal was parametrized using a piecewise cubic Hermite interpolating polynomial with 4 control points evenly distributed in the simulation time. Look of the model in Simulink:

HEAT30 benchmark

When S-Taliro is used to falsify the model, it can run for example for 40 minutes and find a witness Falsifying input signal together with initial conditions and resulting trajectories like in my case when I ran the tool. This is the output:

HEAT30 falsification

MTL in S-TaLiRo

In order to run different experiments on different CPS and other real-time systems I need to understand the usage of MTL specification in S-TaLiRo tools. Traditional MTL operators are translated into S-TaLiRo according to this table:

transform table for MTL in S-TaLiRo


These conversions are used in Matlab scripts to define restriction formulas in MTL. Needles to say that [a,b} are non-negative integers which does not represent simulation time, but number of samples. Example such restriction can be bounded response: Always between 3 to 5 samples in the past 'p1' implies eventually 'p2' within 1 sample -- [.]_[3,5](p1 -> <>_[0,1] p2). More info by typing 'help monitor' (TaliRo) into MATLAB.

For example in the case of Room heating benchmark:

sTaliro room heating benchmark script

We can see that in the section MTL spec there are 4 lines:

This means that there are one or more restrictions on the output values of varibale x. Mind, that there may be not only one x, but more different x as there may be more different outputs. The best ilustration is in the case of demo autotrans (automatic transmition). There are two output values, speed of a car and RPM. Because there are two output values, predicate for speed will be preds(ii).A = [-1 0] and preds(ii).b = -120. This practically says: "I do not care about the RPM, but the speed restriction is x >= 120. That is why A here has two elements.

3rd order Delta-Sigma Modulator

There is another demo based on a model of a 3rd order Delta-Sigma Modulator. The goal here is to find state trajectories that might reach the saturation threshold. In other words, the requirements are that -1 <= x_i <= 1 for i = 1,2,3.

How to specify this in a MTL form and then verify it using S-TaLiRo tools? Well in MTL it is easy. Given that the equation is a formula phi, then simply Ga, because at any time must this restriction hold true. In S-TaLiRo version it would be written as []a. But how to write the restriction itself in S-TaLiRo form of predicates? Let's look on the author's way how to write it down:

sTaliro room 3rdOrderModulator benchmark script

As we can see Preds(i).A has six dimensions, each of those has three variables. Indeed it corresponds with the definition of three output variables x_1, x_2 and x_3. On the other line is a definiton of Preds(i).b. It has only six numbers, all ones. It makes sense because we will be using each number for different dimension in Preds(i).A. First two dimensions in Preds(i).A define restrictions about x_1, namely that 1x_1 <= 1 and then -1x_1 <= 1, which converts into x_1 >= -1 which is exactly what we needed. Similarly it goes for x_2 and x_3. I have tested this hypotesis by modifying the Preds(i).b values and behavior of the system confirmed the assumption.

Here is the output of the system state trajectories with the original definition:

sTaliro room 3rdOrderModulator benchmark default output

And here is the output with my modification of Preds(i).b (all 1 changed to 2):

sTaliro room 3rdOrderModulator benchmark altered

These screenshots nicely demonstrate how one can change the problem of a model verification by changing constraints.


[1] Koymans, R. Real-Time Syst (1990) 2: 255. https://doi.org/10.1007/BF01995674

[2] Annpureddy Y., Liu C., Fainekos G., Sankaranarayanan S. (2011) S-TaLiRo: A Tool for Temporal Logic Falsification for Hybrid Systems. In: Abdulla P.A., Leino K.R.M. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2011. Lecture Notes in Computer Science, vol 6605. Springer, Berlin, Heidelberg

[3] H. Kress-Gazit, G. E. Fainekos and G. J. Pappas, "Temporal-Logic-Based Reactive Mission and Motion Planning," in IEEE Transactions on Robotics, vol. 25, no. 6, pp. 1370-1381, Dec. 2009.

[4] Sriram Sankaranarayanan and Georgios Fainekos. 2012. Falsification of temporal properties of hybrid systems using the cross-entropy method. In Proceedings of the 15th ACM international conference on Hybrid Systems: Computation and Control (HSCC '12). ACM, New York, NY, USA, 125-134. DOI=http://dx.doi.org/10.1145/2185632.2185653

[5] Fehnker A., Ivančić F. (2004) Benchmarks for Hybrid Systems Verification. In: Alur R., Pappas G.J. (eds) Hybrid Systems: Computation and Control. HSCC 2004. Lecture Notes in Computer Science, vol 2993. Springer, Berlin, Heidelberg

[6] Linear Programming course at UCLA