Symbolic reachability analysis and maximally permissive entrance control for globally synchronized templates

This paper studies the symbolic reachability relations of a class of parameterized systems in the framework of regular model checking. The modules of each system are instantiated from a globally synchronized template, and each globally synchronized template is represented by a finite state automaton whose event set consists of global events and local events. It is shown that the symbolic reachability relations of these systems are effectively iteration-closed star languages. And for any iteration-closed star language, there exists a template with only global events that realizes it. Application of the symbolic reachability analysis to computing the entrance control functions that enforce deadlock freeness and blocking freeness is then illustrated for systems with idle modules. In particular, we show that the maximally permissive entrance control functions can be encoded using finite state automata.