Symmetry Reduction and Compositional Verification on Timed Automata

Abstract

This thesis is about techniques for the analysis of concurrent and real-time systems.

As the first contribution, we describe a technique that incorporates automatic symmetry detection and symmetry reduction in the analysis of systems modeled by timed automata. First, our approach detects structural symmetries arising from process templates of realtime systems, requiring no additional input from the user. Then, the technique involves finding all variables of type process identifier and computing a set of generators that forms a group of automorphisms. Our technique is fully automatic, and not restricted to fully symmetric systems.

The second contribution of this thesis is that we combine elements of compositional proof, abstraction and local symmetry to decide whether a safety property holds for every process instance in a parameterized family of real-time process networks. Analysis is performed on a small cut-off network; that is, a small instance whose compositional proof generalizes to the entire parametric family. Our results show that verification is decidable in time polynomial in the state space of the “cut-off” instance. Then we apply these ideas to analyze Fischer’s protocol, CSMA/CD protocol and Train-Bridge protocol.