Modelagem e análise de sistemas de transporte de íons em membranas celulares usando verificação de modelos

AUTOR(ES)
FONTE

IBICT - Instituto Brasileiro de Informação em Ciência e Tecnologia

DATA DE PUBLICAÇÃO

27/07/2011

RESUMO

Recentemente há um interesse crescente na aplicação da Verificação Probabilística de Modelos (PMC) na especificação formal e análise de sistemas biológicos. PMC é uma técnica que permite uma exploração exaustiva do conjunto de estados de um sistema estocástico e pode fornecer visões valiosas do seu comportamento que são mais difíceis de se obter usando somente abordagens tradicionais de análise de sistemas, como as simulações estocástica e determinística. Neste trabalho, propõe-se o uso de PMC para modelar e analisar sistemas em membranas celulares responsáveis pelo transporte de íons e cruciais para a vida das células. Uma especificação formal e quantitativa da bomba de sódio e potássio (Na,K-ATPase) é inicialmente apresentada. Essa bomba é um importante sistema de transporte de íons presente em todas células animais e responsável por manter as concentrações dos íons de sódio e potássio dentro da célula, respectivamente, alta e baixa. O trabalho descreve como modelar o mecanismo da bomba usando PMC, considerando diferentes técnicas de modelagem com o objetivo de lidar com o problema da explosão de estados, inerente da técnica de verificação de modelos, independente do contexto. Importantes propriedades relacionadas à reversibilidade da bomba são verificadas usando PMC. Adicionalmente, o comportamento da bomba é investigado em termos de tendências de reações que computam se existe uma probabilidade superior de certas reações ocorrerem. Essas tendências permitem identificar os gargalos que levam ao lento funcionamento ou mesmo à interrupção da bomba com o passar do tempo. O trabalho também introduz uma abordagem para detectar comportamento periódico com ruídos em sistemas estocásticos usando uma técnica de verificação de modelos estatística. A abordagem proposta é aplicada para um sistema de oscilação intracelular de cálcio, comumentemente encontrado em um grande número de tipos celulares em resposta à estímulos de componentes químicos extracelulares. Finalmente, uma metodologia para lidar com a coexistência de espécies com grandes diferenças em suas concentrações é também introduzida. Os resultados são ainda preliminares, mas indicam os ganhos em escalabilidade de recursos de memória com a abordagem proposta.

ASSUNTO(S)

software verificação teses. métodos estatísticos teses. bioinformática teses. redes biológicas teses. computaçãoteses.

ACESSO AO ARTIGO

Documentos Relacionados