@article{3808,
  abstract     = {Action potentials in central neurons are initiated near the axon initial segment, propagate into the axon, and finally invade the presynaptic terminals, where they trigger transmitter release. Voltage-gated Na(+) channels are key determinants of excitability, but Na(+) channel density and properties in axons and presynaptic terminals of cortical neurons have not been examined yet. In hippocampal mossy fiber boutons, which emerge from parent axons en passant, Na(+) channels are very abundant, with an estimated number of approximately 2000 channels per bouton. Presynaptic Na(+) channels show faster inactivation kinetics than somatic channels, suggesting differences between subcellular compartments of the same cell. Computational analysis of action potential propagation in axon-multibouton structures reveals that Na(+) channels in boutons preferentially amplify the presynaptic action potential and enhance Ca(2+) inflow, whereas Na(+) channels in axons control the reliability and speed of propagation. Thus, presynaptic and axonal Na(+) channels contribute differentially to mossy fiber synaptic transmission.},
  author       = {Engel, Dominique and Peter Jonas},
  journal      = {Neuron},
  number       = {3},
  pages        = {405 -- 17},
  publisher    = {Elsevier},
  title        = {{Presynaptic action potential amplification by voltage-gated Na+ channels in hippocampal mossy fiber boutons}},
  doi          = {10.1016/j.neuron.2004.12.048 },
  volume       = {45},
  year         = {2005},
}

@misc{3142,
  abstract     = {Assembly of neuronal circuits is controlled by the sequential acquisition of neuronal subpopulation-specific identities at progressive developmental steps. Whereas neuronal features involved in initial phases of differentiation are already established at cell-cycle exit, recent findings, based mainly on work in the peripheral nervous system, suggest that the timely integration of signals encountered en route to targets and from the target region itself is essential to control late steps in connectivity. As neurons project towards their targets they require target-derived signals to establish mature axonal projections and acquire neuronal traits such as the expression of distinct combinations of neurotransmitters. Recent evidence presented in this review shows that this principle, of a signaling interplay between target-derived signals and neuronal cell bodies, is often mediated through transcriptional events and is evolutionarily conserved.},
  author       = {Simon Hippenmeyer and Kramer, Ina and Arber, Silvia},
  booktitle    = {Trends in Neurosciences},
  number       = {8},
  pages        = {482 -- 488},
  publisher    = {Elsevier},
  title        = {{Control of neuronal phenotype: What targets tell the cell bodies}},
  doi          = {10.1016/j.tins.2004.05.012},
  volume       = {27},
  year         = {2004},
}

@inproceedings{3894,
  abstract     = {We study infinite stochastic games played by n-players on a finite graph with goals given by sets of infinite traces. The games are stochastic (each player simultaneously and independently chooses an action at each round, and the next state is determined by a probability distribution depending on the current state and the chosen actions), infinite (the game continues for an infinite number of rounds), nonzero sum (the players' goals are not necessarily conflicting), and undiscounted. We show that if each player has a reachability objective, that is, if the goal for each player i is to visit some subset R-i of the states, then there exists an epsilon-Nash equilibrium in memoryless strategies, for every epsilon > 0. However, exact Nash equilibria need not exist. We study the complexity of finding such Nash equilibria, and show that the payoff of some epsilon-Nash equilibrium in memoryless strategies can be epsilon-approximated in NP. We study the important subclass of n-player turn-based probabilistic games, where at each state at most one player has a nontrivial choice of moves. For turn-based probabilistic games, we show the existence of epsilon-Nash equilibria in pure strategies for games where the objective of player i is a Borel set B-i of infinite traces. However, exact Nash equilibria may not exist. For the special case of omega-regular objectives, we show exact Nash equilibria exist, and can be computed in NP when the omega-regular objectives are expressed as parity objectives.},
  author       = {Krishnendu Chatterjee and Majumdar, Ritankar S and Jurdziński, Marcin},
  pages        = {26 -- 40},
  publisher    = {Springer},
  title        = {{On Nash equilibria in stochastic games}},
  doi          = {10.1007/978-3-540-30124-0_6},
  volume       = {3210},
  year         = {2004},
}

@phdthesis{4236,
  author       = {de Vladar, Harold},
  publisher    = {Centro de estudios avazados, IVIC},
  title        = {{Métodos no lineales y sus aplicaciones en dinámicas aleatorias de poblaciones celulares}},
  year         = {2004},
}

@article{4599,
  abstract     = {State-space explosion is a fundamental obstacle in the formal verification of designs and protocols. Several techniques for combating this problem have emerged in the past few years, among which two are significant: partial-order reduction and symbolic state-space search. In asynchronous systems, interleavings of independent concurrent events are equivalent, and only a representative interleaving needs to be explored to verify local properties. Partial-order methods exploit this redundancy and visit only a subset of the reachable states. Symbolic techniques, on the other hand, capture the transition relation of a system and the set of reachable states as boolean functions. In many cases, these functions can be represented compactly using binary decision diagrams (BDDs). Traditionally, the two techniques have been practiced by two different schools—partial-order methods with enumerative depth-first search for the analysis of asynchronous network protocols, and symbolic breadth-first search for the analysis of synchronous hardware designs. We combine both approaches and develop a method for using partial-order reduction techniques in symbolic BDD-based invariant checking. We present theoretical results to prove the correctness of the method, and experimental results to demonstrate its efficacy.},
  author       = {Alur, Rajeev and Brayton, Robert and Henzinger, Thomas A and Qadeer, Shaz and Rajamani, Sriram},
  issn         = {0925-9856},
  journal      = {Formal Methods in System Design},
  number       = {2},
  pages        = {97 -- 116},
  publisher    = {Springer},
  title        = {{Partial-order reduction in symbolic state-space exploration}},
  doi          = {10.1023/A:1008767206905},
  volume       = {18},
  year         = {2001},
}

@article{11694,
  abstract     = {We consider exploration problems where a robot has to construct a complete map of an unknown environment. We assume that the environment is modeled by a directed, strongly connected graph. The robot's task is to visit all nodes and edges of the graph using the minimum number R of edge traversals. Deng and Papadimitriou [Proceedings of the 31st Symposium on the Foundations of Computer Science, 1990, pp. 356-361] showed an upper bound for R ofd O(d)m and Koutsoupias (reported by Deng and Papadimitriou) gave a lower bound of Ω≠(d2m), where m is the number of edges in the graph and d is the minimum number of edges that have to be added to make the graph Eulerian.  We give the 1rst subexponential algorithm for this exploration problem, which achieves an upper bound of dO(logd)m.  We also show a matching lower bound of d≠(logd)m for our algorithm. Additionally, we give lower bounds of 2≠(d)m, respectively, d≠(logd)m for various other natural exploration algorithms.},
  author       = {Albers, Susanne and Henzinger, Monika H},
  issn         = {1095-7111},
  journal      = {SIAM Journal on Computing},
  keywords     = {directed graph, exploration algorithm},
  location     = {El Paso, TX, United States},
  number       = {4},
  pages        = {1164--1188},
  publisher    = {Society for Industrial and Applied Mathematics},
  title        = {{Exploring unknown environments}},
  doi          = {10.1137/s009753979732428x},
  volume       = {29},
  year         = {2000},
}

@article{2593,
  abstract     = {In cat and monkey, lamina I cells can be classified into three basic morphological types (fusiform, pyramidal, and multipolar), and recent intracellular labeling evidence in the cat indicates that fusiform and multipolar lamina I cells are two different types of nociceptive cells, whereas pyramidal cells are innocuous thermoreceptive-specific. Because earlier observations indicated that only nociceptive dorsal horn neurons respond to substance P (SP), we examined which morphological types of lamina I neurons express receptors for SP (NK-1r). We categorized NK-1r- immunoreactive (IR) lamina I neurons in serial horizontal sections from the cervical and lumbar enlargements of four monkeys. Consistent results were obtained by two independent teams of observers. Nearly all NK-1r-IR cells were fusiform (42%) or multipolar (43%), but only 6% were pyramidal (with 9% unclassified). We obtained similar findings in three monkeys in which we used double-labeling immunocytochemistry to identify NK-1r-IR and spinothalamic lamina I neurons retrogradely labeled with cholera toxin subunit b from the thalamus; most NK-1r-IR lamina I spinothalamic neurons were fusiform (48%) or multipolar (33%), and only 10% were pyramidal. In contrast, most (~75%) pyramidal and some (~25%) fusiform and multipolar lamina I spinothalamic neurons did not display NK-1r immunoreactivity. These data indicate that most fusiform and multipolar lamina I neurons in the monkey can express NK-1r, consistent with the idea that both types are nociceptive, whereas only a small proportion of lamina I pyramidal cells express this receptor, consistent with the previous finding that they are nonnociceptive. However, these findings also indicate that not all nociceptive lamina I neurons express receptors for SP.},
  author       = {Yu, Xiao and Zhang, En and Craig, Arthur and Shigemoto, Ryuichi and Ribeiro Da Silva, Alfredo and De Koninck, Yves},
  issn         = {0270-6474},
  journal      = {Journal of Neuroscience},
  number       = {9},
  pages        = {3545 -- 3555},
  publisher    = {Society for Neuroscience},
  title        = {{NK-1 receptor immunoreactivity in distinct morphological types of lamina I neurons of the primate spinal cord}},
  doi          = {10.1523/JNEUROSCI.19-09-03545.1999},
  volume       = {19},
  year         = {1999},
}

@article{4204,
  abstract     = {During the development of the zebrafish nervous system both noi, a zebrafish pax2 homolog, and ace, a zebrafish fgf8 homolog, are required for development of the midbrain and cerebellum. Here we describe a dominant mutation, aussicht (aus), in which the expression of noi and ace is upregulated, In aus mutant embryos, ace is upregulated at many sites in the embryo, while Itoi expression is only upregulated in regions of the forebrain and midbrain which also express ace. Subsequent to the alterations in noi and ace expression, aus mutants exhibit defects in the differentiation of the forebrain, midbrain and eyes. Within the forebrain, the formation of the anterior and postoptic commissures is delayed and the expression of markers within the pretectal area is reduced. Within the midbrain, En and wnt1 expression is expanded. In heterozygous aus embryos, there is ectopic outgrowth of neural retina in the temporal half of the eyes, whereas in putative homozygous aus embryos, the ventral retina is reduced and the pigmented retinal epithelium is expanded towards the midline, The observation that ans mutant embryos exhibit widespread upregulation of ace raised the possibility that aus might represent an allele of the ace gene itself. However, by crossing carriers for both aus and ace, we were able to generate homozygous ace mutant embryos that also exhibited the aus phenotype, This indicated that aus is not tightly linked to ace and is unlikely to be a mutation directly affecting the ace locus. However, increased Ace activity may underly many aspects of the aus phenotype and we show that the upregulation of noi in the forebrain of aus mutants is partially dependent upon functional Ace activity. Conversely, increased ace expression in the forebrain of arcs mutants is not dependent upon functional Noi activity. We conclude that aus represents a mutation involving a locus normally required for the regulation of ace expression during embryogenesis.},
  author       = {Heisenberg, Carl-Philipp J and Brennan, Caroline and Wilson, Stephen},
  issn         = {0950-1991},
  journal      = {Development},
  number       = {10},
  pages        = {2129 -- 2140},
  publisher    = {Company of Biologists},
  title        = {{Zebrafish aussicht mutant embryos exhibit widespread overexpression of ace (fgf8) and coincident defects in CNS development}},
  doi          = {10.1242/dev.126.10.2129},
  volume       = {126},
  year         = {1999},
}

@inproceedings{4608,
  abstract     = {State space explosion is a fundamental obstacle in formal verification of designs and protocols. Several techniques for combating this problem have emerged in the past few years, among which two are significant: partial-order reductions and symbolic state space search. In asynchronous systems, interleavings of independent concurrent events are equivalent, and only a representative interleaving needs to be explored to verify local properties. Partial-order methods exploit this redundancy and visit only a subset of the reachable states. Symbolic techniques, on the other hand, capture the transition relation of a system and the set of reachable states as boolean functions. In many cases, these functions can be represented compactly using binary decision diagrams (BDDs). Traditionally, the two techniques have been practiced by two different schools—partial-order methods with enumerative depth-first search for the analysis of asynchronous network protocols, and symbolic breadth-first search for the analysis of synchronous hardware designs. We combine both approaches and develop a method for using partial-order reduction techniques in symbolic BDD-based invariant checking. We present theoretical results to prove the correctness of the method, and experimental results to demonstrate its efficacy.},
  author       = {Alur, Rajeev and Brayton, Robert and Henzinger, Thomas A and Qadeer, Shaz and Rajamani, Sriram},
  booktitle    = {9th International Conference on Computer Aided Verification},
  isbn         = {9783540631668},
  location     = {Haifa, Israel},
  pages        = {340 -- 351},
  publisher    = {Springer},
  title        = {{Partial-order reduction in symbolic state-space exploration}},
  doi          = {10.1007/3-540-63166-6_34},
  volume       = {1254},
  year         = {1997},
}