On the Effects of Adding Assignments in Linear-Time Temporal Logics Modulo Theories

We introduce linear-time temporal logics with past

operators featuring a simple assignment modality that

performs local changes on the models. Such structures are

infinite sequences of valuations interpreting variables by

elements from a possibly infinite data domain. We study

several fragments as well as the case with the Boolean

domain, for which we establish that it is actually as

expressive as first-order logic over infinite sequences of

propositional valuations. For the logics over concrete

domains N, Z and Q equipped with

the respective linear ordering and equality tests, we show

the satisfiability problem is decidable, and that the

logics are as expressive as the version without the

assignment operator. Interestingly, this entails such

assignments provide a huge concise ness, which is then

helpful for succinct specifications.