Título
[en] EXTENDING PROPOSITIONAL DYNAMIC LOGIC FOR PETRI NETS
Título
[pt] EXTENSÕES DE LÓGICA PROPOSICIONAL DINÂMICA PARA REDES DE PETRI
Autor
[pt] BRUNO LOPES VIEIRA
Vocabulário
[pt] LOGICA
Vocabulário
[pt] REDES DE PETRI ESTOCATISCAS
Vocabulário
[pt] LOGICA DINAMICA
Vocabulário
[pt] LOGICA MODAL
Vocabulário
[pt] REDES DE PETRI
Vocabulário
[en] LOGIC
Vocabulário
[en] STOCHASTIC PETRI NETS
Vocabulário
[en] DYNAMIC LOGIC
Vocabulário
[en] LOGIC MODAL
Vocabulário
[en] PETRI NETS
Resumo
[pt] Lógica Proposicional Dinâmica (PDL) é um sistema lógico multi-modal utilizada para especificar e verificar propriedades em programas sequenciais. Redes de Petri são um formalismo largamente utilizado na especificação de sistemas concorrentes e possuem uma interpretação gráfica bastante intuitiva. Neste trabalho apresentam-se extensões da Lógica Proposicional Dinâmica onde os programas são substituídos por Redes de Petri. Define-se uma codificação composicional para as Redes de Petri através de redes básicas, apresentando uma semântica composicional. Uma axiomatização é definida para a qual o sistema é provado ser correto, e completo em relação à semântica proposta. Três Lógicas Dinâmicas são apresentadas: uma para efetuar inferências sobre Redes de Petri Marcadas ordinárias e duas para inferências sobre Redes de Petri Estocásticas marcadas, possibilitando a modelagem de cenários mais complexos. Alguns sistemas dedutivos para essas lógicas são apresentados. A principal vantagem desta abordagem concerne em possibilitar efetuar inferências sobre Redes de Petri [Estocásticas] marcadas sem a necessidade de traduzí-las a outros formalismos.
Resumo
[en] Propositional Dynamic Logic (PDL) is a multi-modal logic used for specifying and reasoning on sequential programs. Petri Net is a widely used formalism to specify and to analyze concurrent programs with a very intuitive graphical representation. In this work, we propose some extensions of Propositional Dynamic Logic for reasoning about Petri Nets. We define a compositional encoding of Petri Nets from basic nets as terms. Second, we use these terms as PDL programs and provide a compositional semantics to PDL Formulas. Then we present an axiomatization and prove completeness regarding our semantics. Three versions of Dynamic Logics to reasoning with Petri Nets are presented: one of them for ordinary Marked Petri Nets and two for Marked Stochastic Petri Nets yielding to the possibility of model more complex scenarios. Some deductive systems are presented. The main advantage of our approach is that we can reason about [Stochastic] Petri Nets using our Dynamic Logic and we do not need to translate it into other formalisms. Moreover our approach is compositional allowing for construction of complex nets using basic ones.
Orientador(es)
EDWARD HERMANN HAEUSLER
Coorientador(es)
GILLES DOWEK
Banca
EDWARD HERMANN HAEUSLER
Banca
LUIZ CARLOS PINHEIRO DIAS PEREIRA
Banca
GEIZA MARIA HAMAZAKI DA SILVA
Banca
GILLES DOWEK
Banca
CLAUDIA NALON
Banca
JORGE PETRUCIO VIANA
Catalogação
2015-02-10
Apresentação
2014-03-28
Tipo
[pt] TEXTO
Formato
application/pdf
Formato
application/pdf
Formato
application/pdf
Formato
application/pdf
Formato
application/pdf
Formato
application/pdf
Formato
application/pdf
Formato
application/pdf
Idioma(s)
INGLÊS
Referência [pt]
https://www.maxwell.vrac.puc-rio.br/colecao.php?strSecao=resultado&nrSeq=24052@1
Referência [en]
https://www.maxwell.vrac.puc-rio.br/colecao.php?strSecao=resultado&nrSeq=24052@2
Referência DOI
https://doi.org/10.17771/PUCRio.acad.24052
Arquivos do conteúdo
CAPA, AGRADECIMENTOS, ABSTRACT, RESUMO, SUMÁRIO E LISTA DE FIGURAS PDF CAPÍTULO 1 PDF CAPÍTULO 2 PDF CAPÍTULO 3 PDF CAPÍTULO 4 PDF CAPÍTULO 5 PDF CAPÍTULO 6 PDF REFERÊNCIAS BIBLIOGRÁFICAS PDF