Model-checking lock-sharing systems against regular constraints
Formal Languages and Automata Theory
2022-10-17 v1 Distributed, Parallel, and Cluster Computing
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.
Cite
@article{arxiv.2210.07914,
title = {Model-checking lock-sharing systems against regular constraints},
author = {Corto Mascle},
journal= {arXiv preprint arXiv:2210.07914},
year = {2022}
}