A Simple Rewrite System for the Normalization of LTL formulas

This repository contains the implementation of a simple rewrite system to normalize any LTL formula into the class Δ₂ of the safety-progress hierarchy. More precisely, the normal forms produced are Boolean combinations of formulas in Σ₂ and formulas in GF Σ₁.

Usage

The ltlnorm program interactively reads LTL formulas in the Spot format, line by line, and prints their normal forms using the same syntax.

Several test cases in tests and auxiliary scripts in scripts are provided to test and benchmark the implementation. For example, the following command runs a test suite of 1000 random formulas:

$ python scripts/check.py tests/random1000.spot

The option --equiv-check can be passed to check the equivalence of the normal form with regard to the original formula (it may take some time). Owl can also be executed using this script. A statistical summary of the results can be obtained with

$ python scripts/summarize.py result.csv

Spot's Python library is required for the first and other scripts, and Pandas is required for the last one.

How to build

The Meson build system can be used to generate the ltlnorm program.

$ meson --buildtype release build

Input formulas are parsed with Spot, so this library is a required dependency for ltlnorm. If Spot is properly installed, it will be found by Meson through pkg-config.