In this thesis we focus on new methods for probabilistic model checking (PMC) with linear temporal logic (LTL). The standard approach translates an LTL formula into a deterministic ω-automaton with a double-exponential blow up. There are approaches for Markov chain analysis against LTL with exponential runtime, which motivates the search for non-deterministic automata with restricted forms of non-determinism that make them suitable for PMC. For MDPs, the approach via deterministic automata matches the double-exponential lower bound, but a practical application might benefit from approaches via non-deterministic automata. We first investigate good-for-games (GFG) automata. In GFG automata one can resolve the non-determinism for a finite prefix without knowing the infinite suffix and still obtain an accepting run for an accepted word. We explain that GFG automata are well-suited for MDP analysis on a theoretic level, but our experiments show that GFG automata cannot compete with deterministic automata. We have also researched another form of pseudo-determinism, namely unambiguity, where for every accepted word there is exactly one accepting run. We present a polynomial-time approach for PMC of Markov chains against specifications given by an unambiguous Büchi automaton (UBA). Its two key elements are the identification whether the induced probability is positive, and if so, the identification of a state set inducing probability 1. Additionally, we examine the new symbolic Muller acceptance described in the Hanoi Omega Automata Format, which we call Emerson-Lei acceptance. It is a positive Boolean formula over unconditional fairness constraints. We present a construction of small deterministic automata using Emerson-Lei acceptance. Deciding, whether an MDP has a positive maximal probability to satisfy an Emerson-Lei acceptance, is NP-complete. This fact has triggered a DPLL-based algorithm for deciding positiveness.

Denna studie undersöker hur spelupplevelsen i ett "management"-spel förändras om virtuella karaktärer agerar verklighetstroget i sina handlingar och val samt hur en spelutvecklare kan hålla nere påverkan på spelets prestanda och samtidigt bibehålla trovärdigheten hos spelets virtuella karaktärer. Resultat från tidigare forskning om AI-LOD har använts som grund i utvecklingen av en prototyp av ett "management"-spel som sedan testats av åtta deltagare följt av individuella intervjuer gällande deras upplevelser av och reflektioner kring spelet. Studien presenterar förslag på tillvägagångssätt för att använda AI-LOD effektivt samt hur användarnas upplevelser har påverkats positivt och negativt av de designval som gjorts. / This study investigates how the player experience is affected in "management" games when the virtual characters' behaviors are pivoted towards realism. The study also investigates the usage of AI-LOD as a method to reduce the impact on performance by these virtual characters without sacrificing authenticity of their behavior. Results and findings from previous research in this particular field are used as a foundation in the development of a prototype of a "management" game. This prototype has been tested by eight participants followed by individual interviews on their experiences and thoughts on the game. The study presents suggestions on how to use AI-LOD effectively and how player experience has been affected both positively and negatively by design choices made during the development of this prototype.

Results of psychological experiments have shown that humans make assumptions, which are not necessarily valid, that they are influenced by their background knowledge and that they reason non-monotonically. These observations show that classical logic does not seem to be adequate for modeling human reasoning. Instead of assuming that humans do not reason logically at all, we take the view that humans do not reason classical logically. Our goal is to model episodes of human reasoning and for this purpose we investigate the so-called Weak Completion Semantics. The Weak Completion Semantics is a Logic Programming approach and considers the least model of the weak completion of logic programs under the three-valued Łukasiewicz logic. As the Weak Completion Semantics is relatively new and has not yet been extensively investigated, we first motivate why this approach is interesting for modeling human reasoning. After that, we show the formal correspondence to the already established Stable Model Semantics and Well-founded Semantics. Next, we present an extension with an additional context operator, that allows us to express negation as failure. Finally, we propose a contextual abductive reasoning approach, in which the context of observations is relevant. Some properties do not hold anymore under this extension. Besides discussing the well-known psychological experiments Byrne’s suppression task and Wason’s selection task, we investigate an experiment in spatial reasoning, an experiment in syllogistic reasoning and an experiment that examines the belief-bias effect. We show that the results of these experiments can be adequately modeled under the Weak Completion Semantics. A result which stands out here, is the outcome of modeling the syllogistic reasoning experiment, as we have a higher prediction match with the participants’ answers than any of twelve current cognitive theories. We present an abstract evaluation system for conditionals and discuss well-known examples from the literature. We show that in this system, conditionals can be evaluated in various ways and we put up the hypothesis that humans use a particular evaluation strategy, namely that they prefer abduction to revision. We also discuss how relevance plays a role in the evaluation process of conditionals. For this purpose we propose a semantic definition of relevance and justify why this is preferable to a exclusively syntactic definition. Finally, we show that our system is more general than another system, which has recently been presented in the literature. Altogether, this thesis shows one possible path on bridging the gap between Cognitive Science and Computational Logic. We investigated findings from psychological experiments and modeled their results within one formal approach, the Weak Completion Semantics. Furthermore, we proposed a general evaluation system for conditionals, for which we suggest a specific evaluation strategy. Yet, the outcome cannot be seen as the ultimate solution but delivers a starting point for new open questions in both areas.

The underwater mining has increased in the recent years and the growing awareness of the potential impacts on the environment, as results of increasing the encroachment on the marine environment. Therefore, the debate has increased about how to protect this environment by using the scientific research that\'s relevant to the various environmental effects and developing the equipment used in dredging. There is a wide diversity of underwater mining equipments, such as continuous and non-continuous dredging which used for production of sand, gravel, alluvial deposits and raw material. There are a relation between increasingly dredging activities in the recent years and their impacts on the aquatic environment. These impacts are causes by changes in the topography of the sea floor such as turbidity, noise and other environmental impacts. Today, there is an international framework of legislation which has been developed for dredging projects. This contains rules and regulations which must be followed by mining companies and have to implemented by national authorities. The European countries also develop their legislation to control on the dredged material which deposit on land and sea. This legislation is constantly changing related to scientific knowledge and increasing the implementation frameworks. Also, the people become more sensitive to emissions that have a negative attitude towards dredging in the neighborhood. In addition, dredging techniques give rise to objections, which eventually led to think in more environmentally-friendly production methods. After that, the use of dredger is the only alternative in some project. The question is what are the true benefits of these techniques and what is the relation between possible improvements and technological potential as well as the costs. Therefore, it is intended to assess mining techniques in the context of their environmental impact and the costs. There are many systematic approaches which have been used for evaluation and determination of the environmental performances of different dredging equipment, techniques and procedures. Moreover, the new future developments and latest proposals in the dredging industry have been presented. Also, the new proposal to reduce the turbidity and suspended material effect which is the most important environmental impacts during dredging operations has presented. This research work gives a description of underwater mining techniques and different way of evaluating the dredging equipment’s in term of environmental, economic and social aspects. Also, this work presents two different methods of evaluation. The first approach is the statistical analyses method by using the modern Fuzzy evaluation concept. The second slant is a mathematical accounting method by using the information from the Egyptian case study, in order to reach the most environmental-friendly dredging techniques by taking into account the economic and social point of views. The final evaluation showed that the suction and bucket ladder dredger are the best choices. The assessment was made after comparing many parameters such as performance, characteristics, working depth, soil types and project area. Also, this work presents two different new practices for extraction of the underwater placer deposits which occur on the Egyptian Mediterranean coast. The first technique uses floating processing unit in the in situ area, which gets the extracted material and treated it to reduce the transportation costs. The second technique has divided the working area to many stages which make the suction dredger used also for transporting the material into the beach. The pipeline will be the best method of transportation by using the power of suction, which reduce also the transportation costs and also avoid the environmental effects.

In today's versatile requirements for reducing fuel consumption, a lot of different approaches are in development like hybridization, reducing the amount of cylinders with the same power as before or operating point-independent components and auxiliaries. Within this thesis, one of the approaches is shown: electrified auxiliaries including an operation strategy. Replacing conventional auxiliaries with electrified ones, the need of more electrical power becomes bigger. Due to the limits within the 12V power net, the 48V approach is the logical conclusion in terms of cost benefit and availability of the needed resources to use the electrified components. The 48V power net introduces new or modified parts to the vehicle including a new power net topology. Fuzzy logic was chosen to control the auxiliaries, because of the number of input variables, the flexibility of using it for different cars and being robust during the usage. The results showed a significant improvement of fuel consumption with the developed control strategy for the selected power net topology. This improvement was evident in all cycles, which were discussed within this thesis. In this thesis a new approach for reducing fuel consumption was shown, which includes several electrified auxiliaries and the operation strategy to control them within the vehicle during different cycles. The necessary models for the approach were developed including the auxiliaries, the controller and the needed parts for the power net. / In der heutigen Zeit mit den steigenden Ansprüchen zur Reduzierung des Kraftstoffverbrauchs sind viele verschiedene Ansätze und Technologien in der Entwicklung, wie zum Beispiel Hybridisierung, Zylinderreduktion mit der gleichen Leistungsausbeute wie zuvor oder auch vom Verbrennungsmotor unabhängigen Komponenten und Nebenaggregaten. Innerhalb dieser Arbeit wurde einer dieser Ansätze näher erläutert: elektrifizierte Nebenaggregate inklusive einer Betriebsstrategie. Durch den Austausch der konventionellen Nebenaggregate mit den elektrifizierten Nebenaggregaten steigt der Bedarf an mehr elektrischer Leistung. Durch die Limitierungen im 12V Bordnetz, ist der 48V Ansatz der nächste logische Schritt hinsichtlich des Kosten/Nutzen-Verhältnis und der Ressourcenverfügbarkeit für die Nutzung der elektrifizierten Komponenten. Das 48V Bordnetz benötigt neue bzw. modifizierte Komponenten inclusive einer neuen Bordnetztopologie. Fuzzy-Logik wurde zur Regelung der Nebenaggregate ausgewählt. Grund hierfür waren: Anzahl an Eingangsvariablen, Flexibilität in der Übertragung auf andere Fahrzeuge und dem robusten Verhalten in der Anwendung. Die Ergebnisse zeigten ein signifikantes Einsparpotential durch die Verwendung der entwickelten Betriebsstrategie für die ausgewählte Bordnetztopologie. Die Einsparung war in allen diskutierten Zyklen deutlich zu sehen. In dieser Arbeit wurde ein neuer Ansatz zur Verbrauchsreduktion gezeigt inklusive elektrifizierter Nebenaggregate und der benötigten Betriebsstrategie, um diese im Fahrzeug in verschiedenen Zyklen zu steuern. Die benötigten Modelle wurden entwickelt, wie zum Beispiel die Nebenaggregate, der Regler und den Bordnetzkomponenten.

The present work deals with Description Logics (DLs), a class of knowledge representation formalisms used to represent and reason about classes of individuals and relations between such classes in a formally well-defined way. We provide novel results in three main directions. (1) Tractable reasoning revisited: in the 1990s, DL research has largely answered the question for practically relevant yet tractable DL formalisms in the negative. Due to novel application domains, especially the Life Sciences, and a surprising tractability result by Baader, we have re-visited this question, this time looking in a new direction: general terminologies (TBoxes) and extensions thereof defined over the DL EL and extensions thereof. As main positive result, we devise EL++(D)-CBoxes as a tractable DL formalism with optimal expressivity in the sense that every additional standard DL constructor, every extension of the TBox formalism, or every more powerful concrete domain, makes reasoning intractable. (2) Non-standard inferences for knowledge maintenance: non-standard inferences, such as matching, can support domain experts in maintaining DL knowledge bases in a structured and well-defined way. In order to extend their availability and promote their use, the present work extends the state of the art of non-standard inferences both w.r.t. theory and implementation. Our main results are implementations and performance evaluations of known matching algorithms for the DLs ALE and ALN, optimal non-deterministic polynomial time algorithms for matching under acyclic side conditions in ALN and sublanguages, and optimal algorithms for matching w.r.t. cyclic (and hybrid) EL-TBoxes. (3) Non-standard inferences over general concept inclusion (GCI) axioms: the utility of GCIs in modern DL knowledge bases and the relevance of non-standard inferences to knowledge maintenance naturally motivate the question for tractable DL formalism in which both can be provided. As main result, we propose hybrid EL-TBoxes as a solution to this hitherto open question.

Es wird die Axiomatisierbarkeit einer Klasse von temporalen Prädikatenlogiken über verzweigenden Strukturen gezeigt. Entscheidbarkeitsresultate folgen für diverse Fragmente dieser Logiken. Anwendungen werden diskutiert.

An abstract knowledge representation of cognitive robots - as used for reasoning and planning - typically relies on symbols denoting objects of the world and states of affairs. The process of creating and maintaining the correct connection between a symbol denoting an object and its corresponding perceptual image (called percept), both referring to the same physical object, is called symbol anchoring. Most current cognitive systems implement an ad hoc solution which may work for the specific, intended application under certain conditions. Conversely, we suggest a formal and general approach to the symbol anchoring problem, which enhances previous approaches in terms of flexibility, applicability and expressiveness, and which completely automates the process of determining and maintaining all plausible hypotheses of correspondences between object symbols and perceptual images of physical objects. Based on the first-order logical Fluent Calculus, our approach inherits its rich expressiveness with respect to knowledge representation and reasoning. Implementing all required symbol anchoring functionalities, our approach also complies with fundamental concepts of phenomenalism, representationalism and the sense-data theory of philosophy of cognition.

Description Logics (DLs) are a class of knowledge representation formalisms that can represent terminological and assertional knowledge using a well-defined semantics. Often, knowledge engineers are experts in their own fields, but not in logics, and require assistance in the process of ontology design. This thesis presents three methods that can extract terminological knowledge from existing data and thereby assist in the design process. They are based on similar formalisms from Formal Concept Analysis (FCA), in particular the Next-Closure Algorithm and Attribute-Exploration. The first of the three methods computes terminological knowledge from the data, without any expert interaction. The two other methods use expert interaction where a human expert can confirm each terminological axiom or refute it by providing a counterexample. These two methods differ only in the way counterexamples are provided.

Charge sharing poses a fundamental problem in the design of dynamic logic gates, which is nearly as old as digital circuit design itself. Although, many solutions are known, up to now most of them add additional complexity to a given system and require careful optimization of device sizes. Here we propose a simple CMOS-technology compatible transistor level solution to the charge sharing problem, employing a new class of field effect transistors with multiple independent gates (MIGFETs). Based on mixed-mode simulations in a coordinated device-circuit co-design framework, we show that their underlying device physics provides an inherent suppression of the charge sharing effect. Exemplary circuit layouts as well as discussion on the switching performance are given.