TY - CONF
AB - We propose an incremental workflow for the verification of parameterized systems modeled as symmetric networks of timed automata. Starting with a small number of timed automata in the network, a safety property is verified using IC3, a state-of-the-art algorithm based on induction.The result of the verification, an inductive strengthening, is reused proposing a candidate inductive strengthening for a larger network.If the candidate is valid, our main theorem states that the safety property holds for all sizes of the network of timed automata. Otherwise the number of automata is increased and the next iteration is started with a new run of IC3.We propose and thoroughly examine optimizations to our workflow, e.g. Feedback mechanisms to speed up the run of IC3.
AU - Isenberg, Tobias
ID - 285
T2 - Proceedings of the 15th International Conference on Application of Concurrency to System Design (ACSD)
TI - Incremental Inductive Verification of Parameterized Timed Systems
ER -
TY - GEN
AU - Sosniak, Martin
ID - 297
TI - Evaluation of Pairing Optimization for Embedded Platforms
ER -
TY - CONF
AB - Services are self-contained software components that can beused platform independent and that aim at maximizing software reuse. Abasic concern in service oriented architectures is to measure the reusabilityof services. One of the most important qualities is the functionalreusability, which indicates how relevant the task is that a service solves.Current metrics for functional reusability of software, however, have verylittle explanatory power and do not accomplish this goal.This paper presents a new approach to estimate the functional reusabilityof services based on their relevance. To this end, it denes the degreeto which a service enables the execution of other services as its contri-bution. Based on the contribution, relevance of services is dened as anestimation for their functional reusability. Explanatory power is obtainedby normalizing relevance values with a reference service. The applicationof the metric to a service test set conrms its supposed capabilities.
AU - Mohr, Felix
ID - 324
T2 - Proceedings of the 14th International Conference on Software Reuse (ICSR)
TI - A Metric for Functional Reusability of Services
ER -
TY - JOUR
AB - We consider strategic games in which each player seeks a mixed strategy to minimize her cost evaluated by a concave valuation V (mapping probability distributions to reals); such valuations are used to model risk. In contrast to games with expectation-optimizer players where mixed equilibria always exist (Nash 1950; Nash Ann. Math. 54, 286–295, 1951), a mixed equilibrium for such games, called a V-equilibrium, may fail to exist, even though pure equilibria (if any) transfer over. What is the exact impact of such valuations on the existence, structure and complexity of mixed equilibria? We address this fundamental question in the context of expectation plus variance, a particular concave valuation denoted as RA, which stands for risk-averse; so, variance enters as a measure of risk and it is used as an additive adjustment to expectation. We obtain the following results about RA-equilibria:A collection of general structural properties of RA-equilibria connecting to (i) E-equilibria and Var-equilibria, which correspond to the expectation and variance valuations E and Var, respectively, and to (ii) other weaker or incomparable properties such as Weak Equilibrium and Strong Equilibrium. Some of these structural properties imply quantitative constraints on the existence of mixed RA-equilibria.A second collection of (i) existence, (ii) equivalence and separation (with respect to E-equilibria), and (iii) characterization results for RA-equilibria in the new class of player-specific scheduling games. We provide suitable examples with a mixed RA-equilibrium that is not an E-equilibrium and vice versa.A purification technique to transform a player-specific scheduling game on two identical links into a player-specific scheduling game on two links so that all non-pure RA-equilibria are eliminated while no new pure equilibria are created; so, a particular player-specific scheduling game on two identical links with no pure equilibrium yields a player-specific scheduling game with no RA-equilibrium (whether mixed or pure). As a by-product, the first PLS-completeness result for the computation of RA-equilibria follows.
AU - Monien, Burkhard
AU - Mavronicolas, Marios
ID - 398
IS - 3
JF - Theory of Computing Systems
TI - Minimizing Expectation Plus Variance
VL - 57
ER -
TY - JOUR
AB - We analyse an InAs/GaAs-based electric ﬁeld tunable single quantum dot diode with a thin tunnelling barrier between a
buried n þ -back contact and a quantum dot layer. In voltage- dependent photoluminescence measurements, we observe rich signatures from spatially direct and indirect transitions from the wetting layer and from a single quantum dot. By analysing the Stark effect, we show that the indirect transitions result from a recombination between conﬁned holes in the wetting or quantum dot layer with electrons from the edge of the Fermi sea in the back contact. Using a 17 nm tunnel barrier which provides comparably weak tunnel coupling allowed us to observe clear signatures of direct and corresponding indirect lines for a series of neutral and positively charged quantum dot states.
AU - Rai, Ashish K.
AU - Gordon, Simon
AU - Ludwig, Arne
AU - Wieck, Andreas D.
AU - Zrenner, Artur
AU - Reuter, Dirk
ID - 4276
IS - 3
JF - physica status solidi (b)
KW - excitons
KW - GaAs
KW - InAs
KW - quantum dots
KW - spatially indirect transitions
KW - Stark shift
SN - 0370-1972
TI - Spatially indirect transitions in electric field tunable quantum dot diodes
VL - 253
ER -
TY - GEN
AB - Die Erfindung betrifft ein Verfahren zur Präparation einer Besetzungsinversion in einem Quantensystem (Q) mittels Mehrpulsanregung, wobei ein Quantensystem (Q) umfassend wenigstens einen Quantenpunkt mit zwei orthogonalen Zuständen (/X>, /Y>), insbesondere die mit zueinander orthogonalen Polarisationen (P1, P2) optisch anregbar sind, mit einem ersten Laserpuls (L1) beleuchtet wird, welcher zur resonanten Anregung des ersten (/Y>) der zwei Zustände (/X>, /Y>) eingestellt wird und zeitlich nachfolgend mit einem zweiten Laserpuls (L2) beleuchtet wird, der zur resonanten Anregung des zweiten (/X>) der zwei Zustände (/X>, /Y>) eingestellt wird.
AU - Zrenner, Artur
AU - Förstner, Jens
AU - Mantei, Dirk
ID - 4360
KW - tet_topic_qd
TI - A process for the preparation of a population inversion in a quantum system using multi-pulse excitation
ER -
TY - CONF
AU - Klör, Benjamin
AU - Beverungen, Daniel
AU - Bräuer, Sebastian
AU - Plenter, Florian
AU - Monhof, Markus
ID - 3285
T2 - Proceedings of the Twenty-Third European Conference on Information Systems (ECIS 2015)
TI - A Market for Trading Used Electric Vehicle Batteries — Theoretical Foundations and Information Systems
ER -
TY - JOUR
AB - In this paper we consider an extended variant of query learning where the hidden concept is embedded in some Boolean circuit. This additional processing layer modifies query arguments and answers by fixed transformation functions which are known to the learner. For this scenario, we provide a characterization of the solution space and an ordering on it. We give a compact representation of the minimal and maximal solutions as quantified Boolean formulas and we adapt the original algorithms for exact learning of specific classes of propositional formulas.
AU - Bubeck, Uwe
AU - Kleine Büning, Hans
ID - 3343
JF - Artificial Intelligence
KW - Query learning
KW - Propositional logic
SN - 0004-3702
TI - Learning Boolean Specifications
ER -
TY - CONF
AU - Schwichtenberg, Simon
AU - Engels, Gregor
ID - 40
T2 - Proceedings of the 10th International Workshop on Ontology Matching collocated with the 14th International Semantic Web Conference (ISWC 2015), Bethlehem, PA, USA, October 12, 2015.
TI - RSDL workbench results for OAEI 2015
VL - 1545
ER -
TY - JOUR
AB - We investigate the formation of cubic GaN quantum dots (QDs) on pseudomorphic strained cubic AlN layers on
3C-SiC (001) substrates grown by means of molecular beam epitaxy. Surface morphologies of various QD sizes
and densities were obtained from uncapped samples by atomic force microscopy. These results were correlated
with similar but capped samples by photoluminescence experiments. The QD density varies by one order of
magnitude from ~1x10^10 cm^-2 to ~1x10^11 cm^-2 as a function of the GaN coverage on the surface. The initial layer
thickness for the creation of cubic GaN QDs on cubic AlN was obtained to 1.95 monolayers by a comparison
between the experimental results and an analytical model. Our results reveal the strain-driven Stranski-Krastanov
growth mode as the main formation process of the cubic GaN QDs.
AU - Bürger, M.
AU - Lindner, Jörg
AU - Reuter, Dirk
AU - As, D. J.
ID - 4024
IS - 4-5
JF - physica status solidi (c)
SN - 1862-6351
TI - Investigation of cubic GaN quantum dots grown by the Stranski-Krastanov process
VL - 12
ER -