In: Theoretical Computer Science, Vol. 74, No. 1, pages 71-93. July 1990.
Abstract: The paper solves an open problem of R. Howell et al. (1988) by showing a decision algorithm for a temporal logic language L(Q',GF). It implies the decidability of the problem of the existence of an infinite weakly fair occurrence sequence for a given Petri net; thereby an open problem of H. Carstensen (1987) is solved.
Keywords: decidability (of a) temporal logic problem; decision algorithm; infinite weakly fair occurrence sequence.