Monodic temporal logic with quantified propositional variables (Q2893321)

This paper considers first-order linear temporal logic (FO-LTL) and studies its extensions with propositional quantification and right-linear grammar operators. The focus is on decidability and recursive enumerability of these extensions. For that purpose, the authors restrict themselves to a decidable fragment of FO-LTL, that is, the monodic fragment of FO-LTL. A formula is monodic if modal formulas contain at most one free individual variable. The authors show that unsatisfiability is recursively enumerable for the monodic fragment where propositional quantification occurs outside of quantification of individual variables (and grammar operators), inside of which externally quantified propositions are within positive occurrences of existential quantifiers for individual variables in the overall formula. As a second result, the authors show that satisfiability is recursively enumerable and decidable when the number of individual variables is restricted to two. Without this condition, it is shown that even with severe restrictions on the first-order part of the logic, no non-trivial prefix class is recursively enumerable.