反应式系统是指能对外界事件作出反应的系统,其特点是系统持续与所在环境进行交互,此类系统的性质一般涉及无限行为。而运行时验证是一种轻量级程序验证技术,需要根据系统当前运行轨迹判定系统是否满足给定性质,涉及系统的有限行为。众所周知,时序逻辑是描述反应式系统性质的主要形式语言之一。为了兼顾有限与无限行为的性质描述,学术界针对此类逻辑语言提出了不同的语义解释,其中,Patrick Maier等人提出了直觉主义时序逻辑。本文在直觉主义时序逻辑框架下对安全性和活性性质以及迭代布尔博弈开展研究,主要工作包括如下方面:1.提出了直觉主义计算树逻辑ICTL,比较了经典计算树逻辑CTL与直觉主义计算树逻辑ICTL的表达能力。2.在ICTL框架中定义了全局安全性质和活性性质以及存在型安全性质和活性性质的概念,并探究了安全性质和活性性质在并、交、补等操作下的封闭性。3.证明了直觉主义计算树逻辑中的分解定理。并给出ICTL中安全性质和活性性质与ILTL以及CTL中安全性质和活性性质的内在联系。4.在直觉主义线性时序逻辑框架下,研究了迭代布尔博弈中目标公式的可满足性与策略组合的对应关系,以及Nash均衡策略与ILTL公式的关系。