Model-checking lock-sharing systems against regular constraints

TL;DR

This paper investigates the verification of distributed lock-sharing systems with regular constraints, showing complexity bounds and conditions under which the problem becomes more tractable.

Contribution

It introduces restrictions on lock access and release order to reduce the verification problem's complexity, providing tight bounds and a polynomial-time solvable case.

Findings

Verification problem is PSPACE-complete in general

Under certain restrictions, the problem is in NP

A specific subcase can be solved in polynomial time

Abstract

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.