Model-checking parametric lock-sharing systems against regular constraints

TL;DR

This paper studies the verification of parametric lock-sharing systems with pushdown automata processes, establishing decidability and complexity results for checking if infinite behaviors satisfy regular properties, especially under nested lock usage.

Contribution

It introduces a decidable framework for verifying infinite behaviors of parametric lock-sharing systems with nested lock usage, providing complexity bounds and algorithms.

Findings

Decidability of verification for nested lock usage systems.

EXPTIME-completeness of the general verification problem.

Polynomial time algorithm when the number of parameters is bounded.

Abstract

In parametric lock-sharing systems processes can spawn new processes to run in parallel, and can create new locks. The behavior of every process is given by a pushdown automaton. We consider infinite behaviors of such systems under strong process fairness condition. A result of a potentially infinite execution of a system is a limit configuration, that is a potentially infinite tree. The verification problem is to determine if a given system has a limit configuration satisfying a given regular property. This formulation of the problem encompasses verification of reachability as well as of many liveness properties. We show that this verification problem, while undecidable in general, is decidable for nested lock usage. We show Exptime-completeness of the verification problem. The main source of complexity is the number of parameters in the spawn operation. If the number of parameters is bounded, our algorithm works in Ptime for properties expressed by parity automata with a fixed number of ranks.