混成系统是一种既包含离散成分又包含连续成分的计算系统，数控系统等一些与其外部连续变化的物理环境不断交互的嵌入式系统就是其典型的代表．实时系统是一类特殊的混成系统，其连续成分是一组用来表示时间约束条件的时钟．由于这些系统在工业及国防领域有着重要而广泛的应用，它们的安全性和可靠性越来越引起人们的关注，因而对这些系统进行形式化分析以确保其安全性和可靠性也成为近年来的一个研究热点．为了描述实时及混成系统的性质和行为，十多年来，各种不同的时序逻辑如：MetricInterval Temporal Logic，Real-Time Temporal Logic,Integrator Computation TreeLogic和Hybrid Temporal Logic 等相继提出，尽管这些时序逻辑作为规范语言用于描述实时及混成系统的性质时都还比较合适，但它们不适合用来表示实时及混成系统的实现，因为它们缺乏表示系统状态的动态变化的能力．在现有文献中，实时和混成系统通常是用时间自动机、混成自动机、时间转换系统和相位转换系统等来表示的．但这些系统刻画语言却不适合作为规范语言来使用，因为它们不能表示实时和混成系统的一些重要性质（如安全性和活性等）．这样在基于逻辑方法的实时和混成系统的研究中，系统和它的性质通常是用两个不同的语言来表示的．本文定义了一个具有连续语义的线性时序逻辑，记为 LTLC，它是 Manna和Pnueli所提出的线性时序逻辑LTL的一个推广．LTLC既能表示实时和混成系统的性质，又能很方便地表示实时和混成系统的实现，它能在统一的语义框架中表示出从高级的需求规范到低级的实现模型之间的不同抽象层次上的系统描述，并且能用逻辑蕴涵来表示不同抽象层次的系统描述之间的语义一致性．本文还定义了LTLC的三个子语言：LTLC/B、LTLC/R及LTLC/H，并证明了前两者的可满足性问题是可判定的．这三个子语言可分别用来表示有穷状态反应系统、有穷控制状态实时系统以及混成系统．本文所给的关于 LTLC/B－公式的可满足性判定过程可用于检查有穷状态反应系统之间的一致性以及有穷状态反应系统与其规范之间的一致性；所给的关于LTLC/R-公式的可满足性判定过程可用于检查有穷控制状态实时系统之间的一致性以及有穷控制状态实时系统与其规范之间的一致性．此外，本文还给出了在样本控制模式下（在此模式下，混成系统的跳跃转换只发生在整数时间点上）多速率混成系统关于 LTLC/H－公式的一个模型检查过程．