Caríssimos,
mais uma palestra no LoLITA, desta vez:
Lógica Dinâmica e Álgebras de Processo
Prof. Mario Benevides (COPPE-UFRJ)
Local: Sala de Reuniões do DIMAp
Data: Segunda 30/08/2010 às 10:00hs
Resumo: CSS (Calculus of Communication Systems) é uma linguagem algébrica de
especificação de comunicação e sincronização em sistemas concorrentes proposta
por Robin Milner. Ela trata da interação entre processos através de ações de
comunicação. Uma especificação em CCS é uma descrição do comportamento do
sistema em função dos eventos de comunicação que ocorrem.
Lógica Dinâmica Proposicional PDL tem um papel importante na especificação de
propriedades de programas. Várias propostas têm sido feitas de se ter uma
contrapartida lógica para CCS. As mais conhecidas são: Lógica de
Hennessy-Milner, a Lógica Dinâmica Concorrente CPDL e channel-CPDL de David
Peleg. A primeira é simplesmente uma lógica multi-modal com
uma modalidade para cada porta (ação) de comunicação. A segunda e a terceira
são lógicas dinâmicas proposicionais para programas regulares estendida com
um operador de sincronização. CPDL e channel-CPDL são bem próxima da Lógica de
Jogos e elas são bem apropriadas para representar propriedades de sistemas
concorrentes e jogos. A semântica de channel-CPDL é baseada em super-estados
(composição de estados) e super-processos e o problema de satisfabilidade nesta
lógica é indecidível ($\Pi_{1}^{1}$-hard). Ela também não tem uma axiomatização
completa.
Neste trabalho nós gostaríamos de investigar uma lógica dinâmica cujas ações
fossem programas CCS. Nossas fórmulas teriam a forma $[\pi] \varphi$, cujo
significado seria: após a execução do programa $\pi$, é sempre o caso que
$\varphi$ vale. Gostaríamos de ter nos programas CCS os operadores de prefixo,
composição paralela, escolha não-determinística, restrição e renomeação. Com
esta linguagem seríamos capazes raciocinar sobre especificações CCS tanto no
nível das ações como no de comunicações e sincronizações. Por outro lado,
devido ao mecanismo de comunicação simples de CCS temos fortes indícios de que
a lógica seria decidível.
$\pi$-Calculus é uma extensão do CCS para processos móveis \cite{milner99}. A
idéia é permitir que nomes de portas de comunicação possam ser passados como
dados e depois dinâmicamente serem usados para comunicação. Um extensão natural
deste trabalho é desenvolver uma Lógica Dinâmica cujos os programas são
programas (termos) do $\pi$-Calculus.
Atenciosamente,
Regivan
*********************************************************************************
Prof. Dr. Regivan Hugo Nunes Santiago
Group of Logic, Language, Information, Theory and Applications - LoLITA
Department of Informatics and Applied Mathematics - DIMAp
Federal University of Rio Grande do Norte - UFRN
Campus Universitario, Lagoa Nova, 59.072-970, Natal, RN, Brasil
Phone: +55 84 3215-3814 Ext. 228
Fax: +55 84 3215-3813
http://www.dimap.ufrn.br/~regivan
e-mail: regivan AT DOMAIN=dimap,ufrn,br.
*********************************************************************************
Em 25/08/2010, às 22:36, Regivan Santiago escreveu:
> Carissimos,
>
> mais um seminario do LoLITA, desta vez
>
> Sistemas Modais Intuicionistas - Uma abordagem semântica
> Profa. Maria da Paz (DFIL-UFRN)
> Local: Anfi-teatro A do CCET
> Dia: 27-Ago-10
> Horário: 09:00hs
>
> Resumo:
> Discussões acerca dos aspectos intuicionistas de lógicas modais começam a
> surgir especialmente com a publicação dos trabalhos de R. A. Bull na
> década de 60, século passado, cuja preocupação era apresentar uma
> formalização de um conceito intuicionista de modalidade. Essas idéias
> iniciais,
> entretanto, estavam longe de uma aceitação consensual quanto à base dedutiva
> do que deve ser um sistema lógico modal intuicionista. No campo
> semântico a situação não é diferente, também não está estabelecido que
> conexão deva haver entre a relação de ordem dos modelos intuicionistas
> e a relação de acessibilidade dos modelos modais. Analisaremos, a partir da
> diversidade de sistemas surgidos na literatura, que modelos caracetizam
> adequadamente um sistema modal como intuicionista.
>
> Para informações atualizadas visite:
>
>> http://groups.google.com.br/group/lolita-ufrn/web/seminrios-do-lolita?msg=ns
>
>
> Atenciosamente,
> Regivan
> *********************************************************************************
> Prof. Dr. Regivan Hugo Nunes Santiago
> Group of Logic, Language, Information, Theory and Applications - LoLITA
> Department of Informatics and Applied Mathematics - DIMAp
> Federal University of Rio Grande do Norte - UFRN
> Campus Universitario, Lagoa Nova, 59.072-970, Natal, RN, Brasil
> Phone: +55 84 3215-3814 Ext. 228
> Fax: +55 84 3215-3813
> http://www.dimap.ufrn.br/~regivan
> e-mail: regivan AT DOMAIN=dimap,ufrn,br.
> *********************************************************************************
>
_______________________________________________
Logica-l mailing list
[email protected]
http://www.dimap.ufrn.br/cgi-bin/mailman/listinfo/logica-l
