Author's notes on the paper “A Fragment of Linear Temporal Logic for Universal Very Weak Automata”

This page contains some additional information to the paper A Fragment of Linear Temporal Logic for Universal Very Weak Automata by Keerthi Adabala and RĂ¼diger Ehlers.

Errata List

The construction for the Release case on page 8 is incorrect. It works if f^2 does not have any temperal operators after changing f_1 vee f_2 in line 13 to f_1. This is the case needed when encoding a globally operator occurence using the release operator.

The resulting loss of expressivity can be compensated by adding an implementation of the weak-until operator, similar to the until operator, just with the additional state being accepting, rather than rejecting.

The release case has the problem that braching out into f_1 vee f_2 alone is not sufficient for the case that the releast subformula is fulfilled in finite time, from the time step in which f_1 accepts, we need to have that f_2 also accepts from there.

There may be a possibility to fix the release construction by branching off into (mathsf{X} f_1) vee f_2, and using the initial state of f_2 as additional initial state.