Testing the equivalence of two formulas

Using a ltlfilt you can use --equivalent-to=f to filter a list of LTL formula and retain only those equivalent to f. So this gives an easy way to test the equivalence of two formulas:

ltlfilt -f '(a U b) U a' --equivalent-to 'b U a'

(a U b) U a

Since the input formula was output, it means it is equivalent to b U a. You may want to add -c to count the number of formula output if you prefer a 1/0 answer:

ltlfilt -c -f '(a U b) U a' --equivalent-to 'b U a'

1

Or use -q if you only care about the exit status of ltlfilt: the exist status is 0 if some formula matched, and 1 if no formula matched. (The effect of these -c and -q options should be familiar to grep users.)

In Python, we can implement this in a number of ways. The easiest is to use the spot.are_equivalent() function.

import spot
are_eq = spot.are_equivalent("(a U b) U a", "b U a")
print("Equivalent" if are_eq else "Not equivalent")

Equivalent

The equivalence check is done by converting the input formulas \(f\) and \(g\) and their negation into four automata \(A_f\), \(A_{\lnot f}\), \(A_g\), and \(A_{\lnot g}\), and then making sure that \(A_f\otimes A_{\lnot g}\) and \(A_g\otimes A_{\lnot f}\) are empty.

We could also write this check by doing the translation and emptiness check ourselves. For instance:

import spot

def implies(f, g):
    a_f = f.translate()
    a_ng = spot.formula.Not(g).translate()
    return spot.product(a_f, a_ng).is_empty()

def equiv(f, g):
    return implies(f, g) and implies(g, f)

f = spot.formula("(a U b) U a")
g = spot.formula("b U a")
print("Equivalent" if equiv(f, g) else "Not equivalent")

Equivalent

This can also be done via a language_containment_checker object:

import spot
f = spot.formula("(a U b) U a")
g = spot.formula("b U a")
c = spot.language_containment_checker()
print("Equivalent" if c.equal(f, g) else "Not equivalent")

Equivalent

The language_containment_checker object essentially performs the same work, but it also implements a cache to avoid translating the same formulas multiple times when it is used to test multiple equivalences.

Here are possible C++ implementations using either are_equivalent() or the language_containment_checker. Note that the are_equivalent() function also work with automata.

#include <iostream>
#include <spot/tl/parse.hh>
#include <spot/twaalgos/contains.hh>

int main()
{
  spot::formula f = spot::parse_formula("(a U b) U a");
  spot::formula g = spot::parse_formula("b U a");
  std::cout << (spot::are_equivalent(f, g) ?
                "Equivalent\n" : "Not equivalent\n");
}

Equivalent

#include <iostream>
#include <spot/tl/parse.hh>
#include <spot/tl/contain.hh>

int main()
{
  spot::formula f = spot::parse_formula("(a U b) U a");
  spot::formula g = spot::parse_formula("b U a");
  spot::language_containment_checker c;
  std::cout << (c.equal(f, g) ? "Equivalent\n" : "Not equivalent\n");
}

Equivalent