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.