Algorithms for Context-Aided Variable Elimination
Inigo Incer and Albert Benveniste and Richard M. Murray and Alberto L. Sangiovanni-Vincentelli and Sanjit A. Seshia
EECS Department, University of California, Berkeley
Technical Report No. UCB/EECS-2023-15
January 28, 2023
http://www2.eecs.berkeley.edu/Pubs/TechRpts/2023/EECS-2023-15.pdf
Deriving system-level specifications from component specifications usually involves the elimination of variables that are not part of the interface of the top-level system. This paper presents algorithms for eliminating variables from formulas by computing refinements or abstractions of these formulas in a context. We discuss a connection between this problem and optimization and give efficient algorithms to compute refinements and abstractions of linear inequality constraints.
BibTeX citation:
@techreport{Incer:EECS-2023-15, Author= {Incer, Inigo and Benveniste, Albert and Murray, Richard M. and Sangiovanni-Vincentelli, Alberto L. and Seshia, Sanjit A.}, Title= {Algorithms for Context-Aided Variable Elimination}, Year= {2023}, Month= {Jan}, Url= {http://www2.eecs.berkeley.edu/Pubs/TechRpts/2023/EECS-2023-15.html}, Number= {UCB/EECS-2023-15}, Abstract= {Deriving system-level specifications from component specifications usually involves the elimination of variables that are not part of the interface of the top-level system. This paper presents algorithms for eliminating variables from formulas by computing refinements or abstractions of these formulas in a context. We discuss a connection between this problem and optimization and give efficient algorithms to compute refinements and abstractions of linear inequality constraints.}, }
EndNote citation:
%0 Report %A Incer, Inigo %A Benveniste, Albert %A Murray, Richard M. %A Sangiovanni-Vincentelli, Alberto L. %A Seshia, Sanjit A. %T Algorithms for Context-Aided Variable Elimination %I EECS Department, University of California, Berkeley %D 2023 %8 January 28 %@ UCB/EECS-2023-15 %U http://www2.eecs.berkeley.edu/Pubs/TechRpts/2023/EECS-2023-15.html %F Incer:EECS-2023-15