Sampling strategies for characterization of neuropeptides using mass spectrometry and functional implications into cell-cell signaling

In this dissertation, there are developed different analytical strategies to discover and characterize mammalian brain peptides using small amount of tissues. The magnocellular neurons of rat supraoptic nucleus in tissue and cell culture served as the main model to study neuropeptides, in addition to hippocampal neurons and mouse embryonic pituitaries. The neuropeptidomcis studies described here use different extraction methods on tissue or cell culture combined with mass spectrometry (MS) techniques, matrix-assisted laser desorption/ionization (MALDI) and electrospray ionization (ESI). These strategies lead to the identification of multiple peptides from the rat/mouse brain in tissue and cell cultures, including novel compounds One of the goals in this dissertation was to optimize sample preparations on samples isolated from well-defined brain regions for mass spectrometric analysis. Here, the neuropeptidomics study of the SON resulted in the identification of 85 peptides, including 20 unique peptides from known prohormones. This study includes mass spectrometric analysis even from individually isolated magnocellular neuroendocrine cells, where vasopressin and several other peptides are detected. At the same time, it was shown that the same approach could be applied to analyze peptides isolated from a similar hypothalamic region, the suprachiasmatic nucleus (SCN). Although there were some overlaps regarding the detection of the peptides in the two brain nuclei, different peptides were detected specific to each nucleus. Among other peptides, provasopressin fragments were specifically detected in the SON while angiotensin I, somatostatin-14, neurokinin B, galanin, and vasoactive-intestinal peptide (VIP) were detected in the SCN only. Lists of peptides were generated from both brain regions for comparison of the peptidome of SON and SCN nuclei. Moving from analysis of magnocellular neurons in tissue to cell culture, the direct peptidomics of the magnocellular and hippocampal neurons led to the detection of 10 peaks that were assigned to previously characterized peptides and 17 peaks that remain unassigned. Peptides from the vasopressin prohormone and secretogranin-2 are attributed to magnocellular neurons, whereas neurokinin A, peptide J, and neurokinin B are attributed to cultured hippocampal neurons. This approach enabled the elucidation of cell-specific prohormone processing and the discovery of cell-cell signaling peptides. The peptides with roles in the development of the pituitary were analyzed using transgenic mice. Hes1 KO is a genetically modified mouse that lives only e18.5 (embryonic days). Anterior pituitaries of Hes1 null mice exhibit hypoplasia due to increased cell death and reduced proliferation and in the intermediate lobe, the cells differentiate abnormally into somatotropes instead of melanotropes. These previous findings demonstrate that Hes1 has multiple roles in pituitary development, cell differentiation, and cell fate. AVP was detected in all samples. Interestingly, somatostatin [92-100] and provasopressin [151-168] were detected in the mutant but not in the wild type or heterozygous pituitaries while somatostatin-14 was detected only in the heterozygous pituitary. In addition, the putative peptide corresponding to m/z 1330.2 and POMC [205-222] are detected in the mutant and heterozygous pituitaries, but not in the wild type. These results indicate that Hes1 influences the processing of different prohormones having possible roles during development and opens new directions for further developmental studies. This research demonstrates the robust capabilities of MS, which ensures the unbiased direct analysis of peptides extracted from complex biological systems and allows addressing important questions to understand cell-cell signaling in the brain.

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.