ltlparse: temporal expression evaluator
ltlparse provides a language specification for defining temporal expressions which act on timed data, from either a simulation or a real-time system. During execution of either, ltlparse will verify the truthiness of the user-specified formulas.
Timed data is (currently) sourced from a set of user-specified comma-separated-value files, which are written to by external programs, and watched/read by ltlparse.
In the configuration file, each formula defined has an associated csv path, allowing for different formulas to work on data from different sources. Nonetheless, multiple formulas may take data from the same csv file.
The intended use-case of ltlparse is real-time evaluation of temporal formulas for error and safety-checking, especially for robotic systems.
This brings us to the following roadmap:
Development Roadmap
- Define syntax
- Define state-trajectory data format (JSON)
- Parse ASTs
- Finalize CLI
- Support unbounded linear operators
- Create API communication interface. (CSVs, for now)
- Support bounded linear operators
- Automated testing?
Syntax specification
To maximize usability, the arithmetic syntax is an infix representation similar to that used C/C++. Here we define all of the operators included in the syntax, in order of increasing execution priority.
| Priority | Ops | Arity | Description |
|---|---|---|---|
| 1 | || | 2 | Logical OR |
| 2 | ^^ | 2 | Logical XOR |
| 3 | && | 2 | Logical AND |
| 4 | == | 2 | Equals |
| 4 | != | 2 | Not-equals |
| 5 | < | 2 | Less-than |
| 5 | <= | 2 | Less-than-or-equal |
| 5 | > | 2 | Greater-than |
| 5 | >= | 2 | Greater-than-or-equal |
| 6 | + | 2 | Add |
| 6 | - | 2 | Subtract |
| 7 | * | 2 | Multiply |
| 7 | / | 2 | Divide |
| 7 | % | 2 | Modulo (Remainder) |
| 8 | ^ | 2 | Power |
| 9 | ! | 1 | Logical NOT |
| 10 | N: | 1 | Next 1 |
| 10 | A: | 1 | Always 2 |
| 10 | E: | 1 | Eventually 3 |
| 10 | U: | 2 | Until 4 |
| 10 | R: | 2 | Release 5 |
_
| Unbounded LTL Operators | Description |
|---|---|
| N: (x) | x must have held in the previous time instance. |
| A: (x) | x must have held in all previous time instances, as well as the current instance. |
| E: (x) | x must hold in any of the previous time instances, or the current instance. |
| (x) U: (y) | x must have held at least until y became true, which must have held during any point, including now. |
| (x) R: (y) | y had to have held until and including the first instance where x held; if x never holds, y must always hold. |