Verification of parametric concurrent systems with prioritized FIFO resource management

International audience; This paper addresses the problem of parametric verification for a class of concurrent systems with resource sharing. The systems are composed of a parametric number of finite-state processes that are competing for exclusive access to a finite number of resources. Their access to resources is managed by a locker according to a FIFO policy distinguishing low-priority and high-priority resource requests. For such systems, we define a model based on automata with queues recording for each resource the identities of the waiting processes. Then, we address the parametric verification problem for the proposed model and the temporal logic LTL\X with global process quantification. We consider two different interpretation domains for the logic, namely the sets of finite and fair behaviours. In addition, we consider parametric verification of process deadlockability too. We establish several decidability results for different classes of the considered systems and properties by reducing their parametric verification problems to (finite-state) model-checking problems with finite numbers of processes.