Local: Sala Multiuso CIC
Horário: 14h
Palestrante: Vitor Filincowsky Ribeiro (doutorado)
Título: Conflict Detection and Resolution for 4D-EFP Air Navigation using Heuristic Methods
Resumo: The main goal in Performance Based Operations is the management of flight trajectories in order to optimize the operating capability of the aircraft, reducing fuel burn and emissions during each flight phase. At the same time the maximization of airspace efficiency/capacity needs to be addressed considering local airspace requirements and constraints. The en-route coordination task can be viewed as a scenario in which several aircraft issue their desired routes to ATC, which should eliminate eventual conflicts and grant a fair cost propagation to the aircraft. It is proposed a 4D-compliant framework that uses the Aircraft Intent Description Language (AIDL) in order to build the trajectories. Furthermore, heuristic models are used to adjust specific parameters in the provided trajectories. The result is a valid, conflict-free trajectory set that allows each aircraft to perform its near-optimum cost-efficient flight path through space and time.
Horário: 14h30
Palestrante: Washington Carvalho Segundo (doutorado)
Título: A Formalization of Nominal Unification Module C and AC
Resumo: Unification, matching and checking equality are basic operations in many contexts. For example: a) linear programming: equational systems are transformed to simpler "equivalent" ones; b) information retrieval needs to search for matchings to a particular string; and c) programming languages: unification is the core of type checking and type inference process. The equivalence between two objects can be extended to more complex relations. For instance, if one has the definition of a function, the names of its parameters will be irrelevant. Example: def1: (x) := x int x_1/dx{x} and def2: (u) := u int u_1/dw{w}. In the above definitions both functions have the same behaviour, although the names of variables are different. It is also necessary to note that particularly in def1 there are two binding scopes of x: first x was used as the top limit of the integral, and x was also in the body of the differential dx. These two scopes were nested and the name x was used for completely different purposes. So in def2 this difference are explicited by choosing different names u and v for different binding scopes. Another way to extend the notion of equality between objects is to consider some properties over the function symbols, such as: associativity, commutativity, distributivity, neutral element, etc. These properties occur very often in many operators. The main examples are the basic logical connectives (disjunction and conjunction), and the operators of union and intersection of the set theory. We are presenting a formalisation of a unification procedure that uses the nominal approach to deal with binding, and it also allows the occurrence of an enumerable set of C function symbols. This procedure was shown to be terminant and correct, and we hope that an extension of these proofs, including also A and AC function symbols, won't be hard to be done. Moreover, when we started writing the proof of the completeness of the procedure, it gave us a clue that the cardinality of the solutions set has changed. We have as result that nominal commutative unification may give rise to an infinite minimal complete set of solutions.
Horário: 15h
Palestrante: Emerson de Araujo Macedo (doutorado)
Título: Simulação de Enovelamento de Proteínas com Enterramento Atômico em Ambientes Computacionais de Alto Desempenho
Resumo: A função biológica que uma proteína desempenha em nosso organismo está relacionada com sua estrutura nativa, ou seja, a configuração tridimensional (3D) funcional da sua molécula. Uma proteína assume essa configuração 3D através de um processo chamado de enovelamento. Duas questões que envolvem a pesquisa sobre o problema do enovelamento de proteínas são: (i) qual é o código físico do enovelamento, isto é, como as propriedades físico-químicas codificadas na sequência de aminoácidos, sua configuração geométrica unidimensional (1D), determinam a configuração 3D nativa? (ii) é possível desenvolver uma solução computacional que permita predizer a configuração 3D nativa a partir de sua configuração 1D primária? O enterramento atômico é uma hipótese para responder à primeira questão. Trata-se de uma medida relacionada a propriedades como o efeito hidrofóbico e as pontes de hidrogênio e indica a distância física de cada átomo da proteína ao centro geométrico de sua estrutura 3D nativa. Sabe-se que este enterramento atômico possui informação suficiente para se determinar a configuração 3D nativa de pequenas proteinas globulares. A simulação de dinâmica molecular (MD, Molecular Dynamics) é um método computacional que auxilia tanto o processo experimental de determinação de estruturas de proteínas quanto a pesquisa e projeto de novos fármacos para tratar doenças relacionadas, como Alzheimer e Parkinson. A simulação MD é utilizada no estudo do código físico do enovelamento (i) e na predição de estruturas proteicas (ii). Porém, o algoritmo de simulação MD exige um alto custo computacional para modelar o processo de enovelamento de uma proteína. É neste contexto que a computação de alto desempenho é utilizada para viabilizar a simulação MD de enovelamentos de proteínas consideradas grandes e de eventos biológicos de interesse, tais como ataques a vírus HIV. Nessa apresentação, mostrarei uma solução de alto desempenho para a simulação MD, chamada NAMD, e como adaptá-la para auxiliar na pesquisa sobre o efeito do enterramento atômico no enovelamento de proteínas.
Profa Célia Ghedini Ralha (Este endereço de email está sendo protegido de spambots. Você precisa do JavaScript ativado para vê-lo.)
Coordenadora dos Seminários de Pós-Graduação Informática 2017-1