LTL and STL Assignment

Due Date: 9 October 2026, before 23:59.
Team Size: 2 (pair design/programming)
As of the 2017-2018 Academic Year, each International student should team up with a "local" student (i.e., whose Bachelor degree was obtained at the University of Antwerp).
Submission Information:
- Only one member of each team submits a full solution.
- This must be a compressed archive (ZIP, RAR, TAR.GZ...) that includes your report and all models, images, code and other sources that you have used to create your solution.
- The report must be in PDF and must be accompanied by all images.
- Images that are too large to render on one page of the PDF must still be rendered on the PDF (even though unclear), and the image label should mention the appropriate file included in the submission archive.
- Make sure to mention the names and student IDs of both team members.
- The other team member must submit a single HTML file containing the coordinates of both team members using this template.
Submission Medium: BlackBoard Ultra. Beware that BlackBoard's clock may differ slightly from yours. If BlackBoard is not reachable due to an (unpredicted) maintenance, you should submit your solution via e-mail to the TA. Make sure all group members are in CC!
Contact / TA: Rakshit Mittal.

In this assignment, you will use the pyMTL Python library to check temporal properties on traces obtained by simulating different models of complex Cyber-Physical Systems built using formalisms that you will learn in the course.

In each later assignment, you will be asked to verify some properties of your model using the same techniques. So ensure you understand the concepts and techniques well.

Specifically, in this assignment, you will learn:

Linear Temporal Logic (LTL)
Signal Temporal Logic (STL)

You are discouraged but allowed to make use of any GenAI tool in solving the assignment or writing the report (for example, to correct grammatical mistakes) as long as you adhere to the UA Guidelines for students on responsible use of GenAI.

You are required to cite any use of GenAI and describe what portions of the assignment you used it for.
You should also mention all other sources, including collaborations.

Note that a significant part of demonstrating that the learning goals have been achieved includes being able to

explain the relevant concepts in the assignment,
explain the design choices in your implementation, and
critically discuss your solution.

This will be evaluated in a short (~15 minute) individual oral evaluation, which will typically be conducted in the week following the deadline of each assignment.

You will use pyMTL to perform all the tasks. The library is available to install in your Python environment of choice via PyPI (pip install metric-temporal-logic).

pyMTL checks Metric Interval Temporal Logic (MITL). It does not directly accept an LTL or STL formula as you would write it on paper. You translate the formula yourself into the syntax described below, then evaluate it on a trace.

import mtl

phi = mtl.parse("G[0, 4] (red -> X yellow)")
trace = {
    "red":    [(0, True), (1, True), (2, False), (3, False), (4, False)],
    "yellow": [(0, False), (1, False), (2, True), (3, False), (4, False)],
}
print(phi(trace, time=0, quantitative=False, dt=1))  # True at time 0

A trace is implemented as a dictionary: each atomic predicate maps to a list of (time, value) pairs.
For a Boolean answer, pass quantitative=False.
dt is the time step.
time is the instant at which the formula is evaluated, in the same units as the timestamps in the trace. You will always use time=0 in this asignment.

All Boolean operations must be parenthesised, except for a single negation or a single X. For example:
(red & ~yellow) is correct
red & ~yellow is not correct

not: ~red
and: (red & ~yellow)
or: (red | yellow)
implies: (red -> yellow)
if and only if: (red <-> yellow)
next: X yellow
eventually: F[0, 10] green
always: G[0, 10] red
until: (yellow U green)
weak until: (yellow W green)

An interval [a, b] is read as the half-open range [a, b) in pyMTL. An alternative mathematical notation for a half-open interval is [a,b[. The right endpoint is not included. If the last sample is at time T and you want that sample covered, the upper bound must be strictly larger than T.

From LTL to MITL. Untimed G and F become bounded intervals over the recorded trace. X, U and W stay, with the parentheses required above.

$G\,(\mathit{red} \rightarrow X\,\mathit{yellow})$ becomes G[0, 200] (red -> X yellow) when the rows are steps 0..200 and X must still land on a recorded row (steps 0..199).
$F\,\mathit{green}$ becomes F[0, 201] green, which includes step 200.
$(\mathit{yellow}\,U\,\mathit{green})$ and $(\mathit{yellow}\,W\,\mathit{green})$ are already accepted as (yellow U green) and (yellow W green). Strong until requires green to occur; weak until also holds when yellow lasts until the end of the trace.

From STL to MITL. pyMTL does not accept comparisons. A predicate such as $|\theta| \le 1.5$ is not a legal atomic predicate. Compute it yourself while you load the CSV and write the temporal formula over that resultant signal. Use the trace's own time column as the time stamps, not the row index.

$G_{[0,20]}(|\theta| \le 1.5)$ becomes the atomic predicate angle_ok (true when the inequality holds) and the formula G[0, 20.1] angle_ok. The extra 0.1 includes a sample at time 20.
$F_{[0,8]}(x \ge 9.5)$ becomes F[0, 8.1] reached.
$G_{[30,60]}(|e| \le 0.5)$ becomes G[30, 60.1] gap_close.

import pandas as pd
frame = pd.read_csv("gantry.csv")
trace = {
    "angle_ok": list(zip(frame["time"], frame["gantry.theta"].abs() <= 1.5)),
}
phi = mtl.parse("G[0, 20.1] angle_ok")
print(phi(trace, time=0, quantitative=False))

This assignment has two parts. In each part you formalise the listed claims and evaluate them on every provided trace. The result of that evaluation is a CSV file, one per system, in the format described under Practical Issues.

Verifying LTL properties
1. Simple traffic light
2. Simple production system
3. Pipelined production system
Verifying STL properties
1. Cruise control system
2. Gantry crane system
3. Water heating system

Each part is aligned with one of the learning goals.

Each system comes with ten traces, <system>_1.csv through <system>_10.csv. A trace has 201 rows. Values in the step column run from 0 to 200. Every other cell-value is 0 or 1. Use the column name as a Boolean atomic predicate: 1 means the condition holds at that step, and 0 means it does not.

In your report, for each property, write the LTL formula, the corresponding MITL formula, and any explanation (if needed) for this translation.

Simple traffic light

Figure 1:simple traffic light.

This is a simple traffic light with three colours - red, yellow, and green, constructed as a Petri net (you will learn this formalism in Assignment 4). A color can stay 'on' for several steps in a row. The intended order is red, yellow, green, yellow, red.

red, yellow, and green are 1 when that colour is lit. There are 10 traces:

Drivers are fine with this hypothetical traffic light staying red for a while, or green for a while. What they need is that it never shows two colours at once, and that it does not jump from red straight to green, or from green straight back to red.

Check if the traffic light satisfies the following properties, based on the provided traces:

one_lamp: at every step, exactly one of red, yellow, and green holds.
starts_red: the traffic light starts in red. Note that this says nothing about later steps.
always_red: the traffic light is always red.
eventually_green: green is on at some point in the future.
red_stays_or_next_yellow: every red step is followed by red or yellow.
no_red_to_green: red is never followed immediately by green.
no_green_to_red: green is never followed immediately by red.
yellow_opens_to_green: if yellow is 1, alternate is 0, and the next step is not yellow, then the next step is green. The alternate variable tracks the direction red > yellow > green or green > yellow > red. This property evaluates its function.
yellow_returns_to_red: if yellow is 1, alternate is 1, and the next step is not yellow, then the next step is red. The alternate variable tracks the direction red > yellow > green or green > yellow > red. This property evaluates its function.
yellow_after_red_may_wait: whenever red changes to yellow, yellow holds until green, or through the end of the trace if green never comes (weak until).

Simple production system

Figure 2: Petri net of simple production system.

This is a small workshop with two machines and one technician, again modelled as a Petri net. One part comes in, is worked on by machine 1, then by machine 2, and is then output. From there the workshop keeps waiting until a new product appears at the input. There is no buffer between the machines.

When a machine is working on a part, it may break down with the part still inside it. There is one repair technician available. When he is free, he can be assigned to repair a machine that is down. The machine then resumes working on the part inside it. A machine may break down multiple times when working on a single part.

m1_idle, m1_busy, m1_down, and m1_repair are 1 when machine 1 is in that mode.
machine 2 has the same four columns with the prefix m2_.
tech_free and tech_busy say whether the technician is free or repairing.
p_in, p_m1, p_m2, and p_out are 1 when the part is at that stage.
idle signifies the workshop is waiting for a new part to arrive.

There are 10 traces:

A workshop like this has maximum one part at any given time. The technician cannot repair both machines at once. The part should visit machine 1 before machine 2. After machine 2 has finished working, the workshop remains idle until a new part arrives.

Check if the workshop satisfies the following properties, based on the provided traces:

m1_one_mode: machine 1 is always in one of 4 modes.
m2_one_mode: machine 2 is always in one of 4 modes.
max_one_part: the workshop is either idle or has 1 part which is being processed.
not_both_in_repair: machine 1 and machine 2 are never both being repaired at the same time.
part_at_m1_mode: if machine 1 has the part, it is either busy, broken down, or being repaired.
machines_not_both_holding: machine 1 and machine 2 never hold a part at the same time.
m1_before_m2: the part is not on machine 2 until it has been on machine 1.
eventually_shipped: the part reaches the output at some point.
wait_may_continue: whenever the part leaves the output and the workshop starts waiting, it keeps waiting until a new part arrives, or through the end of the trace if none does (weak until).

Pipelined production system

Figure 2: Petri net of pipelined production system.

This is the same workshop on a busier day. A new part can arrive while an earlier one is still being processed. There is a single buffer between the machines. There can be a maximum of one part in the input queue and one part at the output, before it is shipped.

The machine and technician columns mean the same as in the previous system. p_in, p_m1, p_buffer, p_m2, and p_out are 1 when a part is at that stage. Several of them can be 1 at the same time, since this workshop is pipelined. There is no idle column. There are 10 traces:

The technician still cannot repair both machines at once. What is new is that both machines, and the buffer, may hold a part at the same time. A part should still go through machine 1 before machine 2.

NOTE: Why a second workshop? A temporal-logic formula can only talk about what the trace records. Here each column tells you whether a stage holds a part, but not which part. With one part in the building, that is enough to follow the part through the whole workshop. Once several parts are in flight, the same columns can no longer tell them apart, so a claim such as "every part visits machine 1 before machine 2" cannot be written with these atomic predicates. What you can still check are claims about stages and single steps: which stages are occupied together, and what one step changes.

Choosing properties that the can be expressed based on the available observations, or more commonly, designing an experiment which includes observations that are needed to express desired properties is part of systems engineering.

Check if the workshop satisfies the following properties, based on the provided traces:

m1_one_mode: machine 1 is always in one of 4 modes.
not_both_in_repair: machine 1 and machine 2 are never both being repaired at the same time.
both_machines_holding: both machines hold a part at the same time, at some point.
m1_while_buffer_full: machine 1 holds a part while the buffer is also occupied, at some point.
m1_to_buffer: the part leaves machine 1 only when the machine is working and the buffer is free, and it then sits in the buffer. A breakdown or a repair leaves the part on the machine.
ship_removes_only_out: when a finished part is shipped, the parts at the input, on machine 1, in the buffer, and on machine 2 stay where they are.
arrival_only_fills_in: when a new part arrives at the input, the parts already on machine 1, in the buffer, on machine 2, and at the output stay where they are.

Each of the following systems is controlled by a PID controller, tuned by three gains (multiplication factors): Kp (proportional), Ki (integral), and Kd (derivative). Different gains make the same system behave very differently. You will learn more about PID control in the next assignment.

Each system comes with ten traces, <system>_kp<Kp>_ki<Ki>_kd<Kd>.csv, one per set of PID gain parameter settings. The first column, time, is the simulation time in seconds. Every other column is a real-valued signal. Build a Boolean signal for each predicate from these columns, and use the time values as the timestamps.

In your report, for each property, write the STL formula, the Boolean signals you built, the corresponding MITL formula, and any extra explanation (if needed) for this translation.

Cruise control

Figure 4: Cruise control system.

The figure shows an ego car following a car in front of it. The car (physical) and a PID controller adapting its speed (ultimately realized in software) are modelled in Modelica (which will be introduced in the next lecture) and simulated. The goal for the controller is to keep 10 m between the bumpers. Each trace runs for 60 seconds.

Note: This example has been taken from the Modelica assignment of the 2023-2024 iteration of the course. You may learn more about this system on the assignment page.

intervehicular_distance.y is the gap in metres.
ego_car.accSensor.a is the acceleration of the following car, in m/s�.
ego_car.speedSensor.v is the speed of the following car.

There are 10 traces:

A gentle tuning eases into the gap and stays there. An unstable one stamps on the accelerator and the brake. One of the runs gets close enough that you would not want to be in the passenger seat.

Check if the controller satisfies the following properties, based on the provided traces:

reaches_soon: within the first 20 s, the gap is within 0.5 m of 10.
settled_tight: from time 30 through the end, the gap stays within 0.5 m of 10.
settled_loose: from time 20 through the end, the gap stays within 1 m of 10.
keeps_distance: the gap is at least 9 m at every sample.
accel_bounded: the absolute acceleration is at most 10 m/s� at every sample.

Gantry crane

Figure 5: Gantry crane system.

This is a pendulum hanging off a trolley attached to a rail (physical) and a PID controller adapting the trolley's speed (ultimately realized in software) again modelled in Modelica and simulated. The goal is for the trolley to reach position 10 mtrs. Each trace runs for 20 seconds. The filename records the PID gains.

Note: This example has been taken from the Modelica assignment of the 2024-2025 iteration of the course. You may learn more about this system on the assignment page.

gantry.x is the trolley position.
gantry.theta is the sway angle in radians; a swing to the left and a swing to the right are both recorded, with opposite signs.

There are 10 traces:

Move too fast and the pendulum swings too much. Move too slow and it never arrives. The trolley cannot overshoot the target position by too much as the length of the rail is limited.

Check if the crane satisfies the following properties, based on the provided traces:

angle_within_half: the absolute angle is at most 0.5 rad.
angle_within_limit: the absolute angle is at most 1.5 rad.
reaches_by_8s: the position reaches at least 9.5 within the first 8 s.
settled: from time 10 through the end, the position stays within 0.5 of the setpoint.
no_overshoot: the position is always at most 10.5.

Water heating

Figure 6: Water heating system.

This is a a hot-water tank (physical) and a PID controller (ultimately realized in software) that drives a heater to keep the hot-water tank's water temperature at 50°C (323.15 K). A separate on/off controller (also ultimately realized in software) tops the tank up when the level falls. The system is again modelled in Modelica, and simulated for one day (86400 seconds). The filename records the PID gains.

Note: This example has been taken from the Modelica assignment of the 2025-2026 iteration of the course. You may learn more about this system on the assignment page.

plant_block1.T_out is the outlet temperature in kelvin.
plant_block1.level_out is the tank level.
pid_controller1.limiter.y is the heater power.

There are 10 traces:

Some tunings climb to the setpoint and sit there. Others overshoot. The ones with no integral action never ease off the heater. The level should stay in a comfortable band the whole day.

Check if the tank satisfies the following properties, based on the provided traces:

reaches_setpoint: the outlet eventually reaches at least 321.15 K.
no_temperature_overshoot: the outlet stays at or below 330 K.
settled_after_half_day: from time 43200 through the end, the outlet stays within 3 K of 323.15 K.
level_in_band: the level stays between 1.4 and 2.9.
heater_stays_on: the heater power stays at least 150.

Submit one CSV per system, with these exact filenames:

simple_traffic_light_ltl.csv
production_system_ltl.csv
production_system_pipelined_ltl.csv
car_system_stl.csv
gantry_system_stl.csv
water_heating_system_stl.csv

The first row is a header. The first column should be trace. The remaining columns should be the property names for that system.
Each following row should be for one trace. The first cell in a row should be the trace filename, including .csv.
Every other cell should be true or false, in lowercase, with no quotes and no spaces.

The traffic-light file, for example, begins like this. The true and false values are made up:

trace	one_lamp	starts_red	always_red	eventually_green	red_stays_or_next_yellow	no_red_to_green	no_green_to_red	yellow_opens_to_green	yellow_returns_to_red	yellow_after_red_may_wait
simple_traffic_light_1.csv	false	true	false	true	false	true	false	true	false	true

Practical Information

Goals

pyMTL

Assignment Overview

LTL Properties

Simple traffic light

Simple production system

Pipelined production system

STL Properties

Cruise control

Gantry crane

Water heating

Practical Issues