A tableau for general linear temporal logic
We use mosaics to provide a simple, sound, complete and terminating tableau reasoning procedure for the temporal logic of until and since over general linear time.
tableau temporal logic general linear time