TY - INPR
A1 - Arnold, Holger
T1 - A linearized DPLL calculus with clause learning (2nd, revised version)
N2 - Many formal descriptions of DPLL-based SAT algorithms either do not include all essential proof techniques applied by modern SAT solvers or are bound to particular heuristics or data structures. This makes it difficult to analyze proof-theoretic properties or the search complexity of these algorithms. In this paper we try to improve this situation by developing a nondeterministic proof calculus that models the functioning of SAT algorithms based on the DPLL calculus with clause learning. This calculus is independent of implementation details yet precise enough to enable a formal analysis of realistic DPLL-based SAT algorithms.
N2 - Viele formale Beschreibungen DPLL-basierter SAT-Algorithmen enthalten entweder nicht alle wesentlichen Beweistechniken, die in modernen SAT-Solvern implementiert sind, oder sind an bestimmte Heuristiken oder Datenstrukturen gebunden. Dies erschwert die Analyse beweistheoretischer Eigenschaften oder der Suchkomplexität derartiger Algorithmen. Mit diesem Artikel versuchen wir, diese Situation durch die Entwicklung eines nichtdeterministischen Beweiskalküls zu verbessern, der die Arbeitsweise von auf dem DPLL-Kalkül basierenden SAT-Algorithmen mit Klausellernen modelliert. Dieser Kalkül ist unabhängig von Implementierungsdetails, aber dennoch präzise genug, um eine formale Analyse realistischer DPLL-basierter SAT-Algorithmen zu ermöglichen.
KW - Automatisches Beweisen
KW - Logikkalkül
KW - SAT
KW - DPLL
KW - Klausellernen
KW - automated theorem proving
KW - logical calculus
KW - SAT
KW - DPLL
KW - clause learning
Y1 - 2009
U6 - http://nbn-resolving.de/urn/resolver.pl?urn:nbn:de:kobv:517-opus-29080
ER -
TY - JOUR
A1 - Arnold, Holger
T1 - A linearized DPLL calculus with learning
N2 - This paper describes the proof calculus LD for clausal propositional logic, which is a linearized form of the well-known DPLL calculus extended by clause learning. It is motivated by the demand to model how current SAT solvers built on clause learning are working, while abstracting from decision heuristics and implementation details. The calculus is proved sound and terminating. Further, it is shown that both the original DPLL calculus and the conflict-directed backtracking calculus with clause learning, as it is implemented in many current SAT solvers, are complete and proof-confluent instances of the LD calculus.
N2 - Dieser Artikel beschreibt den Beweiskalkül LD für aussagenlogische Formeln in Klauselform. Dieser Kalkül ist eine um Klausellernen erweiterte linearisierte Variante des bekannten DPLL-Kalküls. Er soll dazu dienen, das Verhalten von auf Klausellernen basierenden SAT-Beweisern zu modellieren, wobei von Entscheidungsheuristiken und Implementierungsdetails abstrahiert werden soll. Es werden Korrektheit und Terminierung des Kalküls bewiesen. Weiterhin wird gezeigt, dass sowohl der ursprüngliche DPLL-Kalkül als auch der konfliktgesteuerte Rücksetzalgorithmus mit Klausellernen, wie er in vielen aktuellen SAT-Beweisern implementiert ist, vollständige und beweiskonfluente Spezialisierungen des LD-Kalküls sind.
KW - SAT
KW - DPLL
KW - Klausellernen
KW - Automatisches Beweisen
KW - SAT
KW - DPLL
KW - Clause Learning
KW - Automated Theorem Proving
Y1 - 2007
U6 - http://nbn-resolving.de/urn/resolver.pl?urn:nbn:de:kobv:517-opus-15421
ER -
TY - BOOK
A1 - Schneider, Sven
A1 - Lambers, Leen
A1 - Orejas, Fernando
T1 - A logic-based incremental approach to graph repair
T1 - Ein logikbasierter inkrementeller Ansatz für Graphreparatur
N2 - Graph repair, restoring consistency of a graph, plays a prominent role in several areas of computer science and beyond: For example, in model-driven engineering, the abstract syntax of models is usually encoded using graphs. Flexible edit operations temporarily create inconsistent graphs not representing a valid model, thus requiring graph repair. Similarly, in graph databases—managing the storage and manipulation of graph data—updates may cause that a given database does not satisfy some integrity constraints, requiring also graph repair. We present a logic-based incremental approach to graph repair, generating a sound and complete (upon termination) overview of least-changing repairs. In our context, we formalize consistency by so-called graph conditions being equivalent to first-order logic on graphs. We present two kind of repair algorithms: State-based repair restores consistency independent of the graph update history, whereas deltabased (or incremental) repair takes this history explicitly into account. Technically, our algorithms rely on an existing model generation algorithm for graph conditions implemented in AutoGraph. Moreover, the delta-based approach uses the new concept of satisfaction (ST) trees for encoding if and how a graph satisfies a graph condition. We then demonstrate how to manipulate these STs incrementally with respect to a graph update.
N2 - Die Reparatur von Graphen, die Wiederherstellung der Konsistenz eines Graphen, spielt in mehreren Bereichen der Informatik und darüber hinaus eine herausragende Rolle: Beispielsweise wird in der modellgetriebenen Konstruktion die abstrakte Syntax von Modellen in der Regel mithilfe von Graphen kodiert.
Flexible Bearbeitungsvorgänge erstellen vorübergehend inkonsistente Diagramme, die kein gültiges Modell darstellen, und erfordern daher eine Reparatur des Diagramms.
Auf ähnliche Weise können Aktualisierungen in Graphendatenbanken - die das Speichern und Bearbeiten von Graphendaten verwalten - dazu führen, dass eine bestimmte Datenbank einige Integritätsbeschränkungen nicht erfüllt und auch eine Graphreparatur erforderlich macht.
Wir präsentieren einen logikbasierten inkrementellen Ansatz für die Graphreparatur, der eine solide und vollständige (nach Beendigung) Übersicht über die am wenigsten verändernden Reparaturen erstellt.
In unserem Kontext formalisieren wir die Konsistenz mittels sogenannten Graphbedingungen die der Logik erster Ordnung in Graphen entsprechen.
Wir stellen zwei Arten von Reparaturalgorithmen vor: Die zustandsbasierte Reparatur stellt die Konsistenz unabhängig vom Verlauf der Graphänderung wieder her, während die deltabasierte (oder inkrementelle) Reparatur diesen Verlauf explizit berücksichtigt.
Technisch stützen sich unsere Algorithmen auf einen vorhandenen Modellgenerierungsalgorithmus für in AutoGraph implementierte Graphbedingungen.
Darüber hinaus verwendet der deltabasierte Ansatz das neue Konzept der Erfüllungsbäume (STs) zum Kodieren, ob und wie ein Graph eine Graphbedingung erfüllt.
Wir zeigen dann, wie diese STs in Bezug auf eine Graphaktualisierung inkrementell manipuliert werden.
T3 - Technische Berichte des Hasso-Plattner-Instituts für Digital Engineering an der Universität Potsdam - 126
KW - nested graph conditions
KW - graph repair
KW - model repair
KW - consistency restoration
KW - verschachtelte Graphbedingungen
KW - Graphreparatur
KW - Modellreparatur
KW - Konsistenzrestauration
Y1 - 2019
U6 - http://nbn-resolving.de/urn/resolver.pl?urn:nbn:de:kobv:517-opus4-427517
SN - 978-3-86956-462-3
SN - 1613-5652
SN - 2191-1665
IS - 126
PB - Universitätsverlag Potsdam
CY - Potsdam
ER -
TY - JOUR
A1 - Schneider, Sven
A1 - Lambers, Leen
A1 - Orejas, Fernando
T1 - A logic-based incremental approach to graph repair featuring delta preservation
JF - International journal on software tools for technology transfer : STTT
N2 - We introduce a logic-based incremental approach to graph repair, generating a sound and complete (upon termination) overview of least-changing graph repairs from which a user may select a graph repair based on non-formalized further requirements. This incremental approach features delta preservation as it allows to restrict the generation of graph repairs to delta-preserving graph repairs, which do not revert the additions and deletions of the most recent consistency-violating graph update. We specify consistency of graphs using the logic of nested graph conditions, which is equivalent to first-order logic on graphs. Technically, the incremental approach encodes if and how the graph under repair satisfies a graph condition using the novel data structure of satisfaction trees, which are adapted incrementally according to the graph updates applied. In addition to the incremental approach, we also present two state-based graph repair algorithms, which restore consistency of a graph independent of the most recent graph update and which generate additional graph repairs using a global perspective on the graph under repair. We evaluate the developed algorithms using our prototypical implementation in the tool AutoGraph and illustrate our incremental approach using a case study from the graph database domain.
KW - Nested graph conditions
KW - Graph repair
KW - Model repair
KW - Consistency
KW - restoration
KW - Delta preservation
KW - Graph databases
KW - Model-driven
KW - engineering
Y1 - 2021
U6 - https://doi.org/10.1007/s10009-020-00584-x
SN - 1433-2779
SN - 1433-2787
VL - 23
IS - 3
SP - 369
EP - 410
PB - Springer
CY - Berlin ; Heidelberg
ER -
TY - JOUR
A1 - Hartung, Niklas
A1 - Borghardt, Jens Markus
T1 - A mechanistic framework for a priori pharmacokinetic predictions of orally inhaled drugs
JF - PLoS Computational Biology : a new community journal
N2 - Author summary
The use of orally inhaled drugs for treating lung diseases is appealing since they have the potential for lung selectivity, i.e. high exposure at the site of action -the lung- without excessive side effects. However, the degree of lung selectivity depends on a large number of factors, including physiochemical properties of drug molecules, patient disease state, and inhalation devices. To predict the impact of these factors on drug exposure and thereby to understand the characteristics of an optimal drug for inhalation, we develop a predictive mathematical framework (a "pharmacokinetic model"). In contrast to previous approaches, our model allows combining knowledge from different sources appropriately and its predictions were able to adequately predict different sets of clinical data. Finally, we compare the impact of different factors and find that the most important factors are the size of the inhaled particles, the affinity of the drug to the lung tissue, as well as the rate of drug dissolution in the lung. In contrast to the common belief, the solubility of a drug in the lining fluids is not found to be relevant. These findings are important to understand how inhaled drugs should be designed to achieve best treatment results in patients.
The fate of orally inhaled drugs is determined by pulmonary pharmacokinetic processes such as particle deposition, pulmonary drug dissolution, and mucociliary clearance. Even though each single process has been systematically investigated, a quantitative understanding on the interaction of processes remains limited and therefore identifying optimal drug and formulation characteristics for orally inhaled drugs is still challenging. To investigate this complex interplay, the pulmonary processes can be integrated into mathematical models. However, existing modeling attempts considerably simplify these processes or are not systematically evaluated against (clinical) data. In this work, we developed a mathematical framework based on physiologically-structured population equations to integrate all relevant pulmonary processes mechanistically. A tailored numerical resolution strategy was chosen and the mechanistic model was evaluated systematically against data from different clinical studies. Without adapting the mechanistic model or estimating kinetic parameters based on individual study data, the developed model was able to predict simultaneously (i) lung retention profiles of inhaled insoluble particles, (ii) particle size-dependent pharmacokinetics of inhaled monodisperse particles, (iii) pharmacokinetic differences between inhaled fluticasone propionate and budesonide, as well as (iv) pharmacokinetic differences between healthy volunteers and asthmatic patients. Finally, to identify the most impactful optimization criteria for orally inhaled drugs, the developed mechanistic model was applied to investigate the impact of input parameters on both the pulmonary and systemic exposure. Interestingly, the solubility of the inhaled drug did not have any relevant impact on the local and systemic pharmacokinetics. Instead, the pulmonary dissolution rate, the particle size, the tissue affinity, and the systemic clearance were the most impactful potential optimization parameters. In the future, the developed prediction framework should be considered a powerful tool for identifying optimal drug and formulation characteristics.
Y1 - 2020
U6 - https://doi.org/10.1371/journal.pcbi.1008466
SN - 1553-734X
SN - 1553-7358
VL - 16
IS - 12
PB - PLoS
CY - San Fransisco
ER -
TY - JOUR
A1 - Weise, Martin
T1 - A model for teaching informatics to German secondary school students in English-language bilingual education
JF - Commentarii informaticae didacticae : (CID)
N2 - Informatics as a school subject has been virtually absent from bilingual education programs in German secondary schools. Most bilingual programs in German secondary education started out by focusing on subjects from the field of social sciences. Teachers and bilingual curriculum experts alike have been regarding those as the most suitable subjects for bilingual instruction – largely due to the intercultural perspective that a bilingual approach provides. And though one cannot deny the gain that ensues from an intercultural perspective on subjects such as history or geography, this benefit is certainly not limited to social science subjects. In consequence, bilingual curriculum designers have already begun to include other subjects such as physics or chemistry in bilingual school programs. It only seems a small step to extend this to informatics. This paper will start out by addressing potential benefits of adding informatics to the range of subjects taught as part of English-language bilingual programs in German secondary education. In a second step it will sketch out a methodological (= didactical) model for teaching informatics to German learners through English. It will then provide two items of hands-on and tested teaching material in accordance with this model. The discussion will conclude with a brief outlook on the chances and prerequisites of firmly establishing informatics as part of bilingual school curricula in Germany.
Y1 - 2013
U6 - http://nbn-resolving.de/urn/resolver.pl?urn:nbn:de:kobv:517-opus-64568
SN - 1868-0844
SN - 2191-1940
IS - 6
SP - 127
EP - 137
PB - Universitätsverlag Potsdam
CY - Potsdam
ER -
TY - JOUR
A1 - Perach, Shai
A1 - Alexandron, Giora
T1 - A MOOC-Based Computer Science Program for Middle School
BT - Results, Challenges, and the Covid-19 Effect
JF - EMOOCs 2021
N2 - In an attempt to pave the way for more extensive Computer Science Education (CSE) coverage in K-12, this research developed and made a preliminary evaluation of a blended-learning Introduction to CS program based on an academic MOOC. Using an academic MOOC that is pedagogically effective and engaging, such a program may provide teachers with disciplinary scaffolds and allow them to focus their attention on enhancing students’ learning experience and nurturing critical 21st-century skills such as self-regulated learning. As we demonstrate, this enabled us to introduce an academic level course to middle-school students. In this research, we developed the principals and initial version of such a program, targeting ninth-graders in science-track classes who learn CS as part of their standard curriculum. We found that the middle-schoolers who participated in the program achieved academic results on par with undergraduate students taking this MOOC for academic credit. Participating students also developed a more accurate perception of the essence of CS as a scientific discipline. The unplanned school closure due to the COVID19 pandemic outbreak challenged the research but underlined the advantages of such a MOOCbased blended learning program above classic pedagogy in times of global or local crises that lead to school closure. While most of the science track classes seem to stop learning CS almost entirely, and the end-of-year MoE exam was discarded, the program’s classes smoothly moved to remote learning mode, and students continued to study at a pace similar to that experienced before the school shut down.
Y1 - 2021
U6 - http://nbn-resolving.de/urn/resolver.pl?urn:nbn:de:kobv:517-opus4-517133
SN - 978-3-86956-512-5
VL - 2021
SP - 111
EP - 127
PB - Universitätsverlag Potsdam
CY - Potsdam
ER -
TY - GEN
A1 - Giese, Holger
A1 - Henkler, Stefan
A1 - Hirsch, Martin
T1 - A multi-paradigm approach supporting the modular execution of reconfigurable hybrid systems
N2 - Advanced mechatronic systems have to integrate existing technologies from mechanical, electrical and software engineering. They must be able to adapt their structure and behavior at runtime by reconfiguration to react flexibly to changes in the environment. Therefore, a tight integration of structural and behavioral models of the different domains is required. This integration results in complex reconfigurable hybrid systems, the execution logic of which cannot be addressed directly with existing standard modeling, simulation, and code-generation techniques. We present in this paper how our component-based approach for reconfigurable mechatronic systems, M ECHATRONIC UML, efficiently handles the complex interplay of discrete behavior and continuous behavior in a modular manner. In addition, its extension to even more flexible reconfiguration cases is presented.
T3 - Zweitveröffentlichungen der Universität Potsdam : Mathematisch-Naturwissenschaftliche Reihe - 410
KW - code generation
KW - hybrid systems
KW - reconfigurable systems
KW - simulation
Y1 - 2017
U6 - http://nbn-resolving.de/urn/resolver.pl?urn:nbn:de:kobv:517-opus4-402896
ER -
TY - JOUR
A1 - Navarro, Marisa
A1 - Orejas, Fernando
A1 - Pino, Elvira
A1 - Lambers, Leen
T1 - A navigational logic for reasoning about graph properties
JF - Journal of logical and algebraic methods in programming
N2 - Graphs play an important role in many areas of Computer Science. In particular, our work is motivated by model-driven software development and by graph databases. For this reason, it is very important to have the means to express and to reason about the properties that a given graph may satisfy. With this aim, in this paper we present a visual logic that allows us to describe graph properties, including navigational properties, i.e., properties about the paths in a graph. The logic is equipped with a deductive tableau method that we have proved to be sound and complete.
KW - Graph logic
KW - Algebraic methods
KW - Formal modelling
KW - Specification
Y1 - 2021
U6 - https://doi.org/10.1016/j.jlamp.2020.100616
SN - 2352-2208
SN - 2352-2216
VL - 118
PB - Elsevier Science
CY - Amsterdam [u.a.]
ER -
TY - THES
A1 - Ghasemzadeh, Mohammad
T1 - A new algorithm for the quantified satisfiability problem, based on zero-suppressed binary decision diagrams and memoization
T1 - Ein neuer Algorithmus für die quantifizierte Aussagenlogik, basierend auf Zero-suppressed BDDs und Memoization
N2 - Quantified Boolean formulas (QBFs) play an important role in theoretical computer science. QBF extends propositional logic in such a way that many advanced forms of reasoning can be easily formulated and evaluated. In this dissertation we present our ZQSAT, which is an algorithm for evaluating quantified Boolean formulas. ZQSAT is based on ZBDD: Zero-Suppressed Binary Decision Diagram , which is a variant of BDD, and an adopted version of the DPLL algorithm. It has been implemented in C using the CUDD: Colorado University Decision Diagram package. The capability of ZBDDs in storing sets of subsets efficiently enabled us to store the clauses of a QBF very compactly and let us to embed the notion of memoization to the DPLL algorithm. These points led us to implement the search algorithm in such a way that we could store and reuse the results of all previously solved subformulas with a little overheads. ZQSAT can solve some sets of standard QBF benchmark problems (known to be hard for DPLL based algorithms) faster than the best existing solvers. In addition to prenex-CNF, ZQSAT accepts prenex-NNF formulas. We show and prove how this capability can be exponentially beneficial.
N2 - In der Dissertation stellen wir einen neuen Algorithmus vor, welcher Formeln der quantifizierten Aussagenlogik (engl. Quantified Boolean formula, kurz QBF) löst. QBFs sind eine Erweiterung der klassischen Aussagenlogik um die Quantifizierung über aussagenlogische Variablen. Die quantifizierte Aussagenlogik ist dabei eine konservative Erweiterung der Aussagenlogik, d.h. es können nicht mehr Theoreme nachgewiesen werden als in der gewöhnlichen Aussagenlogik. Der Vorteil der Verwendung von QBFs ergibt sich durch die Möglichkeit, Sachverhalte kompakter zu repräsentieren. SAT (die Frage nach der Erfüllbarkeit einer Formel der Aussagenlogik) und QSAT (die Frage nach der Erfüllbarkeit einer QBF) sind zentrale Probleme in der Informatik mit einer Fülle von Anwendungen, wie zum Beispiel in der Graphentheorie, bei Planungsproblemen, nichtmonotonen Logiken oder bei der Verifikation. Insbesondere die Verifikation von Hard- und Software ist ein sehr aktuelles und wichtiges Forschungsgebiet in der Informatik. Unser Algorithmus zur Lösung von QBFs basiert auf sogenannten ZBDDs (engl. Zero-suppressed Binary decision Diagrams), welche eine Variante der BDDs (engl. Binary decision Diagrams) sind. BDDs sind eine kompakte Repräsentation von Formeln der Aussagenlogik. Der Algorithmus kombiniert nun bekannte Techniken zum Lösen von QBFs mit der ZBDD-Darstellung unter Verwendung geeigneter Heuristiken und Memoization. Memoization ermöglicht dabei das einfache Wiederverwenden bereits gelöster Teilprobleme. Der Algorithmus wurde unter Verwendung des CUDD-Paketes (Colorado University Decision Diagram) implementiert und unter dem Namen ZQSAT veröffentlicht. In Tests konnten wir nachweisen, dass ZQSAT konkurrenzfähig zu existierenden QBF-Beweisern ist, in einigen Fällen sogar bessere Resultate liefern kann.
KW - Binäres Entscheidungsdiagramm
KW - Erfüllbarkeitsproblem
KW - DPLL
KW - Zero-Suppressed Binary Decision Diagram (ZDD)
KW - Formeln der quantifizierten Aussagenlogik
KW - Erfüllbarkeit einer Formel der Aussagenlogik
KW - ZQSA
KW - DPLL
KW - Zero-Suppressed Binary Decision Diagram (ZDD)
KW - Quantified Boolean Formula (QBF)
KW - Satisfiability
KW - ZQSAT
Y1 - 2005
U6 - http://nbn-resolving.de/urn/resolver.pl?urn:nbn:de:kobv:517-opus-6378
ER -
TY - JOUR
A1 - Neher, Dieter
A1 - Kniepert, Juliane
A1 - Elimelech, Arik
A1 - Koster, L. Jan Anton
T1 - A New Figure of Merit for Organic Solar Cells with Transport-limited Photocurrents
JF - Scientific reports
N2 - Compared to their inorganic counterparts, organic semiconductors suffer from relatively low charge carrier mobilities. Therefore, expressions derived for inorganic solar cells to correlate characteristic performance parameters to material properties are prone to fail when applied to organic devices. This is especially true for the classical Shockley-equation commonly used to describe current-voltage (JV)-curves, as it assumes a high electrical conductivity of the charge transporting material. Here, an analytical expression for the JV-curves of organic solar cells is derived based on a previously published analytical model. This expression, bearing a similar functional dependence as the Shockley-equation, delivers a new figure of merit α to express the balance between free charge recombination and extraction in low mobility photoactive materials. This figure of merit is shown to determine critical device parameters such as the apparent series resistance and the fill factor.
KW - Electronic and spintronic devices
KW - Semiconductors
Y1 - 2016
U6 - https://doi.org/10.1038/srep24861
SN - 2045-2322
VL - 6
PB - Nature Publishing Group
CY - London
ER -
TY - GEN
A1 - Neher, Dieter
A1 - Kniepert, Juliane
A1 - Elimelech, Arik
A1 - Koster, L. Jan Anton
T1 - A New Figure of Merit for Organic Solar Cells with Transport-limited Photocurrents
N2 - Compared to their inorganic counterparts, organic semiconductors suffer from relatively low charge carrier mobilities. Therefore, expressions derived for inorganic solar cells to correlate characteristic performance parameters to material properties are prone to fail when applied to organic devices. This is especially true for the classical Shockley-equation commonly used to describe current-voltage (JV)-curves, as it assumes a high electrical conductivity of the charge transporting material. Here, an analytical expression for the JV-curves of organic solar cells is derived based on a previously published analytical model. This expression, bearing a similar functional dependence as the Shockley-equation, delivers a new figure of merit α to express the balance between free charge recombination and extraction in low mobility photoactive materials. This figure of merit is shown to determine critical device parameters such as the apparent series resistance and the fill factor.
T3 - Zweitveröffentlichungen der Universität Potsdam : Mathematisch-Naturwissenschaftliche Reihe - 225
KW - Electronic and spintronic devices
KW - Semiconductors
Y1 - 2016
U6 - http://nbn-resolving.de/urn/resolver.pl?urn:nbn:de:kobv:517-opus4-91414
ER -
TY - CHAP
A1 - Herre, Heinrich
A1 - Hummel, Axel
T1 - A paraconsistent semantics for generalized logic programs
N2 - We propose a paraconsistent declarative semantics of possibly inconsistent generalized logic programs which allows for arbitrary formulas in the body and in the head of a rule (i.e. does not depend on the presence of any specific connective, such as negation(-as-failure), nor on any specific syntax of rules). For consistent generalized logic programs this semantics coincides with the stable generated models introduced in [HW97], and for normal logic programs it yields the stable models in the sense of [GL88].
KW - paraconsistency
KW - generalized logic programs
KW - multi-valued logic
Y1 - 2010
U6 - http://nbn-resolving.de/urn/resolver.pl?urn:nbn:de:kobv:517-opus-41496
ER -
TY - CHAP
A1 - Grüner, Andreas
A1 - Mühle, Alexander
A1 - Gayvoronskaya, Tatiana
A1 - Meinel, Christoph
T1 - A quantifiable trustmModel for Blockchain-based identity management
T2 - IEEE 2018 International Congress on Cybermatics / 2018 IEEE Conferences on Internet of Things, Green Computing and Communications, cyber, physical and Social Computing, Smart Data, Blockchain, Computer and Information Technology
KW - Blockchain
KW - distributed ledger technology
KW - digital identity
KW - self-sovereign identity
KW - trust
KW - identity management
Y1 - 2019
SN - 978-1-5386-7975-3
U6 - https://doi.org/10.1109/Cybermatics_2018.2018.00250
SP - 1475
EP - 1482
PB - IEEE
CY - New York
ER -
TY - BOOK
A1 - Polyvyanyy, Artem
A1 - Kuropka, Dominik
T1 - A quantitative evaluation of the enhanced topic-based vector space model
N2 - This contribution presents a quantitative evaluation procedure for Information Retrieval models and the results of this procedure applied on the enhanced Topic-based Vector Space Model (eTVSM). Since the eTVSM is an ontology-based model, its effectiveness heavily depends on the quality of the underlaying ontology. Therefore the model has been tested with different ontologies to evaluate the impact of those ontologies on the effectiveness of the eTVSM. On the highest level of abstraction, the following results have been observed during our evaluation: First, the theoretically deduced statement that the eTVSM has a similar effecitivity like the classic Vector Space Model if a trivial ontology (every term is a concept and it is independet of any other concepts) is used has been approved. Second, we were able to show that the effectiveness of the eTVSM raises if an ontology is used which is only able to resolve synonyms. We were able to derive such kind of ontology automatically from the WordNet ontology. Third, we observed that more powerful ontologies automatically derived from the WordNet, dramatically dropped the effectiveness of the eTVSM model even clearly below the effectiveness level of the Vector Space Model. Fourth, we were able to show that a manually created and optimized ontology is able to raise the effectiveness of the eTVSM to a level which is clearly above the best effectiveness levels we have found in the literature for the Latent Semantic Index model with compareable document sets.
T3 - Technische Berichte des Hasso-Plattner-Instituts für Digital Engineering an der Universität Potsdam - 19
Y1 - 2007
U6 - http://nbn-resolving.de/urn/resolver.pl?urn:nbn:de:kobv:517-opus-33816
SN - 978-3-939469-95-7
ER -
TY - JOUR
A1 - Doerr, Benjamin
A1 - Krejca, Martin Stefan
T1 - A simplified run time analysis of the univariate marginal distribution algorithm on LeadingOnes
JF - Theoretical computer science
N2 - With elementary means, we prove a stronger run time guarantee for the univariate marginal distribution algorithm (UMDA) optimizing the LEADINGONES benchmark function in the desirable regime with low genetic drift. If the population size is at least quasilinear, then, with high probability, the UMDA samples the optimum in a number of iterations that is linear in the problem size divided by the logarithm of the UMDA's selection rate. This improves over the previous guarantee, obtained by Dang and Lehre (2015) via the deep level-based population method, both in terms of the run time and by demonstrating further run time gains from small selection rates. Under similar assumptions, we prove a lower bound that matches our upper bound up to constant factors.
KW - Theory
KW - Estimation-of-distribution algorithm
KW - Run time analysis
Y1 - 2021
U6 - https://doi.org/10.1016/j.tcs.2020.11.028
SN - 0304-3975
SN - 1879-2294
VL - 851
SP - 121
EP - 128
PB - Elsevier
CY - Amsterdam
ER -
TY - CHAP
A1 - Goltz, Hans-Joachim
A1 - Pieth, Norbert
T1 - A tool for generating partition schedules of multiprocessor systems
N2 - A deterministic cycle scheduling of partitions at the operating system level is supposed for a multiprocessor system. In this paper, we propose a tool for generating such schedules. We use constraint based programming and develop methods and concepts for a combined interactive and automatic partition scheduling system. This paper is also devoted to basic methods and techniques for modeling and solving this partition scheduling problem. Initial application of our partition scheduling tool has proved successful and demonstrated the suitability of the methods used.
Y1 - 2010
U6 - http://nbn-resolving.de/urn/resolver.pl?urn:nbn:de:kobv:517-opus-41556
ER -
TY - BOOK
A1 - Hu, Ji
A1 - Cordel, Dirk
A1 - Meinel, Christoph
T1 - A virtual machine architecture for creating IT-security laboratories
N2 - E-learning is a flexible and personalized alternative to traditional education. Nonetheless, existing e-learning systems for IT security education have difficulties in delivering hands-on experience because of the lack of proximity. Laboratory environments and practical exercises are indispensable instruction tools to IT security education, but security education in con-ventional computer laboratories poses the problem of immobility as well as high creation and maintenance costs. Hence, there is a need to effectively transform security laboratories and practical exercises into e-learning forms. This report introduces the Tele-Lab IT-Security architecture that allows students not only to learn IT security principles, but also to gain hands-on security experience by exercises in an online laboratory environment. In this architecture, virtual machines are used to provide safe user work environments instead of real computers. Thus, traditional laboratory environments can be cloned onto the Internet by software, which increases accessibilities to laboratory resources and greatly reduces investment and maintenance costs. Under the Tele-Lab IT-Security framework, a set of technical solutions is also proposed to provide effective functionalities, reliability, security, and performance. The virtual machines with appropriate resource allocation, software installation, and system configurations are used to build lightweight security laboratories on a hosting computer. Reliability and availability of laboratory platforms are covered by the virtual machine management framework. This management framework provides necessary monitoring and administration services to detect and recover critical failures of virtual machines at run time. Considering the risk that virtual machines can be misused for compromising production networks, we present security management solutions to prevent misuse of laboratory resources by security isolation at the system and network levels. This work is an attempt to bridge the gap between e-learning/tele-teaching and practical IT security education. It is not to substitute conventional teaching in laboratories but to add practical features to e-learning. This report demonstrates the possibility to implement hands-on security laboratories on the Internet reliably, securely, and economically.
T3 - Technische Berichte des Hasso-Plattner-Instituts für Digital Engineering an der Universität Potsdam - 13
Y1 - 2006
U6 - http://nbn-resolving.de/urn/resolver.pl?urn:nbn:de:kobv:517-opus-33077
SN - 978-3-939469-13-1
PB - Universitätsverlag Potsdam
CY - Potsdam
ER -
TY - THES
A1 - Hu, Ji
T1 - A virtual machine architecture for IT-security laboratories
T1 - Eine virtuelle maschinenbasierte Architektur für IT-Sicherheitslabore
N2 - This thesis discusses challenges in IT security education, points out a gap between e-learning and practical education, and presents a work to fill the gap. E-learning is a flexible and personalized alternative to traditional education. Nonetheless, existing e-learning systems for IT security education have difficulties in delivering hands-on experience because of the lack of proximity. Laboratory environments and practical exercises are indispensable instruction tools to IT security education, but security education in conventional computer laboratories poses particular problems such as immobility as well as high creation and maintenance costs. Hence, there is a need to effectively transform security laboratories and practical exercises into e-learning forms. In this thesis, we introduce the Tele-Lab IT-Security architecture that allows students not only to learn IT security principles, but also to gain hands-on security experience by exercises in an online laboratory environment. In this architecture, virtual machines are used to provide safe user work environments instead of real computers. Thus, traditional laboratory environments can be cloned onto the Internet by software, which increases accessibility to laboratory resources and greatly reduces investment and maintenance costs. Under the Tele-Lab IT-Security framework, a set of technical solutions is also proposed to provide effective functionalities, reliability, security, and performance. The virtual machines with appropriate resource allocation, software installation, and system configurations are used to build lightweight security laboratories on a hosting computer. Reliability and availability of laboratory platforms are covered by a virtual machine management framework. This management framework provides necessary monitoring and administration services to detect and recover critical failures of virtual machines at run time. Considering the risk that virtual machines can be misused for compromising production networks, we present a security management solution to prevent the misuse of laboratory resources by security isolation at the system and network levels. This work is an attempt to bridge the gap between e-learning/tele-teaching and practical IT security education. It is not to substitute conventional teaching in laboratories but to add practical features to e-learning. This thesis demonstrates the possibility to implement hands-on security laboratories on the Internet reliably, securely, and economically.
N2 - Diese Dissertation beschreibt die Herausforderungen in der IT Sicherheitsausbildung und weist auf die noch vorhandene Lücke zwischen E-Learning und praktischer Ausbildung hin. Sie erklärt einen Ansatz sowie ein System, um diese Lücke zwischen Theorie und Praxis in der elektronischen Ausbildung zu schließen. E-Learning ist eine flexible und personalisierte Alternative zu traditionellen Lernmethoden. Heutigen E-Learning Systemen mangelt es jedoch an der Fähigkeit, praktische Erfahrungen über große Distanzen zu ermöglichen. Labor- bzw. Testumgebungen sowie praktische Übungen sind jedoch unverzichtbar, wenn es um die Ausbildung von Sicherheitsfachkräften geht. Konventionelle Laborumgebungen besitzen allerdings einige Nachteile wie bspw. hoher Erstellungsaufwand, keine Mobilität, hohe Wartungskosten, etc. Die Herausforderung heutiger IT Sicherheitsausbildung ist es daher, praktische Sicherheitslaborumgebungen und Übungen effektiv mittels E-Learning zu unterstützen. In dieser Dissertation wird die Architektur von Tele-Lab IT-Security vorgestellt, die Studenten nicht nur erlaubt theoretische Sicherheitskonzepte zu erlernen, sondern darüber hinaus Sicherheitsübungen in einer Online-Laborumgebung praktisch zu absolvieren. Die Teilnehmer können auf diese Weise wichtige praktische Erfahrungen im Umgang mit Sicherheitsprogrammen sammeln. Zur Realisierung einer sicheren Übungsumgebung, werden virtuelle Maschinen anstatt reale Rechner im Tele-Lab System verwendet. Mittels virtueller Maschinen können leicht Laborumgebungen geklont, verwaltet und über das Internet zugänglich gemacht werden. Im Vergleich zu herkömmlichen Offline-Laboren können somit erhebliche Investitions- und Wartungskosten gespart werden. Das Tele-Lab System bietet eine Reihe von technischen Funktionen, die den effektiven, zuverlässigen und sicheren Betrieb dieses Trainingssystems gewährleistet. Unter Beachtung angemessener Ressourcennutzung, Softwareinstallationen und Systemkonfigurationen wurden virtuelle Maschinen als Übungsstationen erstellt, die auf einem einzelnen Rechner betrieben werden. Für ihre Zuverlässigkeit und Verfügbarkeit ist das Managementsystem der virtuellen Maschinen verantwortlich. Diese Komponente besitzt die notwendigen Überwachungs- und Verwaltungsfunktionen, um kritische Fehler der virtuellen Maschinen während der Laufzeit zu erkennen und zu beheben. Damit die Übungsstationen nicht bspw. zur Kompromittierung von Produktivnetzwerken genutzt werden, beschreibt die Dissertation Sicherheits-Managementlösungen, die mittels Isolation auf System und Netzwerk Ebene genau dieses Risiko verhindern sollen. Diese Arbeit ist der Versuch, die Lücke zwischen E-Learning/Tele-Teaching und praktischer Sicherheitsausbildung zu schließen. Sie verfolgt nicht das Ziel, konventionelle Ausbildung in Offline Laboren zu ersetzen, sondern auch praktische Erfahrungen via E-Learning zu unterstützen. Die Dissertation zeigt die Möglichkeit, praktische Erfahrungen mittels Sicherheitsübungsumgebungen über das Internet auf zuverlässige, sichere und wirtschaftliche Weise zu vermitteln.
KW - Computersicherheit
KW - VM
KW - E-Learning
KW - IT security
KW - virtual machine
KW - E-Learning
Y1 - 2006
U6 - http://nbn-resolving.de/urn/resolver.pl?urn:nbn:de:kobv:517-opus-7818
ER -
TY - JOUR
A1 - Respondek, Tobias
T1 - A workflow for computing potential areas for wind turbines
JF - Process design for natural scientists: an agile model-driven approach
N2 - This paper describes the implementation of a workflow model for service-oriented computing of potential areas for wind turbines in jABC. By implementing a re-executable model the manual effort of a multi-criteria site analysis can be reduced. The aim is to determine the shift of typical geoprocessing tools of geographic information systems (GIS) from the desktop to the web. The analysis is based on a vector data set and mainly uses web services of the “Center for Spatial Information Science and Systems” (CSISS). This paper discusses effort, benefits and problems associated with the use of the web services.
Y1 - 2014
SN - 978-3-662-45005-5
IS - 500
SP - 200
EP - 215
PB - Springer
CY - Berlin
ER -