2022/10/14 by Corto Mascle, Mascle, Corto
Computer Science · #Formal Methods in Verification #Security and Verification in Computing #Petri Nets in System Modeling
paper · pdf · doi:10.48550/arxiv.2210.07914
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.