In Incer Romeo et al., we propose a measure and a metric on the sets of infinite traces generated by a set of atomic propositions. To compute these quantities, we first map properties to subsets of the real numbers and then take the Lebesgue measure of the resulting sets. We analyze how this measure is computed for Linear Temporal Logic (LTL) formulas. Here you find our implementation for computing the measure of bounded LTL properties. This implementation leverages SAT model counting (see sharpSAT) and effects independence checks on subexpressions to compute the measure and metric compositionally.
-
To install, run:
pip install -e . -
To install dependencies, run:
./install_deps
NOTE: building sharpSAT requires G++ 4.7.
For a timebound of 5, calculate the measure of 'F a => F b':
python measure.py 5 'F a -> F b'
For a timebound of 5, calculate the distance between formulas 'F a' and 'XF a':
python measure.py -d 5 'F a' 'XF a'
This project is licensed under the terms of the GNU General Public License v3.0 license.