@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{3812,
abstract = {Hippocampal GABAergic interneurons show diverse molecular and morphological properties. The functional significance of this diversity for information processing is poorly understood. Here we show that cholecystokinin (CCK)-expressing interneurons in rat dentate gyrus release GABA in a highly asynchronous manner, in contrast to parvalbumin (PV) interneurons. With a gamma-frequency burst of ten action potentials, the ratio of asynchronous to synchronous release is 3:1 in CCK interneurons but is 1:5 in parvalbumin interneurons. N-type channels trigger synchronous and asynchronous release in CCK interneuron synapses, whereas P/Q-type Ca(2+) channels mediate release at PV interneuron synapses. Effects of Ca(2+) chelators suggest that both a long-lasting presynaptic Ca(2+) transient and a large distance between Ca(2+) source and sensor of exocytosis contribute to the higher ratio of asynchronous to synchronous release in CCK interneuron synapses. Asynchronous release occurs at physiological temperature and with behaviorally relevant stimulation patterns, thus generating long-lasting inhibition in the brain.},
author = {Hefft, Stefan and Peter Jonas},
booktitle = {Nature Neuroscience},
number = {10},
pages = {1319 -- 28},
publisher = {Nature Publishing Group},
title = {{Asynchronous GABA release generates long-lasting inhibition at a hippocampal interneuron-principal neuron synapse (Review)}},
doi = {10.1038/nn1542},
volume = {8},
year = {2005},
}
@inproceedings{3892,
abstract = {In 2-player non-zero-sum games, Nash equilibria capture the options for rational behavior if each player attempts to maximize her payoff. In contrast to classical game theory, we consider lexicographic objectives: first, each player tries to maximize her own payoff, and then, the player tries to minimize the opponent's payoff. Such objectives arise naturally in the verification of systems with multiple components. There, instead of proving that each component satisfies its specification no matter how the other components behave, it often suffices to prove that each component satisfies its specification provided that the other components satisfy their specifications. We say that a Nash equilibrium is secure if it is an equilibrium with respect to the lexicographic objectives of both players. We prove that in graph games with Borel winning conditions, which include the games that arise in verification, there may be several Nash equilibria, but there is always a unique maximal payoff profile of a secure equilibrium. We show how this equilibrium can be computed in the case of omega-regular winning conditions, and we characterize the memory requirements of strategies that achieve the equilibrium.},
author = {Krishnendu Chatterjee and Thomas Henzinger and Jurdziński, Marcin},
pages = {141 -- 161},
publisher = {Springer},
title = {{Games with secure equilibria}},
doi = {10.1007/11561163_7},
volume = {3657},
year = {2005},
}
@inproceedings{3893,
abstract = {We study infinite stochastic games played by two-players on a finite graph with goals specified by sets of infinite traces. The games are concurrent (each player simultaneously and independently chooses an action at each round), stochastic (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 an W-regular objective expressed as a paxity objective, then there exists an epsilon-Nash equilibrium, for every epsilon > 0. However, exact Nash equilibria need not exist. We study the complexity of finding values (payoff profile) of an epsilon-Nash equilibrium. We show that the values of an epsilon-Nash equilibrium in nonzero-sum concurrent parity games can be computed by solving the following two simpler problems: computing the values of zero-sum (the goals of the players axe strictly conflicting) concurrent parity games and computing epsilon-Nash equilibrium values of nonzero-sum concurrent games with reachability objectives. As a consequence we establish that values of an epsilon-Nash equilibrium can be computed in TFNP (total functional NP), and hence in EXPTIME.},
author = {Krishnendu Chatterjee},
pages = {413 -- 427},
publisher = {Schloss Dagstuhl - Leibniz-Zentrum für Informatik},
title = {{Two-player nonzero-sum ω-regular games}},
doi = {10.1007/11539452_32},
volume = {3653},
year = {2005},
}
@inproceedings{3896,
abstract = {Temporal Logic Model Checking is one of the most potent tools for the verification of finite state systems. Computation Tree Logic (CTL) has gained popularity because unlike most other logics, CTL model checking of a single transition system can be achieved in polynomial time. However, in most real-life problems, specially in distributed and parallel systems, the system consist of a set of concurrent processes and the verification problem translates to model check the composition of the component processes. Since explicit composition leads to state explosion, verifying the system without actually composing the components is attractive, even for possibly restrictive class of systems. We show that the problem of compositional CTL model checking is PSPACE complete for the class of systems composed of components that are tree-like transition structure and do not interact among themselves. For the simplest forms of existential and universal CTL formulas model checking turns out to be NP complete and coNP complete, respectively. The results hold for both synchronous and asynchronous composition.},
author = {Krishnendu Chatterjee and Dasgupta, Pallab and Chakrabarti, Partha P},
pages = {89 -- 102},
publisher = {Springer},
title = {{Complexity of compositional model checking of computation tree logic on simple structures}},
doi = {10.1007/978-3-540-30536-1_13},
volume = {3326},
year = {2005},
}