关于分支时间时序逻辑范式表达力的考察

随着涉及复杂分布式系统的新兴应用的出现，分支时间规约尤为重要，因为它们反映了此类应用的动态与非确定性本质。我们描述了一种简单而强大的分支时间规约框架——分支时间范式（BNF）的表达力，该范式是作为分支时间时序逻辑的子句归结的一部分而开发的。我们展示了 Büchi 树自动机在该范式语言中的编码，从而以高层方式在语法上表示树自动机。因此我们可以将 BNF 视为后者的一种范式。这些结果使我们能够（1）将给定问题规约转化为范式，并应用一种演绎推理技术——子句时序归结作为验证方法；（2）应用归结方法的核心组件之一——循环搜索，以语法方式在广泛复杂时序规约中提取隐藏的不变量。