论文标题
对定期限制的模型检查锁定共享系统
Model-checking lock-sharing systems against regular constraints
论文作者
论文摘要
我们研究了分布式系统的验证，其中流程是有限自动机，可以访问共享的锁池。我们认为目标是当地常规约束的布尔组合。我们表明，PSPACE完全完整的问题属于NP，并具有正确的假设。我们对过程可以访问的锁数量以及可以释放锁的顺序使用限制。我们提供紧密的复杂性范围，以及可以在PTIME中解决的兴趣子。
We study the verification of distributed systems where processes are finite automata with access to a shared pool of locks. We consider objectives that are boolean combinations of local regular constraints. We show that the problem, PSPACE-complete in general, falls in NP with the right assumptions on the system. We use restrictions on the number of locks a process can access and the order in which locks can be released. We provide tight complexity bounds, as well as a subcase of interest that can be solved in PTIME.
