Synthesizing nonanomalous event-based controllers for liveness goals

We present SGR(1), a novel synthesis technique and methodological guidelines for automatically constructing event-based behavior models. Our approach works for an expressive subset of liveness properties, distinguishes between controlled and monitored actions, and differentiates system goals from en...

Descripción completa

Guardado en:
Detalles Bibliográficos
Autor principal: Braberman, Víctor Adrián
Publicado: 2013
Materias:
Acceso en línea:https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_1049331X_v22_n1_p_DIppolito
http://hdl.handle.net/20.500.12110/paper_1049331X_v22_n1_p_DIppolito
Aporte de:
Descripción
Sumario:We present SGR(1), a novel synthesis technique and methodological guidelines for automatically constructing event-based behavior models. Our approach works for an expressive subset of liveness properties, distinguishes between controlled and monitored actions, and differentiates system goals from environment assumptions. We show that assumptions must be modeled carefully in order to avoid synthesizing anomalous behavior models. We characterize nonanomalous models and propose assumption compatibility, a sufficient condition, as a methodological guideline. © 2013 ACM.