@article{2197,
abstract = {We present an analytic model of the refractive index for matter waves propagating through atomic or molecular gases. The model, which combines the Wentzel-Kramers-Brillouin (WKB) treatment of the long-range attraction with the Fraunhofer model treatment of the short-range repulsion, furnishes a refractive index in compelling agreement with recent experiments of Jacquey [Phys. Rev. Lett.PRLTAO0031-900710.1103/PhysRevLett.98.240405 98, 240405 (2007)] on Li atom matter waves passing through dilute noble gases. We show that the diffractive contribution, which arises from scattering by a two-dimensional "hard core" of the potential, is essential for obtaining a correct imaginary part of the refractive index.},
author = {Mikhail Lemeshko and Friedrich, Břetislav},
journal = {Physical Review A - Atomic, Molecular, and Optical Physics},
number = {2},
publisher = {American Physical Society},
title = {{Multiple scattering of matter waves: An analytic model of the refractive index for atomic and molecular gases}},
doi = {10.1103/PhysRevA.82.022711},
volume = {82},
year = {2010},
}
@inproceedings{488,
abstract = {Streaming string transducers [1] define (partial) functions from input strings to output strings. A streaming string transducer makes a single pass through the input string and uses a finite set of variables that range over strings from the output alphabet. At every step, the transducer processes an input symbol, and updates all the variables in parallel using assignments whose right-hand-sides are concatenations of output symbols and variables with the restriction that a variable can be used at most once in a right-hand-side expression. It has been shown that streaming string transducers operating on strings over infinite data domains are of interest in algorithmic verification of list-processing programs, as they lead to PSPACE decision procedures for checking pre/post conditions and for checking semantic equivalence, for a well-defined class of heap-manipulating programs. In order to understand the theoretical expressiveness of streaming transducers, we focus on streaming transducers processing strings over finite alphabets, given the existence of a robust and well-studied class of "regular" transductions for this case. Such regular transductions can be defined either by two-way deterministic finite-state transducers, or using a logical MSO-based characterization. Our main result is that the expressiveness of streaming string transducers coincides exactly with this class of regular transductions. },
author = {Alur, Rajeev and Cerny, Pavol},
location = {Chennai, India},
pages = {1 -- 12},
publisher = {Schloss Dagstuhl - Leibniz-Zentrum für Informatik},
title = {{Expressiveness of streaming string transducers}},
doi = {10.4230/LIPIcs.FSTTCS.2010.1},
volume = {8},
year = {2010},
}
@inproceedings{489,
abstract = {Graph games of infinite length are a natural model for open reactive processes: one player represents the controller, trying to ensure a given specification, and the other represents a hostile environment. The evolution of the system depends on the decisions of both players, supplemented by chance. In this work, we focus on the notion of randomised strategy. More specifically, we show that three natural definitions may lead to very different results: in the most general cases, an almost-surely winning situation may become almost-surely losing if the player is only allowed to use a weaker notion of strategy. In more reasonable settings, translations exist, but they require infinite memory, even in simple cases. Finally, some traditional problems becomes undecidable for the strongest type of strategies.},
author = {Cristau, Julien and David, Claire and Horn, Florian},
booktitle = {Proceedings of GandALF 2010},
location = {Minori, Amalfi Coast, Italy},
pages = {30 -- 39},
publisher = {Open Publishing Association},
title = {{How do we remember the past in randomised strategies? }},
doi = {10.4204/EPTCS.25.7},
volume = {25},
year = {2010},
}
@misc{5388,
abstract = {We present an algorithmic method for the synthesis of concurrent programs that are optimal with respect to quantitative performance measures. The input consists of a sequential sketch, that is, a program that does not contain synchronization constructs, and of a parametric performance model that assigns costs to actions such as locking, context switching, and idling. The quantitative synthesis problem is to automatically introduce synchronization constructs into the sequential sketch so that both correctness is guaranteed and worst-case (or average-case) performance is optimized. Correctness is formalized as race freedom or linearizability.
We show that for worst-case performance, the problem can be modeled
as a 2-player graph game with quantitative (limit-average) objectives, and
for average-case performance, as a 2 1/2 -player graph game (with probabilistic transitions). In both cases, the optimal correct program is derived from an optimal strategy in the corresponding quantitative game. We prove that the respective game problems are computationally expensive (NP-complete), and present several techniques that overcome the theoretical difficulty in cases of concurrent programs of practical interest.
We have implemented a prototype tool and used it for the automatic syn- thesis of programs that access a concurrent list. For certain parameter val- ues, our method automatically synthesizes various classical synchronization schemes for implementing a concurrent list, such as fine-grained locking or a lazy algorithm. For other parameter values, a new, hybrid synchronization style is synthesized, which uses both the lazy approach and coarse-grained locks (instead of standard fine-grained locks). The trade-off occurs because while fine-grained locking tends to decrease the cost that is due to waiting for locks, it increases cache size requirements.},
author = {Chatterjee, Krishnendu and Cerny, Pavol and Henzinger, Thomas A and Radhakrishna, Arjun and Singh, Rohit},
issn = {2664-1690},
pages = {17},
publisher = {IST Austria},
title = {{Quantitative synthesis for concurrent programs}},
doi = {10.15479/AT:IST-2010-0004},
year = {2010},
}
@misc{5389,
abstract = {Boolean notions of correctness are formalized by preorders on systems. Quantitative measures of correctness can be formalized by real-valued distance functions between systems, where the distance between implementation and specification provides a measure of “fit” or “desirability.” We extend the simulation preorder to the quantitative setting, by making each player of a simulation game pay a certain price for her choices. We use the resulting games with quantitative objectives to define three different simulation distances. The correctness distance measures how much the specification must be changed in order to be satisfied by the implementation. The coverage distance measures how much the im- plementation restricts the degrees of freedom offered by the specification. The robustness distance measures how much a system can deviate from the implementation description without violating the specification. We consider these distances for safety as well as liveness specifications. The distances can be computed in polynomial time for safety specifications, and for liveness specifications given by weak fairness constraints. We show that the distance functions satisfy the triangle inequality, that the distance between two systems does not increase under parallel composition with a third system, and that the distance between two systems can be bounded from above and below by distances between abstractions of the two systems. These properties suggest that our simulation distances provide an appropriate basis for a quantitative theory of discrete systems. We also demonstrate how the robustness distance can be used to measure how many transmission errors are tolerated by error correcting codes.},
author = {Cerny, Pavol and Henzinger, Thomas A and Radhakrishna, Arjun},
issn = {2664-1690},
pages = {24},
publisher = {IST Austria},
title = {{Simulation distances}},
doi = {10.15479/AT:IST-2010-0003},
year = {2010},
}