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 does not have any temperal operators after changing in line 13 to . 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 alone is not sufficient for the case that the releast subformula is fulfilled in finite time, from the time step in which accepts, we need to have that also accepts from there.

There may be a possibility to fix the release construction by branching off into , and using the initial state of as additional initial state.