Three-dimensional kinetic simulations of active suspensions: effect of chemotaxis and steric interaction

In this work, the effects of chemotaxis and steric interactions in active suspensions are analyzed by extending the kinetic model proposed by Saintillan and Shelley [1, 2]. In this model, a conservation equation for the active particle configuration is coupled to the Stokes equation for the flow arising from the force dipole exerted by the particles on the fluid. The fluid flow equations are solved spectrally and the conservation equation is solved by second-order finite differencing in space and second-order Adams-Bashforth time marching. First, the dynamics in suspensions of oxytactic run-and-tumble bacteria confined in thin liquid films surrounded by air is investigated. These bacteria modify their tumbling behavior by making temporal comparisons of the oxygen concentration, and, on average, swim towards high concentrations of oxygen. The kinetic model proposed by Saintillan and Shelley [1, 2] is modified to include run-and-tumble effects and oxygentaxis. The spatio-temporal dynamics of the oxygen and bacterial concentration are analyzed. For small film thicknesses, there is a weak migration of bacteria to the boundaries, and the oxygen concentration is high inside the film as a result of diffusion; both bacterial and oxygen concentrations quickly reach steady states. Above a critical film thickness (approximately 200 micron), a transition to chaotic dynamics is observed and is characterized by turbulent-like 3D motion, the formation of bacterial plumes, enhanced oxygen mixing and transport into the film, and hydrodynamic velocities of magnitudes up to 7 times the single bacterial swimming speed. The simulations demonstrate that the combined effects of hydrodynamic interactions and oxygentaxis create collective three-dimensional instabilities which enhances oxygen availability for the bacteria. Our simulation results are consistent with the experimental findings of Sokolov et al. [3], who also observed a similar transition with increasing film thickness. Next, the dynamics in concentrated suspensions of active self-propelled particles in a 3D periodic domain are analyzed. We modify the kinetic model of Saintillan and Shelley [1, 2] by including an additional nematic alignment torque proportional to the local concentration in the equation for the rotational velocity of the particles, causing them to align locally with their neighbors (Doi and Edwards [4]). Large-scale three- dimensional simulations show that, in the presence of such a torque both pusher and puller suspensions are unstable to random fluctuations and are characterized by highly nematic structures. Detailed measures are defined to quantify the degree and direction of alignment, and the effects of steric interactions on pattern formation will be presented. Our analysis shows that steric interactions have a destabilizing effect in active suspensions.

Formalizing operator task analysis

Human operators are unique in their decision making capability, judgment and nondeterminism. Their sense of judgment, unpredictable decision procedures, susceptibility to environmental elements can cause them to erroneously execute a given task description to operate a computer system. Usually, a computer system is protected against some erroneous human behaviors by having necessary safeguard mechanisms in place. But some erroneous human operator behaviors can lead to severe or even fatal consequences especially in safety critical systems. A generalized methodology that can allow modeling and analyzing the interactions between computer systems and human operators where the operators are allowed to deviate from their prescribed behaviors will provide a formal understanding of the robustness of a computer system against possible aberrant behaviors by its human operators. We provide several methodology for assisting in modeling and analyzing human behaviors exhibited while operating computer systems. Every human operator is usually given a specific recommended set of guidelines for operating a system. We first present process algebraic methodology for modeling and verifying recommended human task execution behavior. We present how one can perform runtime monitoring of a computer system being operated by a human operator for checking violation of temporal safety properties. We consider the concept of a protection envelope giving a wider class of behaviors than those strictly prescribed by a human task that can be tolerated by a system. We then provide a framework for determining whether a computer system can maintain its guarantees if the human operators operate within their protection envelopes. This framework also helps to determine the robustness of the computer system under weakening of the protection envelopes. In this regard, we present a tool called Tutela that assists in implementing the framework. We then examine the ability of a system to remain safe under broad classes of variations of the prescribed human task. We develop a framework for addressing two issues. The first issue is: given a human task specification and a protection envelope, will the protection envelope properties still hold under standard erroneous executions of that task by the human operators? In other words how robust is the protection envelope? The second issue is: in the absence of a protection envelope, can we approximate a protection envelope encompassing those standard erroneous human behaviors that can be safely endured by the system? We present an extension of Tutela that implements this framework. The two frameworks mentioned above use Concurrent Game Structures (CGS) as models for both computer systems and their human operators. However, there are some shortcomings of this formalism for our uses. We add incomplete information concepts in CGSs to achieve better modularity for the players. We introduce nondeterminism in both the transition system and strategies of players and in the modeling of human operators and computer systems. Nondeterministic action strategies for players in \emph{i}ncomplete information \emph{N}ondeterministic CGS (iNCGS) is a more precise formalism for modeling human behaviors exhibited while operating a computer system. We show how we can reason about a human behavior satisfying a guarantee by providing a semantics of Alternating Time Temporal Logic based on iNCGS player strategies. In a nutshell this dissertation provides formal methodology for modeling and analyzing system robustness against both expected and erroneous human operator behaviors.