Extensions of Logics Used in Computer Science and Their Decision Procedures

目前在计算机科学中使用的逻辑的扩展正在被调查。特别考虑的是时序逻辑和动态逻辑的扩展，它们看起来非常自然，并具有相当大的表达能力。一种在树上工作的新的交替自动机模型正在被使用，它允许非常简单和有效的决策程序。在基本情况下，给出了预期逻辑可判断性的证明，这些证明比未扩展逻辑的标准证明简单。正在尝试将这些方法扩展到涉及协议的问题，其中通信系统应该考虑知识。还在考虑一些具有无限运行量词的非常强的动态逻辑，在这些逻辑中基本上可以表示任何公平条件。PI们建议使用他们最近在形式语言理论方面的创新工作中开发的工具来研究计算机科学中使用的逻辑。理论计划可以适当地将资金投入到理论计算机科学中此类方法的开发和使用上。拟议中的工作以积极的方式将美国和法国的理论传统联系在一起。

Extensions of logics currently used in computer science are being investigated. Under particular consideration are extensions of temporal and dynamic logic which appear to be quite natural and to have considerable expressive power. A new model of alternating automata working on trees is being used that allows very simple and efficient decision procedures. In basic cases, proofs of decidability of the intended logics are being given that are simpler than the standard proofs for the unextended logics. Extensions of these methods are being attempted to questions involving protocols where knowledge should be taken into account for communicating systems. Also under consideration are some extremely strong dynamic logics with infinitary run quantifiers in which essentially any fairness condition can be expressed. The PIs propose to use tools they have developed in recent innovative work in formal language theory to investigate logics used in computer science. The theory program can properly devote funds toward the development and use of such methods in theoretical computer science. The proposed work ties together in a positive way the theory traditions of the U.S. and France.