一般的命题时态逻辑TL是在通常的命题逻辑基础上扩充而成的。除了命题逻辑中的运算符┐、∧、∨、→、 ≡ 等之外，增加了表示时间关系的运算符□(Always)、◇(Sometimes) 、○(Next) 、∪(Until)。其中前三个为一元运算符，最后一个为二元运算符。各运算符的意义如下：
　　□P：从当前时刻起，P恒成立。
　　◇P：从当前时刻起，至少存在某一时刻使P成立。
　　○P：下一时刻P成立。
　　P∪Q：从当前时刻起，在Q成立之前P保持成立。
　　这里时间关系是建立在一个离散的时间序列的基础上：
　　　　　　T = { t0, t1,..., tn,... }
它是一个无限序列。
　　我们考虑问题时，总是在某一确定时刻的前提下，来判断逻辑表达式的真假。对于无时序运算符的一般逻辑表达式，我们只考虑当前时刻其值的真假。
　　时态逻辑TL的合式公式可定义如下：
　　(1)原子命题变元本身是一个TL公式。
　　(2)如果A、B为TL，则┐A、A∧B、A∨B、A→B、A≡B、□A、◇A、○A、A∪B也是TL公式。
　　(3)当且仅当能够有限次地应用(1)、(2)所得到的包含命题变元、运算符和括号的符号串是TL公式。
　　由合式公式的定义可知，运算符的组合可以构成复杂的表达式。我们规定，复杂逻辑表达式中各运算符的优先次序为（由高到低）：
　　　　　　<一元运算符>、∧、∨、→ 、≡、∪
其中一元运算符包括 ～、□、◇、○等。当这些符号连在一起时，遵循右优先规则。括号可以用来改变优先级。例如：(□U )→(□V )可以简写为□U→□V。┐(□ (┐P ) )可以简写为┐□┐P。
　　下面是含有时序运算符□ 、◇ 、○ 、∪的合式公式的几个例子：
　　P→◇Q：若P在当前时刻为真，则Q在此后某一时刻为真。比如当前时刻发一个请求信号(P)，其后必有某时刻出现响应(Q)。
　　□(P→◇Q)：从当前时刻起，无论何时一旦P为真，则其后必有某一时刻Q为真。这个表达式把P→◇Q推广到所有时刻，表示了某一种规则。
　　◇□P：存在将来某一时刻，其后P恒为真。在电路波形中，反映了某一时刻有一个上跳变，且再没有下跳变的情况可用◇□P表示，但◇□P也包括P恒为真的情况。
　　◇(P∧○┐P)：存在将来某一时刻，其时P为真，而其下一时刻P不为真。它可以用来表示某一时刻必存在一个下跳变的情况。
　　□◇P：从当前时刻起无论何时，其后都存在P为真的情况。这种情况包括P无限恒真的情况和无限次P的上跳变情况。
　　□(P→□Q)：从当前时刻起，无论何时，如果P一旦为真，则其时之后Q一直保持为真。