The paper addresses the problem of designing a component that combined with a known part of a system, called the context FSM, is a reduction of a given specification FSM. We study compositionally progressive solutions of synchronous FSM equations. Such solutions, when combined with the context, do not block any input that may occur in the specification, so they are of practical use. We show that if a synchronous FSM equation has a compositionally progressive solution, then the equation has a largest compositionally progressive solution. We provide two different algorithms to compute a largest compositionally progressive solution: one deletes all compositionally non-progressive strings from a largest solution, the other splits states of a largest solution and then removes those inducing a non-progressive composition.
Compositionally progressive solutions of synchronous FSM equations
VILLA, Tiziano;
2008-01-01
Abstract
The paper addresses the problem of designing a component that combined with a known part of a system, called the context FSM, is a reduction of a given specification FSM. We study compositionally progressive solutions of synchronous FSM equations. Such solutions, when combined with the context, do not block any input that may occur in the specification, so they are of practical use. We show that if a synchronous FSM equation has a compositionally progressive solution, then the equation has a largest compositionally progressive solution. We provide two different algorithms to compute a largest compositionally progressive solution: one deletes all compositionally non-progressive strings from a largest solution, the other splits states of a largest solution and then removes those inducing a non-progressive composition.
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
