Thesis Abstract: Reactive Graphs, introduced by Dov Gabbay, are transition structures that evolve along its execution. These structures are suitable to compactly represent complex reactive and reconfigurable behaviors. Variations of this type of reconfigurable structures have been explored within the scientific community. However, their impact in the context of specific domain applications remains underexplored. A potential barrier to their widespread adoption among communities less familiar with the formal specification of systems and logics could be the absence of computational support for analyzing such models. This dissertation aims to overcome these gaps by studying the generalization of the Labelled Transition System (LTS) to a dynamic structure called the Labelled Reactive Graph (LRG), building on the theory already developed in the literature for LTS. A new product is introduced, the intrusive product, which allows for the addition of intrusive edges between models to enable their mutual reconfiguration. Additionally, a Hennessy-Milner Logic is presented to specify and verify properties of these models. The dissertation introduces with the implementation of Marge, a web-based tool designed to visualize and animate reactive graphs, perform products, and verify the existence of some properties.'