Analise e sintese de sistemas a eventos discretos via logica modal

AUTOR(ES)
DATA DE PUBLICAÇÃO

1998

RESUMO

The problem of verification of a specification and controller synthesis in a class of discrete event dynamic systems is addressed. We propose a new propositional modallogic, named NK logic, and we show that a set of formulas of this logic is completely equivalent to a set of equations written in the context of the theory of dioids. Therefore, a system described by an event graph can be modeled by a set of formulas in NK logic. Then we use the technique of the analytic tableaux to develop an algorithm to decide if a specification, also expressed in NK logic, is satisfied. If a specification is not satisfied then there exists a solution for the equations written in dioid context that violates the specification. The method of analytic tableaux gives this solution. Conceming the synthesis problem, the solution obtained by the analytic tableau is used to determine the NK-formulas, and therefore the controller, that makes the specification be verified. The main advantage of this approach is allow us to use the technique of analytic tableaux to investigate problems of analysis and synthesis of controllers for discrete event systems

ASSUNTO(S)

redes de petri logica matematica não-classica algoritmos

ACESSO AO ARTIGO

Documentos Relacionados