V. Rybakov, “Discrete linear temporal logic with current time point clusters, deciding algorithms”, LLP, vol. 17, no. 1-2, pp. 143–161, Jun. 2008.