TLA+（时序动作逻辑）将系统建模为一组行为，每个行为是一系列状态。通过使用时序算子，它可以表达不变量（例如，[]P 表示 P 在每个状态都成立）以及动作性质，如 [](x' >= x)（x 的新值始终不小于旧值）。活性属性断言“好事总会发生”，它们基于 <> 算子构建，例如 <>[]P（最终 P 永远保持为真）和 P ~> Q（P 蕴含 Q）。这些属性在所有可能的行为上进行评估，以确保它们普遍成立。

一个根本的局限是 TLA+ 无法表达需要对行为进行存在量化的属性。例如，可达性属性如“存在一个行为使得 P 为真”——这对于证明一个游戏是可赢的是必需的——超出了语言的范围。同样，TLA+ 也无法表达超属性，即行为集合上的属性；一个例子是验证节能模式在所有可能的动作序列中始终比正常模式消耗更少的能量，这需要比较两个不同的行为。

虽然存在一些变通方法——例如使用辅助变量存储状态历史，采用自组合来建模多个行为，或者在 TLC 模型检查器中利用 REACHABLE 关键字和 TLCGet ——但它们会带来严重的缺点。辅助变量会使细化变得复杂，自组合会导致状态空间呈指数级增长，而且这些技术经常产生看起来混乱且不再直接对应实际系统的模型。其他工具如 CTL 或 PRISM 可以处理其中的一些属性，但它们在安全性和活性检查方面（而 TLA+ 在这些方面表现出色）会变得较弱。