提出于20世纪的STIT理论是以分支时间、非决定论与自由选择为哲学前提的一类行动逻辑。利用STIT算子可以对能动句进行清晰的形式分析,从而揭示主体的能动性。尽管如此,主体的选择本身却无法在经典STIT理论中得到表达。通过引入新初始符号并丰富语义结构,主体在语义模型中的选择能够在形式语言中得到表示。可以证明新得逻辑具有可靠并完全的公理系统。