+**********************************************************************
*
*
* Einladung
*
*
*
* Informatik-Kolloquium
*
*
*
+**********************************************************************
Zeit: Dienstag, 10. September 2024, 14.00 Uhr
Ort: Raum 9222, Gebäude E3, Ahornstr. 55
Referentin: Prof. Dr. Paula Herber
University of Münster
Title: Formal Verification of Cyber-physical Systems using Domain-specific
Abstractions
Abstract:
Cyber-physical systems have become ubiquitous in our daily lives, and their
complexity continually evolves to unprecedented levels. In addition to their
heterogeneity and interaction with a physical environment, we see a
tremendous increase in the use of learning to make autonomous decisions in
dynamic environments. These developments pose significant challenges for
ensuring the safety and reliability of cyber-physical systems. Formal
methods have the potential to guarantee crucial safety properties under all
circumstances, but are incredibly expensive and severely suffer from
scalability issues. In this talk, I will summarize some of our recent
efforts towards reusable specification and more scalable verification of
cyber-physical systems using domain-specific abstractions.
Es laden ein: die Dozentinnen und Dozenten der Informatik
**********************************************************************
*
*
* Einladung
*
*
*
* Informatik-Oberseminar
*
*
*
***********************************************************************
Zeit: Mittwoch, 28 August 2024, 15:30 Uhr
Ort: Raum 9222, E3, Informatikzentrum
Zoom:
https://rwth.zoom-x.de/j/66261562709?pwd=2driMW8j0cRJLiYFWNJRqRp4Lya80Z.1
Meeting-ID: 662 6156 2709
Kenncode: 337848
Referent: Yingbo Gao, M.Sc. (Lehrstuhl Informatik 6)
Thema: Language Modeling and Machine Translation: Improvements in
Training and Modeling
Abstract:
Substantial improvements in language modeling and machine translation
have been achieved since the wide adoption of artificial neural
networks. In this talk, we discuss three directions related to training
and modeling in neural language modeling and neural machine translation.
First, sampling-based training criteria are investigated in order to
speed up the training of neural language models with large vocabularies.
Second, label smoothing, input smoothing as well as multi-agent training
are studied to improve the generalization of neural machine translation
models. Finally, a language modeling approach for machine translation is
proposed to simplify the architecture of existing translation models.
Es laden ein: die Dozentinnen und Dozenten der Informatik
--
Stephanie Jansen
Faculty of Mathematics, Computer Science and Natural Sciences
Chair of Computer Science 6
ML - Machine Learning and Reasoning
RWTH Aachen University
Theaterstraße 35-39
D-52062 Aachen
Tel: +49 241 80-21601
sek(a)ml.rwth-aachen.de
www.hltpr.rwth-aachen.de
+**********************************************************************
*
*
* Einladung
*
*
*
* Informatik-Oberseminar
*
*
*
+**********************************************************************
Zeit: Freitag, 30. August 2024, 11:00 Uhr
Ort: Raum 9222 (Informatikzentrum E3, Ahornstraße 55)
Referent: Matthias Naaf, M.Sc.
LuFG Mathematische Grundlagen der Informatik
Thema: Logic, Semirings, and Fixed Points
Abstract:
Why does my SQL query return a particular answer? How does Hanna win an
infinite graph game against Simon? These questions can be answered with
semiring semantics, which was introduced by Green, Karvounarakis, and
Tannen (2007) for database provenance and has since been extended to
various logics within and beyond the database setting. In this talk,
we study semiring semantics for the fixed-point logic LFP, which
(despite its name) features both least and greatest fixed points.
The common theme in semiring semantics is the interplay of logic and
algebra, such as the compatibility with semiring homomorphisms and the
use of freely generated semirings to represent provenance information.
This becomes particularly interesting for fixed-point logic, where
additional algebraic and order-theoretic assumptions on the semirings
must be made to ensure the existence of fixed points. A key question
is the algorithmic computation of fixed points in these semirings.
Several techniques have been developed for least fixed points,
with the Newton iteration (Esparza, Kiefer, and Luttenberger, 2010)
emerging as the most general technique, but it was not known how to
compute greatest fixed points. We address this issue by providing an
efficient closed-form solution for greatest fixed points of polynomial
systems over absorptive semirings.
Using the example of Büchi games, we show how semiring semantics of
LFP can be applied to analyse winning strategies in infinite games.
Lastly, we take the perspective of model theory and study how the
classical 0-1 laws about the asymptotic behaviour of logic on random
structures can be generalised to semiring semantics of first-order
logic. By combining our proof with the fixed-point computation,
we further extend the 0-1 law to semiring semantics of LFP.
Es laden ein: die Dozentinnen und Dozenten der Informatik
+**********************************************************************
*
*
* Einladung
*
*
*
* Informatik-Oberseminar
*
*
*
+**********************************************************************
Zeit: Freitag, 16.08.2024, 10:00 Uhr
Ort: Informatikzentrum der RWTH Aachen University, Gebäude E3, 2.
Etage, Raum 9222
Referent: Eva Fluck, M.Sc.
Lehrstuhl für Logik und Theorie diskreter Systeme
Thema: Graph decompositions. A study on decompositions of graphs and
their application to logic and data science
Abstract:
We study decompositions of graphs and their application to the
expressiveness of first-order logic with counting quantifiers and
clustering data. Besides the decompositions themselves we also consider
graph parameters that arise from these decompositions as well as
obstructions to the existence of good decompositions.
The graph class T_q^k are all graphs which have a bounded tree-depth
decomposition that also bounds the width. Its homomorphism
indistinguishability relation enjoys a rich connection to the
expressiveness of counting logic, as shown by Dawar, Jakl and Reggio
(2021). Building upon ideas by Dvořák (2010), we reprove this
connection. Our proof strategy also enables to construct a graph class
which characterizes equivalence under guarded counting logic. A graph
theoretic analysis of T_q^k allows us separate it from the intersection
of TW_k−1 , the class of graphs of tree-width at most k−1, and TD_q the
graphs of tree-depth at most q, if q is sufficiently larger than k.
This also yields a new characterization of tree-depth via
treedecompositions and a characterization of T_q^k via a Cops-and-
Robber game. To lift this separation to the respective equivalence
relations, we show that this game is monotone, that is Robber can never
reach a vertex that was cleared in some earlier round. This also give a
novel proof of the monotonicity of the Cops-and-Robber game for tree-
width without the use of any dual object, like brambles. Another part
of the separation of the equivalence classes is to prove that T_q^k and
TD_q are homomorphism distinguishing closed, which was conjectured by
Roberson (2022).
Tangles are a concept to formalize regions of high connectivity in
graphs in an unambiguous way. It can be translated to more abstract
connectivity systems, where they describe highly connected regions in
the underling universe. Recently they emerged as a new approach to
clustering data. We find that the non-trivial clusters resulting from
the well known single linkage hierarchical clustering algorithm are
exactly the tangles of an appropriately chosen connectivity function on
the data points. We generalize this connection to a one-to-one
correspondence between connectivity functions that are maximum-
submodular and dendograms which are a way to represent the result of an
arbitrary hierarchical clustering algorithm.
Es laden ein: die Dozentinnen und Dozenten der Informatik
+**********************************************************************
*
*
* Einladung
*
*
*
* Informatik-Oberseminar
*
*
*
+**********************************************************************
Zeit: Freitag, 16. August 2024, 10:00 Uhr
Ort: UMIC_025 (2165|025), Mies-van-der-Rohe-Str. 15, EG
Referent: Malte Breuer M.Sc.
Lehr- und Forschungsgebiet IT-Sicherheit
Thema: Privacy-Preserving Kidney Exchange
Abstract:
Chronic kidney disease has become one of the most common causes of
natural death in our modern society. The preferred treatment for chronic
kidney disease is the transplant of a kidney from a living donor, who is
typically a close friend or relative of the patient. An impediment that
prevents such a living donation is that the found living donor is
sometimes not medically compatible with the patient. Kidney exchange
enables a patient to still receive a kidney transplant in such a
situation by exchanging the living donor with other patients. Nowadays,
many countries have centralized systems that organize kidney exchange,
often on a nationwide scale. Hospitals can register their associated
pairs of patients and medically incompatible donors with a central
platform, which then tries to find potential exchanges among all
registered pairs of patients and donors.
Such a centralized kidney exchange system, however, harbors severe
security risks that make the central platform susceptible to
manipulation and corruption. The core issue is that the operator of the
platform alone is responsible for the entire computation of the
exchanges. This, for example, allows the platform operator to manipulate
the computation such that a particular patient is treated with priority.
This does not only make the platform operator susceptible to corruption
but it also makes the platform a prime target for high impact attacks
aimed at manipulating the computation of exchanges. The central platform
becomes an even more attractive target for attackers as it stores the
sensitive data of many patients and donors. Thus, any attack that leads
to a data breach has a direct impact on the privacy of the sensitive
data of many individuals.
The main research goal of this thesis is to develop an alternative
approach for kidney exchange that is resistant to manipulation and
corruption, and protects the sensitive data of the involved patients and
donors. To this end, we propose the model of a privacy-preserving kidney
exchange system that follows a decentralized approach, where the
computation of exchanges is distributed among a set of so-called
computing peers. This model ensures that a computing peer is neither
able to manipulate the computation of the exchanges nor to learn any
information on the sensitive data of the involved patients and donors.
We achieve this by using a cryptographic technique called secure
multi-party computation. This allows a set of parties to compute a
functionality on their private inputs such that each party only learns
its own input and output and what can be deduced from both. The core
contribution of this thesis is then the development of secure
multi-party computation protocols that enable the computing peers to
efficiently compute the exchanges for a set of patients and their
associated medically incompatible donors. We evaluate the run time of
all our protocols and show that our most efficient protocol scales for
the large numbers of patients and donors that are to be expected in
practice. Thereupon, we simulate the use of our most efficient protocols
in our model of a privacy-preserving kidney exchange system over time
using real-world data. Our simulations show that the number of
transplants achieved over time in our privacy-preserving model is
comparable to the number of transplants achieved in the model that is
implemented by the existing kidney exchange systems that are susceptible
to manipulation and corruption. Thus, our model allows for the
replacement of most existing kidney exchange systems at a small or
sometimes even negligible impact on the number of transplants over time,
while significantly increasing the security guarantees compared to the
existing systems.
Es laden ein: die Dozentinnen und Dozenten der Informatik