Data tracking in parameterized systems

We study parameterized verification problems for concurrent systems with data enriched with a permission model for invoking remote services. Processes are modelled via register automata. Communication is achieved by rendez-vous with value passing. Permissions are represented as graphs with an additional conflict relation to specify incompatible access rights. The resulting model is inspired by communication architectures underlying operating systems for mobile devices. We consider decision problems involving permission violations and data tracking formulated for an arbitrary number of processes and use reductions to well structured transition systems to obtain decidable fragments of the model.