Verifying Implicitly Quantified Modal Logic over Dynamic Networks of Processes

Abstract

When we consider systems with process creation and exit, we have potentially infinite state systems where the number of processes alive at any state is unbounded. Properties of such systems are naturally specified using modal logics with quantification, but they are hard to verify even over finite state systems. In [11] we proposed (formula presented), an implicitly quantified modal logic where we can have assertions of the form every live agent has an (formula presented)-successor, and presented a complete axiomatization of valid formulas. Here we show that model checking for (formula presented) is efficient even when we consider systems with infinitely many processes, provided we can efficiently present such collections of processes, and check non-emptiness of intersection efficiently. As a case study, we present a model checking algorithm over systems in which at any state, the collection of live processes is regular.