Better Under-approximation of Programs by Hiding Variables
	  
  Abstraction frameworks use under-approximating transitions in order
  to prove existential properties of concrete systems.
  Under-approximating transitions refer to the concrete states that
  correspond to a particular abstract state in a universal manner.
  For example, there is a {\em must} transition from abstract state
  $a$ to abstract state $a'$ only if all the concrete states in $a$
  have successors in $a'$.
  
  The universal nature of under-approximating transitions makes them
  closed under transitivity. Consequently, reachability queries about
  the concrete system, which have applications in falsification and
  testing, can be answered by reasoning about its abstraction.  On the
  negative side, the universal nature of under-approximating
  transitions makes them dependent on all the variables of the program.
  The abstraction, on the other hand, often hides some of the
  variables.  Since the universal quantification in must transitions
  ranges over all variables, this often prevents the abstraction from
  associating a must transition with statements that refer to hidden
  variables. 
  
  We introduce and study {\em partitioned-must\/} transitions. The idea
  is to partition the program variables to relevant and irrelevant
  ones, and restrict the universal quantification inside must
  transitions to the relevant variables.   Usual must transitions are a
  special case of partitioned-must transitions in which all variables
  are relevant.  Partitioned-must transitions exist in many realistic
  settings in which usual must transitions do not exist. As we show,
  they retain the advantages of must transitions: they are closed
  under transitivity, their calculation can be automated, and the
  three-valued semantics induced by usual must transitions is refined
  to a multi-valued semantics that takes into an account the set of
  relevant variables.