Explain difference between "propositional not" and "logical not" in LTLf and PLTLf

[marcofavorito]

Currently, in LTLf and PLTLf, there is no enough stress on the difference between the "propositional not" and the "logical not" in front of propositional atoms.

Consider the LTLf syntax in negation normal form:

f := a  |  !a  |  f1 & f2  |  f1|f2  |  X[!](f)  |  X(f)  |  f1 U f2  |  f1 R f2

The formula a accepts the following language: all the non-empty traces that start with a propositional interpretation in which a holds.

Let's denote the propositional negation with ! (can only occur in front of atomic formulas), and the logical negation with ~ .

A logical negation of a, let us write it ~a, results in a language whose traces are: either empty-trace or any trace that starts with a propositional interpretation in which a does not hold.

However, a propositional negation !a differs from ~a by NOT accepting the empty trace.

To give a better idea, here are the automata corresponding to each formula:

• a:
  

• !a:
  

• ~a:
  

• ~(!a):
  

Similar reasoning applies to PLTLf.

The purpose of this issue is to keep track of this subtle difference. My opinion is to avoid introducing two different symbols for the negation, ~ and ! in the example above, as it leads to confusion.
We could assume that !f of ~f means "logical not f" if f is NOT an atomic formula, and "propositional not f" if f is an atomic formula; then, to write ~a in the example above (i.e. the logical not in front of atomic formula), one could rely on the equivalence:

~a <-> (!a | end)

Where end is a formula that only accepts the empty trace, e.g. by convention it could be G(false).

Then, the logical negation of !a can be rewritten as:

~(!a) <-> ~(~a & ~end) <-> (a | end)

In summary, I propose to have two equivalent symbols for the negation, i.e. ! and ~ are interchangeable. However, the negation assumes two different meanings depending on what kind of formula is in its argument; if it is an atomic formula, then it is interpreted as a propositional negation, and if not, it is interpreted as a logical negation.
For example, the above three formulas would have been written as: a, !a, !a | end and a | end, respectively.

The implementer of the grammar will take into account these two differences at the code level, and e.g. to transform in NNF it should rely on the above equivalences.