Efficient verification of concurrent and distributed infinite-state systems

随着多处理器架构、廉价低功耗设备和自然计算的进步，并发和分布式系统正变得越来越普遍。以可靠的方式开发这样的系统是具有挑战性的，特别是在关键系统的故障可能会危及生命，危害环境，损坏昂贵的设备或泄漏私人数据的情况下。算法验证是一种强大的方法，可以用来解决这个问题。它涉及将并发或分布式系统抽象为数学模型，然后可以对其进行详尽、严格和自动的分析。大多数实际使用的并发和分布式系统都有无限多个配置。不幸的是，无限状态系统的中心验证问题具有极高的计算复杂度。尽管如此，在无限状态系统的算法验证方面已经取得了重要进展。然而，目前基于精确算法的技术似乎已经达到了上限，因此需要新的见解来进一步扩展。我打算通过开发一种新颖而统一的低复杂性无限状态系统（LCIS）理论框架来打破这个天花板。这将通过(a)研究扩展Petri网的松弛来逐步实现，扩展Petri网是LCIS的一个突出类别；(b)通过证明该理论在验证群体系统（一种新兴的分布式计算范例）方面的适用性和效率；(c)在结构良好的过渡系统理论的启发下，为抽象的LCIS框架奠定基础。

Concurrent and distributed systems are becoming more widespread as advances are made on multiprocessor architectures, cheap low-power devices, and natural computing. It is challenging to develop such systems in a reliable way, especially in the context of critical systems whose malfunction can, e.g., endanger lives, harm the environment, damage expensive equipment, or leak private data. Algorithmic verification is a powerful method that can be used to tackle this task. It involves abstracting concurrent or distributed systems into mathematical models which can then be analyzed exhaustively, rigorously and automatically. Most concurrent and distributed systems of practical use have infinitely many configurations. Unfortunately, central verification problems for infinite-state systems suffer from tremendously high computational complexity. Despite this, there has been important progress on the algorithmic verification of infinite-state systems. However, current techniques based on exact algorithms seem to have reached a ceiling, and hence new insights are needed to scale further. I intend to break this ceiling by developing a novel and unified theoretical framework of low complexity infinite-state systems (LCIS). This will be achieved incrementally by (a) studying relaxations of extended Petri nets, a prominent class of LCIS; (b) by demonstrating the applicability and efficiency of the theory to the verification of crowd systems, an emerging paradigm of distributed computing; and (c) by laying the foundations of an abstract LCIS framework inspired by the theory of well-structured transition systems.