On Presburger arithmetic extended with non-unary counting quantifiers. - In: Logical methods in computer science, ISSN 1860-5974, Bd. 19 (2023), 3, S. 4:1-4:32
We consider a first-order logic for the integers with addition. This logic extends classical first-order logic by modulo-counting, threshold-counting and exact-counting quantifiers, all applied to tuples of variables (here, residues are given as terms while moduli and thresholds are given explicitly). Our main result shows that satisfaction for this logic is decidable in two-fold exponential space. If only threshold- and exact-counting quantifiers are allowed, we prove an upper bound of alternating two-fold exponential time with linearly many alternations. This latter result almost matches Berman's exact complexity of first-order logic without counting quantifiers. To obtain these results, we first translate threshold- and exact-counting quantifiers into classical first-order logic in polynomial time (which already proves the second result). To handle the remaining modulo-counting quantifiers for tuples, we first reduce them in doubly exponential time to modulo-counting quantifiers for single elements. For these quantifiers, we provide a quantifier elimination procedure similar to Reddy and Loveland's procedure for first-order logic and analyse the growth of coefficients, constants, and moduli appearing in this process. The bounds obtained this way allow to restrict quantification in the original formula to integers of bounded size which then implies the first result mentioned above. Our logic is incomparable with the logic considered by Chistikov et al. in 2022. They allow more general counting operations in quantifiers, but only unary quantifiers. The move from unary to non-unary quantifiers is non-trivial, since, e.g., the non-unary version of the Härtig quantifier results in an undecidable theory.
https://doi.org/10.46298/lmcs-19(3:4)2023
MLflow2PROV: extracting provenance from machine learning experiments. - In: Proceedings of the Seventh Workshop on Data Management for End-to-End Machine Learning (DEEM), (2023), 9, insges. 4 S.
Supporting iterative and explorative workflows for developing machine learning (ML) models, ML experiment management systems (ML EMSs), such as MLflow, are increasingly used to simplify the structured collection and management of ML artifacts, such as ML models, metadata, and code. However, EMSs typically suffer from limited provenance capabilities. As a consequence, it is hard to analyze provenance information and gain knowledge that can be used to improve both ML models and their development workflows. We propose a W3C-PROV-compliant provenance model capturing ML experiment activities that originate from Git and MLflow usage. Moreover, we present the tool MLflow2PROV that extracts provenance graphs according to our model, enabling querying, analyzing, and further processing of collected provenance information.
https://doi.org/10.1145/3595360.3595859
Processing-in-Memory for databases: query processing and data transfer. - In: 19th International Workshop on Data Management on New Hardware, (DaMoN 2023), June 19th 2023, (2023), S. 107-111
The Processing-in-Memory (PIM) paradigm promises to accelerate data processing by pushing down computation to memory, reducing the amount of data transfer between memory and CPU, and - in this way - relieving the CPU from processing. Particularly, in in-memory databases memory access becomes a performance bottleneck. Thus, PIM seems to offer an interesting solution for database processing. In this work, we investigate how commercially available PIM technology can be leveraged to accelerate query processing by offloading (parts of) query operators to memory. Furthermore, we show how to address the problem of limited PIM storage capacity by interleaving transfer and computation and present a cost model for the data placement problem.
https://doi.org/10.1145/3592980.3595323
Zielonka DAG acceptance and regular languages over infinite words. - In: Developments in language theory, (2023), S. 143-155
We study an acceptance type for regular ω-languages called Zielonka DAG acceptance. We focus on deterministic automata with Zielonka DAG acceptance (DZA) and show that they are the first known automaton type with all of the following properties: 1. Emptiness can be decided in non-deterministic logspace. 2. Boolean operations on DZA cause at most polynomial blowup. 3. DZA capture exactly the ω-regular languages. We compare Zielonka DAG acceptance to many other known acceptance types and give a complete description of their relative succinctness. Further, we show that non-deterministic Zielonka DAG automata turn out to be polynomial time equivalent to non-deterministic Büchi automata. We introduce extension acceptance as a helpful tool to establish these results. Extension acceptance also leads to new acceptance types, namely existential and universal extension acceptance.
https://doi.org/10.1007/978-3-031-33264-7_12
Trust me: explainable ML in Self-Organized Network management. - In: Proceedings of IEEE/IFIP Network Operations and Management Symposium 2023, (2023), insges. 6 S.
Machine Learning (ML) powered Self-Organizing Network (SON) functions are an integral part of the 5G(+) network management to automatically learn and optimize the network performance. Third Generation Partnership Project (3GPP) Release 17 confirmed it by providing a foundation for studying ML-based solutions to tackle network management problems. However, despite their ability to provide high-quality solutions, most ML algorithms lack interpretability, leading to a lack of trust from Mobile Network Operators (MNOs) and delaying the fast integration of ML solutions into operational networks. To address this issue, Explainable Machine Learning (xML) techniques can be used to make complex ML models more interpretable, manageable, and trustworthy. In this work, we apply xML methods to explain an implicit coordination scenario between two conflicting SON functions (SFs): Coverage and Capacity optimization (CCO) and Inter Cell Interference Coordination (ICIC). We show how xML methods can be used to see the coordination problem from an ML model point of view, get meaningful insights, and confirm that the ML model captured all the relevant relationships correctly. This in turn helps to build trust in the ML model which allows it to be used for automatic network management.
https://doi.org/10.1109/NOMS56928.2023.10154447
Communication-efficient and scalable management of self-organizing mobile networks. - In: Proceedings of IEEE/IFIP Network Operations and Management Symposium 2023, (2023), insges. 5 S.
The diverse Self-Organizing Network (SON) Functions (SFs) targeted for the different network goals, while executing concurrently, tend to conflict with the operation of each other. It is possible to train data-driven models for SON self-coordination that can capture the complex dynamics between the simultaneously operating SFs. Standardized functions like Management Data Analytics Service (MDAS) would enable several solution providers to participate in the SON ecosystem but the high cost of data-off loading along with privacy concerns render it unfavourable for the mobile network operators. In this work, we propose a Federated Learning (FL) enabled G-SHOCC (Generic engine for Self-Healing, self-optimization and self-Coordination in Cellular networks) framework that provides a communication-efficient and scalable platform to generate high-quality models for SON without the need for transferring raw network data. We train a Deep Neural Network (DNN) model using the FL-enabled G-SHOCC framework to achieve implicit coordination between three intertwined SON functions - CCO, ICIC and COC, and evaluate its performance in terms of coverage and capacity during normal and faulty network scenarios. Finally, we demonstrate that the overall parameter recommendations and the closed-loop performance of the FL model are comparable to the centrally trained version of the DNN model.
https://doi.org/10.1109/NOMS56928.2023.10154274
ATTACH dataset: annotated two-handed assembly actions for human action understanding. - In: ICRA 2023, (2023), S. 11367-11373
With the emergence of collaborative robots (cobots), human-robot collaboration in industrial manufacturing is coming into focus. For a cobot to act autonomously and as an assistant, it must understand human actions during assembly. To effectively train models for this task, a dataset containing suitable assembly actions in a realistic setting is cru-cial. For this purpose, we present the ATTACH dataset, which contains 51.6 hours of assembly with 95.2k annotated fine-grained actions monitored by three cameras, which represent potential viewpoints of a cobot. Since in an assembly context workers tend to perform different actions simultaneously with their two hands, we annotated the performed actions for each hand separately. Therefore, in the ATTACH dataset, more than 68% of annotations overlap with other annotations, which is many times more than in related datasets, typically featuring more simplistic assembly tasks. For better generalization with respect to the background of the working area, we did not only record color and depth images, but also used the Azure Kinect body tracking SDK for estimating 3D skeletons of the worker. To create a first baseline, we report the performance of state-of-the-art methods for action recognition as well as action detection on video and skeleton-sequence inputs. The dataset is available at https://www.tu-ilmenau.de/neurob/data-sets-code/attach-dataset.
https://doi.org/10.1109/ICRA48891.2023.10160633
A little bit attention is all you need for person re-identification. - In: ICRA 2023, (2023), S. 7598-7605
Person re-identification plays a key role in applications where a mobile robot needs to track its users over a long period of time, even if they are partially unobserved for some time, in order to follow them or be available on demand. In this context, deep-learning-based real-time feature extraction on a mobile robot is often performed on special-purpose devices whose computational resources are shared for multiple tasks. Therefore, the inference speed has to be taken into account. In contrast, person re-identification is often improved by architectural changes that come at the cost of significantly slowing down inference. Attention blocks are one such example. We will show that some well-performing attention blocks used in the state of the art are subject to inference costs that are far too high to justify their use for mobile robotic applications. As a consequence, we propose an attention block that only slightly affects the inference speed while keeping up with much deeper networks or more complex attention blocks in terms of re-identification accuracy. We perform extensive neural architecture search to derive rules at which locations this attention block should be integrated into the architecture in order to achieve the best trade-off between speed and accuracy. Finally, we confirm that the best performing configuration on a re-identification benchmark also performs well on an indoor robotic dataset.
https://doi.org/10.1109/ICRA48891.2023.10160304
Three-dimensional light field fundus imaging: automatic determination of diagnostically relevant optic nerve head parameters. - In: Translational Vision Science & Technology, ISSN 2164-2591, Bd. 12 (2023), 7, 21, S. 1-16
Purpose: Morphological changes to the optic nerve head (ONH) can be detected at the early stages of glaucoma. Three-dimensional imaging and analysis may aid in the diagnosis. Light field (LF) fundus cameras can generate three-dimensional (3D) images of optic disc topography from a single shot and are less susceptible to motion artifacts. Here, we introduce a processing method to determine diagnostically relevant ONH parameters automatically and present the results of a subject study performed to validate this method. Methods: The ONHs of 17 healthy subjects were examined and images were acquired with both an LF fundus camera and by optical coherence tomography (OCT). The LF data were analyzed with a novel algorithm and compared with the results of the OCT study. Depth information was reconstructed, and a model with radial basis functions was used for processing of the 3D point cloud and to provide a finite surface. The peripapillary rising and falling edges were evaluated to determine optic disc and cup contours and finally calculate the parameters. Results: Nine of the 17 subjects exhibited prominent optic cups. The contours and ONH parameters determined by an analysis of LF 3D imaging largely agreed with the data obtained from OCT. The median disc areas, cup areas, and cup depths differed by 0.17 mm^2, -0.04 mm^2, and -0.07 mm, respectively. Conclusions: The findings presented here suggest the possibility of using LF data to evaluate the ONH. Translational Relevance: LF data can be used to determine geometric parameters of the ONH and thus may be suitable for future use in glaucoma diagnostics.
https://doi.org/10.1167/tvst.12.7.21
Multivariate assessment of linear and non-linear causal coupling pathways within the central-autonomic-network in patients suffering from schizophrenia. - Ilmenau : Universitätsbibliothek, 2023. - 1 Online-Ressource (viii, 153 Seiten)
Technische Universität Ilmenau, Dissertation 2023
Im Bereich der Zeitreihenanalyse richtet sich das Interesse zunehmend darauf, wie Einblicke in die Interaktions- und Regulationsprozesse von pathophysiologischen- und physiologischen Zuständen erlangt werden können. Neuste Fortschritte in der nichtlinearen Dynamik, der Informationstheorie und der Netzwerktheorie liefern dabei fundiertes Wissen über Kopplungswege innerhalb (patho)physiologischer (Sub)Systeme. Kopplungsanalysen zielen darauf ab, ein besseres Verständnis dafür zu erlangen, wie die verschiedenen integrierten regulatorischen (Sub)Systeme mit ihren komplexen Strukturen und Regulationsmechanismen das globale Verhalten und die unterschiedlichen physiologischen Funktionen auf der Ebene des Organismus beschreiben. Insbesondere die Erfassung und Quantifizierung der Kopplungsstärke und -richtung sind wesentliche Aspekte für ein detaillierteres Verständnis physiologischer Regulationsprozesse. Ziel dieser Arbeit war die Charakterisierung kurzfristiger unmittelbarer zentral-autonomer Kopplungspfade (top-to-bottom und bottom to top) durch die Kopplungsanalysen der Herzfrequenz, des systolischen Blutdrucks, der Atmung und zentraler Aktivität (EEG) bei schizophrenen Patienten und Gesunden. Dafür wurden in dieser Arbeit neue multivariate kausale und nicht-kausale, lineare und nicht-lineare Kopplungsanalyseverfahren (HRJSD, mHRJSD, NSTPDC) entwickelt, die in der Lage sind, die Kopplungsstärke und -richtung, sowie deterministische regulatorische Kopplungsmuster innerhalb des zentralen-autonomen Netzwerks zu quantifizieren und zu klassifizieren. Diese Kopplungsanalyseverfahren haben ihre eigenen Besonderheiten, die sie einzigartig machen, auch im Vergleich zu etablierten Kopplungsverfahren. Sie erweitern das Spektrum neuartiger Kopplungsansätze für die Biosignalanalyse und tragen auf ihre Weise zur Gewinnung detaillierter Informationen und damit zu einer verbesserten Diagnostik/Therapie bei. Die Hauptergebnisse dieser Arbeit zeigen signifikant schwächere nichtlineare zentral-kardiovaskuläre und zentral-kardiorespiratorische Kopplungswege und einen signifikant stärkeren linearen zentralen Informationsfluss in Richtung des Herzkreislaufsystems auf, sowie einen signifikant stärkeren linearen respiratorischen Informationsfluss in Richtung des zentralen Nervensystems in der Schizophrenie im Vergleich zu Gesunden. Die detaillierten Erkenntnisse darüber, wie die verschiedenen zentral-autonomen Netzwerke mit paranoider Schizophrenie assoziiert sind, können zu einem besseren Verständnis darüber führen, wie zentrale Aktivierung und autonome Reaktionen und/oder Aktivierung in physiologischen Netzwerken unter pathophysiologischen Bedingungen zusammenhängen.
https://doi.org/10.22032/dbt.57589