Python library for working with Metric Temporal Logic (MTL)

# mvcisback/py-metric-temporal-logic

Switch branches/tags
Nothing to show

A tag already exists with the provided branch name. Many Git commands accept both tag and branch names, so creating this branch may cause unexpected behavior. Are you sure you want to create this branch?

## Files

Failed to load latest commit information.
Type
Name
Commit time A library for manipulating and evaluating metric temporal logic.

Python library for working with Metric Temporal Logic (MTL). Metric Temporal Logic is an extension of Linear Temporal Logic (LTL) for specifying properties over time series (See Alur). Some practical examples are given in the usage.

# Installation

If you just need to use `metric-temporal-logic`, you can just run:

`\$ pip install metric-temporal-logic`

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

To begin, we import `mtl`.

`import mtl`

There are two APIs for interacting with the `mtl` module. Namely, one can specify the MTL expression using:

We begin with the Python Operator API:

## Python Operator API

### Propositional logic (using python syntax)

```a, b = mtl.parse('a'), mtl.parse('b')
phi0 = ~a
phi1 = a & b
phi2 = a | b
phi3 = a ^ b
phi4 = a.iff(b)
phi5 = a.implies(b)```

### Modal Logic (using python syntax)

```a, b = mtl.parse('a'), mtl.parse('b')

# Eventually `a` will hold.
phi1 = a.eventually()

# `a & b` will always hold.
phi2 = (a & b).always()

# `a` until `b`
phi3 = a.until(b)

# `a` weak until `b`
phi4 = a.weak_until(b)

# Whenever `a` holds, then `b` holds in the next two time units.
phi5 = (a.implies(b.eventually(lo=0, hi=2))).always()

# We also support timed until.
phi6 = a.timed_until(b, lo=0, hi=2)

# `a` holds in two time steps.
phi7 = a >> 2```

## String based API

### Propositional logic (parse api)

```# - Lowercase strings denote atomic predicates.
phi0 = mtl.parse('atomicpred')

# - infix operators need to be surrounded by parens.
phi1 = mtl.parse('((a & b & c) | d | e)')
phi2 = mtl.parse('(a -> b) & (~a -> c)')
phi3 = mtl.parse('(a -> b -> c)')
phi4 = mtl.parse('(a <-> b <-> c)')
phi5 = mtl.parse('(x ^ y ^ z)')

# - Unary operators (negation)
phi6 = mtl.parse('~a')
phi7 = mtl.parse('~(a)')```

### Modal Logic (parser api)

```# Eventually `x` will hold.
phi1 = mtl.parse('F x')

# `x & y` will always hold.
phi2 = mtl.parse('G(x & y)')

# `x` holds until `y` holds.
# Note that since `U` is binary, it requires parens.
phi3 = mtl.parse('(x U y)')

# Weak until (`y` never has to hold).
phi4 = mtl.parse('(x W y)')

# Whenever `x` holds, then `y` holds in the next two time units.
phi5 = mtl.parse('G(x -> F[0, 2] y)')

# We also support timed until.
phi6 = mtl.parse('(a U[0, 2] b)')

# Finally, if time is discretized, we also support the next operator.
# Thus, LTL can also be modeled.
# `a` holds in two time steps.
phi7 = mtl.parse('XX a')```

## Quantitative Evaluate (Signal Temporal Logic)

Given a property `phi`, one can evaluate if a timeseries satisifies `phi`. Time Series can either be defined using a dictionary mapping atomic predicate names to lists of (`time`, `val`) pairs or using the DiscreteSignals API (used internally).

There are two types of evaluation. One uses the boolean semantics of MTL and the other uses Signal Temporal Logic like semantics.

```# Assumes piece wise constant interpolation.
data = {
'a': [(0, 100), (1, -1), (3, -2)],
'b': [(0, 20), (0.2, 2), (4, -10)]
}

phi = mtl.parse('F(a | b)')
print(phi(data))
# output: 100

# Evaluate at t=3
print(phi(data, time=3))
# output: 2

# Evaluate with discrete time
phi = mtl.parse('X b')
print(phi(data, dt=0.2))
# output: 2```

## Boolean Evaluation

To Boolean semantics can be thought of as a special case of the quantitative semantics where `True ↦ 1` and `False ↦ -1`. This conversion happens automatically using the `quantitative=False` flag.

```# Assumes piece wise constant interpolation.
data = {
'a': [(0, True), (1, False), (3, False)],
'b': [(0, False), (0.2, True), (4, False)]
}

phi = mtl.parse('F(a | b)')
print(phi(data, quantitative=False))
# output: True

phi = mtl.parse('F(a | b)')
print(phi(data))
# output: True

# Note, quantitative parameter defaults to False

# Evaluate at t=3.
print(phi(data, time=3, quantitative=False))
# output: False

# Compute sliding satisifaction.
print(phi(data, time=None, quantitative=False))
# output: [(0, True), (0.2, True), (4, False)]

# Evaluate with discrete time
phi = mtl.parse('X b')
print(phi(data, dt=0.2, quantitative=False))
# output: True```

## Utilities

```import mtl
from mtl import utils

print(utils.scope(mtl.parse('XX a'), dt=0.1))
# output: 0.2

print(utils.discretize(mtl.parse('F[0, 0.2] a'), dt=0.1))
# output: (a | X a | XX a)```

# Similar Projects

Feel free to open up a pull-request to add other similar projects. This library was written to meet some of my unique needs, for example I wanted the AST to be immutable and wanted the library to just handle manipulating MTL. Many other similar projects exist with different goals.

# Citing

``````@misc{pyMTL,
author       = {Marcell Vazquez-Chanlatte},
title        = {mvcisback/py-metric-temporal-logic: v0.1.1},
month        = jan,
year         = 2019,
doi          = {10.5281/zenodo.2548862},
url          = {https://doi.org/10.5281/zenodo.2548862}
}
``````

Python library for working with Metric Temporal Logic (MTL)

1 tags

## Packages 0

No packages published