2134/14855
Walter Hussak
Monodic temporal logic with quantified propositional variables
2014
Loughborough University
Monodic temporal logic
Quasimodels
Decidability
Recursive enumerability
2014-06-13 07:59:33
article
https://repository.lboro.ac.uk/articles/Monodic_temporal_logic_with_quantified_propositional_variables/9402557
We extend the monodic fragment of ﬁrst-order linear temporal logic to include right-linear grammar operators and
quantiﬁcation of propositional variables. Unlike propositional temporal logic, the use of grammar operators in ﬁrst-order
temporal logic is not equivalent to general propositional quantiﬁcation, as the latter admit satisﬁable formulae without
countable models. We consider the decision problem for fragments where propositional quantiﬁcation occurs outside of
quantiﬁcation of individual variables and temporal (grammar) operators. We show that if externally quantiﬁed propositions
inside temporal operators occur within positive occurrences of universal quantiﬁers for individual variables, then validity
for all propositional preﬁx classes is recursively enumerable and decidable in the two-variable case. Without this condition
we show that, even with very severe restrictions on the ﬁrst-order part of the logic, no non-trivial preﬁx class is recursively
enumerable.