Parameterized model checking of weighted networks

We consider networks of weighted processes that consist of an arbitrary number of weighted automata equipped with weights taken from a monoid. We investigate parameterized model checking problems used to verify whether certain qualitative and quantitative properties hold independently of the number of processes. We prove that model checking properties expressed in a weighted extension of LTL is decidable if the monoid satisfies some simple properties. We further present decision procedures for checking global properties of weighted networks. (C) 2014 Published by Elsevier B.V.