In nature, there are two main nucleic acids: DNA and RNA. The central dogma of molecular biology describes the process by which DNA is transcribed into RNA, which in turn is translated into proteins. Contrary to the classical view of this dogma, it has been discovered that DNA transcription also generates non-coding nucleic acids, such as microRNAs and long non-coding RNAs. These ncRNAs play essential roles in gene regulation and other cellular processes, highlighting the complexity of the genetic machinery and the functional diversity of ncRNAs in cell biology. In this context, the optimization and enhancement of the Perci Database, a centralized and reliable source of information on colorectal cancer (CRC), has the potential to significantly boost research in this area. This improvement is important to facilitate understanding of the cellular mechanisms underlying tumor detection, progression and prognosis. Furthermore, this study aims to compile relevant data on colorectal cancer, with a focus on ncRNAs, in order to make them available for public consultation. An online database was developed covering five CRC descriptors and three specific categories of ncRNAs: long ncRNAs (lncRNAs), long circular ncRNAs (circ ncRNAs) and microRNAs (miRNAs), along with associated transcriptomic features. The cancer descriptors covered include colorectal cancer, colon cancer, adenocarcinoma, tumor and liver metastasis of colorectal cancer. Questions such as "Which circRNAs are implicated in colorectal neoplasia?", "Which circRNAs and miRNAs are associated with colorectal cancer liver metastasis?" and "Given a specific lncRNA (H19), which cancer descriptors are related to this ncRNA?" can be answered using our database. The web system can be accessed at: http://percidatabase.com.br/.

Nowadays, scientific and commercial applications are often deployed to cloud environments requiring multiple resource types. This scenario increases the necessity for efficient resource management. However, efficient resource management remains challenging due to the complex nature of modern cloud-distributed systems since resources involve different characteristics, technologies, and financial costs. Thus, optimized cloud resource management to support the heterogeneous nature of applications balancing cost, time, and waste remains a challenge. Multi-agent technologies can offer noticeable improvements for resource management, with intelligent agents deciding on Virtual Machine (VM) resources. This article proposes MAS-Cloud+, a novel agent-based architecture for predicting, provisioning, and monitoring optimized cloud computing resources. MAS-Cloud+ implements agents with three reasoning models including heuristic, formal optimization, and metaheuristic. MAS-Cloud+ instantiates VMs considering Service Level Agreement (SLA) on cloud platforms, prioritizing user needs considering time, cost, and waste of resources providing appropriate selection for evaluated workloads. To validate MAS-Cloud+, we use a DNA sequence comparison application subjected to different workload sizes and a comparative study with state-of-the-art work with Apache Spark benchmark applications executed on the AWS EC2. Our results show that to execute the sequence comparison application, the best performance was obtained by the optimization model, whereas the heuristic model presented the best cost. By providing the choice among multiple reasoning models, our results show that MAS-Cloud+ could provide a more cost-effective selection of the instances reducing approx 58% of execution average cost of WordCount, Sort and PageRank BigDataBench benchmarking workloads. As for the execution time, the WordCount and PageRank present reduction, the latter with approx 58%. The results indicate a promising solution for efficient cloud resource management.

Elastic Optical Networks (EONs) emerge as a technology for efficient spectral allocation in optical fibers. A single EON fiber supports multiple circuits in parallel, allocating distinct spectral channels and accommodating circuits with variable bandwidth requirements. Multi-core fibers (MCF) emerge to increase resource availability further. The MCF can hold multiple cores (usually 7 or 12). Conceptually, each MCF operates as a group of single-core fibers. MCFs enable Spatial Division Multiplexing (SDM) in EON, which increases spectral resources by utilizing the different spatial channels (cores). The current SDM-EON literature branches into two main paradigms: core-constrained and Spatial Lane Change (SLC). The former defines architectures where a circuit must remain in the same core along its route. The latter, SLC architectures, allow the core switching along the route. The impact caused by the two architectures lies in the deployment and energy cost versus the degree of flexibility in the resource allocation procedure. This thesis proposes solutions to improve resource utilization efficiency in both paradigms. A resource allocation solution with dedicated cores for different circuit categories is proposed for architectures focused on the core-constrained paradigm. This solution aims to maintain circuits that are more resilient to physical interferences in the most affected cores, besides adopting techniques to reduce spectral fragmentation in allocation. For the SLC paradigm, this thesis presents a solution adapted to network defragmentation scenarios. The proposed solution combines a defragmentation heuristic with two techniques for spectral reorganization without service interruption or suspension. The goal is to reduce the fragmentation state whenever a trigger is activated, resulting in greater resource availability after spectral reorganization. Finally, a novel core switching paradigm, named sparse core switching, is introduced, which entails an architecture on which different nodes in the network possess distinct degrees of flexibility to perform core switching. The main objective is to reduce drastically the deployment cost while maintaining switching flexibility only in more advantageous nodes. This approach saves resources on multiple levels and performs efficiently compared to core-constrained and SLC approaches.

The need to leverage means to specify robotic missions from a high abstraction level has gained momentum due to the popularity growth of robotic applications. As such, it is paramount to provide means to guarantee that not only the robotic mission is correctly specified, but that it also guarantees degrees of safety given the growing complexity of tasks assigned to Multi-Robot Systems (MRS). Therefore, robot missions now need to be specified and formally verified for both robots and other agents involved in the robotic mission operation. However, many mission specifications lack a streamlined verification process that ensures that all mission properties are thoroughly verified through model checking. This work proposes a preliminary model checking process for mission specification and decomposition of MRS in UPPAAL model checker. In particular, we present a semi-automated model containing hierarchical domain definition properties transformed into UPPAAL templates and mission properties formalized into the UPPAAL timed automata language TCTL. In the future, we intend to fully generate models automatically and verify additional mission specification properties not covered currently. We have evaluated our approach in a robotic mission of a food logistic mission specification and results show that the expected behaviour is correctly verified and the corresponding properties satisfied in the UPPAAL model checking tool.

Osteoporosis is synonymous with bone fragility, and it is a silent disease that is only detected
commonly after it has already caused harm to the person who has it. This disease of frailty
bone makes the fracture more common and more harmful to its bearers, and for this reason it is a
public health issue. Identifying disease at an early stage is essential to help
prevent its damage, and in this task artificial intelligence and machine learning have
shown great help in recent years. Machine learning algorithms
can predict the risk of osteoporosis by analyzing patient images from
routine tests, such as panoramic radiographs.
The proposed methodology has a two-step process, which is composed of
image preprocessing and machine learning. The image preprocessing
consisted of transforming the raw original panoramic buccal images into regions of
reduced interest, more specific and clearer for classification. The learning stage
machine learning consisted of supplying these preprocessed images to algorithms
computations classify them. This work proposes a Neural Network architecture
Convolutional (CNN), compared with Support Vector Machine (SVM) and Random Forest
(RF), which aims to identify signs of osteoporosis in this type of image, with the aim of
improve the results of reference technique, the CNN of the article [1], when using the s-
CNN trutra modified to perform an automatic detection of osteoporosis with high
sensitivity and use the RF method for a system with high specificity.
In sensitivity, the proposed customized CNN obtained 77.19%, while the CNN of
reference obtained 70.18%. In specificity, the proposed Random Forest obtained 75.95%,
while the reference CNN obtained 22.78%. Combining these results,
we continue to improve what is obtained by the reference technique for the dataset
presented, which is quite challenging, of elderly patients from poor communities, in
analog images with various artifacts and characteristics that make classification difficult.

This work implements a noise detection algorithm recommendation using meta-learning techniques. First, a systematic review of the literature on the subject of meta-learning for preprocessing algorithm recommendation was performed. The review verified which preprocessing techniques, meta-features, machine learning algorithms and performance metrics are commonly used in the area of recommending preprocessing algorithms. Next, two different approaches were implemented for recommending noise filters using meta- learning techniques. The first is a ranking approach (MtL-Rank), which performs the suggestion using regressors and predicts the value of the performance metric f1-score. The other approach performs the recommendation through a sequence of linked classifiers (MtL-Multi). The performance of the approaches was also evaluated when recommending the filters together with their hyperparameters. In total, we used eight noise filters or 27 when considering their hyperparameter variations, four machine learning techniques to extract the performance metric and three meta-rankers or meta-classifiers to perform the recommendation. The system is evaluated at both the meta and base levels. At the meta level, the performance of a meta-learner is evaluated through their accuracy. At the base level, the average gain in the performance metric (f1-score) is verified. The results showed that the MtL-Rank approach obtained a higher average gain at the base level, obtaining significantly better results than the filter used as baseline. On the other hand, the MtL-Multi approach obtained better results at the meta level, reaching an accuracy up to 49%. In addition, it was verified that the suggestion of hyperparameters together with the noise filter can generate a gain in the performance when compared with only recommending the filter.

Background: Requirements elicitation techniques are essential to support requirements
engineers to gain a better understanding of the needs of users and stakeholders. Al-
though there are several techniques available to support the Requirements Engineering
(RE) software development teams might be doubtful about which technique to use during
requirements elicitation. Objective: The goal of this work is to identify Requirements
Elicitation (RE) Techniques most used in the literature and compare with the techniques
most used by professionals in the industry. In addition, we identified the challenges re-
lated to requirements elicitation, the pros and cons of the main techniques identified in
the literature, and based on the pros and cons, analyze possible combinations of require-
ments elicitation techniques that can minimize the challenges identified in literature and
industry. Method: We performed a Systematic Literature Review (SLR) to identify
requirements elicitation techniques and challenges discussed in the literature or industry.
Moreover, we performed a Survey to investigate the perception of software practitioners
(individuals working in the software industry in a large variety of roles and positions)
in relation to the techniques identified and subsequently compare them with the results
obtained in the SLR. Finally, using Focus Group technique, we executed two validation
sessions with nineteen specialists to evaluate technique combinations and the findings
provided on this guide. Results: 54 primary studies were identified in the SLR and they
demonstrated that traditional techniques are still the most used in both literature and
software industry projects. In addition, some techniques, such as Persona, are gaining
ground, helping requirements engineers to find different ways to elicit requirements from
end users and stakeholders. Moreover, we have investigated combinations of techniques
already discussed and presented in literature, also based on the strengths found in the
literature for each technique, it was possible to identify combinations of techniques that
by the forces or points in favor identified in the SLR, could be combined to overcome most
of the challenges identified. Furthermore, validation sessions provided the view of special-
ists that complemented the techniques and combinations under use by the community.
Conclusion The most mentioned techniques in the literature at the same time they are
used in the software industry are: Prototyping, Interview, User Stories, Brainstorming,
Observation, Scenarios, Questionnaires and Mind Mapping. In addition, Ethnography,
Joint Application Development (JAD) and Workshop have many references in literature
while are not appealing for real projects in industry. On the other hand, Persona at least
from the papers retrieved during this search is not largely discussed in literature whereas
it has shown to be widely used in the industry. Combine the use of RE techniques can
help overcome the challenges identified in the literature. A guide with a description of all
techniques identified in the literature, containing their advantages and disadvantages can
support the requirements engineers during the requirements elicitation. The provision
of this study to support software practitioners in eliciting requirements, will allow the
software engineering community to contribute feedback related to the combination of the
use of techniques, thus allowing an improvement and dissemination of the perceptions of
the combinations made between the RE techniques by the professionals of the software
development teams. Hence, the guide can support software practitioners in choosing the
techniques to be used and (or) combined.

Forensic face comparison is becoming more relevant as the number of devices with image recording capabilities increases, with a consequential increase in the number of crimes in which the face of the perpetrator is recorded. This forensic examination is still based on the manual analysis and comparison of morphological features of the faces. Its results are expressed qualitatively, making it difficult to reproduce and combine with other evidence. This work evaluates methods to obtain a quantitative result for the examination, with the computation of score-based Likelihood-Ratio - LR. Face recognition systems are used to obtain scores that are then converted to an LR. The methods investigated in this work facilitate reproducibility, a critical aspect in forensics, and it also allows for the empirical validation of performance in the conditions of each forensic case. We evaluate parametric and non-parametric methods for LR computation. Two open-source face recognition models were used (ArcFace and FaceNet) on images from five datasets that are representative of common scenarios in forensic casework: images from social media and images from CCTV cameras. We also investigate strategies for embedding aggregation in cases where there is more than one image of the person of interest. These experiments demonstrate substantial improvements in forensic evaluation settings, with improvements in Cllr of up to 95% (from 0.249 to 0.012) for CCTV images and of up to 96% (from 0.083 to 0.003) for social media images.

This work proposes an application to help teachers identify students suspected of plagiarism in source codes in an introductory programming course with a virtual teaching environment. This is done through the integration of automatic plagiarism detection tools with data on student behavior in the course, for the generation of unified reports. This behavioral data includes the assignment submission pattern and classroom data such as attendance and grades. It can be applied in distance or face-to-face teaching. This application will be tested with real data in order to simplify the plagiarism identification process. It is also expected to learn more about the profile of students who copy source codes to outline policies aimed at reducing the occurrence of this practice.

This work discusses how the presence of round errors involved in real-world implementations of the
NASA management system for unmanned vehicles DAIDALUS affect the overal safety of the system. The
DAIDALUS library provides formal definitions for avionics’ Detect and Avoid concepts mechanically
demonstrated in the proof assistant PVS. However, such verifications are just certificates of the well-
behavior of the specification from the logical point of view, which do not guarantee the accuracy
of the algorithms implemented under floating-point arithmetic.Our analysis assumes the IEEE 754
floating point standards, implemented in several programming languages, and the verification technique
is grounded on generating a first-order specification of the numerical computations. A prominent feature
of the approach is splitting the specification into slices defined according to the different computation
branches. Slicing is crucial to simplify the formal analysis of floating point arithmetic computations

Nota: Suplente Mariano Miguel Moscato - National Insitute of Airspace - NASA LaRC

Training data labeling has become one of the main obstacles to the use of machine learning. Among several data labeling paradigms, weak supervision has shown as an opportunity to alleviate the bottleneck of manual labeling, since from supervision we can programmatically synthesize the training of labels from multiple sources generated by potentially noisy supervision. This dissertation presents experiments on one of the weak supervision application approaches. In particular, a brief literature review was carried out on the theoretical basis that supports the use of this approach and describes in general a learning and labeling workflow within the problem of named entity recognition from weak supervision. Finally, experiments were carried out to evaluate the gains of using this approach to assist in the labeling of bases within the context of Public Administration in Brazil, and thus, to inspire future research directions in the field.

Colorectal cancer (CRC) is one of the most frequent and lethal types of cancer around the world, being the second most frequent cancer in Brazil [1]. CRC is a heterogenous cancer that settles in the lower part of the large bowel and can be classified according to its anatomical site as:colon, rectum, and rectosigmoid junction cancer. The most common type of CRC is the adenocarcinoma, which accounts for 90% of the cases. Most of CRC deaths are related to its metastases, and if early detected, it improves considerably the patient survival chances. This disease can be impacted by many environmental aspects such as: eating habits, age, and weight. Its treatment can also differ according to its anatomical site and its recommended treatment, usually, first surgery and then chemotherapy. An inaccurate identification of the CRC anatomical site can lead to under or overtreatment, which can impact the patient’s likelihood of mortality. In order to help CRC prognosis, prevention, and treatment, it is crucial to understand the molecular mechanisms and external factors that affect CRC development and progression. 

Regarding the biological aspects of CRC, we can describe the impact of coding and non-coding RNAs on the disease’s underlying mechanisms. In specific, we can highlight three molecules: long non-coding RNAs (lncRNAs), micro RNAs (miRNAs), and messenger RNAs (mRNAs). In eukaryotes, the mature mRNAs are formed after the pre-mRNA generated from the transcription undergoes a process known as splicing, which removes some regions (introns) of the pre-mRNA, while binding others (exons), thus forming the mature mRNA. The splicing process can generate more than one protein from a single gene in a process known as alternative splicing. The generated proteins then are used to regulate the organism’s functions by being used in metabolic reactions and affecting many biological processes, such as disease development. 

The miRNAs play an essential role in gene expression, more specifically, by binding to mRNAs and then starting the processes of inhibition or degradation of their target. On the other hand, the lncRNAs are not directly portrayed in this mRNA expression regulation process but play essential roles, such as altering other molecules’ functions and therefore affecting protein expression affecting disease development and suppression. Given the specific role of each described molecule in disease development, recent studies also highlighted the importance of a mechanism known as competing endogenous RNAs (ceRNAs) networks, in which lncRNAs, miRNAs, and mRNAs interact among themselves. In this mechanism, the miRNAs, in addition to their capability of binding to

the mRNAs, can also bind to the ceRNAs, which then, act as modulators of miRNAs, therefore, indirectly regulating the mRNA expression. The identification of ceRNA networks related to CRC development and its underlying mechanisms can help doctors to understand better the disease and better identify the patient’s prognosis. In literature, we can find some studies that use bioinformatic approaches to analyze and create ceRNA networks and to indicate potential prognosis biomarkers for colon, rectal, and colorectal cancer in general [2, 3, 4, 5, 6, 7, 8].

Although some studies were done with the ceRNAs networks constructions in mind, to the best of our  knowledge, our study was the first to establish specific ceRNA networks for: (i) colon; (ii) rectum; and (iii) rectosigmoid junction, and to relate them with specific biological mechanisms in order to clarify the differences and common factors between these sites.

On the other hand, some studies suggest the use of machine learning methods using clinical features to predict CRC patient prognosis [9, 10, 11]. In specific, Gründner et al. [9] explored a method that combined biological and clinical features to predict prognosis aspects for CRC patients from South Africa. These studies showed promising results in predicting CRC patient’s prognosis, but to the best of our knowledge, our study was the
first one that used open data and machine learning to predict CRC recurrence and patient survival by using biological markers extracted from the colon, rectal and rectosigmoid cancer ceRNA networks combined with clinical features.

In this thesis, as the first step, we propose a pipeline by using open-access data from patients with CRC extracted from The Cancer Genome Atlas (TCGA) to construct CRC-specific ceRNA networks and potential biological markers that affect patient prognosis. We aim to perform an analysis to identify molecules that can be used as biological markers for the three CRC anatomical sites:colon, rectum, and rectosigmoid junction. To 
construct these networks and propose the biological markers, RNA raw expression and clinical data from the CRC patients were collected.The RNA expression profiles were assessed by the use of bioinformatic analysis tools, and a ceRNA network was constructed for each CRC anatomical site, where as output we got the ceRNA networks and the molecules present on them. After, a functional enrichment analysis was performed, where we assessed the potential biological pathways activated by the molecules obtained in the previous step. Finally, an overall survival analysis to identify the impact of these molecules on patient prognosis was performed, giving as output a list of potential biological markers. 

As an overall result of the first pipeline of this thesis, several potential prognostic markers for colon, rectum, and rectosigmoid junction cancer were found.Also, specific ceRNA networks for each anatomical site were constructed, and we identified different biological pathways that highlight differences in CRC behavior at the different anatomical sites, thus reinforcing the importance of correctly identifying the tumor site. As output, a group of potential biological markers involved in CRC prognosis was generated, in specific, we can highlight the site-specific prognosis biomarkers: hsa-miR-1271-5p,NRG1, hsa-miR-130a-3p,SNHG16, and hsa-miR-495-3p in the colon;E2F8in the rectum; and DMDand hsa-miR-130b-3p in the rectosigmoid junction.

With the list of potential biological markers related to CRC prognosis, then we proceeded to the second part of this thesis, the proposal of a pipeline to predict CRC recurrence and patient survival using supervised machine learning (ML) methods. Clinical factors such as age and weight, as well as biological factors, can affect CRC progression and prognosis. To better understand the mechanisms of CRC and to identify the impact of both clinical and biological factors in its prognosis, we used patient clinical features combined with the previously found biological markers as biological features, to train our ML models.In order to achieve higher predictive performance and interpretability of the proposed findings, we evaluated and compared the following ML algorithms: Random Forest (RF), Logistic Regression (LR), Support Vector Machine (SVM), K-Nearest
Neighbors (KNN), Decision Tree (DT) e Adaptative Boosting (AB). To establish the importance of each feature while building the models to predict CRC recurrence and patient survival, first, a feature extraction analysis was performed, to filter and rank which of these features in fact have an impact on the constructed prediction model. With the selected relevant biological and clinical features in hand, we then constructed the ML models and evaluated their performance. Finally, as output, we generated ML models to predict CRC recurrence and patient survival and a list of potential biological and clinical features relevant to patient prognosis.

Regarding the overall result from the second pipeline, several potential biological and clinical markers were pointed out as important in CRC recurrence and patient survival. For feature importance, we pointed out: SNHG16, hsa-miR-130b-3p, hsa-miR-495-3p, and KCNQ1OT1 as biological features; and age, ethnicity, pathological stage, chemotherapy, height and weight, positive lymph node count and lymph node count as clinical features. Finally, by using LR and RF we achieved the best accuracy of 90% and 82% for predicting
patient survival and CRC recurrence, respectively. Also, the use of the six proposed ML algorithms showed an overall good performance, in specific, LR and RF displayed good overall results, which was also highlighted in other studies [9, 10, 11].

This study strongly suggests that the use of bioinformatic approaches should be concurrently used with ML algorithms to enhance the interpretation of CRC mechanisms and patient prognosis. However, we should highlight some limiting factors such as: the amount of available data, as the number of available patients for certain anatomical sites was low; and that the data mainly consisted of patients from the USA. Following the proposed pipelines, doctors can better understand the underlying mechanisms of CRC in its anatomical sites, and also use our model to help predict patient prognosis. Finally, running these pipelines in Brazilian patient data could lead to an increase in CRC data interpretation, especially in a circumstance where there is diversity and inequality in the country’s demographic landscape, which can affect CRC prognosis.

The emergence of Transformer — a model pre-trained over a large-scale dataset — and the recent new versions have revolutionized research in Machine Learning, especially in Natural Language Processing (NLP) and Computer Vision. The excellent results of Tranformer-based models depend on labeled and high-quality domain specific data. How- ever, due to the diversity of contexts in which these models are used, it is challenging to create models that learn from limited data. The model may suffer from a lack of gener- alization, language bias, and fairness issues caused by large pre-trained models, resulting in unexpected outcomes in real-world applications. This open problem leads to research in multimodal Few-Shot Learning (FSL).

In this thesis, we propose the Generic Multimodal Gradient-Based Meta Framework (GeMGF). To compensate for the scarcity of data, we use multimodal data in which supplementary and complementary information of one modality can help the data repre- sentation. The multimodal data are extracted using deep learning models and represented in a unified vector space. The framework uses the Prototypical Network and Relation Net- work in the FSL. The Reptile — an optimization-based meta-learner — helps the model avoid model degradation with unseen data. In addition to the multimodal framework, we propose the unimodal version to evaluate the flexibility and adaptability of the framework in different scenarios.

The framework was evaluated using ten datasets from various domains and charac- teristics, including short texts from Twitter, legal domain long text, text with alphabetic (English and Portuguese) and non-alphabetic (Japanese) languages, medical domain im- ages, and multimodal benchmark datasets. Our multimodal framework was evaluated using CUB-200-2011 and Oxford-102 datasets, outperforming the state-of-the-art model of Munjal et al. [1] by 1.43% with CUB-200-2011 and Pahde et al. [2] by 1.93% with Oxford-102. The result of the multimodal framework with CUB-200-2011 was 34.68% higher than the unimodal framework for image and 13.96% higher with Oxford-102. The results suggest that text and image data jointly helped the framework learn rich informa- tion and improve overall performance. The multimodal GeMGF is a simple and compact framework using only 14 million parameters, 99.8% less than the Multimodal Trans former. The unimodal framework for text achieved excellent results with the Japanese dataset, outperforming Transformer BERT by 58.30% with 90.90% fewer parameters. These results suggest that our framework achieved better performance with a significant computational cost reduction.

The main contributions of our research are: (i) a novel multimodal FSL framework, GeMGF is developed to reduce the model degradation trained over a few data; (ii) GeMGF is trained without external knowledge avoiding language bias and fairness issues; (iii) GeMGF has independent and flexible feature extractors that enhance its applicability; and (iv) the unimodal framework for text can be adapted to process alphabetic and non- alphabetic languages with high performance.

This work describes the mechanization of the computational properties of a functional-language model that has been applied to reasoning about the automation of program termination. The formalization was developed using the higher-order proof assistant Prototype Verification System (PVS). The language model was designed to mimic the first-order fragment of PVS functional specifications and is called PV0. Two different computational models are considered: the first model specifies functional programs through a unique function (single-function PVS0 model, or SF-PVS0), and the second model allows simultaneous specification of multiple functions (multiple-function PVS0 model, or MF-PVS0). The operational semantics of recursion in single-function PVS0 specification supports recursion over the whole program.

In contrast, in multiple-function PVS0 programs,  functional calls are allowed to all functions specified in the program. This work aims to mathematically certify the robustness of the PVS0 models as universal computational models. For doing that, crucial properties and theorems were formalized, including Turing Completeness, the undecidability of the Halting Problem,  the Recursion Theorem, Rice's Theorem, and the Fixed Point Theorem. Furthermore,  the work discusses advances in the undecidability of the Word Problem and the Post Correspondence Problem.

The undecidability of the Halting Problem was formalized considering properties of the semantic evaluation of PVS0 programs that were applied in verifying the termination of PVS specifications. The equivalence between predicative and functional evaluation operators was vital to this aim. Furthermore, the compositionality of multiple-function PVS0 programs, straightforwardly enabled by the possibility of calling different functions, makes it easy formalization of properties as Turing Completeness. Therefore, enriching the model was an important design decision to simplify the mechanization of this property and the theorems mentioned above.

This thesis explores Multi-Agent Planning (MAP) and its application in dynamic environments. MAP combines artificial intelligence planning with multi-agent systems to coordinate intelligent agents achieving individual or group goals. Planning in dynamic environments introduces challenges in coordination and execution due to non-deterministic outcomes. Plan recovery strategies, like replanning and repairing, aim to handle failures and restore desired conditions. A comprehensive literature review highlighted key contributors and institutions in the MAP research offering insights into concepts, techniques,
and open challenges. However, the combination of different recovery strategies for MAP models is a research challenge not yet accomplished in the present literature. In this thesis, we address this challenge by proposing an evaluation method for recovery strategies in dynamic environments, combining replanning and repairing. This approach considers planning complexity, coordination allied to execution issues, and agents attempting local repairs before seeking other agents’ assistance. The main objective and results aim to contribute to the MAP field by evaluating the combination of replanning and repairing in planning solution models for dynamic environments.

When watching 360◦videos, the user has higher content control interactivity, and , thus,
the conventional visual quality is not enough to describe stimulus, that in turn extends to
the concept of quality of experience (QoE). This dissertation examines quality factors of
today‘s most popular immersive media format, the 360◦videos. Particularly important,
the subjective assessment of quality of experience. Subjective experiments provide data
to build adequate solutions and are essential to developing and improving multimedia
systems and applications. The visual quality assessment support researchers to establish
baselines for coding, and streaming applications.However, the reliability level of the
measurement of quality in subjective experiments can vary depending on the type of me-
dia. The optimization of QoE faces two major roadblocks: inaccurate viewport prediction
and viewers missing the plot of a story.Alignment edits have emerged as a promising
mechanism to avoid both issues at once. These “re-targeting edits” act on the content in
real-time, aligning the user’s viewport with a region of interest in the video content. In
this dissertation, we investigate the effects of alignment edits on user QoE by conducting
two subjective experiments, where we introduce gradual alignment editions in the videos,
inspired by a VR gaming technique.The results confirmed that the proposed gradual
alignment achieves a level of comfort and presence similar to that of instant editions.
Moreover, all alignment edits tested reduced the head speed after the edit, confirming
the usefulness of these edits for streaming video on-demand. Furthermore, we observed
that the proposed gradual editions can achieve a reduction in head speed of 8% greater
compared to the instant alignment techniques.

Image segmentation aims to simplify the understanding of digital images. Deep learning-based
methods using convolutional neural networks were game-changing, allowing the exploration of
different tasks (e.g., semantic, instance, and panoptic segmentation).Semantic segmentation
assigns a class to every pixel in an image, instance segmentation classifes objects at a pixel
level with a unique identifer for each target, and panoptic segmentation combines instance-
level predictions with different backgrounds.Remote sensing data largely benefts from those
methods, being very suitable for developing new DL algorithms and creating solutions using
top-view images.However, some peculiarities prevent remote sensing using orbital and aerial
imagery from growing when compared to traditional ground-level images (e.g., camera photos):
(1) The images are extensive, (2) it presents different characteristics (e.g., number of channels
and image format), (3) a high number of pre-processes and post-processes steps (e.g., extracting
patches and classifying large scenes), and (4) most open software for labeling and deep learn-
ing applications are not friendly to remote sensing due to the aforementioned reasons.This
dissertation aims to advance in all three main categories of image segmentation. Within the in-
stance segmentation domain, we proposed three experiments. First, we enhanced the box-based
instance segmentation approach for classifying large scenes, allowing practical pipelines to be
implemented. Second, we created a bounding-box free method to reach instance segmentation
results by using semantic segmentation models in a scenario with sparse objects.Third, we
improved the previous method for crowded scenes and developed the first study considering
semi-supervised learning using remote sensing and GIS data. Next, in the panoptic segmenta-
tion domain, we presented the first remote sensing panoptic segmentation dataset containing
fourteen classes and disposed of software and methodology for converting GIS data into the
panoptic segmentation format. Since our first study considered RGB images, we extended this
approach for multispectral data.Finally, we leveraged the box-free method initially designed
for instance segmentation to the panoptic segmentation task. This dissertation analyzed various
segmentation methods and types of images, and the developed solutions enable the exploration
of new tasks (such as panoptic segmentation), the simplification of labeling data (using the pro-
posed semi-supervised learning procedure), and a simplified way to obtain instance and panoptic
predictions using simple semantic segmentation models.

Deep learning methods have demonstrated remarkable performance in pathology image
segmentation and classification tasks. However, these models require a large amount of
annotated training data. Training data generation is a labor intensive process in digital
pathology, often requiring substantial time commitment from expert pathologists. Ac-
tive learning (AL) offers an iterative approach to generate training data needed by deep
learning models, reducing the cost of manual data annotation. In this work, a new AL
acquisition method, named Diversity-Aware Data Aquisition (DADA), is proposed and
evaluated regarding its effectiveness in patch-based detection and classification of tissue
image regions. The proposed method uses a clustering logic that takes into account image
features, extracted from the deep learning model being trained, and model prediction un-
certainty to select meaningful training samples (image patches). Besides reducing training
set sizes, annotation costs are also diminished by computation time gains using a CNN
simplification solution also developed in this work, the Network Auto-Reduction (NAR).
With NAR, both uncertainty calculation costs and model training times are strongly re-
duced. Additionally, to make these solutions viable in practice, a Web based graphical
interface was adapted to be used with DADA. The DADA/NAR solutions were exper-
imentally evaluated with a collection of cancer tissue images and are able to: (i) select
image patches that accelerate the training process by reducing the number of patches
required to attain a given Area Under the Curve (AUC) value; (ii) using a subpooling
approach, DADA dramatically reduces iteration times needed to select a new annota-
tion set; and (iii) the combination of DADA and NAR brings down the execution times
even more, reaching practical levels while keeping the predictive capacity of models. The
generalisation of both DADA and NAR to other contexts and applications are expected
future work, including application in areas such as remote sensing and image segmentation
problems.