Аннотация:В работе предлагается особая троичная логика линейного времени, предназначенная для точного описания смысла неопределённости "0 или 1, но неизвестно, что именно", ставится задача верификации относительно этой логики, и для этой задачи предлагаются решающие алгоритмы с оценками сложности.