4. Aktuelle tiltak
4.2 Tiltak for fredskriser og begrenset angrep
A Tabela 6.8 apresenta um resumo dos resultados da verificação de algumas proprie- dades, considerando as abordagens de modelagem apresentadas e também dois sistemas biológicos: as reações mostradas na Figura 3.9 e a bomba de sódio-potássio, modelada neste capítulo. Parâmetros para esses sistemas são variados, como volume e número de bombas. A seguir é apresentada uma breve descrição de cada um deles:
• Reacao1: modelo de reações químicas entre as moléculas A e B (ver Figura 3.9)
encontrado na Seção 3.3.3 do Capítulo 3;
• Reacao2: modelo de reações químicas entre as moléculas A e B (ver Figura 3.9)
em um volume de 10−18 litros. Os demais parâmetro considerados são [A]
inicial =
[B]inicial = 0, 5 mM , [AB]inicial = 0, r1 = 1011M−1s−1, r2 = 1 s−1, r3 = 0, 1 s−1.
O modelo PRISM baseado em níveis para esse sistema emprega um valor de h = 2, 5 × 10−5M , que equivale a 15 moléculas, dado o volume de 10−18 litros. O
estudo detalhado desse sistema pode ser encontrado na Seção 5.6 do Capítulo 5; • bomba1: modelo da Na,K-ATPase em um volume de 10−20 litros e considerando
apenas uma bomba. Os demais parâmetros podem ser vistos na Tabela 6.2 deste capítulo. O modelo PRISM baseado em níveis para esse sistema emprega um valor de h = 5 íons ou moléculas, dado o volume de 10−20 litros;
• bomba2: modelo da Na,K-ATPase em um volume de 10−12 litros e considerando
apenas uma bomba. Os demais parâmetros podem ser vistos na Tabela 6.2. O modelo PRISM baseado em níveis para esse sistema emprega um valor de h = 5 × 10−5M , que equivale a 6, 022 × 106 íons ou moléculas, dado o volume de
10−12 litros;
• bomba3: modelo da Na,K-ATPase em um volume de 10−20 litros e considerando
8 bombas. Os demais parâmetros podem ser vistos na Tabela 6.2.
A Tabela 6.8 fornece a sumarização dos resultados. O modelo que fornece um me- nor tempo de verificação, considerando um par constituído por um sistema biológico e uma propriedade de interesse, é destacado em negrito na tabela. Além disso, entradas com o símbolo- indicam que a propriedade de interesse não pôde ser verificada para o sistema biológico em questão com a abordagem de modelagem sendo considerada. Isso pode ocorrer, por exemplo, na verificação de propriedades sem intervalo de tempo em- pregando modelos BIOLAB ou quando o modelo PRISM baseado na química discreta é intratável.
Note que não existe uma abordagem de modelagem incondicionalmente melhor que a outra. Para cada uma delas, conforme já discutido, existem vantagens e des- vantagens. O modelo PRISM baseado na química discreta muitas vezes é intratável, não sendo possível, por exemplo, verificar propriedades para a Na,K-ATPase consi- derando um volume real (sistema bomba2 da tabela). Entretanto, pode ser a me-
lhor alternativa em certas situações, como para verificar a propriedade P≤0[ F ( (atp =
0) & !(′naInOver′) & !(′kOutOver′) ) ] no sistema bomba
3. Como o BIOLAB é uma al-
Tabela 6.8. Tabela com resumo dos resultados da verificação dos vários modelos para o sistema de reações mostrado na Figura 3.9 e para a bomba de sódio e potássio. A coluna Tempo da tabela para modelos PRISM apresenta a soma dos tempos de construção e verificação. Adicionalmente, os valores T e F na coluna de Resultado indicam, respectivamente, se a propriedade sendo verificada é verdadeira ou falsa.
Sistema
Propriedade M odelo T empo (s) Resultado
Biológico Reacao1 1 molécula P≥0,5 [ F≤1ab = 1 ] PRISM discreto 0,0010 T PRISM níveis - - BIOLAB 177,0120 T Reacao2 10−18l P≥0,5 [ F≤1ab ≥ 1 ] PRISM discreto - - PRISM níveis 1712,9080 T BIOLAB 47,4054 T P≥0,5 [ F ab ≥ 1 ] PRISM discreto 8,0340 T PRISM níveis 0,0390 T BIOLAB - - bomba1 10−20l
P≤0[ F ( (atp = 0) & PRISM discreto 48,53274 T
!(′naInOver′) & PRISM níveis 1,5810 T
!(′kOutOver′) ) ] BIOLAB - - P≤0,1[ F≤1 ′kOutOver′] PRISM discreto 92,1814 T PRISM níveis 14,2070 F BIOLAB 133,2400 T bomba2 10−12l
P≤0[ F ( (atp = 0) & PRISM discreto - -
!(′naInOver′) & PRISM níveis 648,9242 T
!(′kOutOver′) ) ] BIOLAB - - P≤0,1[ F≤1 ′kOutOver′] PRISM discreto - - PRISM níveis 852,7572 T BIOLAB 133,5336 T bomba3 10−20l 8 bombas
P≤0[ F ( (atp = 0) & PRISM discreto 284,7140 T
!(′naInOver′) & PRISM níveis - -
!(′kOutOver′) ) ] BIOLAB - -
P≤0,1[ F≤1 ′kOutOver′]
PRISM discreto 385.484,4660 T
PRISM níveis - -
BIOLAB 142,9634 T
no tempo, essa propriedade não pode ser verificada por ele, já que não envolve um in- tervalo de tempo que representa o tempo de simulação. Nesse caso, é preciso construir todo o espaço de estados alcançáveis do sistema, sendo o PRISM o algoritmo de ve- rificação apropriado. Adicionalmente, o modelo bomba3 modela um número específico
de bombas, sendo assim, pouco apropriado o uso da modelagem baseada em níveis. Além disso, a abstração introduzida por esse modelo pode acarretar no problema da imprecisão, discutido na Seção 5.5.1 do Capítulo 5, conforme pode ser visto na veri- ficação da propriedade P≤0,1[ F≤1 ′kOutOver′] para o sistema bomba1. Nesse caso, a
abstração, embora produza uma verificação mais rápida, acarreta em uma resposta in- correta. Finalmente, quando a propriedade de interesse envolve intervalos de tempo, a modelagem através do BIOLAB é geralmente indicada, embora, ainda sim, para alguns sistemas simples, o seu tempo de verificação seja superior aos das demais modelagens, como nos casos destacados na coluna Tempos da tabela, dado o seu custo fixo.
Assim, a escolha da modelagem mais adequada deve levar em conta o sistema sendo modelado e a propriedade que se deseja verificar.
Análise da Bomba de Sódio-Potássio
Esta seção mostra como a técnica de verificação de modelos pode ajudar na me- lhor compreensão da dinâmica da Na,K-ATPase. A ocorrência de certos eventos, como o esgotamento de substratos e a propriedade de reversibilidade da bomba, podem ser estudados através da técnica de maneira direta, enquanto que com as abordagens tradi- cionais de análise esses eventos podem não ser identificados. Também um entendimento da dinâmica da bomba em certas configurações em termos de tendências de reações é apresentado. Esse estudo permite compreender, por exemplo, porque a reversibili- dade da bomba necessita de longos tempos para ocorrer e, mais ainda, possibilita a identificação dos substratos e configurações da proteína da bomba que são os grandes responsáveis pelo lento funcionamento da mesma no seu sentido normal.
7.1 Modelo Empregado
As análises desta seção empregam o modelo baseado na química discreta da Na,K- ATPase construído na ferramenta PRISM, o qual foi apresentado na Seção 6.3 do capítulo anterior. Um dos motivos que levou a escolha desse modelo se deve ao fato de que algumas das propriedades a serem verificadas dizem respeito a eventos que per- sistem indefinidamente e que não são limitadas a um intervalo de tempo e, portanto, só podem ser tratadas por modelos construídos na ferramenta PRISM. Além disso, o modelo CTMC baseado na química discreta construído na ferramenta PRISM, apesar de ter a restrição de utilizar um volume reduzido, estratégia comum na modelagem de sistemas biológicos [Sauro et al., 2006], permite um estudo cujo comportamento mantém as proporções reais dos substratos ao longo do tempo. Vale ressaltar, entre- tanto, que o modelo CTMC baseado em níveis poderia ser similarmente empregado nos estudos realizados ao longo deste capítulo e o modelo BIOLAB poderia também ser empregrado para verificar algumas propriedades que consideram intervalos de tempo.
O volume celular empregado ao longo do capítulo é 10−20 litros. Evidentemente,
quanto maior o valor do volume mais acurado será o modelo. Entretanto, esse valor foi escolhido de maneira a não se obter tempos de verifição tão longos, o que permite ex- plorar os modelos através de um número maior de análises, embora mesmo com o valor escolhido a verificação de certas propriedades leve cerca de 17 horas. Adicionalmente, o estudo apresentado aqui considera apenas uma bomba, embora todas as definições sejam estensíveis para modelos que considerem quantidades superiores de bombas.