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 - 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 - 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 - 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 - 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 - 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 - 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 - 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 - 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 - GEN
A1 - Wallenta, Daniel
T1 - A Lefschetz fixed point formula for elliptic quasicomplexes
T2 - Postprints der Universität Potsdam : Mathematisch Naturwissenschaftliche Reihe
N2 - In a recent paper, the Lefschetz number for endomorphisms (modulo trace class operators) of sequences of trace class curvature was introduced. We show that this is a well defined, canonical extension of the classical Lefschetz number and establish the homotopy invariance of this number. Moreover, we apply the results to show that the Lefschetz fixed point formula holds for geometric quasiendomorphisms of elliptic quasicomplexes.
T3 - Zweitveröffentlichungen der Universität Potsdam : Mathematisch-Naturwissenschaftliche Reihe - 885
KW - elliptic complexes
KW - Fredholm complexes
KW - Lefschetz number
Y1 - 2020
U6 - http://nbn-resolving.de/urn/resolver.pl?urn:nbn:de:kobv:517-opus4-435471
SN - 1866-8372
IS - 885
SP - 577
EP - 587
ER -