We present a new family of modal temporal logics of the past, obtained by
extending Past LTL with a rich set of temporal operators based on the theory by
Krohn and Rhodes for automata cascades. The theory says that every automaton
can be expressed as a cascade of some basic automata called prime automata.
They are the building blocks of all automata, analogously to prime numbers
being the building blocks of all natural numbers. We show that Past LTL
corresponds to cascades of one kind of prime automata called flip-flops. In
particular, the temporal operators of Past LTL are captured by flip-flops, and
they cannot capture any other prime automaton, confining the expressivity
within the star-free regular languages. We propose novel temporal operators
that can capture other prime automata, and hence extend the expressivity of
Past LTL. Such operators are infinitely-many, and they yield an infinite number
of logics capturing an infinite number of distinct fragments of the regular
languages. The result is a yet unexplored landscape of extensions of Past LTL,
that we call Krohn-Rhodes Logics, each of them with the potential of matching
the expressivity required by specific applications.

本论文提出了一种新的过去式模态时态逻辑家族，通过扩展 Past LTL 变得更加丰富，以 Krohn and Rhodes 关于自动机串联理论为基础，并展示了该家族被称为 Krohn-Rhodes Logics 的无穷多个扩展，可以捕捉到更多的基础自动机和扩展其表达能力。