Constraint-based model checking for parameterized synchronous systems

We present a fully-automatic method for checking safety properties of parameterized synchronous systems based on a backward reachability procedure working over real arithmetics. We consider here concurrent systems consisting of many identical (finite-state) processes and one monitor where processes may react non-deterministically to the messages sent by the monitor. This type of non-determinism allows us to model abstractions of situations in which processes are re-allocated according to individual properties. We represent concisely collections of global states counting the number of processes in a given state during a run of the global system, i.e., we reason modulo symmetries. We use a special class of linear arithmetic constraints to represent collections of global system states. We define a decision procedure for checking safety properties for parameterized systems using efficient constraints operations defined over real arithmetics. The procedure can be implemented using existing constraint-based symbolic model checkers or tools for program analysis defined over real-arithmetics.