Lista de Exercícios de Fund. de Validação de Sistemas (Pós-Graduação)

Prof. Edward Hermann Haeusler 99.1

1.

Qual a importância da existência de um processo de eliminação da regra do corte em um cálculo se sequentes para uma dada lógica ?

2.

Quais as dificuldades encontradas para o uso do método de resolução lógicas modais em geral.

3.

Pesquise na literatura um método de tableaux para a lógica intuicionista e comente uma possível adaptação do mesmo para um método de resolução.

4.

Escreva uma função que dada uma prova intuicionista em dedução natural de $\alpha$ a partir de um conjunto $\Delta$ retorne uma prova em cálculo de sequentes intuicionista de $\Delta\vdash\alpha$. Só pode existir uma função com esta finalidade ?

5.

Compare os diversos tipos de sistemas mostrados no curso sob o ponto de vista de legibilidade, complexidade computacional e adequabilidade como suporte a uma ferramenta de validação/verificação de Software.

6.

Do ponto de vista de prova automática de Teoremas, utilizando-se Cálculo de Sequentes, porque a lógica intuicionista merece maior atenção do que a clássica ?

7.

Para cada um dos esquemas modais abaixo, exiba um Frame que o torne válido e outro que não, demonstrando em cada caso. Considere [] como a necessidade e <> como a possibilidade.

• $A \rightarrow []A$
• $[] A \rightarrow <>A$
• $[]([]A \rightarrow A) \rightarrow []A$
• $[][]A \rightarrow A$
• $A \rightarrow []<>A$
• $[]([]A \wedge A \rightarrow B) \vee []([]B \wedge B\rightarrow A)$
• $<>[]A\rightarrow []<>A$

8.

Que estrutura temporal teriam os modelos de uma lógica com os seguintes axiomas. Considere $[Next]A = \bot[Until]A$

• $A \rightarrow [P]<F> A$
• $[F]A \rightarrow [F][F] A$
• $[P]A \rightarrow <F> A$
• $A \rightarrow [F]<P> A$
• $[P]A \rightarrow [P][P] A$
• $<P>\top$
• $<F>\top$
• $<P> A \rightarrow [Next]A \wedge [Next]\neg A$
• $[]([]A\rightarrow A)\rightarrow (<>[]A\rightarrow []A)$

9.

Qual a importância do método de filtragem para lógicas modais.

10.

Prove que a lógica S4.2 é determinada pela classe dos frames (fracamente) dirigidos, reflexivos e transitivos. Mostre que S4.2 é decidível.

11.

(opcional) Pesquise na literatura o resultado que mostra que o número de modalidades possíveis é finito e bem determinado.

12.

Qual a importância da propriedade do modelo finito. Cite , com demonstração, uma lógica que tem esta propriedade e uma que não a tem.

13.

CTL é uma lógica de tempo ramificado. Comente como seria um model-checker baseado em lógica de tempo linear. Este seria de interesse prático ?

14.

Especifique um dos problemas dados na última aula em SMV e algum outro model-checker. Valide-o e compare o processo como um todo (fase de especificação, fase de validação e reespecificação) nos dois casos, comparando. Escreva esta questão na forma de um uma seção de um artigo. O Objetivo é juntar todos os trabalhos, após revisão, em uma monografia do departamento. Se cada um escolher um model-checker diferente (além do SMV) o trabalho ficará mais rico.