Model Checking of Navigation Logics (MoNaLog)

软件是系统的重要组成部分，其故障可能会导致严重的后果，如大规模的经济损失，甚至生命或肢体的威胁。因此，软件可靠性是计算机科学的核心问题。传统的验证技术，如测试或模拟，根本不能提供强有力的正确性保证，因为它们只考虑可能的程序执行的选择。现代系统中并发性(并行性)的存在通常意味着不确定的行为，这加剧了这个问题。因此，程序验证的形式化方法应运而生，它依赖于数学和数理逻辑的技术，原则上能够提供强大的正确性保证。然而，经典的程序验证，例如霍尔-弗洛伊德，只是部分自动化的。这使得它们很难集成到传统的软件开发中。因此，自20世纪80年代以来，已经发展了全自动验证方法，特别是所谓的模型检查，其中通过算法来确定程序抽象是否满足由时态逻辑公式给出的形式化规范。该项目的目的是开发和分析新的时态逻辑，该时态逻辑除了考虑时态之外，仅允许连续的动作继承，用于在制定属性时考虑系统行为描述的特征方面。在这种情况下，重点放在复杂控制结构上的导航，特别是那些描述递归和多线程的结构。我们的目标是定义逻辑，这些逻辑通过相应的概念丰富现有的逻辑，并且模型检查问题仍然有效。对于新的逻辑和相应的系统模型类，我们希望研究模型检测问题的复杂性，并开发模型检测算法。这些算法应该在原型上实现，并在特征基准上进行评估。此外，我们还想研究相关方面，如可满足性问题的可判定性。

Software is a crucial component of systems whose failure can cause severe consequences like massive financial damages or even threats to life or limb. Software reliability is therefore a core problem of computer science. Classical validation techniques like testing or simulation are fundamentally unable to provide strong correctness guarantees since they only consider a selection of possible program executions. This problem is exacerbated by the presence of concurrency (parallelism) in modern systems which commonly implies non-deterministic behavior. Therefore, formal methods of program verification were invented which rely on techniques from mathematics and mathematical logic and are in principle able to provide strong correctness guarantees. However, classical program verification, e.g. à la Hoare-Floyd, is only partially automatable. This makes their integration into traditional software development difficult. Therefore, since the 1980s, fully automatic verification methods have been developed, in particular so called model checking, in which it is algorithmically decided whether a program abstraction satisfies a formal specification given by a formula of temporal logic.The purpose of the proposed project is the development and analysis of novel temporal logics which allow, in addition to the consideration of temporal, merely sequential succession of actions, for the consideration of characteristic aspects of the system behavior's description when formulating properties. In this context, the focus is on the navigation over complex control structures, in particular those that describe recursion and multithreading. Our aim is to define logics which enrich existing logics by corresponding concepts and for which the model checking problem remains effective. For the new logics and the corresponding classes of system models, we want to study the complexity of the model checking problem and develop model checking algorithms. These algorithms should be implemented prototypically and evaluated on characteristic benchmarks. Furthermore, we also want to study related aspects like the decidability of the satisfiability problem.