Examples

MTL Formulas

The TLTk uses python objects to represent MTL operations. The currently supported MTL operarations are:

Predicate Definition:

MTL.Predicate(dataName, AMatrix, bMatrix) 

The predicate is defined as a polyhedron in the form Ax ≤ b. For higher diminsional problems dataName can be a list of names and TLTk will zip those rows together. It is recommended to have the data in the correct format before hand and not zip for speed.

For example, we can define

speedPred = Predicate('speed', AMatrix, bMatrix) 

rpmPred = Predicate('rpm', AMatrix, bMatrix) 

MTL Operators

Not:

phi = MTL.Not(speedPred)

And:

phi = MTL.And(speedPred,rpmPred)

Or:

phi = MTL.Or(speedPred,rpmPred)

Next:

phi = MTL.Next(speedPred)

Eventually:

phi = MTL.Finally(lowerTimeBound,upperTimeBound,Subformula) 

The first argument is the lower time bound. The second argument is the upper time bound and can be float(’inf’) to represent infinity. The third argument is either a predicate or another MTL operation.

Always:

phi = MTL.Globaly(lowerTimeBound,upperTimeBound,Subformula) 

The first argument is the lower time bound. The second argument is the upper time bound and can be float(’inf’) to represent infinity. The third argument is either a predicate or another MTL formula.

Until:

phi = MTL.Until(lowerTimeBound,upperTimeBound,Subformula1,Subformula2) 

The first argument is the lower time bound. The second argument is the upper time bound and can be float(’inf’) to represent infinity. The third argument is either a predicate or another MTL operation. The fourth argument is either a predicate or another MTL formula.

Simple MTL Formula Example

We define a simple predicate as follows:

r1 = MTL.Predicate('data1', [1, 1], [150]) 

Mathematically, this defines the set:

$$r1: \begin{bmatrix} 1 & 1 \end{bmatrix} \begin{bmatrix} x_1 \\ x_2 \end{bmatrix} \le 150$$

Where $x_1$ and $x_2$ are the signals the trajectory is defined over.

We define the MTL formula $\varphi=F_{[0,3.14]} (r1)$ as:

phi = MTL.Finally(0,3.14,r1) 

Getting Started Script

The script can be found in tltk/gettingStarted/hello-tltk-rob.py

First, we import the python libraries

import sys
import os
import tltk_mtl as MTL
import numpy as np
import time

Then, we define the options. In this case, we set the computation mode to cpu_threaded.

## Options
mode = 'cpu_threaded'

Next, we define the predicates and MTL formula for $\varphi=\neg(F_{[0,\infty]}(speed>160 \wedge rpm>4500))$

## Predicates and Formulas
Ar1 = -1
br1 = -160
r1 = MTL.Predicate('data1',Ar1,br1)
root = MTL.Not(MTL.Finally(0,float('inf'),r1))

Ar2 = -1
br2 = -4500
r2 = MTL.Predicate('data2',Ar2,br2)

# root = F(r1 /\ r2)
root = MTL.Not(MTL.Finally(0,float('inf'),MTL.And(r1,r2)))

After, we set the system output trace and time stamps.

## Trace and Time Stamps

#trace defined as a dictionary
traces = {'data1': np.ones(10,dtype=np.float32)*5, 'data2': np.ones(10,dtype=np.float32)*10} 
time_stamps = np.arange(1, 10 + 1,dtype=np.float32)

Finally, we compute and print the robustness of the trace with respect to the MTL specification.

## Evaluate Robustness    

t0 = time.time()
root.eval_interval(traces, time_stamps)
t1 = time.time()

print("TLTk" ,"\t | Mode:" ,mode,'\t| Time: ', '%.4f'%(t1 - t0), '    \t| Robustness:', root.robustness)

Falsification Example

We will run the falsification script found in tltk/experiments/falsification/AT1.py

First, we import the python libraries

import matlab.engine
import sys
sys.path.insert(1, '../../')
import numpy as np
import tltk
import tltk_mtl as MTL

Note that this script requires a matlab installation on the system. In addtion, the matlab python package should be configured.

We define the model and simulation parameters:

model = 'models/sldemo_autotrans_mod01'
model_outputs = ['speed','rpm','gear']

step = 0.05
inp_range = [0, 100]
simulation_time = 30

opt = ['simulink', step, inp_range, simulation_time, model_outputs]
interpolation = 'pconst'
mode = 'cpu_threaded'

The specification:

r1 = MTL.Predicate('speed',1,120)    
predicates = [r1]

The control points for the input signal:

cp_bounds = [(0,100) for i in range(7)]

Finally, we run the falsification algorithm:

root = MTL.Global(0,20,r1)
results = tltk.falsify(model, interpolation, cp_bounds, predicates, root, opt)