Parameterized model checking of weighted networks (Q2447757)

This publication is one among many that consider the verification of the correctness of systems that consist of a single server and an unknown number of identical users. Whether or not verification is decidable depends strongly on the details of the formalisms for specifying the systems and their correctness properties. Here, communication between processes is similar to the Calculus of Communicating Systems, that is, it consists of one process executing a communication action while another process simultaneously executes its corresponding co-action. More than one process may be ready to execute the action or the co-action. The opposite process does not know with which of them it is synchronizing. A central aspect in the publication is weights of transitions. They may model the production or consumption of some resource such as time or fuel, but also other uses are possible, such as keeping track of a maximum value. Correctness is specified in the well-known linear temporal logic extended with the ability to say that the weight of the next transition is within a certain interval, or the joint weight before the satisfaction of the right-hand side of an until operator is within a certain interval. Even if the weights are picked from an unbounded dense set such as the non-negative rational numbers, it is sometimes possible to ensure that only a finite number of different values are relevant for a verification problem. This facilitates the translation of the weighted verification problem to the classical one. In addition to this main result, the publication presents decidability and undecidability results for variants of the problem.