Аннотация:В работе рассматривается расширение темпоральной логики до логики первого порядка с одноместными предикатными символами, термы которой задаются арифметическими выражениями, составленными из операции сложения и констант. Такие термы, с одной стороны, позволяют устанавливать более глубокие связи между моментами времени, с другой – гарантируют разрешимость рассматриваемой логики. Для введенной логики в работе представлен алгоритм проверки истинности формул, который расширяет известный алгоритм проверки истинности формул в линейной темпоральной логике на более широкий класс формул.