New aspects of the mu-calculus

形式逻辑为我们提供了一种数学语言来指定和描述系统，以及推理逻辑语句在给定情况下是否为真的强大方法，逻辑语句从哪个逻辑语句得出，等等-这些方法通常可以自动化。模型检查应用这些思想来提供强大的自动化工具，以验证软件是否满足其规范。这可以为公司节省资金，并为软件的可靠性提供广泛的社会信心。传统的模型检验在工业上已经取得了巨大的成功，但大多数都认为时间是离散的- 0，1，2等等。对于某些计算机系统，物理学中使用的连续时间更合适。这个项目的一部分将研究在涉及实时模型的情况下进行模型检查的可能性，使用一个非常强大的逻辑，时间μ演算。从长远来看，它可能会导致新的方法模型检查更复杂的系统。以及时间，空间是一个重要的方面，许多现代应用程序，包括数据库，地理信息系统和几何推理。逻辑也可以用来对空间进行陈述，并与之推理。许多不同的逻辑系统已经被使用，但是非常强大的μ演算在这方面还没有得到很大的研究。本项目旨在研究空间语境中的模态μ演算，试图确定它的表达能力，以及需要什么样的机器才能正确地推理它。从长远来看，这项工作有可能提高我们对涉及空间的情况进行指定和推理的能力。我们也将借此机会尝试建立一些关于μ演算定义情况类别的能力的基本事实，这与简单逻辑中所谓的戈德布拉特-罗森定理相呼应。如果成功，这将为研究人员提供一个基本的工具，可用于许多需要μ演算的领域。这个雄心勃勃的项目只有三个月的研究时间，可能不会解决所有问题，但我们希望能取得良好的进展。

Formal logic provides us with a mathematical language for specifying and describing systems, as well as powerful methods for reasoning about whether a logical statement is true in a given situation, which logical statements follow from which, and so on - and these methods can often be automated. Model checking applies these ideas to provide powerful automated tools for verifying that software meets its specification. This can save companies money and provide confidence to wide society of the reliability of software. Conventional model checking has been enormously successful industrially, but much of it has considered time as discretely ticking - 0, 1, 2, and so on. For some computer systems, continuous time as used in physics is more appropriate. Part of this project will study the possibilities for model checking in situations concerning real-time models, using a very powerful logic, the temporal mu-calculus. In the long term, it may lead to new ways of model checking more sophisticated systems.As well as time, space is an important aspect of many modern applications, including databases, geographic information systems, and geometrical reasoning. Logic can also be used to make statements about space, and reason with them. Many different logical systems have been used, but again the very powerful mu-calculus has not been greatly investigated in this context. This project aims to study the modal mu-calculus in spatial contexts, trying to ascertain its expressiveness, and what machinery is needed to reason correctly with it. The work has the potential in the long run to improve our ability to specify and reason about situations involving space.We will also take the opportunity to try to establish some fundamental facts about the mu-calculus's power to define classes of situations, echoing the so-called Goldblatt-Thomason theorem for simpler logics. If successful, this will provide researchers with a basic tool usable in many areas requiring the mu-calculus.Only three months is available for the research on this ambitious project, and it is likely that not all problems will be solved, but we hope that good progress will be made.