@inproceedings{4470,
abstract = {Giotto is a platform-independent language for specifying software for high-performance control applications. In this paper we present a new approach to the compilation of Giotto. Following this approach, the Giotto compiler generates code for a virtual machine, called the E machine, which can be ported to different platforms. The Giotto compiler also checks if the generated E code is time safe for a given platform, that is, if the platform offers sufficient performance to ensure that the E code is executed in a timely fashion that conforms with the Giotto semantics. Time-safety checking requires a schedulability analysis. We show that while for arbitrary E code, the analysis is exponential, for E code generated from typical Giotto programs, the analysis is polynomial. This supports our claim that Giotto identifies a useful fragment of embedded programs.},
author = {Thomas Henzinger and Kirsch, Christoph M and Majumdar, Ritankar S and Matic, Slobodan},
pages = {76 -- 92},
publisher = {ACM},
title = {{Time-safety checking for embedded programs}},
doi = {10.1007/3-540-45828-X_7},
volume = {2491},
year = {2002},
}
@inproceedings{4471,
abstract = {The sequential synthesis problem, which is closely related to Church’s solvability problem, asks, given a specification in the form of a binary relation between input and output streams, for the construction of a finite-state stream transducer that converts inputs to appropriate outputs. For efficiency reasons, practical sequential hardware is often designed to operate without prior initialization. Such hardware designs can be modeled by uninitialized state machines, which are required to satisfy their specification if started from any state. In this paper we solve the sequential synthesis problem for uninitialized systems, that is, we construct uninitialized finite-state stream transducers. We consider specifications given by LTL formulas, deterministic, nondeterministic, universal, and alternating Büchi automata. We solve this uninitialized synthesis problem by reducing it to the well-understood initialized synthesis problem. While our solution is straightforward, it leads, for some specification formalisms, to upper bounds that are exponentially worse than the complexity of the corresponding initialized problems. However, we prove lower bounds to show that our simple solutions are optimal for all considered specification formalisms. We also study the problem of deciding whether a given specification is uninitialized, that is, if its uninitialized and initialized synthesis problems coincide. We show that this problem has, for each specification formalism, the same complexity as the equivalence problem.},
author = {Thomas Henzinger and Krishnan, Sriram C and Kupferman, Orna and Mang, Freddy Y},
pages = {644 -- 656},
publisher = {Springer},
title = {{Synthesis of uninitialized systems}},
doi = {10.1007/3-540-45465-9_55},
volume = {2380},
year = {2002},
}
@inproceedings{4472,
abstract = {We present a methodology and tool for verifying and certifying systems code. The verification is based on the lazy-abstraction paradigm for intertwining the following three logical steps: construct a predicate abstraction from the code, model check the abstraction, and automatically refine the abstraction based on counterexample analysis. The certification is based on the proof-carrying code paradigm. Lazy abstraction enables the automatic construction of small proof certificates. The methodology is implemented in Blast, the Berkeley Lazy Abstraction Software verification Tool. We describe our experience applying Blast to Linux and Windows device drivers. Given the C code for a driver and for a temporal-safety monitor, Blast automatically generates an easily checkable correctness certificate if the driver satisfies the specification, and an error trace otherwise.},
author = {Thomas Henzinger and Necula, George C and Jhala, Ranjit and Sutre, Grégoire and Majumdar, Ritankar S and Weimer, Westley},
pages = {526 -- 538},
publisher = {Springer},
title = {{Temporal safety proofs for systems code}},
doi = {10.1007/3-540-45657-0_45},
volume = {2404},
year = {2002},
}
@article{4473,
abstract = {The simulation preorder on state transition systems is widely accepted as a useful notion of refinement, both in its own right and as an efficiently checkable sufficient condition for trace containment. For composite systems, due to the exponential explosion of the state space, there is a need for decomposing a simulation check of the form P ≤s Q, denoting "P is simulated by Q," into simpler simulation checks on the components of P and Q. We present an assume-guarantee rule that enables such a decomposition. To the best of our knowledge, this is the first assume-guarantee rule that applies to a refinement relation different from trace containment. Our rule is circular, and its soundness proof requires induction on trace trees. The proof is constructive: given simulation relations that witness the simulation preorder between corresponding components of P and Q, we provide a procedure for constructing a witness relation for P ≤s Q. We also extend our assume-guarantee rule to account for fairness constraints on transition systems.},
author = {Thomas Henzinger and Qadeer,Shaz and Rajamani, Sriram K and Tasiran, Serdar},
journal = {ACM Transactions on Programming Languages and Systems (TOPLAS)},
number = {1},
pages = {51 -- 64},
publisher = {ACM},
title = {{An assume-guarantee rule for checking simulation}},
doi = {10.1145/509705.509707},
volume = {24},
year = {2002},
}
@article{4474,
abstract = {The simulation preorder for labeled transition systems is defined locally, and operationally, as a game that relates states with their immediate successor states. Simulation enjoys many appealing properties. First, simulation has a denotational characterization: system S simulates system I iff every computation tree embedded in the unrolling of I can be embedded also in the unrolling of S. Second, simulation has a logical characterization: S simulates I iff every universal branching-time formula satisfied by S is satisfied also by I. It follows that simulation is a suitable notion of implementation, and it is the coarsest abstraction of a system that preserves universal branching-time properties. Third, based on its local definition, simulation between finite-state systems can be checked in polynomial time. Finally, simulation implies trace containment, which cannot be defined locally and requires polynomial space for verification. Hence simulation is widely used both in manual and in automatic verification. Liveness assumptions about transition systems are typically modeled using fairness constraints. Existing notions of simulation for fair transition systems, however, are not local, and as a result, many appealing properties of the simulation preorder are lost. We propose a new view of fair simulation by extending the local definition of simulation to account for fairness: system View the MathML sourcefairly simulates system View the MathML source iff in the simulation game, there is a strategy that matches with each fair computation of View the MathML source a fair computation of View the MathML source. Our definition enjoys a denotational characterization and has a logical characterization: View the MathML source fairly simulates View the MathML source iff every fair computation tree (whose infinite paths are fair) embedded in the unrolling of View the MathML source can be embedded also in the unrolling of View the MathML source or, equivalently, iff every Fair-∀AFMC formula satisfied by View the MathML source is satisfied also by View the MathML source (∀AFMC is the universal fragment of the alternation-free μ-calculus). The locality of the definition leads us to a polynomial-time algorithm for checking fair simulation for finite-state systems with weak and strong fairness constraints. Finally, fair simulation implies fair trace containment and is therefore useful as an efficiently computable local criterion for proving linear-time abstraction hierarchies of fair systems.},
author = {Thomas Henzinger and Kupferman, Orna and Rajamani, Sriram K},
journal = {Information and Computation},
number = {1},
pages = {64 -- 81},
publisher = {Elsevier},
title = {{Fair simulation}},
doi = {10.1006/inco.2001.3085},
volume = {173},
year = {2002},
}
@inproceedings{4476,
abstract = {One approach to model checking software is based on the abstract-check-refine paradigm: build an abstract model, then check the desired property, and if the check fails, refine the model and start over. We introduce the concept of lazy abstraction to integrate and optimize the three phases of the abstract-check-refine loop. Lazy abstraction continuously builds and refines a single abstract model on demand, driven by the model checker, so that different parts of the model may exhibit different degrees of precision, namely just enough to verify the desired property. We present an algorithm for model checking safety properties using lazy abstraction and describe an implementation of the algorithm applied to C programs. We also provide sufficient conditions for the termination of the method.},
author = {Thomas Henzinger and Jhala, Ranjit and Majumdar, Ritankar S and Sutre, Grégoire},
pages = {58 -- 70},
publisher = {ACM},
title = {{Lazy abstraction}},
doi = {10.1145/503272.503279},
year = {2002},
}
@inproceedings{4562,
abstract = {We present interface models that describe both the input assumptions of a component, and its output behavior. By enabling us to check that the input assumptions of a component are met in a design, interface models provide a compatibility check for component-based design. When refining a design into an implementation, interface models require that the output behavior of a component satisfies the design specification only when the input assumptions of the specification are satisfied, yielding greater flexibility in the choice of implementations. Technically, our interface models are games between two players, Input and Output; the duality of the players accounts for the dual roles of inputs and outputs in composition and refinement. We present two interface models in detail, one for a simple synchronous form of interaction between components typical in hardware, and the other for more complex synchronous interactions on bidirectional connections. As an example, we specify the interface of a bidirectional bus, with the input assumption that at any time at most one component has write access to the bus. For these interface models, we present algorithms for compatibility and refinement checking, and we describe efficient symbolic implementations.},
author = {Chakrabarti, Arindam and de Alfaro, Luca and Thomas Henzinger and Mang, Freddy Y},
pages = {414 -- 427},
publisher = {Springer},
title = {{Synchronous and bidirectional component interfaces}},
doi = {10.1007/3-540-45657-0_34},
volume = {2404},
year = {2002},
}
@inproceedings{4563,
abstract = {We present a formal methodology and tool for uncovering errors in the interaction of software modules. Our methodology consists of a suite of languages for defining software interfaces, and algorithms for checking interface compatibility. We focus on interfaces that explain the method-call dependencies between software modules. Such an interface makes assumptions about the environment in the form of call and availability constraints. A call constraint restricts the accessibility of local methods to certain external methods. An availability constraint restricts the accessibility of local methods to certain states of the module. For example, the interface for a file server with local methods open and read may assert that a file cannot be read without having been opened. Checking interface compatibility requires the solution of games, and in the presence of availability constraints, of pushdown games. Based on this methodology, we have implemented a tool that has uncovered incompatibilities in TinyOS, a small operating system for sensor nodes in adhoc networks.},
author = {Chakrabarti, Arindam and de Alfaro, Luca and Thomas Henzinger and Jurdziński, Marcin and Mang, Freddy Y},
pages = {428 -- 441},
publisher = {Springer},
title = {{Interface compatibility checking for software modules}},
doi = {10.1007/3-540-45657-0_35},
volume = {2404},
year = {2002},
}
@inproceedings{4565,
abstract = {In the literature, we find several formulations of the control
problem for timed and hybrid systems. We argue that formulations where
a controller can cause an action at any point in dense (rational or real)
time are problematic, by presenting an example where the controller
must act faster and faster, yet causes no Zeno effects (say, the control
actions are at times 0, 1/2, 1, 1 1/4, 2, 2 1/8, 3, 3 1/16 ,...). Such a controller is,
of course, not implementable in software. Such controllers are avoided by formulations where the controller can cause actions only at discrete (integer) points in time. While the resulting control problem is well- understood if the time unit, or “sampling rate” of the controller, is fixed a priori, we define a novel, stronger formulation: the discrete-time control problem with unknown sampling rate asks if a sampling controller exists for some sampling rate. We prove that this problem is undecidable even in the special case of timed automata.},
author = {Cassez, Franck and Thomas Henzinger and Raskin, Jean-François},
pages = {134 -- 148},
publisher = {Springer},
title = {{A comparison of control problems for timed and hybrid systems}},
doi = {10.1007/3-540-45873-5_13},
volume = {2289},
year = {2002},
}
@article{4595,
abstract = {Temporal logic comes in two varieties: linear-time temporal logic assumes implicit universal quantification over all paths that are generated by the execution of a system; branching-time temporal logic allows explicit existential and universal quantification over all paths. We introduce a third, more general variety of temporal logic: alternating-time temporal logic offers selective quantification over those paths that are possible outcomes of games, such as the game in which the system and the environment alternate moves. While linear-time and branching-time logics are natural specification languages for closed systems, alternating-time logics are natural specification languages for open systems. For example, by preceding the temporal operator "eventually" with a selective path quantifier, we can specify that in the game between the system and the environment, the system has a strategy to reach a certain state. The problems of receptiveness, realizability, and controllability can be formulated as model-checking problems for alternating-time formulas. Depending on whether or not we admit arbitrary nesting of selective path quantifiers and temporal operators, we obtain the two alternating-time temporal logics ATL and ATL*.ATL and ATL* are interpreted over concurrent game structures. Every state transition of a concurrent game structure results from a choice of moves, one for each player. The players represent individual components and the environment of an open system. Concurrent game structures can capture various forms of synchronous composition for open systems, and if augmented with fairness constraints, also asynchronous composition. Over structures without fairness constraints, the model-checking complexity of ATL is linear in the size of the game structure and length of the formula, and the symbolic model-checking algorithm for CTL extends with few modifications to ATL. Over structures with weak-fairness constraints, ATL model checking requires the solution of 1-pair Rabin games, and can be done in polynomial time. Over structures with strong-fairness constraints, ATL model checking requires the solution of games with Boolean combinations of Büchi conditions, and can be done in PSPACE. In the case of ATL*, the model-checking problem is closely related to the synthesis problem for linear-time formulas, and requires doubly exponential time.},
author = {Alur, Rajeev and Thomas Henzinger and Kupferman, Orna},
journal = {Journal of the ACM},
number = {5},
pages = {672 -- 713},
publisher = {ACM},
title = {{Alternating-time temporal logic}},
doi = {10.1145/585265.585270},
volume = {49},
year = {2002},
}
@inproceedings{4631,
abstract = {We present a theory of timed interfaces, which is capable of specifying both the timing of the inputs a component expects from the environment, and the timing of the outputs it can produce. Two timed interfaces are compatible if there is a way to use them together such that their timing expectations are met. Our theory provides algorithms for checking the compatibility between two interfaces and for deriving the composite interface; the theory can thus be viewed as a type system for real-time interaction. Technically, a timed interface is encoded as a timed game between two players, representing the inputs and outputs of the component. The algorithms for compatibility checking and interface composition are thus derived from algorithms for solving timed games.},
author = {de Alfaro, Luca and Thomas Henzinger and Stoelinga, Mariëlle},
pages = {108 -- 122},
publisher = {ACM},
title = {{Timed interfaces}},
doi = {10.1007/3-540-45828-X_9},
volume = {2491},
year = {2002},
}
@article{6158,
abstract = {Wild isolates of Caenorhabditis elegans can feed either alone or in groups1,2. This natural variation in behaviour is associated with a single residue difference in NPR-1, a predicted G-protein-coupled neuropeptide receptor related to Neuropeptide Y receptors2. Here we show that the NPR-1 isoform associated with solitary feeding acts in neurons exposed to the body fluid to inhibit social feeding. Furthermore, suppressing the activity of these neurons, called AQR, PQR and URX, using an activated K+ channel, inhibits social feeding. NPR-1 activity in AQR, PQR and URX neurons seems to suppress social feeding by antagonizing signalling through a cyclic GMP-gated ion channel encoded by tax-2 and tax-4. We show that mutations in tax-2 or tax-4 disrupt social feeding, and that tax-4 is required in several neurons for social feeding, including one or more of AQR, PQR and URX. The AQR, PQR and URX neurons are unusual in C. elegans because they are directly exposed to the pseudocoelomic body fluid3. Our data suggest a model in which these neurons integrate antagonistic signals to control the choice between social and solitary feeding behaviour.},
author = {Coates, Juliet C. and de Bono, Mario},
issn = {0028-0836},
journal = {Nature},
number = {6910},
pages = {925--929},
publisher = {Springer Nature},
title = {{Antagonistic pathways in neurons exposed to body fluid regulate social feeding in Caenorhabditis elegans}},
doi = {10.1038/nature01170},
volume = {419},
year = {2002},
}
@article{6159,
abstract = {Natural Caenorhabditis elegans isolates exhibit either social or solitary feeding on bacteria. We show here that social feeding is induced by nociceptive neurons that detect adverse or stressful conditions. Ablation of the nociceptive neurons ASH and ADL transforms social animals into solitary feeders. Social feeding is probably due to the sensation of noxious chemicals by ASH and ADL neurons; it requires the genes ocr-2 and osm-9, which encode TRP-related transduction channels, and odr-4 and odr-8, which are required to localize sensory chemoreceptors to cilia. Other sensory neurons may suppress social feeding, as social feeding in ocr-2 and odr-4 mutants is restored by mutations in osm-3, a gene required for the development of 26 ciliated sensory neurons. Our data suggest a model for regulation of social feeding by opposing sensory inputs: aversive inputs to nociceptive neurons promote social feeding, whereas antagonistic inputs from neurons that express osm-3 inhibit aggregation.},
author = {de Bono, Mario and Tobin, David M. and Davis, M. Wayne and Avery, Leon and Bargmann, Cornelia I.},
issn = {0028-0836},
journal = {Nature},
number = {6910},
pages = {899--903},
publisher = {Springer Nature},
title = {{Social feeding in Caenorhabditis elegans is induced by neurons that detect aversive stimuli}},
doi = {10.1038/nature01169},
volume = {419},
year = {2002},
}
@article{2620,
abstract = {An ion channel's function depends largely on its location and density on neurons. Here we used high-resolution immunolocalization to determine the subcellular distribution of the hyperpolarization-activated and cyclic-nucleotide-gated channel subunit 1 (HCN1) in rat brain. Light microscopy revealed graded HCN1 immunoreactivity in apical dendrites of hippocampal, subicular and neocortical layer-5 pyramidal cells. Quantitative comparison of immunogold densities showed a 60-fold increase from somatic to distal apical dendritic membranes. Distal dendritic shafts had 16 times more HCN1 labeling than proximal dendrites of similar diameters. At the same distance from the soma, the density of HCN1 was significantly higher in dendritic shafts than in spines. Our results reveal the complex cell surface distribution of voltage-gated ion-channels, and predict its role in increasing the computational power of single neurons via subcellular domain and input-specific mechanisms.},
author = {Lörincz, Andrea and Notomi, Takuya and Tamás, Gábor and Ryuichi Shigemoto and Nusser, Zoltán},
journal = {Nature Neuroscience},
number = {11},
pages = {1185 -- 1193},
publisher = {Nature Publishing Group},
title = {{Polarized and compartment-dependent distribution of HCN1 in pyramidal cell dendrites}},
doi = {10.1038/nn962},
volume = {5},
year = {2002},
}
@article{2621,
abstract = {The release properties of glutamatergic nerve terminals are influenced by a number of factors, including the subtype of voltage-dependent calcium channel and the presence of presynaptic autoreceptors. Group III metabotropic glutamate receptors (mGluRs) mediate feedback inhibition of glutamate release by inhibiting Ca2+ channel activity. By imaging Ca2+ in preparations of cerebrocortical nerve terminals, we show that voltage-dependent Ca2+ channels are distributed in a heterogeneous manner in individual nerve terminals. Presynaptic terminals contained only N-type (47.5%; conotoxin GVIA-sensitive), P/Q-type (3.9%; agatoxin IVA-sensitive), or both N- and P/Q-type (42.6%) Ca2+ channels, although the remainder of the terminals (6.1%) were insensitive to these two toxins. In this preparation, two mGluRs with high and low affinity for L(+)-2-amino-4-phosphonobutyrate were identified by immunocytochemistry as mGluR4 and mGluR7, respectively. These receptors were responsible for 22.2 and 24.1% reduction of glutamate release, and they reduced the Ca2+ response in 24.4 and 30.3% of the nerve terminals, respectively. Interestingly, mGluR4 was largely (73.7%) located in nerve terminals expressing both N- and P/Q-type Ca2+ channels, whereas mGluR7 was predominantly (69.9%) located in N-type Ca2+ channel-expressing terminals. This specific coexpression of different group III mGluRs and Ca2+ channels may endow synaptic terminals with distinct release properties and reveals the existence of a high degree of presynaptic heterogeneity.},
author = {Millán, Carmelo and Luján, Rafael and Ryuichi Shigemoto and Sánchez-Prieto, José},
journal = {Journal of Biological Chemistry},
number = {49},
pages = {47796 -- 47803},
publisher = {American Society for Biochemistry and Molecular Biology},
title = {{Subtype-specific expression of Group III metabotropic glutamate receptors and Ca2+ channels in single nerve terminals}},
doi = {10.1074/jbc.M207531200},
volume = {277},
year = {2002},
}
@article{2622,
abstract = {To understand the possible contribution of metabotropic γ-aminobutyric acid receptors (GABABR) in cortical development, we investigated the expression pattern and the cellular and subcellular localization of the GABABR1 and GABABR2 subtypes in the rat neocortex from embryonic day 14 (E14) to adulthood. At the light microscopic level, both GABABR1 and GABABR2 were detected as early as E14. During prenatal development, both subtypes were expressed highly in the cortical plate. Using double immunofluorescence, GABABR1 colocalized with GABABR2 in neurons of the marginal zone and subplate, indicating that these proteins are coexpressed and could be forming functional GABABRs during prenatal development in vivo. In contrast, only GABABR1 but not GABABR2 was detected in the tangentially migratory cells in the lower intermediate zone. During postnatal development, immunoreactivity for GABABR1 and GABABR2 was distributed mainly in pyramidal cells. Discrete GABABR1-immunopositive cell bodies of interneurons were present throughout the neocortex. In addition, GABABR1 but not GABABR2 was found in identified Cajal-Retzius cells in layer I. At the electron microscopic level, immunoreactivity for GABABR1 and GABABR2 was found in dendritic spines and dendritic shafts at extrasynaptic and perisynaptic sites throughout postnatal development. We further demonstrated the presynaptic localization of GABABR1 and GABABR2, as well as the association of the receptors with asymmetrical synaptic junctions. These results indicate potentially important roles for the GABABRs in the regulation of migratory processes during corticogenesis and in the modulation of synaptic transmission during early development of cortical circuitry.},
author = {López-Bendito, Guillermina and Ryuichi Shigemoto and Kulik, Ákos and Paulsen, Ole and Fairén, Alfonso and Luján, Rafael},
journal = {European Journal of Neuroscience},
number = {11},
pages = {1766 -- 1778},
publisher = {Wiley-Blackwell},
title = {{Expression and distribution of metabotropic GABA receptor subtypes GABABR1 and GABABR2 during rat neocortical development}},
doi = {10.1046/j.1460-9568.2002.02032.x},
volume = {15},
year = {2002},
}
@article{2624,
abstract = {Metabotropic γ-aminobutyric acid receptors (GABABRs) are involved in modulation of synaptic transmission and activity of cerebellar and thalamic neurons. We used subtype-specific antibodies in pre- and postembedding immunohistochemistry combined with three-dimensional reconstruction of labelled profiles and quantification of immunoparticles to reveal the subcellular distribution of pre- and postsynaptic GABABR1a/b and GABABR2 in the rat cerebellum and ventrobasal thalamus. GABABR1a/b and R2 were extensively colocalized in most brain regions including the cerebellum and thalamus. In the cerebellum, immunoreactivity for both subtypes was prevalent in the molecular layer. The most intense immunoreactivity was found in Purkinje cell spines with a high density of immunoparticles at extrasynaptic sites peaking at around 240 nm from glutamatergic synapses between spines and parallel fibre varicosities. This is in contrast to dendrites at sites around GABAergic synapses where sparse and random distribution was found for both subtypes. In addition, more than one-tenth of the synaptic membrane specialization of spine-parallel fibre synapses were labelled at pre- or postsynaptic sites. Weak immunolabelling for both subtypes was also seen in parallel fibres but only rarely in GABAergic axons. In the ventrobasal thalamus, immunolabelling for both receptor subtypes was intense over the dendritic field of thalamocortical cells. Electron microscopy demonstrated an extrasynaptic localization of GABABR1a/b and R2 exclusively in postsynaptic elements. Quantitative analysis further revealed the density of GABABR1a/b around GABAergic synapses was higher than glutamatergic synapses on thalamocortical cell dendrites. The distinct localization of GABABRs relative to synaptic sites in the cerebellum and ventrobasal thalamus suggests that GABABRs differentially regulate activity of different neuronal populations.},
author = {Kulik, Ákos and Nakadate, Kazuhiko and Nyíri, Gábor and Notomi, Takuya and Malitschek, Barbara and Bettler, Bernhard and Ryuichi Shigemoto},
journal = {European Journal of Neuroscience},
number = {2},
pages = {291 -- 307},
publisher = {Wiley-Blackwell},
title = {{Distinct localization of GABAB receptors relative to synaptic sites in the rat cerebellum and ventrobasal thalamus}},
doi = {10.1046/j.0953-816x.2001.01855.x},
volume = {15},
year = {2002},
}
@inproceedings{2694,
abstract = {We outline the status of rigorous derivations of certain classical evolution equations as limits of Schrödinger dynamics. We explain two recent results jointly with H.T. Yau in more details. The first one is the derivation of the linear Boltzmann equation as the long time limit of the one-body Schrödinger equation with a random potential. The second one is the mean field limit of high density bosons with Coulomb interaction that leads to the nonlinear Hartree equation.},
author = {László Erdös},
pages = {487 -- 506},
publisher = {Springer},
title = {{Scaling limits of Schrödinger quantum mechanics}},
doi = {10.1007/3-540-46122-1_19},
volume = {597},
year = {2002},
}
@inproceedings{2708,
author = {László Erdös},
pages = {129 -- 133},
publisher = {World Scientific Publishing},
title = {{Two dimensional Pauli operator via scalar potential}},
doi = {10.1090/conm/307},
volume = {307},
year = {2002},
}
@article{2737,
abstract = {We derive the time-dependent Schrödinger–Poisson equation as the weak coupling limit of the N-body linear Schrödinger equation with Coulomb potential.},
author = {Bardos, Claude and László Erdös and Golse, François and Mauser, Norbert J and Yau, Horng-Tzer},
journal = {Comptes Rendus Mathematique},
number = {6},
pages = {515 -- 520},
publisher = {Elsevier},
title = {{Derivation of the Schrödinger-Poisson equation from the quantum N-body problem}},
doi = {10.1016/S1631-073X(02)02253-7},
volume = {334},
year = {2002},
}