Aplicações de Lógicas Modais a Teoria de Grafos e Sistemas Concorrentes
Autores
4747 |
1954,273
|
|
4940 |
1954,273
|
Informações:
Publicações do PESC
Neste trabalho, desenvolvemos novas aplicações de lógicas modais em duas áreas. Primeiramente, analisamos como descrever e verificar de maneira eficiente conectividade, aciclicidade e as propriedades hamiltoniana e euleriana utilizando lógicas modais. Para esta tarefa, utilizamos lógicas híbridas e lógicas modais graduadas. Ainda no estudo de propriedades de grafos, também determinamos uma condição necessária e suficiente para um grafo ser um produto cartesiano de grafos, obtendo um avanço em relação a um resultado anterior da literatura, que fornecia uma condição necessária, mas não suficiente. Além disto, utilizamos esta caracterização para obter axiomatizações corretas e completas para vários produtos de lógicas modais de dimensões arbitrárias. Este é um segundo avanço em relação a resultados anteriores da literatura, onde a maior parte dos sistemas axiomáticos corretos e completos apresentados se restringe a produtos de um par de lógicas modais.
Posteriormente, consideramos extensões da Lógica Dinâmica Proposicional (PDL) com operadores para a descrição de comportamentos concorrentes. Nosso objetivo é construir lógicas dinâmicas que sejam apropriadas para a descrição e verificação de propriedades de sistemas comunicantes concorrentes, de maneira análoga ao uso de PDL para o caso sequencial. Primeiramente, adicionamos a PDL o operador paralelo de CCS e, posteriormente, também adicionamos a possibilidade de passagem de nomes presente no Pi-Cálculo. Diferentemente de outras lógicas dinâmicas para sistemas concorrentes apresentadas anteriormente na literatura, nossas lógicas possuem semânticas de Kripke simples, axiomatizações completas e a propriedade do modelo finito.
In the present work, we develop new applications of modal logics in two areas. First, we analyze how to describe and efficiently verify connectivity, acyclicity and the Hamiltonian and Eulerian properties using modal logics. For this task, we use hybrid logics and graded modal logics. Still on the study of graph properties, we also determine a necessary and sufficient condition for a graph to be a cartesian product of graphs, improving on a previous result from the literature, that stated a necessary, but not sufficient, condition. Besides that, we use this characterization to build sound and complete axiomatic systems for many products of modal logics of arbitrary dimensions. This also improves previous results from the literature, where most of the sound and complete axiomatic systems that are presented are for products of a pair of modal logics.
In the second topic, we consider extensions of Propositional Dynamic Logic (PDL) with operators that describe concurrent behavior. Our goal is to build dynamic logics that are suitable for the description and verification of properties of communicating concurrent systems, in a similar way as PDL is used for the sequential case. First, we add to PDL the parallel operator from CCS and then we also add the possibility of name passing from the Pi-Calculus. Unlike previous dynamic logics for concurrency from the literature, our logics have simple Kripke semantics, complete axiomatizations and the finite model property.