metric-temporal-logic
Python library for working with Metric Temporal Logic (MTL)
Science Score: 77.0%
This score indicates how likely this project is to be science-related based on various indicators:
-
✓CITATION.cff file
Found CITATION.cff file -
✓codemeta.json file
Found codemeta.json file -
✓.zenodo.json file
Found .zenodo.json file -
✓DOI references
Found 4 DOI reference(s) in README -
✓Academic publication links
Links to: springer.com, zenodo.org -
✓Committers with academic emails
2 of 9 committers (22.2%) from academic institutions -
○Institutional organization owner
-
○JOSS paper metadata
-
○Scientific vocabulary similarity
Low similarity (14.0%) to scientific vocabulary
Repository
Python library for working with Metric Temporal Logic (MTL)
Basic Info
Statistics
- Stars: 100
- Watchers: 5
- Forks: 18
- Open Issues: 1
- Releases: 1
Metadata Files
README.md
Table of Contents
About
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.
python
import mtl
There are two APIs for interacting with the mtl module. Namely, one can specify the MTL expression using:
1. Python Operators.
2. Strings + The parse API.
We begin with the Python Operator API:
Python Operator API
Propositional logic (using python syntax)
python
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)
```python 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)
```python
- 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)
```python
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.
```python
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.
```python
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
```python 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.
- https://github.com/doganulus/python-monitors
- https://github.com/STLInspector/STLInspector
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}
}
Owner
- Name: Marcell Vazquez-Chanlatte
- Login: mvcisback
- Kind: user
- Website: mjvc.me
- Repositories: 78
- Profile: https://github.com/mvcisback
Citation (CITATION.cff)
cff-version: 1.2.0 message: "If you use this software, please cite it as below." authors: - family-names: "Vazquez-Chanlatte" given-names: "Marcell" orcid: "https://orcid.org/0000-0002-1248-0000" title: "py-metric-temporal-logic" version: 0 date-released: 2021-08-02 url: "https://github.com/mvcisback/py-metric-temporal-logic"
GitHub Events
Total
- Watch event: 6
- Fork event: 1
Last Year
- Watch event: 6
- Fork event: 1
Committers
Last synced: almost 3 years ago
All Time
- Total Commits: 307
- Total Committers: 9
- Avg Commits per committer: 34.111
- Development Distribution Score (DDS): 0.15
Top Committers
| Name | Commits | |
|---|---|---|
| Marcell Vazquez-Chanlatte | m****c@l****m | 261 |
| pyup-bot | g****t@p****o | 29 |
| Shromona MacBook | s****h@b****u | 7 |
| Gaudeval | m****c@g****m | 4 |
| jimkapin | j****n@a****m | 2 |
| Andrea Burattin | d****s@u****m | 1 |
| Daniel Fremont | d****t@u****u | 1 |
| Dreossi | d****t@3****m | 1 |
| Konstantin Veretennicov | k****b@g****m | 1 |
Committer Domains (Top 20 + Academic)
Issues and Pull Requests
Last synced: 6 months ago
All Time
- Total issues: 10
- Total pull requests: 90
- Average time to close issues: 5 months
- Average time to close pull requests: 12 days
- Total issue authors: 6
- Total pull request authors: 8
- Average comments per issue: 3.2
- Average comments per pull request: 0.92
- Merged pull requests: 7
- Bot issues: 0
- Bot pull requests: 1
Past Year
- Issues: 0
- Pull requests: 0
- Average time to close issues: N/A
- Average time to close pull requests: N/A
- Issue authors: 0
- Pull request authors: 0
- Average comments per issue: 0
- Average comments per pull request: 0
- Merged pull requests: 0
- Bot issues: 0
- Bot pull requests: 0
Top Authors
Issue Authors
- Gaudeval (3)
- sokolsky (2)
- xian49930 (2)
- jpk15211 (1)
- ZikangXiong (1)
- mvcisback (1)
Pull Request Authors
- pyup-bot (80)
- Gaudeval (4)
- delas (1)
- dfremont (1)
- jpk15211 (1)
- dreossi (1)
- dependabot[bot] (1)
- kveretennicov (1)
Top Labels
Issue Labels
Pull Request Labels
Packages
- Total packages: 1
-
Total downloads:
- pypi 1,393 last-month
- Total dependent packages: 4
- Total dependent repositories: 3
- Total versions: 15
- Total maintainers: 1
pypi.org: metric-temporal-logic
A library for manipulating and evaluating metric temporal logic.
- Homepage: https://github.com/mvcisback/py-metric-temporal-logic
- Documentation: https://metric-temporal-logic.readthedocs.io/
- License: MIT
-
Latest release: 0.4.1
published about 3 years ago
Rankings
Maintainers (1)
Dependencies
- apipkg 1.5 develop
- atomicwrites 1.4.0 develop
- certifi 2020.6.20 develop
- chardet 3.0.4 develop
- codecov 2.1.8 develop
- colorama 0.4.3 develop
- coverage 4.5.4 develop
- execnet 1.7.1 develop
- flake8 3.8.3 develop
- hypothesis 4.24.1 develop
- hypothesis-cfg 0.2 develop
- idna 2.10 develop
- importlib-metadata 1.7.0 develop
- iniconfig 1.0.1 develop
- mccabe 0.6.1 develop
- more-itertools 8.4.0 develop
- packaging 20.4 develop
- pluggy 0.13.1 develop
- py 1.9.0 develop
- pycodestyle 2.6.0 develop
- pyflakes 2.2.0 develop
- pyparsing 2.4.7 develop
- pytest 6.0.1 develop
- pytest-cov 2.10.1 develop
- pytest-flake8 1.0.6 develop
- pytest-forked 1.3.0 develop
- pytest-sugar 0.9.4 develop
- pytest-xdist 1.34.0 develop
- requests 2.24.0 develop
- termcolor 1.1.0 develop
- toml 0.10.1 develop
- urllib3 1.25.10 develop
- zipp 3.1.0 develop
- attrs 19.3.0
- discrete-signals 0.7.3
- funcy 1.14
- lenses 0.5.0
- parsimonious 0.8.1
- singledispatch 3.4.0.3
- six 1.15.0
- sortedcontainers 2.2.2