Efficient verification of concurrent and distributed infinite-state systems

点击翻译按钮获取中文摘要

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.