Please use this identifier to cite or link to this item: http://repositorio.unicamp.br/jspui/handle/REPOSIP/260168
Type: DISSERTAÇÃO
Degree Level: Mestrado
Title: Logica modal aplicada a verificação de sistemas a eventos discretos
Author: Pessanha, Christiano Pereira
Advisor: Mendes, Rafael Santos, 1957-
Abstract: Resumo: Este trabalho objetiva o estudo da verificação de especificações em sistemas dinâmicos a eventos mscretos via lógica modal.Um grafo de eventos temporizado (ou GET) é utilizado para modelar o sistema dinâmicoque se deseja analisar. Asrelações entre as transições do GET e a especificaçãoque se deseja verificar são expressasatravés de fórmulas da lógica modal NK. Um tableau analítico é utilizado para verificar se a especificaçãoé conseqüência lógica do conjuntode fórmulas que representaa rede. Os ramos abertos retomados pelo tableau estão associados a modelos que falseiam a especificação.Introduz..seo conceitode terminaçãode um ramo e prova-seque a solução retomada por um ramo terminado está associada às caracteristicas de minimalidade, causalidade,unicidadee impulsividade.Com base nesses teoremas propoo-seum algoritmo para o tableau. Descreve-se a implementaçãocomputacionaldo algoritmo.Exemplos de sua utilizaçãosão apresentados

Abstract: This works is a study on the verification of specification in discrete event dynamicsystemsthroughthe use of modallogic. TimedEvent Graphs(TEG)describedby its eqmtions in dioids are used to model the systemwhose propertiesshouldbe verified. NK modallogic formulasexpressthe dynamicsof the systemas well as the specificationto be verified. An Analytic Tableau is used to verify if the formula correspondingto the specificationis a logica1consequenceof the formulasdescribingthe system.The tableau will retum open branchesassociatedto modelsthat falsifythe specification.The conceptof branch termination is introduced and proved to be associatedto featores as minimality, causality,unicity and impulsivity. A new algorithm, based on these conceptsis proposed and its computational implementation is described. Examples are presented.
Subject: Teoria dos sistemas dinâmicos
Lógica matemática não-clássica
Demonstração automática de teoremas
Language: Português
Editor: [s.n.]
Date Issue: 2004
Appears in Collections:FEEC - Tese e Dissertação

Files in This Item:
File SizeFormat 
Pessanha_ChristianoPereira_M.pdf4.3 MBAdobe PDFView/Open


Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.