Abstract

Abstract
Nowadays, ocean exploration is far from complete and the development of suitable recognition systems are crucial, to allow that the robots perform inspection and monitoring tasks in diverse conditions. The online available datasets are incomplete for these kinds of scenarios and, so it is important to build datasets that covered real condition in a simulated environment. Thus, it was developed a dataset with some man-made objects presents in the underwater environment. Moreover, it is also presented the developed method (Convolutional Neural Network) and its evaluation in diverse conditions is performed. It is also presented a comparative analysis and a discussion between the proposed algorithm and the ResNet architecture. The obtained results showed that the developed method is appropriate to classify 7 critical different objects with good performance.

Abstract
Causal Loop Diagrams (CLDs) are a modeling tool employed in Business Dynamics. Such a diagram consists of many tightly coupled loops to capture dynamic behavior of systems. Intuitive operational semantics, describing how changes are propagated among the loops, provide a basis for model animation or manual inspection. They are, however, not precise enough to enable automated property checking. This paper proposes and defines a net-based formal framework, showing true concurrency, so that automated analysis is made possible.

Abstract
In the last decade, we have witnessed the emergence of a new socioeconomic paradigm related to Internet-based virtual communities that promote practices of sharing the use or consumption of products and services: the collaborative economy. Despite growing research on the most diverse areas of the collaborative economy, research on the integration of blockchain systems into collaborative economy organizations is still rather limited. By the present investigation, purely explanatory and based on a comparative and interpretive case study, we intend to verify the susceptibility of the blockchain systems to foster the emergence of new business models. Due to the small number of organizations in the collaborative economy currently operating with blockchain-based business models, it will be important in future investigations to identify and study the influence of these systems on the business models of other organizations, in particular whether their adoption represents a source of competitive advantage.

Abstract
In two-dimensional nesting problems (irregular packing problems) small pieces with irregular shapes must be packed in large objects. A small number of exact methods have been proposed to solve nesting problems, typically focusing on a single problem variant, the strip packing problem. There are however several other variants of the nesting problem which were identified in the literature and are very relevant in the industry. In this paper, constraint programming (CP) is used to model and solve all the variants of irregular cutting and packing problems proposed in the literature. Three approaches, which differ in the representation of the variable domains, in the way they deal with the core constraints and in the objective functions, are the basis for the three models proposed for each variant of the problem. The non-overlap among pieces, which must be enforced for all the problem variants, is guaranteed through the new global constraint NoOverlap in one of the proposed approaches. Taking the benchmark instances for the strip-packing problem, new instances were generated for each problem variant. Extensive computational experiments were run with these problem instances from the literature to evaluate the performance of each approach applied to each problem variant. The models based on the global constraint NoOverlap performed consistently better for all variants due to the increased propagation and to the low memory usage. The performance of the CP model for the strip packing problem with the global constraint NoOverlap was then compared with the Dotted Board with Rotations using larger instances from the literature. The experiments show that the CP model with global constraint NoOverlap can quickly find good quality solutions in shorter computational times even for large instances.

Abstract
Kleene algebra with tests (KAT) was introduced as an algebraic structure to model and reason about classic imperative programs, i.e. sequences of discrete transitions guarded by Boolean tests. This paper introduces two generalisations of this structure able to express programs as weighted transitions and tests with outcomes in non necessarily bivalent truth spaces: graded Kleene algebra with tests (GKAT) and a variant where tests are also idempotent (I-GKAT). In this context, and in analogy to Kozen's encoding of Propositional Hoare Logic (PHL) in KAT we discuss the encoding of a graded PHL in I-GKAT and of its while-free fragment in GKAT. Moreover, to establish semantics for these structures four new algebras are defined: FSET(T), FREL(K,T) and FLANG(K,T) over complete residuated lattices K and T, and M (n, A) over a GKAT or I-GKAT A. As a final exercise, the paper discusses some program equivalence proofs in a graded context.