@inproceedings{4627,
abstract = {We consider two-player games, which are played on a finite state space for an infinite number of rounds. The games are concurrent, that is, in each round, the two players choose their moves independently and simultaneously; the current state and the two moves determine a successor state. We consider omega-regular winning conditions on the resulting infinite state sequence. To model the independent choice of moves, both players are allowed to use randomization for selecting their moves. This gives rise to the following qualitative modes of winning, which can be studied without numerical considerations concerning probabilities: sure-win (player 1 can ensure winning with certainty), almost-sure-win (player 1 can ensure winning with probability 1), limit-win (player 1 can ensure winning with probability arbitrarily close to 1), bounded-win (player 1 can ensure winning with probability bounded away from 0), positive-win (player 1 can ensure winning with positive probability), and exist-win (player 1 can ensure that at least one possible outcome of the game satisfies the winning condition).We provide algorithms for computing the sets of winning states for each of these winning modes. In particular, we solve concurrent Rabin-chain games in n0 (m) time, where n is the size of the game structure and m is the number of pairs in the Rabin-chain condition. While this complexity is in line with traditional turn-based games, where in each state only one of the two players has a choice of moves, our algorithms are considerably more involved than those for turn-based games are. This is because concurrent games violate two of the most fundamental properties of turn-based games. First, concurrent games are not determined, but rather exhibit a more general duality property, which involves multiple modes of winning. Second, winning strategies for concurrent games may require infinite memory.},
author = {de Alfaro, Luca and Thomas Henzinger},
pages = {141 -- 154},
publisher = {IEEE},
title = {{Concurrent omega-regular games}},
doi = {10.1109/LICS.2000.855763},
year = {2000},
}
@inproceedings{4637,
abstract = {In the synchronous composition of processes, one process may prevent another process from proceeding unless compositions without a well-defined product behavior are ruled out. They can be ruled out semantically, by insisting on the existence of certain fixed points, or syntactically, by equipping processes with types, which make the dependencies between input and output signals transparent. We classify various typing mechanisms and study their effects on the control problem.
A static type enforces fixed, acyclic dependencies between input and output ports. For example, synchronous hardware without combinational loops can be typed statically. A dynamic type may vary the dependencies from state to state, while maintaining acyclicity, as in level-sensitive latches. Then, two dynamically typed processes can be syntactically compatible, if all pairs of possible dependencies are compatible, or semantically compatible, if in each state the combined dependencies remain acyclic. For a given plant process and control objective, there may be a controller of a static type, or only a controller of a syntactically compatible dynamic type, or only a controller of a semantically compatible dynamic type. We show this to be a strict hierarchy of possibilities, and we present algorithms and determine the complexity of the corresponding control problems.
Furthermore, we consider versions of the control problem in which the type of the controller (static or dynamic) is given. We show that the solution of these fixed-type control problems requires the evaluation of partially ordered (Henkin) quantifiers on boolean formulas, and is therefore harder (nondeterministic exponential time) than more traditional control questions},
author = {de Alfaro, Luca and Thomas Henzinger and Mang, Freddy Y},
pages = {458 -- 473},
publisher = {Schloss Dagstuhl - Leibniz-Zentrum für Informatik},
title = {{The control of synchronous systems}},
doi = {10.1007/3-540-44618-4_33},
volume = {1877},
year = {2000},
}
@inproceedings{4638,
abstract = {Any formal method or tool is almost certainly more often applied in situations where the outcome is failure (a counterexample) rather than success (a correctness proof). We present a method for symbolic model checking that can lead to significant time and memory savings for model-checking runs that fail, while occurring only a small overhead for model-checking runs that succeed. Our method discovers an error as soon as it cannot be prevented, which can be long before it actually occurs; for example, the violation of an invariant may become unpreventable many transitions before the invariant is violated.
The key observation is that “unpreventability” is a local property of a single module: an error is unpreventable in a module state if no environment can prevent it. Therefore, unpreventability is inexpensive to compute for each module, yet can save much work in the state exploration of the global, compound system. Based on different degrees of information available about the environment, we define and implement several notions of “unpreventability,” including the standard notion of uncontrollability from discrete-event control. We present experimental results for two examples, a distributed database protocol and a wireless communication protocol.},
author = {de Alfaro, Luca and Thomas Henzinger and Mang, Freddy Y},
pages = {186 -- 201},
publisher = {Springer},
title = {{Detecting errors before reaching them}},
doi = {10.1007/10722167_17},
volume = {1855},
year = {2000},
}
@article{3149,
abstract = {The prohormone convertases (PCs) are an evolutionarily ancient group of proteases required for the maturation of neuropeptide and peptide hormone precursors. In Drosophila melanogaster, the homolog of prohormone convertase 2, dPC2 (amontillado), is required for normal hatching behavior, and immunoblotting data indicate that flies express 80- and 75-kDa forms of this protein. Because mouse PC2 (mPC2) requires 7B2, a helper protein for productive maturation, we searched the fly data base for the 7B2 signature motif PPNPCP and identified an expressed sequence tag clone encoding the entire open reading frame for this protein. dPC2 and d7B2 cDNAs were subcloned into expression vectors for transfection into HEK-293 cells; mPC2 and rat 7B2 were used as controls. Although active mPC2 was detected in medium in the presence of either d7B2 or r7B2, dPC2 showed no proteolytic activity upon coexpression of either d7B2 or r7B2. Labeling experiments showed that dPC2 was synthesized but not secreted from HEK-293 cells. However, when dPC2 and either d7B2 or r7B2 were coexpressed in Drosophila S2 cells, abundant immunoreactive dPC2 was secreted into the medium, coincident with the appearance of PC2 activity. Expression and secretion of dPC2 enzyme activity thus appears to require insect cell-specific posttranslational processing events. The significant differences in the cell biology of the insect and mammalian enzymes, with 7B2 absolutely required for secretion of dPC2 and zymogen conversion occurring intracellularly in the case of dPC2 but not mPC2, support the idea that the Drosophila enzyme has specific requirements for maturation and secretion that can be met only in insect cells.},
author = {Hwang, Jae R and Daria Siekhaus and Fuller, Robert S and Taghert, Paul H and Lindberg, Iris},
journal = {Journal of Biological Chemistry},
number = {23},
pages = {17886 -- 17893},
publisher = {American Society for Biochemistry and Molecular Biology},
title = {{Interaction of Drosophila melanogaster prohormone convertase 2 and 7B2: Insect cell specific processing and secretion}},
doi = {10.1074/jbc.M000032200 },
volume = {275},
year = {2000},
}
@article{3489,
abstract = {We have examined factors that determine the strength and dynamics of GABAergic synapses between interneurons [dentate gyrus basket cells (BCs)] and principal neurons [dentate gyrus granule cells (GCs)] using paired recordings in rat hippocampal slices at 34°C. Unitary IPSCs recorded from BC–GC pairs in high intracellular Cl− concentration showed a fast rise and a biexponential decay, with mean time constants of 2 and 9 msec. The mean quantal conductance change, determined directly at reduced extracellular Ca2+/Mg2+concentration ratios, was 1.7 nS. Quantal release at the BC–GC synapse occurred with short delay and was highly synchronized. Analysis of IPSC peak amplitudes and numbers of failures by multiple probability compound binomial analysis indicated that synaptic transmission at the BC–GC synapse involves three to seven release sites, each of which releases transmitter with high probability (∼0.5 in 2 mMCa2+/1 mM Mg2+). Unitary BC–GC IPSCs showed paired-pulse depression (PPD); maximal depression, measured for 10 msec intervals, was 37%, and recovery from depression occurred with a time constant of 2 sec. Paired-pulse depression was mainly presynaptic in origin but appeared to be independent of previous release. Synaptic transmission at the BC–GC synapse showed frequency-dependent depression, with half-maximal decrease at 5 Hz after a series of 1000 presynaptic action potentials. The relative stability of transmission at the BC–GC synapse is consistent with a model in which an activity-dependent gating mechanism reduces release probability and thereby prevents depletion of the releasable pool of synaptic vesicles. Thus several mechanisms converge on the generation of powerful and sustained transmission at interneuron–principal neuron synapses in hippocampal circuits.},
author = {Kraushaar, Udo and Peter Jonas},
journal = {Journal of Neuroscience},
number = {15},
pages = {5594 -- 5607},
publisher = {Society for Neuroscience},
title = {{Efficacy and stability of quantal GABA release at a hippocampal interneuron-principal neuron synapse}},
volume = {20},
year = {2000},
}