From boxes to worlds

In this paper we show an innovative way to represent graphic designs 01 systems and to verify design properties. The graphic designs are thought as models of an extended modal logic; and the methods used to verify properties are developed from techniques typical of classic modal logic, extended to c...

Descripción completa

Guardado en:
Detalles Bibliográficos
Autores principales: Hirsch, Dan Francisco, Areces, Carlos Eduardo
Formato: Objeto de conferencia
Lenguaje:Inglés
Publicado: 1995
Materias:
Acceso en línea:http://sedici.unlp.edu.ar/handle/10915/24296
Aporte de:
Descripción
Sumario:In this paper we show an innovative way to represent graphic designs 01 systems and to verify design properties. The graphic designs are thought as models of an extended modal logic; and the methods used to verify properties are developed from techniques typical of classic modal logic, extended to cover the differences in the underlying formalism. We present the procedures orlogical tools to derive the modal model associated to a given design, the filtration of models and the construction 01 modal descriptions. A higher level of abstraction is obtained in this way, and it lets us reason over designs in a strictly formal manner. The power of formal provability is also achieved. We use a working example to show how our tools help to veri1y properties 01 design like the detection of cycles (self loops).