118
8 Generating Droplet Sequences
flows into channel c 11 in time step t = 11 as its hydraulic resistance is smaller
than those of c 12 . When the payload arrives at the second bifurcation in time
step t = 12, the header is already in channel c 13 . Hence, the hydraulic resistance
of channel c 11 is, again, less than those of channel c 12 . This causes the payload
to flow into channel c 11 and, finally, into module m 4 . However, the requested
experiment (m 2 , m 3 ) does not contain module m 4 . Therefore, this droplet sequence
is invalid as well.
As illustrated by the example above, determining a droplet sequence, which
correctly executes the given experiment φ = (m 2 , m 3 ), is a nontrivial task.
This motivates the question whether there exists a valid droplet sequence for this
experiment. Actually, for the given microfluidic network no droplet sequence exists,
which would realize the experiment φ = (m 2 , m 3 ). This motivates the following
problem statement:
Given is the microfluidic network (i.e. its architecture and the specification of the discrete
model) as well as the experiments .
Wanted is a verification whether all experiments can be realized on the given microfluidic
network, i.e. whether for each experiment φ ∈ a droplet sequence can be determined on
the discrete model, which routes the payload droplet through all modules defined in φ.
Next, the proposed automatic method to the problem motivated here is described.
Therefore, the following sections describe the verification strategy and its symbolic
formulation.
8.3.1 Verification Strategy
In order to verify whether a microfluidic network allows to execute an experiment,
all possible droplet sequences have to be considered. To this end, it is important to
know the maximum length of the droplet sequences to be considered (as this defines
the search space). In fact, the given microfluidic network bounds the maximum
length of a droplet sequence to a finite number as follows:
The time a payload p needs to execute an experiment is specified by the required
modules and channels it flows through—denoted as T path p . Only header droplets,
which are in the microfluidic network during the execution of an experiment, can
have an impact on the payload’s path (i.e., on the taken channels). Therefore, it can
be derived how many time steps headers can be injected before or after the payload
and still may have an impact on the payload’s path. Then, the time span between
the earliest and the latest possible time defines the maximal length of the droplet
sequence. This earliest and latest possible time is given as follows:
• The earliest possible time for injecting headers is given by the longest path
through the microfluidic network. This longest path is defined as the entities
(modules and channels) with the largest sum of time steps—denoted as T maxP ath
8 Generating Droplet Sequences
flows into channel c 11 in time step t = 11 as its hydraulic resistance is smaller
than those of c 12 . When the payload arrives at the second bifurcation in time
step t = 12, the header is already in channel c 13 . Hence, the hydraulic resistance
of channel c 11 is, again, less than those of channel c 12 . This causes the payload
to flow into channel c 11 and, finally, into module m 4 . However, the requested
experiment (m 2 , m 3 ) does not contain module m 4 . Therefore, this droplet sequence
is invalid as well.
As illustrated by the example above, determining a droplet sequence, which
correctly executes the given experiment φ = (m 2 , m 3 ), is a nontrivial task.
This motivates the question whether there exists a valid droplet sequence for this
experiment. Actually, for the given microfluidic network no droplet sequence exists,
which would realize the experiment φ = (m 2 , m 3 ). This motivates the following
problem statement:
Given is the microfluidic network (i.e. its architecture and the specification of the discrete
model) as well as the experiments .
Wanted is a verification whether all experiments can be realized on the given microfluidic
network, i.e. whether for each experiment φ ∈ a droplet sequence can be determined on
the discrete model, which routes the payload droplet through all modules defined in φ.
Next, the proposed automatic method to the problem motivated here is described.
Therefore, the following sections describe the verification strategy and its symbolic
formulation.
8.3.1 Verification Strategy
In order to verify whether a microfluidic network allows to execute an experiment,
all possible droplet sequences have to be considered. To this end, it is important to
know the maximum length of the droplet sequences to be considered (as this defines
the search space). In fact, the given microfluidic network bounds the maximum
length of a droplet sequence to a finite number as follows:
The time a payload p needs to execute an experiment is specified by the required
modules and channels it flows through—denoted as T path p . Only header droplets,
which are in the microfluidic network during the execution of an experiment, can
have an impact on the payload’s path (i.e., on the taken channels). Therefore, it can
be derived how many time steps headers can be injected before or after the payload
and still may have an impact on the payload’s path. Then, the time span between
the earliest and the latest possible time defines the maximal length of the droplet
sequence. This earliest and latest possible time is given as follows:
• The earliest possible time for injecting headers is given by the longest path
through the microfluidic network. This longest path is defined as the entities
(modules and channels) with the largest sum of time steps—denoted as T maxP ath