随着大规模复杂的实时嵌入式系统的广泛使用,程序运行的实时性要求受到了越来越多的关注。时间敏感的下推系统是一类上下文切换受到时间约束的系统。它对具有实时要求的程序分析和系统验证具有重要的理论和应用价值。目前时间敏感上下文切换系统的验证研究还不够成熟,相关成果较少,因此值得关注和研究。在时间敏感的下推系统中,用来约束的时钟可以分为全局时钟(所有上下文都能够修改时钟的值并受其约束)、局部时钟(只有当前上下文可以修改时钟的值并受其约束)、冷冻时钟(该时钟绑定当前上下文,如果遇到上下文切换,时钟将停止运行,直到回到当前上下文时,时钟才重新运行)和可调整时钟(该时钟允许基于原先值做加一和减一操作)等,而用来测试的时间约束可以分为无对角线约束(允许对一个时钟的值测试是否在某个范围)和对角线约束(允许对两个时钟的值的差值测试是否在某个范围)。下推系统在不同时钟和不同测试时间约束的影响下的系统验证可判定性问题是目前实时验证领域的一个研究热点。本文贡献是基于一种时间敏感下推系统即嵌套时间自动机,解决了关于时间敏感的下推系统的以下三个问题:第一,对一般化嵌套时间自动机的可达性问题,证明了该问题是不可判定的,同时,当加上不允许冷冻时钟的限制时,可达性问题是可判定的;第二,对无对角线约束的嵌套时间自动机的状态可达性算法设计问题,给出一个前向可达性分析算法,并证明算法正确性;第三,对单个可更调整时钟的可调整时间自动机的可达性问题,证明了有对角约束时是不可判定而无对角性约束时是可判定的,并进一步提出了嵌套可调整时间自动机的模型,探讨了其终止性和有限性问题。虽然我们结论是基于嵌套时间自动机,但很容易推广到其它时间敏感的下推系统。本文中关于时间敏感的下推系统的判定性方面的结论填补了当前研究的一些空白,为下一步得到时间敏感下推系统的高效工具做铺垫。