Search

The class of Boolean combinations of tree languages recognized by deterministic top-down tree automata (also known as deterministic root-to-frontier automata) is studied. The problem of determining for a given regular tree language whether it belongs to this class is open. We provide some progress by two results: First, a characterization of this class by a natural extension of deterministic top-down tree automata is presented, and as an application we obtain a convenient method to show that certain regular tree languages are outside this class. In the second result, it is shown that, for fixed $k$, it is decidable whether a regular tree language is a Boolean combination of $k$ tree languages recognized by deterministic top-down tree automata., Comment: This is a preprint of a paper published in a special issue dedicated to the memory of Magnus Steinby in the International Journal of Foundations of Computer Science. Compared to the published journal version, reference [8] has been added in a comment at the end of the introduction

Logical Methods in Computer Science ist eine wissenschaftsgesteuerte Diamond-Open-Access-Zeitschrift im Gebiet der Theoretischen Informatik. Wir berichten über die Entwicklung der Zeitschrift seit ihrer Gründung in 2004 und stellen Herausforderung und Erfolgsfaktoren dar., Logical Method in Computer Science is a scholar-led diamond open access journal in theoretical computer science. We report on the development of the journal since its foundation in 2004 discuss challenges and success factors., Peer Reviewed

Infinite games (in the form of Gale-Stewart games) are studied where a play is a sequence of natural numbers chosen by two players in alternation, the winning condition being a subset of the Baire space $\omega^\omega$. We consider such games defined by a natural kind of parity automata over the alphabet $\mathbb{N}$, called $\mathbb{N}$-MSO-automata, where transitions are specified by monadic second-order formulas over the successor structure of the natural numbers. We show that the classical B\"uchi-Landweber Theorem (for finite-state games in the Cantor space $2^\omega$) holds again for the present games: A game defined by a deterministic parity $\mathbb{N}$-MSO-automaton is determined, the winner can be computed, and an $\mathbb{N}$-MSO-transducer realizing a winning strategy for the winner can be constructed., Comment: Updated header on title page. 26 pages, 1 figure

Um Barrique-Weine herzustellen, werden neben der Fasslagerung auch Eichenholzspäne (Chips) verwendet. Es ist noch unklar, welche Aromastoffe ihre Barrique-Note hervorrufen. In Wasser/Ethanol-Extrakten aus stark getoasteten Chips konnten durch Anwendung des Sensomics-Verfahrens 39 geruchsaktive Substanzen charakterisiert und durch Stabilisotopenassays quantifiziert werden, mit hohen Aromawerten von cis-Whiskylacton, Vanillin und 2-Methoxyphenol. Das Aroma der Extrakte und das von mit Chips gelagertem Jungwein – nach Angleichung der Konzentrationen von 12 Aromastoffen in Jungwein ohne Chips auf die im mit Chips versetzten Wein gemessenen Konzentrationen – konnten erfolgreich simuliert werden., In addition to the traditionally applied barrique barrel storage, oak wood chips are used to produce wines with oak wood aromas. It is still unclear, which aroma compounds evoke the barrique note of those wines. In hydro-alcoholic extracts from heavily toasted chips, 39 aroma compounds were characterized by the Sensomics concept and quantified by stable isotope assays, with cis-oak lactone, 2 methoxyphenol and vanillin and featuring the highest odour activity values. The aroma of the extracts could be simulated successfully. The simulation of the aroma of oak treated Jungwein succeeded after adjusting the concentrations of 12 substances in wine without chips to the concentrations measured in the oak treated wine.

Um Barrique-Weine herzustellen, werden neben der Fasslagerung auch Eichenholzspäne (Chips) verwendet. Es ist noch unklar, welche Aromastoffe ihre Barrique-Note hervorrufen. In Wasser/Ethanol-Extrakten aus stark getoasteten Chips konnten durch Anwendung des Sensomics-Verfahrens 39 geruchsaktive Substanzen charakterisiert und durch Stabilisotopenassays quantifiziert werden, mit hohen Aromawerten von cis-Whiskylacton, Vanillin und 2-Methoxyphenol. Das Aroma der Extrakte und das von mit Chips gelagertem Jungwein – nach Angleichung der Konzentrationen von 12 Aromastoffen in Jungwein ohne Chips auf die im mit Chips versetzten Wein gemessenen Konzentrationen – konnten erfolgreich simuliert werden., In addition to the traditionally applied barrique barrel storage, oak wood chips are used to produce wines with oak wood aromas. It is still unclear, which aroma compounds evoke the barrique note of those wines. In hydro-alcoholic extracts from heavily toasted chips, 39 aroma compounds were characterized by the Sensomics concept and quantified by stable isotope assays, with cis-oak lactone, 2 methoxyphenol and vanillin and featuring the highest odour activity values. The aroma of the extracts could be simulated successfully. The simulation of the aroma of oak treated Jungwein succeeded after adjusting the concentrations of 12 substances in wine without chips to the concentrations measured in the oak treated wine.

Thesis: S.M. in Aerospace Engineering, Massachusetts Institute of Technology, Department of Aeronautics and Astronautics, 2017., Cataloged from PDF version of thesis., Includes bibliographical references (pages 73-75)., In modern combat, helmets play a vital role in protecting the head. Before being delivered to the soldier, combat helmets undergo a series of tests to determine their threat mitigation performance. During ballistic testing, current combat helmet test protocols use clay to record the helmet backface deformation signature, which is used as an important criterion to measure the helmet effectiveness at preventing head injury. However, according to a recent review of the test protocols by the National Research Council, the current test protocols establish no correlation between the backface deformation signature in the clay and head/brain injury. Modeling and simulation are valuable tools to complement experimental helmet testing and can assist in establishing this correlation. The objective of this work is to develop a comprehensive computational framework for the simulation and analysis of the helmet test protocols. In order to achieve this objective the following steps were performed. First, a suitable constitutive model for ballistic clay based on Cam-Clay theory was implemented into the computational framework SUMMIT. Next, a detailed model of the headform used in the helmet test protocols was created. The model was developed using the scanned geometry data from the experimental headform and includes the metal frame, Roma Plastilina clay and a full combat helmet with pads. Subsequently, ballistic impact simulations using the model were performed and the backface deformation signatures of the helmet are recorded in the clay. The results from these impact simulations are compared to results from impact simulations on a human head model. The intracranial pressure distribution in the human head is compared to the pressure distribution in the clay and the differences in the responses are highlighted. We conclude that the proposed computational framework is an effective tool of the analysis of helmet test protocols, which could be used to establish the correlation with in, by Thomas Wolfgang Fronk., S.M. in Aerospace Engineering

[no abstract]

We solve a generalized version of Church's Synthesis Problem where a play is given by a sequence of natural numbers rather than a sequence of bits; so a play is an element of the Baire space rather than of the Cantor space. Two players Input and Output choose natural numbers in alternation to generate a play. We present a natural model of automata ("N-memory automata") equipped with the parity acceptance condition, and we introduce also the corresponding model of "N-memory transducers". We show that solvability of games specified by N-memory automata (i.e., existence of a winning strategy for player Output) is decidable, and that in this case an N-memory transducer can be constructed that implements a winning strategy for player Output., Comment: In Proceedings Cassting'16/SynCoP'16, arXiv:1608.00177

In this report, the program, research issues, and results of Dagstuhl Seminar 15061 "Non-Zero-Sum-Games and Control" are described. The area of non-zero-sum games is addressed in a wide range of topics: multi-player games, partial-observation games, quantitative game models, and - as a special focus - connections with control engineering (supervisory control).

This paper studies the innovation strategy of Russian Railways, the biggest transport company in the world. Russian Railways has chosen a strategy of international science, technology and innovation (STI) cooperation outside their own network. This strategy is a novel approach for Russian State-owned enterprises (SOE). Based on the analysis of innovation development program and interviews with managers, the paper studies the company’s experience with the chosen strategy. Thereby, the paper enhances the understanding of innovation processes in major public service companies which are crucial for the socio-economic processes inside and outside national boundaries.

We show the existence and effective computability of optimal winning strategies for request-response games in case the quality of a play is measured by the limit superior of the mean accumulated waiting times between requests and their responses., Comment: The present paper is a revised version with simplified proofs of results announced in the conference paper of the same name presented at ATVA 2008, which in turn extended results of the third author's dissertation

We reviewed the output of research and innovation cooperation between Russia and the US, including publications and patents, in the four prospective areas of energy efficiency and renewable energy during 2007-2011. Joint US-Russia research groups appear to focus primarily on hydrogen energy (fuel cells), followed by solar photovoltaics. The upcoming areas of smart grid and biofuels were left out entirely both from research and innovation collaboration. Russian patents in green energy technologies registered in the US are very low in comparison to those from Japan, Korea, and China.

Ein der Biologie zugrunde liegender Prozess ist die Fortpflanzung. Einzeller wachsen dazu heran und teilen sich. Grundlage hierfür sind ausreichend Nahrung und Ressourcen, um die eigene Masse und alle Zellbestandteile, insbesondere die DNS, zu verdoppeln. Fehler bei der Wachstumsregulation oder der DNS-Verdopplung können schwerwiegende Folgen haben und stehen beim Menschen im Zusammenhang z.B. mit Krebs. In dieser Arbeit werden mathematische Modelle für die Mechanismen zur Wachstumsregulierung und DNS-Verdopplung in der Bäckerhefe, Saccharomyces cerevisiae, vorgestellt. Modellierung kann entscheident zum Verstehen von komplexen, dynamischen Systemen beitragen. Wir haben ein Modell für Einzellerwachstum entwickelt und leiten das Wachstumsverhalten von Zellkulturen von diesem Modell, mittels einer hierfür programmierten Software, ab. Außerdem haben wir ein Model für die Verdopplung der DNS entwickelt, um Auswirkungen verschiedener Aktivierungsmuster auf die Replikation zu testen. Zusätzlich wurde die Verlängerung entstehender DNS Stränge, Elongation, mit einem detaillierten, stochastischen Modell untersucht. Wir haben unsere Ergebnisse zur DNS-Verdopplung mit einer abschließenden Untersuchung ergänzt, die funktionelle Beziehungen von Genen aufzeigt, welche sich in der Nähe von Aktivierungsstellen der Verdopplung befinden. Folgende Einsichten in die komplexe Koordination von Wachstum und Teilung wurden gewonnen: (i) Wachstumskontrolle ist eine inhärente Eigenschaft von Hefezellpopulationen, welche weder Signale noch Messmechanismen benötigt, (ii) DNS Verdopplung ist robuster in kleinen Chromosomen mit hoher Dichte an Aktivierungsstellen, (iii) Elongation ist weitgehend uniform, weicht aber an genau definierten Stellen signifikant ab und (iv) katabole Gene häufen sich nahe der frühen Aktivierungsstellen und anabole Gene nahe der späten. Unsere Ergebnisse tragen zum Verständniss von zellulären Mechanismen zur Wachstumskontrolle und DNS-Verdopplung bei., One of the most fundamental processes in biology is reproduction. To achieve this, single cellular organisms grow, proliferate and divide. The prerequisite for this is acquiring sufficient resources to double size and cellular components, most importantly the DNA. Defects in either sufficient gain in size or chromosomal doubling can be severe for the organism and have been related to diseases in humans, such as cancer. Therefore, the cell has developed sophisticated regulatory mechanisms to control the orderly fashion of growth and duplication. We have developed mathematical models to study systemic properties of size control and DNA replication in the premier eukaryotic model organism Saccharomyces cerevisiae. Modeling can help understanding the complex nature of dynamic systems. We provide a single cell model to explore size control. We deduced population behavior from the single cell model through multi-cell simulations using a tailor-made software. Also, we implemented an algorithm that simulates the DNA replication process to test the impact of different replication activation patterns. Additionally, elongation dynamics were assessed with a fine-grained stochastic model for the replication machinery motion. We complemented our analysis of DNA replication by studying the functional association of genes and replication origins. Our systems-level analysis reveals novel insights into the coordination of growth and division, namely that (i) size regulation is an intrinsic property of yeast cell populations and not due to signaling or size sensing, (ii) DNA replication is more robust in small chromosomes with high origin density, (iii) the elongation process is strongly biased at distinct locations in the genome and (iv) catabolic genes are over-represented near early origins and anabolic genes near late origins. Our results contribute to explaining mechanisms of size control and DNA replication.

We study variants of regular infinite games where the strict alternation of moves between the two players is subject to modifications. The second player may postpone a move for a finite number of steps, or, in other words, exploit in his strategy some lookahead on the moves of the opponent. This captures situations in distributed systems, e.g. when buffers are present in communication or when signal transmission between components is deferred. We distinguish strategies with different degrees of lookahead, among them being the continuous and the bounded lookahead strategies. In the first case the lookahead is of finite possibly unbounded size, whereas in the second case it is of bounded size. We show that for regular infinite games the solvability by continuous strategies is decidable, and that a continuous strategy can always be reduced to one of bounded lookahead. Moreover, this lookahead is at most doubly exponential in the size of a given parity automaton recognizing the winning condition. We also show that the result fails for non-regular gamesxwhere the winning condition is given by a context-free omega-language., Comment: LMCS submission

Die homogene Kompressionszündung von hochsiedenden, zündwilligen Kraftstoffen wie handelsüblichem Diesel neigt zu einer frühen Zündung und bei hoher Last zu hohen Druckanstiegsraten, sowie Ruß- und Stickoxidemissionen. Sämtliche dieser Nachteile können durch die zusätzliche Einbringung von Wasser gemildert werden, wie experimentell und numerisch gezeigt wurde. Eine getrennte Wasser-Einspritzung senkt besonders effektiv den Druckanstieg, sowie die Rußemissionen. Emulsionen haben durch die höhere räumliche Übereinstimmung von Kraftstoff und Wasser Vorteile bei der Verschleppung der Zündung sowie Reduktion der Stickoxidemissionen., The homogeneous charge compression ignition of diesel fuel tends to an early ignition as well as high pressure rise rates, soot and NOx-emissions at high load. The addition of water acts in a positive way to all of these shortcomings as demonstrated experimentally and numerically. The seperate water injection shows advantages in reducing the pressure rise rates as well as the soot emissions. In contrast, emulsions delay ignition and reduce NOx-emissions more effective due to the better overlapping of fuel and water.

The aim of the seminar was to discuss and systematize the recent fast progress in automata theory and to identify important directions for future research. For this, the seminar brought together more than 40 researchers from automata theory and related fields of applications. We had 19 talks of 30 minutes and 5 one-hour lectures leaving ample room for discussions. In the following we describe the topics in more detail.

From 12.12.2010 to 17.12.2010, the Dagstuhl Seminar 10501 ``Advances and Applications of Automata on Words and Trees'' was held in Schloss Dagstuhl~--~Leibniz Center for Informatics. During the seminar, several participants presented their current research, and ongoing work and open problems were discussed. Abstracts of the presentations given during the seminar as well as abstracts of seminar results and ideas are put together in this paper. The first section describes the seminar topics and goals in general. Links to extended abstracts or full papers are provided, if available.

Seminar: 10501 - Advances and Applications of Automata on Words and Trees. The aim of the seminar was to discuss and systematize the recent fast progress in automata theory and to identify important directions for future research. For this, the seminar brought together more than 40 researchers from automata theory and related fields of applications. We had 19 talks of 30 minutes and 5 one-hour lectures leaving ample room for discussions. In the following we describe the topics in more detail.

From 12.12.2010 to 17.12.2010, the Dagstuhl Seminar 10501 "Advances and Applications of Automata on Words and Trees" was held in Schloss Dagstuhl - Leibniz Center for Informatics. During the seminar, several participants presented their current research, and ongoing work and open problems were discussed. Abstracts of the presentations given during the seminar as well as abstracts of seminar results and ideas are put together in this paper. The first section describes the seminar topics and goals in general. Links to extended abstracts or full papers are provided, if available.

Die homogene Kompressionszündung von hochsiedenden, zündwilligen Kraftstoffen wie handelsüblichem Diesel neigt zu einer frühen Zündung und bei hoher Last zu hohen Druckanstiegsraten, sowie Ruß- und Stickoxidemissionen. Sämtliche dieser Nachteile können durch die zusätzliche Einbringung von Wasser gemildert werden, wie experimentell und numerisch gezeigt wurde. Eine getrennte Wasser-Einspritzung senkt besonders effektiv den Druckanstieg, sowie die Rußemissionen. Emulsionen haben durch die höhere räumliche Übereinstimmung von Kraftstoff und Wasser Vorteile bei der Verschleppung der Zündung sowie Reduktion der Stickoxidemissionen., The homogeneous charge compression ignition of diesel fuel tends to an early ignition as well as high pressure rise rates, soot and NOx-emissions at high load. The addition of water acts in a positive way to all of these shortcomings as demonstrated experimentally and numerically. The seperate water injection shows advantages in reducing the pressure rise rates as well as the soot emissions. In contrast, emulsions delay ignition and reduce NOx-emissions more effective due to the better overlapping of fuel and water.

A game-theoretic model for the study of dynamic networks is analyzed. The model is motivated by communication networks that are subject to failure of nodes and where the restoration needs resources. The corresponding two-player game is played between "Destructor" (who can delete nodes) and "Constructor" (who can restore or even create nodes under certain conditions). We also include the feature of information flow by allowing Constructor to change labels of adjacent nodes. As objective for Constructor the network property to be connected is considered, either as a safety condition or as a reachability condition (in the latter case starting from a non-connected network). We show under which conditions the solvability of the corresponding games for Constructor is decidable, and in this case obtain upper and lower complexity bounds, as well as algorithms derived from winning strategies. Due to the asymmetry between the players, safety and reachability objectives are not dual to each other and are treated separately., Comment: In Proceedings GandALF 2011, arXiv:1106.0814

We provide decidability and undecidability results on the model-checking problem for infinite tree structures. These tree structures are built from sequences of elements of infinite relational structures. More precisely, we deal with the tree iteration of a relational structure M in the sense of Shelah-Stupp. In contrast to classical results where model-checking is shown decidable for MSO-logic, we show decidability of the tree model-checking problem for logics that allow only path quantifiers and chain quantifiers (where chains are subsets of paths), as they appear in branching time logics; however, at the same time the tree is enriched by the equal-level relation (which holds between vertices u, v if they are on the same tree level). We separate cleanly the tree logic from the logic used for expressing properties of the underlying structure M. We illustrate the scope of the decidability results by showing that two slight extensions of the framework lead to undecidability. In particular, this applies to the (stronger) tree iteration in the sense of Muchnik-Walukiewicz., Comment: In Proceedings INFINITY 2011, arXiv:1111.2678

We present a game-theoretic framework for modeling and solving routing problems in dynamically changing networks. The model covers the aspects of reactivity and non-termination, and it is motivated by quality-of-service provisioning in cognitive radio networks where data transmissions are interfered by primary systems. More precisely, we propose an infinite two-player game where a routing agent has to deliver network packets to their destinations while an adversary produces demands by generating packets and blocking connections. We obtain results on the status of basic problems, by showing principal limitations to solvability of routing requirements and singling out cases with algorithmic solutions., QC 20140102

From June 29, 2008, to July 4, 2008, the Dagstuhl Seminar 08271 ``Topological and Game-Theoretic Aspects of Infinite Computations'' was held in the International Conference and Research Center (IBFI), Schloss Dagstuhl. During the seminar, many participants presented their current research, and ongoing work and open problems were discussed. Abstracts of the presentations given during the seminar as well as abstracts of seminar results and ideas are put together in this paper. The first section describes the seminar topics and goals in general. Links to extended abstracts or full papers are provided, if available.

The theory of the infinite behaviour of continuously operating computing devices is of primary importance for several branches of theoretical and practical computer science. In particular, it is fundamental for the verification and synthesis of reactive systems like microprocessors or operating systems, for the understanding of dataflow computation, and for the development of adequate mathematical foundations for exact real computation. The seminar brought together researchers from many different disciplines who are working on theoretical or practical aspects of infinite computations. In this summary we describe the topics, the goals, and the contributions of the seminar.

Formal verification using the model checking paradigm has to deal with two aspects: The system models are structured, often as products of components, and the specification logic has to be expressive enough to allow the formalization of reachability properties. The present paper is a study on what can be achieved for infinite transition systems under these premises. As models we consider products of infinite transition systems with different synchronization constraints. We introduce finitely synchronized transition systems, i.e. product systems which contain only finitely many (parameterized) synchronized transitions, and show that the decidability of FO(R), first-order logic extended by reachability predicates, of the product system can be reduced to the decidability of FO(R) of the components. This result is optimal in the following sense: (1) If we allow semifinite synchronization, i.e. just in one component infinitely many transitions are synchronized, the FO(R)-theory of the product system is in general undecidable. (2) We cannot extend the expressive power of the logic under consideration. Already a weak extension of first-order logic with transitive closure, where we restrict the transitive closure operators to arity one and nesting depth two, is undecidable for an asynchronous (and hence finitely synchronized) product, namely for the infinite grid., Comment: 18 pages

From 12.06.05 to 17.06.2005 the Dagstuhl Seminar 05241 ``Synthesis and Planning'' was held in the International Conference and Research Center (IBFI), Schloss Dagstuhl. During the seminar, several participants presented their current research, and ongoing work and open problems were discussed. Abstracts of the presentations given during the seminar as well as abstracts of seminar results and ideas are put together in this paper. The first section describes the seminar topics and goals in general. Links to extended abstracts or full papers are provided, if available.

This seminar has brought together researchers working in two complementary fields: automatic synthesis of (control) programs, and methods for devising planning algorithms in artifical intelligence (AI). This combines a strong thread of current research in automata theory with an area of possible but so far unexplored applications.

The problem of relating inter-agent and intra-agent behavioral specifications is investigated. These two views are complimentary, in that the former is closer to scenario-based user requirements whereas the latter is design-oriented. We use a graphical, user-friendly and very simple language as inter-agent specification language: Live Sequence Charts (LSC). LSC is presented and its properties are investigated: it is highly succinct, but inexpressive. There are essentially two ways to relate inter-agent and intra-agent specifications: (i) by checking that an intra-agent specification is correct with respect to some LSC specification and (ii) by automatically building an intra-agent specification from an LSC specification. Several variants of these problems exist: closed/open systems and centralized/distributed systems. We give inefficient but optimal algorithms solving all problems, besides synthesis of open distributed systems, which we show is undecidable. All the problems considered are difficult, even for a very restricted subset of LSCs, without alternatives, interleaving, conditions nor loops. We investigate the cost of extending the language with control flow constructs, conditions, real-time and symbolic instances. An implementation of the algorithms is proposed. The applicability of the language is illustrated on a real-world case study., (DOCSC06)--FUNDP, 2005

We investigate bottom-up and top-down deterministic automata on unranked trees. We show that for an appropriate definition of bottom-up deterministic automata it is possible to minimize the number of states efficiently and to obtain a unique canonical representative of the accepted tree language. For top-down deterministic automata it is well known that they are less expressive than the non-deterministic ones. By generalizing a corresponding proof from the theory of ranked tree automata we show that it is decidable whether a given regular language of unranked trees can be recognized by a top-down deterministic automaton. The standard deterministic top-down model is slightly weaker than the model we use, where at each node the automaton can scan the sequence of the labels of its successors before deciding its next move.

Daselbst gehalten/ und auff Begehren zum Druck ubergeben/ Von Wolffgango Thoma, Pfarrern zu Beuna

Daselbst gehalten/ und auff Begehren zum Druck ubergeben/ Von Wolffgango Thoma, Pfarrern zu Beuna