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...
Guardado en:
Autor principal: | |
---|---|
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: |
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. |
---|