Monodic Packed Fragment with Equality is Decidable

We prove decidability of satisfiability of sentences of the monodic packed fragment of first-order temporal logic with equality and connectives Until and Since, in models with various flows of time and domains of arbitrary cardinality. We also prove decidability over models with finite domains, over flows of time including the real order.