On-line system for faults detection in induction motors based on PCA

Dissertation to obtain the degree of Master in Electrical and Computer Engineering

Probabilistic constraint reasoning

Dissertação apresentada para obtenção do Grau de Doutor em Engenharia Informática, pela Universidade Nova de Lisboa, Faculdade de Ciências e Tecnologia

Production of aluminium based composites reinforced with embedded NiTi by friction stir welding

Dissertação para a obtenção do grau de Mestre em Engenharia Mecânica

The tight grip of a debt based global economy: A study on banking regulation and the implementation of the Basel II Accord in Portugal

A Work Project, presented as part of the requirements for the Award of a Masters Degree in Management from the NOVA – School of Business and Economics

Development of chitosan-based microparticles for pulmonary drug delivery

Dissertação para obtenção do Grau de Mestre em Engenharia Química e Bioquímica

Data-centric concurrency control on the java programming language

Dissertação para obtenção do Grau de Mestre em Engenharia Informática

Earth-based repair mortars: experimental analysis with different binders and natural fibers

RESTAPIA 2012 - Int. Conf. on Rammed Earth Conservation, Valencia, 21-23 June 2012

A nanopore-based stochastic detection method: Single molecule characterisation of nanoparticles using ()- hemolysin

Dissertation presented to obtain the Ph.D degree in Chemistry.

Earth-based mortars for masonry plastering

9th International Masonry Conference 2014, 7-9 July, Universidade do Minho, Guimarães

Probabilistic constraint reasoning with Monte Carlo integration to robot localization

This work studies the combination of safe and probabilistic reasoning through the hybridization of Monte Carlo integration techniques with continuous constraint programming. In continuous constraint programming there are variables ranging over continuous domains (represented as intervals) together with constraints over them (relations between variables) and the goal is to find values for those variables that satisfy all the constraints (consistent scenarios). Constraint programming “branch-and-prune” algorithms produce safe enclosures of all consistent scenarios. Special proposed algorithms for probabilistic constraint reasoning compute the probability of sets of consistent scenarios which imply the calculation of an integral over these sets (quadrature). In this work we propose to extend the “branch-and-prune” algorithms with Monte Carlo integration techniques to compute such probabilities. This approach can be useful in robotics for localization problems. Traditional approaches are based on probabilistic techniques that search the most likely scenario, which may not satisfy the model constraints. We show how to apply our approach in order to cope with this problem and provide functionality in real time.

State detection in a financial portfolio: a self-organizing maps approach for financial time series

This study analyses financial data using the result characterization of a self-organized neural network model. The goal was prototyping a tool that may help an economist or a market analyst to analyse stock market series. To reach this goal, the tool shows economic dependencies and statistics measures over stock market series. The neural network SOM (self-organizing maps) model was used to ex-tract behavioural patterns of the data analysed. Based on this model, it was de-veloped an application to analyse financial data. This application uses a portfo-lio of correlated markets or inverse-correlated markets as input. After the anal-ysis with SOM, the result is represented by micro clusters that are organized by its behaviour tendency. During the study appeared the need of a better analysis for SOM algo-rithm results. This problem was solved with a cluster solution technique, which groups the micro clusters from SOM U-Matrix analyses. The study showed that the correlation and inverse-correlation markets projects multiple clusters of data. These clusters represent multiple trend states that may be useful for technical professionals.

Efficient paraconsistent reasoning with rules and ontologies for the semantic web

Ontologies formalized by means of Description Logics (DLs) and rules in the form of Logic Programs (LPs) are two prominent formalisms in the field of Knowledge Representation and Reasoning. While DLs adhere to the OpenWorld Assumption and are suited for taxonomic reasoning, LPs implement reasoning under the Closed World Assumption, so that default knowledge can be expressed. However, for many applications it is useful to have a means that allows reasoning over an open domain and expressing rules with exceptions at the same time. Hybrid MKNF knowledge bases make such a means available by formalizing DLs and LPs in a common logic, the Logic of Minimal Knowledge and Negation as Failure (MKNF). Since rules and ontologies are used in open environments such as the Semantic Web, inconsistencies cannot always be avoided. This poses a problem due to the Principle of Explosion, which holds in classical logics. Paraconsistent Logics offer a solution to this issue by assigning meaningful models even to contradictory sets of formulas. Consequently, paraconsistent semantics for DLs and LPs have been investigated intensively. Our goal is to apply the paraconsistent approach to the combination of DLs and LPs in hybrid MKNF knowledge bases. In this thesis, a new six-valued semantics for hybrid MKNF knowledge bases is introduced, extending the three-valued approach by Knorr et al., which is based on the wellfounded semantics for logic programs. Additionally, a procedural way of computing paraconsistent well-founded models for hybrid MKNF knowledge bases by means of an alternating fixpoint construction is presented and it is proven that the algorithm is sound and complete w.r.t. the model-theoretic characterization of the semantics. Moreover, it is shown that the new semantics is faithful w.r.t. well-studied paraconsistent semantics for DLs and LPs, respectively, and maintains the efficiency of the approach it extends.

A logical foundation for session-based concurrent computation

Linear logic has long been heralded for its potential of providing a logical basis for concurrency. While over the years many research attempts were made in this regard, a Curry-Howard correspondence between linear logic and concurrent computation was only found recently, bridging the proof theory of linear logic and session-typed process calculus. Building upon this work, we have developed a theory of intuitionistic linear logic as a logical foundation for session-based concurrent computation, exploring several concurrency related phenomena such as value-dependent session types and polymorphic sessions within our logical framework in an arguably clean and elegant way, establishing with relative ease strong typing guarantees due to the logical basis, which ensure the fundamental properties of type preservation and global progress, entailing the absence of deadlocks in communication. We develop a general purpose concurrent programming language based on the logical interpretation, combining functional programming with a concurrent, session-based process layer through the form of a contextual monad, preserving our strong typing guarantees of type preservation and deadlock-freedom in the presence of general recursion and higher-order process communication. We introduce a notion of linear logical relations for session typed concurrent processes, developing an arguably uniform technique for reasoning about sophisticated properties of session-based concurrent computation such as termination or equivalence based on our logical approach, further supporting our goal of establishing intuitionistic linear logic as a logical foundation for sessionbased concurrency.

Characterization of earth-based mortars for rammed earth repair

All over the world, many earth buildings are deteriorating due to lack of maintenance and repair. Repairs on rammed earth walls are mainly done with mortars, by rendering application; however, often the repair is inadequate, resorting to the use of incompatible materials, including cement-based mortars. It has been observed that such interventions, in walls that until that day only had presented natural ageing issues, created new problems, much more dangerous for the building than the previous ones, causing serious deficiencies in this type of construction. One of the problems is that the detachment of the new cement-based mortar rendering only occurs after some time but, until that occurrence, degradations develop in the wall itself. When the render detaches, instead of needing only a new render, the surface has to be repaired in depth, with a repair mortar. Consequently, it has been stablished that the renders, and particularly repair mortars, should have physical, mechanical and chemical properties similar to those of the rammed earth walls. This article intends to contribute to a better knowledge of earth-based mortars used to repair the surface of rammed earth walls. The studied mortars are based on four types of earth: three of them were collected from non-deteriorated parts of walls of unstabilized rammed earth buildings located in Alentejo region, south of Portugal; the fourth is a commercial earth, consisting mainly of clay. Other components were also used, particularly: sand to control shrinkage; binders stabilizers such as dry hydrated air-lime, natural hydraulic lime, Portland cement and natural cement; as well as natural vegetal fibers (hemp fibers). The experimental analysis of the mortars in the fresh state consisted in determining the consistency by flow table and the bulk density. In the hardened state, the tests made it possible to evaluate the following properties: linear and volumetric shrinkage; capillary water absorption; drying capacity; dynamic modulus of elasticity; flexural and compressive strength.

Rely-guarantee protocols for safe interference over shared memory

Mutable state can be useful in certain algorithms, to structure programs, or for efficiency purposes. However, when shared mutable state is used in non-local or nonobvious ways, the interactions that can occur via aliases to that shared memory can be a source of program errors. Undisciplined uses of shared state may unsafely interfere with local reasoning as other aliases may interleave their changes to the shared state in unexpected ways. We propose a novel technique, rely-guarantee protocols, that structures the interactions between aliases and ensures that only safe interference is possible. We present a linear type system outfitted with our novel sharing mechanism that enables controlled interference over shared mutable resources. Each alias is assigned separate, local roles encoded in a protocol abstraction that constrains how an alias can legally use that shared state. By following the spirit of rely-guarantee reasoning, our rely-guarantee protocols ensure that only safe interference can occur but still allow many interesting uses of shared state, such as going beyond invariant and monotonic usages. This thesis describes the three core mechanisms that enable our type-based technique to work: 1) we show how a protocol models an alias’s perspective on how the shared state evolves and constrains that alias’s interactions with the shared state; 2) we show how protocols can be used while enforcing the agreed interference contract; and finally, 3) we show how to check that all local protocols to some shared state can be safely composed to ensure globally safe interference over that shared memory. The interference caused by shared state is rooted at how the uses of di↵erent aliases to that state may be interleaved (perhaps even in non-deterministic ways) at run-time. Therefore, our technique is mostly agnostic as to whether this interference was the result of alias interleaving caused by sequential or concurrent semantics. We show implementations of our technique in both settings, and highlight their di↵erences. Because sharing is “first-class” (and not tied to a module), we show a polymorphic procedure that enables abstract compositions of protocols. Thus, protocols can be specialized or extended without requiring specific knowledge of the interference produce by other protocols to that state. We show that protocol composition can ensure safety even when considering abstracted protocols. We show that this core composition mechanism is sound, decidable (without the need for manual intervention), and provide an algorithm implementation.