Parameterized Verification of Leader/Follower Systems via Arithmetic Constraints

We introduce a variant of a formalism appearing in recent work geared towards modelling systems in which a distinguished entity (leader) orchestrates the operation of an arbitrary number of identical entities (followers). Our variant is better suited for the verification of system properties involving complex arithmetic conditions. Whereas the original formalism is translated into a tractable fragment of first-order temporal logic, aiming to utilize automated (first-order temporal logic) theorem provers for verification, our variant is translated into linear integer arithmetic, aiming to utilize satisfiability modulo theories (SMT) solvers for verification. In particular, for any given system specified in our formalism, we prove, for any natural number <italic xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">n</i>, the existence of a linear integer arithmetic formula whose models are in one-to-one correspondence with certain counting abstractions (profiles) of executions of the system for <italic xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">n</i> time steps. Thus, one is able to verify, for any natural number <italic xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">n</i>, that all executions for <italic xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">n</i> time steps of any such system have a given property by establishing that said formula logically entails the property. To highlight the practical utility of our approach, we specify and verify three consensus protocols, actively used in distributed database systems and low-power wireless networks.