@article{NavarroOrejasPinoetal.2021,
author = {Navarro, Marisa and Orejas, Fernando and Pino, Elvira and Lambers, Leen},
title = {A navigational logic for reasoning about graph properties},
series = {Journal of logical and algebraic methods in programming},
volume = {118},
journal = {Journal of logical and algebraic methods in programming},
publisher = {Elsevier Science},
address = {Amsterdam [u.a.]},
issn = {2352-2208},
doi = {10.1016/j.jlamp.2020.100616},
pages = {33},
year = {2021},
abstract = {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.},
language = {en}
}
@misc{GieseHenklerHirsch2017,
author = {Giese, Holger and Henkler, Stefan and Hirsch, Martin},
title = {A multi-paradigm approach supporting the modular execution of reconfigurable hybrid systems},
url = {http://nbn-resolving.de/urn:nbn:de:kobv:517-opus4-402896},
pages = {34},
year = {2017},
abstract = {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.},
language = {en}
}
@article{PerachAlexandron2021,
author = {Perach, Shai and Alexandron, Giora},
title = {A MOOC-Based Computer Science Program for Middle School},
series = {EMOOCs 2021},
volume = {2021},
journal = {EMOOCs 2021},
publisher = {Universit{\"a}tsverlag Potsdam},
address = {Potsdam},
isbn = {978-3-86956-512-5},
doi = {10.25932/publishup-51713},
url = {http://nbn-resolving.de/urn:nbn:de:kobv:517-opus4-517133},
pages = {111 -- 127},
year = {2021},
abstract = {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.},
language = {en}
}
@article{Weise2013,
author = {Weise, Martin},
title = {A model for teaching informatics to German secondary school students in English-language bilingual education},
series = {Commentarii informaticae didacticae : (CID)},
journal = {Commentarii informaticae didacticae : (CID)},
number = {6},
publisher = {Universit{\"a}tsverlag Potsdam},
address = {Potsdam},
issn = {1868-0844},
url = {http://nbn-resolving.de/urn:nbn:de:kobv:517-opus-64568},
pages = {127 -- 137},
year = {2013},
abstract = {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.},
language = {en}
}
@article{HartungBorghardt2020,
author = {Hartung, Niklas and Borghardt, Jens Markus},
title = {A mechanistic framework for a priori pharmacokinetic predictions of orally inhaled drugs},
series = {PLoS Computational Biology : a new community journal},
volume = {16},
journal = {PLoS Computational Biology : a new community journal},
number = {12},
publisher = {PLoS},
address = {San Fransisco},
issn = {1553-734X},
doi = {10.1371/journal.pcbi.1008466},
pages = {24},
year = {2020},
abstract = {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.},
language = {en}
}
@article{SchneiderLambersOrejas2021,
author = {Schneider, Sven and Lambers, Leen and Orejas, Fernando},
title = {A logic-based incremental approach to graph repair featuring delta preservation},
series = {International journal on software tools for technology transfer : STTT},
volume = {23},
journal = {International journal on software tools for technology transfer : STTT},
number = {3},
publisher = {Springer},
address = {Berlin ; Heidelberg},
issn = {1433-2779},
doi = {10.1007/s10009-020-00584-x},
pages = {369 -- 410},
year = {2021},
abstract = {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.},
language = {en}
}
@book{SchneiderLambersOrejas2019,
author = {Schneider, Sven and Lambers, Leen and Orejas, Fernando},
title = {A logic-based incremental approach to graph repair},
number = {126},
publisher = {Universit{\"a}tsverlag Potsdam},
address = {Potsdam},
isbn = {978-3-86956-462-3},
issn = {1613-5652},
doi = {10.25932/publishup-42751},
url = {http://nbn-resolving.de/urn:nbn:de:kobv:517-opus4-427517},
publisher = {Universit{\"a}t Potsdam},
pages = {34},
year = {2019},
abstract = {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.},
language = {en}
}
@article{Arnold2007,
author = {Arnold, Holger},
title = {A linearized DPLL calculus with learning},
url = {http://nbn-resolving.de/urn:nbn:de:kobv:517-opus-15421},
year = {2007},
abstract = {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.},
language = {en}
}
@unpublished{Arnold2009,
author = {Arnold, Holger},
title = {A linearized DPLL calculus with clause learning (2nd, revised version)},
url = {http://nbn-resolving.de/urn:nbn:de:kobv:517-opus-29080},
year = {2009},
abstract = {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.},
language = {en}
}
@misc{Wallenta2014,
author = {Wallenta, Daniel},
title = {A Lefschetz fixed point formula for elliptic quasicomplexes},
series = {Postprints der Universit{\"a}t Potsdam : Mathematisch Naturwissenschaftliche Reihe},
journal = {Postprints der Universit{\"a}t Potsdam : Mathematisch Naturwissenschaftliche Reihe},
number = {885},
issn = {1866-8372},
doi = {10.25932/publishup-43547},
url = {http://nbn-resolving.de/urn:nbn:de:kobv:517-opus4-435471},
pages = {577 -- 587},
year = {2014},
abstract = {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.},
language = {en}
}