100
8 Generating Droplet Sequences
by this, the position of each droplet at each time. But therefore, the equation systems
have to be constantly re-evaluated in order to guarantee a correct determination of
the droplet behavior (which is performed by the simulator described in Sect. 3.3).
Obviously, the resulting complexity makes it infeasible to use the 1D analysis model
for automatic methods for generating droplet sequences.
Hence, this chapter proposes an abstraction of the flow behavior in the form of a
discrete model (based on [43]). This discrete model allows for a consideration of the
droplet flow on a more abstract level and enables designers and design automation
tools to intuitively and efficiently determine the droplets’ paths and positions during
the execution of an experiment. This discrete model is presented in Sect. 8.1.
Based on this discrete model, the droplet sequence can now be formulated as
a combinatorial problem and, hence, allows for automatic methods for generating
droplet sequences. A corresponding automatic method (based on [50]) for the
generation of droplet sequences realizing the desired experiments is described in
Sect. 8.2. To this end, a two-step approach is proposed: First, a droplet sequence
is generated on the discrete model. Afterwards, the obtained droplet sequence
is validated using simulations on the 1D analysis model as described in Chap. 3
and [52]. This validation guarantees that all interdependencies between droplets are
considered and, hence, confirms the suitability of the obtained results.
The resulting automatic method does not consider all droplet sequences possible
on the discrete model but only promising candidates. Therefore, this method cannot
guarantee to determine a droplet sequence. Furthermore, it is not guaranteed that
such a droplet sequence even exists which would correctly realize the desired
experiment on the given microfluidic network. In order to check this, Sect. 8.3
proposes an automatic verification method (based on [44]), which verifies whether
there exists a droplet sequence for each desired experiment. To this end, all possible
droplet sequences and, hence, routings are symbolically considered. Afterwards, an
SMT-solver is applied to prove the existence or non-existence of a droplet sequence
on the discrete model realizing an experiment on the given microfluidic network.
The remainder of this chapter is structured as follows: Sect. 8.1 defines the
discrete model and how it abstracts the flow of droplets. Afterwards, Sect. 8.2
proposes a method which considers promising candidates of droplet sequences
and additionally validates the resulting droplet sequences. Section 8.3 proposes a
verification method, which allows to check whether there exists for each experiment
a droplet sequence, which would correctly execute the respective experiment at least
on the discrete model. Finally, this chapter is concluded in Sect. 8.4.
8.1 Discrete Model
In this section, a discrete model for the flow of droplets is proposed which allows
to determine the droplets’ paths and positions in a discrete fashion. At the same
time, it avoids the constant re-evaluations necessary in the 1D analysis model
described in Sect. 3.2. Therefore, first, the proposed model is defined (Sect. 8.1.1)
8 Generating Droplet Sequences
by this, the position of each droplet at each time. But therefore, the equation systems
have to be constantly re-evaluated in order to guarantee a correct determination of
the droplet behavior (which is performed by the simulator described in Sect. 3.3).
Obviously, the resulting complexity makes it infeasible to use the 1D analysis model
for automatic methods for generating droplet sequences.
Hence, this chapter proposes an abstraction of the flow behavior in the form of a
discrete model (based on [43]). This discrete model allows for a consideration of the
droplet flow on a more abstract level and enables designers and design automation
tools to intuitively and efficiently determine the droplets’ paths and positions during
the execution of an experiment. This discrete model is presented in Sect. 8.1.
Based on this discrete model, the droplet sequence can now be formulated as
a combinatorial problem and, hence, allows for automatic methods for generating
droplet sequences. A corresponding automatic method (based on [50]) for the
generation of droplet sequences realizing the desired experiments is described in
Sect. 8.2. To this end, a two-step approach is proposed: First, a droplet sequence
is generated on the discrete model. Afterwards, the obtained droplet sequence
is validated using simulations on the 1D analysis model as described in Chap. 3
and [52]. This validation guarantees that all interdependencies between droplets are
considered and, hence, confirms the suitability of the obtained results.
The resulting automatic method does not consider all droplet sequences possible
on the discrete model but only promising candidates. Therefore, this method cannot
guarantee to determine a droplet sequence. Furthermore, it is not guaranteed that
such a droplet sequence even exists which would correctly realize the desired
experiment on the given microfluidic network. In order to check this, Sect. 8.3
proposes an automatic verification method (based on [44]), which verifies whether
there exists a droplet sequence for each desired experiment. To this end, all possible
droplet sequences and, hence, routings are symbolically considered. Afterwards, an
SMT-solver is applied to prove the existence or non-existence of a droplet sequence
on the discrete model realizing an experiment on the given microfluidic network.
The remainder of this chapter is structured as follows: Sect. 8.1 defines the
discrete model and how it abstracts the flow of droplets. Afterwards, Sect. 8.2
proposes a method which considers promising candidates of droplet sequences
and additionally validates the resulting droplet sequences. Section 8.3 proposes a
verification method, which allows to check whether there exists for each experiment
a droplet sequence, which would correctly execute the respective experiment at least
on the discrete model. Finally, this chapter is concluded in Sect. 8.4.
8.1 Discrete Model
In this section, a discrete model for the flow of droplets is proposed which allows
to determine the droplets’ paths and positions in a discrete fashion. At the same
time, it avoids the constant re-evaluations necessary in the 1D analysis model
described in Sect. 3.2. Therefore, first, the proposed model is defined (Sect. 8.1.1)