PyTWTL is a Python 2.7 implementation of the algorithms proposed in [1] based on LOMAP [2], ANTLRv3 [3] and networkx [4] libraries. PyTWTL implementation is released under the GPLv3 license. The library can be used to:
- construct DFAs and annotated DFAs from TWTL formulae;
- monitor the satisfaction of a TWTL formula;
- monitor the satisfaction of an arbitrary relaxation of a TWTL formula;
- compute the temporal relaxation of a trace with respect to a TWTL formula;
- compute a satisfying control policy with respect to a TWTL formula;
- compute a minimally relaxed control policy with respect to a TWTL formula;
- verify if all traces of a system satisfy some relaxed version of a TWTL formula;
- learn the parameters of a TWTL formula, i.e. the deadlines.
The parsing of TWTL formulae is performed using ANTLRv3 framework. The package provides grammar files which may be used to generate lexers and parsers for other programming languages such as Java, C/C++, Ruby. To support Python 2.7, we used version 3.1.3 of ANTLRv3 and the corresponding Python runtime ANTLR library, which we included in our distribution for convenience.
If you use TWTL or PyTWTL, then please consider citing the reference paper:Cristian-Ioan Vasile, Derya Aksaray, and Calin Belta. "Time Window Temporal Logic". Theoretical Computer Science, 691(Supplement C):27–54, August 2017. doi:10.1016/j.tcs.2017.07.012, [bib]
Download The package is written for python 2.7. The following python packages are required:- NumPy
- NetworkX (<=1.11)
- ParallelPython
- matplotlib
- setuptools
- ANTLRv3 python runtime
pip install networkx==1.11, numpy, matplotlib, pp, antlr-python-runtime, setuptools
See examples_tcs.py for examples of the algorithms and the PyTWTL API.
An ANT build file build.xml is provided to generate the lexer and parser from the ANTLR3 grammar files.
Copyright (C) 2015-2018 Cristian Ioan Vasile <cvasile@;mit.edu>
Hybrid and Networked Systems (HyNeSs) Group, BU Robotics Lab, Boston UniversityThis program is free software: you can redistribute it and/or modify it under the terms of the GNU General Public License as published by the Free Software Foundation, either version 3 of the License, or (at your option) any later version.
This program is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License for more details.
You should have received a copy of the GNU General Public License along with this program. If not, see <http://www.gnu.org/licenses/>.
A copy of the GNU General Public License is included in the source folder in a file called 'gpl.txt'.
TWTL uses the ANTLR (version 3.1.3) third party Java library to generate the lexers and parsers. It is included for convenience in the 'lib' folder of the distribution source tree. The library can be downloaded from https://github.com/antlr/website-antlr3/tree/gh-pages/download. See the file names 'license.txt' for copyright notices and license information of packages used in PyTWTL.
[1] Cristian Ioan Vasile, Derya Aksaray, and Calin Belta. "Time Window Temporal Logic". Theoretical Computer Science, 691(Supplement C):27–54, August 2017. doi:10.1016/j.tcs.2017.07.012.
[2] Alphan Ulusoy, Stephen L. Smith, Xu Chu Ding, Calin Belta, and Daniela Rus. "Optimality and robustness in multi-robot path planning with temporal logic constraints." The International Journal of Robotics Research 32, no. 8 (2013): 889-911.
[3] Terence Parr. "The Definitive ANTLR Reference: Building Domain-Specific Languages." Pragmatic Bookshelf, 2007. ISBN 978-0978739256.
[4] Aric A. Hagberg, Daniel A. Schult, and Pieter J. Swart. "Exploring network structure, dynamics, and function using NetworkX." 2008.