Constraint solving over multi-valued logics - application to digital circuits

Due to usage conditions, hazardous environments or intentional causes, physical and virtual systems are subject to faults in their components, which may affect their overall behaviour. In a ‘black-box’ agent modelled by a set of propositional logic rules, in which just a subset of components is externally visible, such faults may only be recognised by examining some output function of the agent. A (fault-free) model of the agent’s system provides the expected output given some input. If the real output differs from that predicted output, then the system is faulty. However, some faults may only become apparent in the system output when appropriate inputs are given. A number of problems regarding both testing and diagnosis thus arise, such as testing a fault, testing the whole system, finding possible faults and differentiating them to locate the correct one. The corresponding optimisation problems of finding solutions that require minimum resources are also very relevant in industry, as is minimal diagnosis. In this dissertation we use a well established set of benchmark circuits to address such diagnostic related problems and propose and develop models with different logics that we formalise and generalise as much as possible. We also prove that all techniques generalise to agents and to multiple faults. The developed multi-valued logics extend the usual Boolean logic (suitable for faultfree models) by encoding values with some dependency (usually on faults). Such logics thus allow modelling an arbitrary number of diagnostic theories. Each problem is subsequently solved with CLP solvers that we implement and discuss, together with a new efficient search technique that we present. We compare our results with other approaches such as SAT (that require substantial duplication of circuits), showing the effectiveness of constraints over multi-valued logics, and also the adequacy of a general set constraint solver (with special inferences over set functions such as cardinality) on other problems. In addition, for an optimisation problem, we integrate local search with a constructive approach (branch-and-bound) using a variety of logics to improve an existing efficient tool based on SAT and ILP.

Constraint reasoning for differential models

The basic motivation of this work was the integration of biophysical models within the interval constraints framework for decision support. Comparing the major features of biophysical models with the expressive power of the existing interval constraints framework, it was clear that the most important inadequacy was related with the representation of differential equations. System dynamics is often modelled through differential equations but there was no way of expressing a differential equation as a constraint and integrate it within the constraints framework. Consequently, the goal of this work is focussed on the integration of ordinary differential equations within the interval constraints framework, which for this purpose is extended with the new formalism of Constraint Satisfaction Differential Problems. Such framework allows the specification of ordinary differential equations, together with related information, by means of constraints, and provides efficient propagation techniques for pruning the domains of their variables. This enabled the integration of all such information in a single constraint whose variables may subsequently be used in other constraints of the model. The specific method used for pruning its variable domains can then be combined with the pruning methods associated with the other constraints in an overall propagation algorithm for reducing the bounds of all model variables. The application of the constraint propagation algorithm for pruning the variable domains, that is, the enforcement of local-consistency, turned out to be insufficient to support decision in practical problems that include differential equations. The domain pruning achieved is not, in general, sufficient to allow safe decisions and the main reason derives from the non-linearity of the differential equations. Consequently, a complementary goal of this work proposes a new strong consistency criterion, Global Hull-consistency, particularly suited to decision support with differential models, by presenting an adequate trade-of between domain pruning and computational effort. Several alternative algorithms are proposed for enforcing Global Hull-consistency and, due to their complexity, an effort was made to provide implementations able to supply any-time pruning results. Since the consistency criterion is dependent on the existence of canonical solutions, it is proposed a local search approach that can be integrated with constraint propagation in continuous domains and, in particular, with the enforcing algorithms for anticipating the finding of canonical solutions. The last goal of this work is the validation of the approach as an important contribution for the integration of biophysical models within decision support. Consequently, a prototype application that integrated all the proposed extensions to the interval constraints framework is developed and used for solving problems in different biophysical domains.

Modern techniques for constraint solving the CASPER experience

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

Constraint-based modeling of minimum set covering: application to species differentation

Work presented in the context of the European Master in Computational Logics, as partial requisit for the graduation as Master in Computational Logics

Constraint-based verification of imperative programs

work presented in the context of the European Master’s program in Computational Logic, as the partial requirement for obtaining Master of Science degree in Computational Logic

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

Making sense of the experimental evidence on endogenous timing in duopoly markets

The prediction of asymmetric equilibria with Stackelberg outcomes is clearly the most frequent result in the endogenous timing literature. Several experiments have tried to validate this prediction empirically, but failed to find support for it. By contrast, the experiments find that simultaneous-move outcomes are modal and that behavior in endogenous timing games is quite heterogeneous. This paper generalizes Saloner’s (1987) and Hamilton and Slutsky’s (1990) endogenous timing games by assuming that players are averse to inequality in payoffs. We explore the theoretical implications of inequity aversion and compare them to the empirical evidence. We find that this explanation is able to organize most of the experimental evidence on endogenous timing games. However, inequity aversion is not able to explain delay in Hamilton and Slutsky’s endogenous timing games.

Constraint-based modelling of mixed microbial populations: Application to polyhydroxyalkanoates production

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

Constraint reasoning with local search for continuous optimization

Optimization is a very important field for getting the best possible value for the optimization function. Continuous optimization is optimization over real intervals. There are many global and local search techniques. Global search techniques try to get the global optima of the optimization problem. However, local search techniques are used more since they try to find a local minimal solution within an area of the search space. In Continuous Constraint Satisfaction Problems (CCSP)s, constraints are viewed as relations between variables, and the computations are supported by interval analysis. The continuous constraint programming framework provides branch-and-prune algorithms for covering sets of solutions for the constraints with sets of interval boxes which are the Cartesian product of intervals. These algorithms begin with an initial crude cover of the feasible space (the Cartesian product of the initial variable domains) which is recursively refined by interleaving pruning and branching steps until a stopping criterion is satisfied. In this work, we try to find a convenient way to use the advantages in CCSP branchand- prune with local search of global optimization applied locally over each pruned branch of the CCSP. We apply local search techniques of continuous optimization over the pruned boxes outputted by the CCSP techniques. We mainly use steepest descent technique with different characteristics such as penalty calculation and step length. We implement two main different local search algorithms. We use “Procure”, which is a constraint reasoning and global optimization framework, to implement our techniques, then we produce and introduce our results over a set of benchmarks.

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.

Exploiting the cointrgration between vix and CDS in a credit market timing model

We investigate the cointegration between VIX and CDS indices, and the possibility of exploiting it in an existing credit market timing investment model. We find cointegration over most of the sample period and the leadership of VIX over the CDS in the price discovery process. We present two methods for including cointegration into the model. Both strategies improve the in-sample and out-of-sample model performances, even though out-of-sample results are weaker. We find that in-sample better performances are explained by a stronger cointegration, concluding that in the presence of cointegration our strategies can be profitable in an investment model that considers transaction costs.

Pine processionary moth (Thaumetopoea pityocampa) and great tit (Parus major) in Portugal

In the present work, we studied a common outbreaking Lepidoptera species in Portuguese pine stands – Thaumetopoea pityocampa (Den. & Schiff.) - and one of its potential predators – Parus major (L.). The population dynamics of the immature stages of the Lepidoptera was studied in several types of Pinus pinaster (Aiton) plantations in three different areas: Setúbal Peninsula, Abrantes and National Pine Forest of Leiria. Location and plantation structure was the most important factors determining population density of T. pityocampa. Setubal and Abrantes was highly susceptible to attacks by the Lepidoptera, whereas Leiria had lower densities. Young and homogeneous pine stands was more susceptible to attacks than older and more heterogeneous pines stands. However, a desynchronized population of T. pityocampa, in which the larvae develops during summer instead of during winter, reached high densities also in Leiria. The impact of several mortality factors and climatic conditions on the immature stages of the insect (eggs and larvae), in normal and desynchronized populations are discussed, as well as possible evolutionary implications of the sudden appearance of the new version of T. pityocampa. The break of the pupa diapause and adult emergence times the annual life cycle of this insect. Adults from the desynchronized population emerged earlier than adults from the normal population, which in turn determined the change in the larvae development period. Different factors, potentially affecting the timing of adult emergence in both normal and abnormal populations are also discussed. To study P. Major, nest-boxes were placed in the areas of Setúbal and Leiria and they were monitored during three seasons. The nest-boxes increased the density of breeding and wintering birds in the studied pine plantations, indicating that a lack of natural holes are in fact a limiting factor for this populations. The earliest breeding start for this species was recorded in my study area, indicating that Portuguese coastal pines provide good breeding conditions earlier than in other areas of Europe and North Africa. This leads to an overlap between the end of the larvae stage of T. pityocampa and the beginning of the breeding season of P. major. Key-words: Thaumetopoea pityocampa, Parus major, Pinus pinaster, population dynamics, Portugal.

Patterns of Associational Life in Western Europe, 1800-2000

Thesis submitted for assessment with a view to obtaining the degree of Doctor of Political and Social Science of the European University Institute

Integrating protein structural information

Dissertação apresentada para obtenção de Grau de Doutor em Bioquímica,Bioquímica Estrutural, pela Universidade Nova de Lisboa, Faculdade de Ciências e Tecnologia

Refinamento de diagramas de classes: análise e verificação

Dissertação apresentada na Faculdade de Ciências e Tecnologia da Universidade Nova de Lisboa para obtenção do grau de Mestre em Engenharia Informática