Deciding Kleene Algebra Terms Equivalence in Coq

This paper presents a mechanically verified implementation of an algorithm for deciding the equivalence of Kleene algebra terms within the Coq proof assistant. The algorithm decides equivalence of two given regular expressions through an iterated process of testing the equivalence of their partial derivatives and does not require the construction of the corresponding automata. Recent theoretical and experimental research provides evidence that this method is, on average, more efficient than the classical methods based on automata. We present some performance tests, comparisons with similar approaches, and also introduce a generalization of the algorithm to decide the equivalence of terms of Kleene algebra with tests. The motivation for the work presented in this paper is that of using the libraries developed as trusted frameworks for carrying out certified program verification.

A exoneração do passivo restante: considerações sobre as causas de indeferimento liminar

Dissertação de Mestrado em Solicitadoria

Análise da sonolência na condução rodoviária a partir de sinais EEG

A Sociedade Europeia de Pesquisa do Sono realizou muito recentemente um estudo, onde mostrou que a prevalência média de adormecimento ao volante nos últimos 2 anos foi de 17%. Além disto, tem sido provado por todo o mundo que a sonolência durante a condução é uma das principais causas de acidentes de trânsito. Torna-se assim conveniente, o desenvolvimento de sistemas que analisem a suscetibilidade de um determinado condutor para adormecer no trânsito, bem como de ferramentas que monitorem em tempo real o estado físico e mental do condutor, para alertarem nos momentos críticos. Apesar do estudo do sono se ter iniciado há vários anos, a maioria das investigações focaram-se no ciclo normal do sono, estudando os indivíduos de forma relaxada e de olhos fechados. Só mais recentemente, têm surgido os estudos que se focam nas situações de sonolência em atividade, como _e o caso da condução. Uma grande parte Dos estudos da sonolência em condução têm utilizado a eletroencefalografia (EEG), de forma a perceber se existem alterações nas diferentes bandas de frequência desta, que possam indicar o estado de sonolência do condutor. Além disso, a evolução da sonolência a partir de alterações no piscar dos olhos (que podem ser vistas nos sinais EEG) também tem sido alvo de grande pesquisa, tendo vindo a revelar resultados bastante promissores. Neste contexto e em parceria com a empresa HealthyRoad, esta tese está integrada no projeto HealthyDrive, que visa o desenvolvimento de um sistema de alerta e deteção de sinais de fadiga e sonolência nos condutores de veículos automóveis. A contribuição desta tese no projeto prendeu-se com o estudo da sonolência dos indivíduos em condução a partir de sinais EEG, para desta forma investigar possíveis indicadores dos diferentes níveis desta que possam ser utilizados pela empresa no projeto. Foram recolhidos e analisados 17 sinais EEG de indivíduos em simulação de condução. Além disso foram desenvolvidos dois métodos de análise destes sinais: O primeiro para a deteção e análise dos piscar de olhos a partir de EEG, o segundo para análise do espetro de potência. Ambos os métodos foram utilizados para analisar os sinais recolhidos e investigar que tipo de relação existe entre a sonolência do condutor e as alterações nos piscares dos olhos, bem como as alterações do espetro do EEG. Os resultados mostraram uma correlação entre a duração do piscar de olhos e a sonolência do condutor. Com o aumento da sonolência velicou-se um aumento da duração do piscar, desencadeado principalmente pelo aumento na duração de fecho, que chegou aos 51.2%. Em relação ao espectro de potência, os resultados sugerem que a potência relativa de todas as bandas analisadas fornecem informações relevantes sobre a sonolência do condutor. Além disso, o parâmetro (_+_)/_ demostrou estar relacionado com variações da sonolência, diminuindo com o seu avanço e aumentando significativamente (111%) no instante em que os condutores adormeceram.