Verification of Parameterized Concurrent Systems with Resource Sharing

One very common source of potential errors in concurrent systems isthat of access to shared resources. It is thus desirable to be able toverify correctness of the way shared resources are treated in suchsystems. In the report, we discuss verification of parameterizedsystems of processes competing for access to shared resources under theFIFO resource management policy with or without priorities. We dealwith various generic property classes expressible in (fragments of)temporal logics and covering certain forms of safety, deadlockability,as well as liveness.In particular, we present three kinds of results. (1) We prove someparametric verification problems arising in the considered context tobe efficiently reducible to finite-state verification. This is done byarguing that to prove a given property for any number of processes, itis often sufficient to consider a certain ``cut-off'' number ofprocesses depending on the number of processes made visible in theformula of interest and/or the number of resources available. (2) Forsome problems in the domain of FIFO with priorities, we show that usinga simple cut-off as in the previous case is in general insufficient.However, such problems may still be decidable, and there may existcut-offs taking additionally into account the structure of the processcontrol automaton and/or the formula to be verified. We show an exampleof such a cut-off for 1-index liveness properties. (3) Finally, wediscuss some undecidability results related to the given area.