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.

翻译：在带参数锁共享系统中，进程可以生成新进程以并行运行，并可创建新锁。每个进程的行为由下推自动机定义。我们考虑在强进程公平性条件下此类系统的无限行为。系统潜在无限执行的结果是极限配置，即一个潜在的无限树。验证问题在于判定给定系统是否存在满足特定正则属性的极限配置。该问题的表述涵盖了可达性验证以及许多活跃性属性的验证。我们证明，尽管该问题在一般情况下不可判定，但在嵌套锁使用场景下是可判定的，并表明其验证复杂度为指数时间完备性。复杂度主要来源于生成操作中的参数数量。若参数数量有界，对于由固定秩数奇偶自动机表达的性质，我们的算法可在多项式时间内完成验证。