Título: | EXTENDING PROPOSITIONAL DYNAMIC LOGIC FOR PETRI NETS | ||||||||||||||||||||||||||||||||||||||||
Autor: |
BRUNO LOPES VIEIRA |
||||||||||||||||||||||||||||||||||||||||
Colaborador(es): |
EDWARD HERMANN HAEUSLER - Orientador GILLES DOWEK - Coorientador |
||||||||||||||||||||||||||||||||||||||||
Catalogação: | 10/FEV/2015 | Língua(s): | ENGLISH - UNITED STATES |
||||||||||||||||||||||||||||||||||||||
Tipo: | TEXT | Subtipo: | THESIS | ||||||||||||||||||||||||||||||||||||||
Notas: |
[pt] Todos os dados constantes dos documentos são de inteira responsabilidade de seus autores. Os dados utilizados nas descrições dos documentos estão em conformidade com os sistemas da administração da PUC-Rio. [en] All data contained in the documents are the sole responsibility of the authors. The data used in the descriptions of the documents are in conformity with the systems of the administration of PUC-Rio. |
||||||||||||||||||||||||||||||||||||||||
Referência(s): |
[pt] https://www.maxwell.vrac.puc-rio.br/projetosEspeciais/ETDs/consultas/conteudo.php?strSecao=resultado&nrSeq=24052&idi=1 [en] https://www.maxwell.vrac.puc-rio.br/projetosEspeciais/ETDs/consultas/conteudo.php?strSecao=resultado&nrSeq=24052&idi=2 |
||||||||||||||||||||||||||||||||||||||||
DOI: | https://doi.org/10.17771/PUCRio.acad.24052 | ||||||||||||||||||||||||||||||||||||||||
Resumo: | |||||||||||||||||||||||||||||||||||||||||
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.
|
|||||||||||||||||||||||||||||||||||||||||
|