Logica modal aplicada a verificação de sistemas a eventos discretos
AUTOR(ES)
Christiano Pereira Pessanha
DATA DE PUBLICAÇÃO
2004
RESUMO
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
ASSUNTO(S)
logica matematica não-classica teoria dos sistemas dinamicos demonstração automatica de teoremas
ACESSO AO ARTIGO
http://libdigi.unicamp.br/document/?code=vtls000317427Documentos Relacionados
- Analise e sintese de sistemas a eventos discretos via logica modal
- Logica temporal de tempo real generalizada aplicada ao controle e simulação de sistemas dinamicos e eventos discretos
- Identificação de Sistemas a Eventos Discretos Maxplus lineares
- Sistemas de lógica modal em dedução natural
- Controle multivariavel de sistemas a eventos discretos em dioides
