8.3 Verification
119
in the following. That means, if headers are injected at most T maxP ath time steps
before the payload, they can still be in the microfluidic network when the payload
is injected (here, indirect effects where headers route other headers are ignored).
So these headers may have an impact on the payload’s path.
• The latest possible time for injecting headers is given by the time required to
execute the experiment (i.e., T path p ). Even if headers enter the microfluidic
network after the payload, they potentially may impact the payload’s path
(i.e., headers may “overtake” the payload by taking another path and then block
a channel). Therefore, the latest possible time a header can be injected and still
may have an impact on the payload’s path is given by the time required to execute
the experiment T path p .
Definition 8.2 Let T up be the maximal length (i.e., the upper bound) of a droplet
sequence, which is given by T up = T maxP ath + T path p .
This upper bound of the droplet sequence length guarantees that, if the microfluidic network allows to execute an experiment φ, a valid droplet sequence is within
this bound. Otherwise, if within this upper bound no droplet sequence can be
determined, it is verified that the given microfluidic network does not allow to
execute the experiment φ.
However, even with this upper bound a significant amount of sequences have to
be considered. More precisely, for an upper bound T up , there are T up − 1 possible
time steps, where either a header droplet can be injected or not (in the remaining
time step, the payload is injected)—resulting in 2 T up −1 possibilities. Even if many
of those can easily be excluded, still a huge (exponential) search space results.
Hence, this problem is not addressed by enumerating all possible droplet
sequences and validating whether they execute the given experiment. Instead, the
determination of a droplet sequence is transformed into a decision problem, i.e.
“Is there at least one valid droplet sequence for each experiment φ ∈ , which correctly
executes φ using a droplet sequence consisting of at most T up time steps?”
This decision problem is symbolically formulated as a Satisfiability Modulo Theories (SMT, [5]) instance. Corresponding SMT-solvers are also applied in the method
presented in the previous chapter as discussed in Sect. 7.3.
8.3.2 Symbolic Formulation
This section provides the details of the symbolic formulation, which initially
represents all (also invalid) droplet sequences and flows. Afterwards, constraints
are introduced which ensure a valid droplet flow, enforce the execution of the
experiment, and prevent the coalescence of droplets.
119
in the following. That means, if headers are injected at most T maxP ath time steps
before the payload, they can still be in the microfluidic network when the payload
is injected (here, indirect effects where headers route other headers are ignored).
So these headers may have an impact on the payload’s path.
• The latest possible time for injecting headers is given by the time required to
execute the experiment (i.e., T path p ). Even if headers enter the microfluidic
network after the payload, they potentially may impact the payload’s path
(i.e., headers may “overtake” the payload by taking another path and then block
a channel). Therefore, the latest possible time a header can be injected and still
may have an impact on the payload’s path is given by the time required to execute
the experiment T path p .
Definition 8.2 Let T up be the maximal length (i.e., the upper bound) of a droplet
sequence, which is given by T up = T maxP ath + T path p .
This upper bound of the droplet sequence length guarantees that, if the microfluidic network allows to execute an experiment φ, a valid droplet sequence is within
this bound. Otherwise, if within this upper bound no droplet sequence can be
determined, it is verified that the given microfluidic network does not allow to
execute the experiment φ.
However, even with this upper bound a significant amount of sequences have to
be considered. More precisely, for an upper bound T up , there are T up − 1 possible
time steps, where either a header droplet can be injected or not (in the remaining
time step, the payload is injected)—resulting in 2 T up −1 possibilities. Even if many
of those can easily be excluded, still a huge (exponential) search space results.
Hence, this problem is not addressed by enumerating all possible droplet
sequences and validating whether they execute the given experiment. Instead, the
determination of a droplet sequence is transformed into a decision problem, i.e.
“Is there at least one valid droplet sequence for each experiment φ ∈ , which correctly
executes φ using a droplet sequence consisting of at most T up time steps?”
This decision problem is symbolically formulated as a Satisfiability Modulo Theories (SMT, [5]) instance. Corresponding SMT-solvers are also applied in the method
presented in the previous chapter as discussed in Sect. 7.3.
8.3.2 Symbolic Formulation
This section provides the details of the symbolic formulation, which initially
represents all (also invalid) droplet sequences and flows. Afterwards, constraints
are introduced which ensure a valid droplet flow, enforce the execution of the
experiment, and prevent the coalescence of droplets.