Propriedades críticas do modelo z(4) em sistemas bi e tridimensionais

A real space renormalization group method is used to investigate the criticality (phase diagrams, critical expoentes and universality classes) of Z(4) model in two and three dimensions. The values of the interaction parameters are chosen in such a way as to cover the complete phase diagrams of the model, which presents the following phases: (i) Paramagnetic (P); (ii) Ferromagnetic (F); (iii) Antiferromagnetic (AF); (iv) Intermediate Ferromagnetic (IF) and Intermediate Antiferromagnetic (IAF). In the hierarquical lattices, generated by renormalization the phase diagrams are exact. It is also possible to obtain approximated results for square and simple cubic lattices. In the bidimensional case a self-dual lattice is used and the resulting phase diagram reproduces all the exact results known for the square lattice. The Migdal-Kadanoff transformation is applied to the three dimensional case and the additional phases previously suggested by Ditzian et al, are not found

Estendendo CRefine para o suporte de táticas de refinamento

The use of increasingly complex software applications is demanding greater investment in the development of such systems to ensure applications with better quality. Therefore, new techniques are being used in Software Engineering, thus making the development process more effective. Among these new approaches, we highlight Formal Methods, which use formal languages that are strongly based on mathematics and have a well-defined semantics and syntax. One of these languages is Circus, which can be used to model concurrent systems. It was developed from the union of concepts from two other specification languages: Z, which specifies systems with complex data, and CSP, which is normally used to model concurrent systems. Circus has an associated refinement calculus, which can be used to develop software in a precise and stepwise fashion. Each step is justified by the application of a refinement law (possibly with the discharge of proof obligations). Sometimes, the same laws can be applied in the same manner in different developments or even in different parts of a single development. A strategy to optimize this calculus is to formalise these application as a refinement tactic, which can then be used as a single transformation rule. CRefine was developed to support the Circus refinement calculus. However, before the work presented here, it did not provide support for refinement tactics. The aim of this work is to provide tool support for refinement tactics. For that, we develop a new module in CRefine, which automates the process of defining and applying refinement tactics that are formalised in the tactic language ArcAngelC. Finally, we validate the extension by applying the new module in a case study, which used the refinement tactics in a refinement strategy for verification of SPARK Ada implementations of control systems. In this work, we apply our module in the first two phases of this strategy