Local: Sala Multiuso CIC
Horário: 14h
Palestrante: Lucas Angelo Silveira (doutorando)
Título: Parallel Multi-Island Genetic Algorithms for Sorting Unsigned Genomes by Reversals
Resumo: Sorting unsigned permutations by reversals is an
N P-hard optimization problem with applications in compu-
tational molecular biology. Several approximation and meta-heuristic algorithms were proposed, among them, in a previous work, a competitive genetic algorithm and its parallel version using island models were proposed. In this paper, focusing on improving accuracy, new island models are proposed by diversifying the distribution of genetic material between islands through static and dynamic communication topologies. In static topologies, communication between islands is predefined and maintained during the computation, while in dynamic topologies the communication is continuously modified. The proposed island models use parallelism in a global and a local level, in which respectively occurs the exchange of individuals between islands and the fitness computation.
Results from the experiments performed with randomly generated synthetic permutations show that parallel island models using both dynamic and static communication topologies outperform parallel approaches found in the literature in terms of speed-up as well as accuracy.
Horário: 14h30
Palestrante: Daniela Angelos (mestranda)
Título: Combined Proof Methods for Multimodal Logic
Resumo:Lógicas modais têm sido estudadas na Ciência da Computação por permitirem a caracterização de sistemas complexos, envolvendo noções tais como conhecimento e crença, por exemplo. Neste trabalho, focamos no provador dej teoremas para a lógica multimodal básica Kn : KSP, que implementa um método baseado em resolução clausal. Cláusulas são rotuladas pelo nível modal em que ocorrem, auxiliando a restringir aplicações desnecessárias das regras de inferência. KSP apresenta uma boa performance se o conjunto de símbolos proposicionais estão bem distribuídos entre os níveis modais. Entretanto, quando há um grande número de variáveis em um nível específico, o tempo de execução aumenta. Uma das razões é que a transformação para a forma normal utilizada sempre gera conjuntos satisfatíveis de cláusulas proposicionais. Isto pode acarretar em uma significativa perda de performance, uma vez que resolução é baseada em saturação. Atualmente, estamos investigando o uso de provadores para o problema de Satisfatibilidade Booleana, ou SAT solvers, uma vez que já se mostraram capazes de resolver eficientemente problemas difíceis. Acreditamos poder utilizar as técnicas desenvolvidas depois de décadas de esforços práticos e teóricos direcionados a estes provadores. Nossa implementação, que é um trabalho em andamento, utiliza um SAT solver baseado em aprendizado de cláusulaatravés de análise de conflito. Damos como entrada a este solver, o conjunto satisfatível de cláusulas gerado pela transformação e, toda vez que um conflito é identificado, uma ou mais cláusulas são aprendidas pelo procedimento de análise de conflito. Acreditamos que, cuidadosamente escolhendo o conjunto de cláusulas e usando as cláusulas aprendidas geradas pelo solver, podemos reduzir o tempo que KSP gasta durante a saturação.
Horário: 15h
Palestrante: Felipe Rodopoulos de Oliveira (mestrando)
Título: Verificação do Protocolo de Autorização Dinâmica
Resumo: Questões em segurança compõem grande parte dos desafios das soluções de internet banking. Diferentes protocolos de segurança foram projetados visando prover confiabilidade para transações bancárias online. O Protocolo de Autorização Dinâmica é uma estratégia interessante, onde uma chave compartilhada entre o banco e o usuário é estabelecida para futuras mensagens. Para cada transação, o usuário é desafiado a recuperar e apresentar uma chave de transação única ao servidor, usando um smartphone como uma entidade externa de validação, escaneando um QR-code para testes de integridade. Dessa forma, o usuário consegue realizar operações em um computador inseguro e validá-las em um canal offline. Entretanto, o protocolo não é formalmente verificado. Neste trabalho, pretendemos realizar a especificação e verificação formal do protocolo, usando uma técnica de prova de teoremas bem estabelecida, o Método Indutivo. No fim, esperamos ter um dos dois resultados: um certificado formal de correção das crenças de segurança do protocolo ou um contra-exemplo válido para a falha do mesmo.
Horário: 15h30
Palestrante: Lucas Amaral (mestrando)
Título: Um cálculo baseado em resolução para E-conexões
Resumo: E-conexões são um método para combinar-se diferentes lógicas modais, sejam elas com características espaciais, temporais ou descritivas. Neste trabalho, apresentamos um cálculo baseado em resolução para a combinação de duas lógicas utilizando este método. Assumimos cálculos para as lógicas componentes, e utilizamos de "perguntas" a estas componentes para transferir conhecimento entre elas. Assim, não é necessário conhecimento dos estados de cada componente, e resolvemos o problema da satisfatibilidade focando apenas nas cláusulas que realizam as conexões.
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 em Informática 2018-1