000085675 001__ 85675
000085675 005__ 20180317093432.0
000085675 037__ $$aREP_WORK
000085675 245__ $$aThree Algorithms for Interface Synthesis: A Comparative Study
000085675 269__ $$a2006
000085675 260__ $$c2006
000085675 336__ $$aReports
000085675 520__ $$aA temporal interface for a system component is a finite automaton that specifies the legal sequences of input events.  We evaluate and compare three different algorithms for automatically extracting the temporal interface from the transition graph of a component: (1) a game algorithm that computes the interface as a representation of the most general environment strategy to avoid a safety violation; (2) a learning algorithm that repeatedly queries the component to construct the minimal interface automaton; and (3) a CEGAR algorithm that iteratively refines an abstract interface hypothesis by adding relevant state information from the component.  Since algorithms (2) and (3) have been published in different software contexts, for comparison purposes, we present the three algorithms in a uniform finite-state setting.  We furthermore extend the three algorithms to construct maximally permissive interface automata, which accept all legal input sequences.  While the three algorithms have similar worst-case complexities, their actual running times differ greatly depending on the component whose interface is computed.  On the theoretical side, we provide families of components that exhibit exponential differences in the performance of the three algorithms. On the practical side, we evaluate the three algorithms experimentally on a variety of real world examples.  Not surprisingly, the experimental evaluation confirms the theoretical expectation: learning performs best if the minimal interface automaton is small; CEGAR performs best if only few component variables are needed to prove an interface hypothesis safe and permissive; and the direct (game) algorithm outperforms both approaches if neither is the case.
000085675 6531_ $$aCounterexample guided abstraction refinement
000085675 6531_ $$aLearning
000085675 6531_ $$aInterfaces
000085675 6531_ $$aSynthesis
000085675 6531_ $$aNCCR-MICS
000085675 6531_ $$aNCCR-MICS/CL2
000085675 700__ $$aBeyer, Dirk
000085675 700__ $$0243550$$aHenzinger, Thomas A.$$g162366
000085675 700__ $$aSingh, Vasu
000085675 8564_ $$s359814$$uhttps://infoscience.epfl.ch/record/85675/files/Three_Algorithms_for_Interface_Synthesis_A_Comparative_Study.pdf$$zn/a
000085675 909CO $$ooai:infoscience.tind.io:85675$$preport
000085675 909C0 $$0252230$$pMTC$$xU10969
000085675 937__ $$aMTC-REPORT-2006-001
000085675 973__ $$aEPFL$$sPUBLISHED
000085675 980__ $$aREPORT