TTA启动算法一直受到多个基于模型检查技术的形式化分析的支配。模型检查技术的一个共同的方面是相当一大部分的努力致力于保持模型的大小在一个计算上可行的范围之内，而在同时，针对现实的形式化模型不采用过于简单化的抽象。

对于启动问题，主要内容就是如何在形式化的模型中充分捕捉时间概念。定时自动机是针对实时系统验证的一种成功的形式主义，并且以最现实的形式化方式把时间看作一个连续变量。尽管如此，模型检查定时自动机是可判定的，并存在专门的模型检测工具如Kronos和UPPAAL。Lönn^[21]认为TDMA系统的启动算法类似TTA的启动算法，并使用UPPAAL验证其中的一种。

由于模型检查定时自动机计算复杂，因此当重点从时间方面转移到分析复杂的故障行为或大量的不同的故障工况时，可能需要其他的形式主义和抽象。在TTA启动的分析中，Steiner等^[9]采用把时槽作为不可分割单位的离散时间来进行抽象。与上一节中所描述的同步模型相似，该模型根据具体的时隙的具体时间和在不同的节点的时隙偏移多少进行抽象。节点通过在TDMA调度表中报出时槽数来计时，且一组节点的集体行为被建模为离散系统的同步组合。

Dutertre和Sorea描述了一种把时间保存为一个连续变量的方法，但也通过模型检验程序使定时系统负责分析离散过渡系统^[7]。然而，由于状态空间变得无限大，以满足度模数理论为基础的（基于SMT）有界模型检验程序是必要的。应用这些方法来验证使用k归纳的TTA启动算法。(www.daowen.com)

这些做法的中心是事件日历的概念，众所周知它是来自于离散事件仿真领域。一个事件日历存储某些事件发生的时间，如某个节点信息接收的未来发生时间。这样的日历自动机的两种类型的转换是有区别的：推进时间的时间进度转换；更新状态变量的离散转换。在每一步，只启用一种过渡类型：要么时间推进到下一个事件日历控制的调度事件发生时刻；要么是采用当前时刻发生事件的离散转换之一。附加的约束确保时间总是被最大限度地推进，且保证在没有时间进度的情况下，不存在离散转换的无限序列。这种方法的优点是，所有的变量包括时间，在离散步骤中演变，因此也没有必要通过允许任意小的时间步来近似连续动态性能。实际上，这减少了可能的转换数量和系统模型的大小。

使用日历自动机，系统组件如TTA中的节点的模型异步组成，且通过序贯应用离散转换，建立同步通信模型。Pike^[22]观察到通过使用同步合成，多路转换可以同时应用。建立在Dutertre和Sorea的基础上，他发明了同步超时自动机模型。在该模型中，状态变量的子集是可分辨的，它代表了同步更新的部分系统状态。就像在日历自动机模型中一样，附加的规则确保该系统进展。此外，可以谨慎地除去同步超时自动机模型中的时钟（按照它被更新的量），因此它的当前值可以由模型的其他组件得到。这种优化降低了状态空间和系统转换的数目，从而可以分析更大规模的模型。Pike把他的方法，用在一个称为Spider的相关的分布式容错架构中实施的整合协议中^[23]。