Past MTL Monitors

A library for creating past metric temporal logic monitors.

Table of Contents

• Past MTL Monitors
• Installation
• Usage

Installation

If you just need to use past-mtl-monitors, you can just run:

$ pip install past-mtl-monitors

For developers, note that this project uses the poetry python package/dependency management tool. Please familarize yourself with it and then run:

$ poetry install

Usage

The primary entry point to the past-mtl-monitors package is the atom function. This exposes a monitor factory which can be combined with other monitor factories to create complex property monitors.

Under the hood, these monitor factories are just wrappers around python coroutines that expect a (time, val) pair, where time is a float and val is a mapping from strings to robustness values (float).

Note past-mtl-monitors only implements a quantitative semantics where a value greater than 0 implies sat and a value less than 0 implies unsat.

Thus if one would like to use Boolean semantics, use 1 for True and -1 for False.

from past_mtl_monitors import atom

x, y, z = atom('x'), atom('y'), atom('z')

# Monitor that historically, x has been equal to y.
monitor = (x == y).hist().monitor()

#                    time         values
assert monitor.send((0    , {'x': 1, 'y': 1}))  ==  1   # sat
assert monitor.send((1.1  , {'x': 1, 'y': -1})) == -1   # unsat
assert monitor.send((1.5  , {'x': 1, 'y': 1}))  == -1   # unsat

monitor2 = x.once().monitor()  # Monitor's x's maximum value.
assert monitor2.send((0 , {'x': -10, 'y': 1})) == -10
assert monitor2.send((0 , {'x': 100, 'y': 2})) == 100
assert monitor2.send((0 , {'x': -100, 'y': -1})) == 100

# Monitor that x & y have been true since the last
# time that z held for 3 time units.
monitor3 = (x & y).since(z.hist(0, 3)).monitor()