602 Search Results for "R�mmele, Stefan"


Document
Skyline Operators for Document Spanners

Authors: Antoine Amarilli, Benny Kimelfeld, Sébastien Labbé, and Stefan Mengel

Published in: LIPIcs, Volume 290, 27th International Conference on Database Theory (ICDT 2024)


Abstract
When extracting a relation of spans (intervals) from a text document, a common practice is to filter out tuples of the relation that are deemed dominated by others. The domination rule is defined as a partial order that varies along different systems and tasks. For example, we may state that a tuple is dominated by tuples that extend it by assigning additional attributes, or assigning larger intervals. The result of filtering the relation would then be the skyline according to this partial order. As this filtering may remove most of the extracted tuples, we study whether we can improve the performance of the extraction by compiling the domination rule into the extractor. To this aim, we introduce the skyline operator for declarative information extraction tasks expressed as document spanners. We show that this operator can be expressed via regular operations when the domination partial order can itself be expressed as a regular spanner, which covers several natural domination rules. Yet, we show that the skyline operator incurs a computational cost (under combined complexity). First, there are cases where the operator requires an exponential blowup on the number of states needed to represent the spanner as a sequential variable-set automaton. Second, the evaluation may become computationally hard. Our analysis more precisely identifies classes of domination rules for which the combined complexity is tractable or intractable.

Cite as

Antoine Amarilli, Benny Kimelfeld, Sébastien Labbé, and Stefan Mengel. Skyline Operators for Document Spanners. In 27th International Conference on Database Theory (ICDT 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 290, pp. 7:1-7:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)


Copy BibTex To Clipboard

@InProceedings{amarilli_et_al:LIPIcs.ICDT.2024.7,
  author =	{Amarilli, Antoine and Kimelfeld, Benny and Labb\'{e}, S\'{e}bastien and Mengel, Stefan},
  title =	{{Skyline Operators for Document Spanners}},
  booktitle =	{27th International Conference on Database Theory (ICDT 2024)},
  pages =	{7:1--7:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-312-6},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{290},
  editor =	{Cormode, Graham and Shekelyan, Michael},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICDT.2024.7},
  URN =		{urn:nbn:de:0030-drops-197898},
  doi =		{10.4230/LIPIcs.ICDT.2024.7},
  annote =	{Keywords: Information Extraction, Document Spanners, Query Evaluation}
}
Document
Direct Access for Conjunctive Queries with Negations

Authors: Florent Capelli and Oliver Irwin

Published in: LIPIcs, Volume 290, 27th International Conference on Database Theory (ICDT 2024)


Abstract
Given a conjunctive query Q and a database 𝐃, a direct access to the answers of Q over 𝐃 is the operation of returning, given an index j, the j-th answer for some order on its answers. While this problem is #P-hard in general with respect to combined complexity, many conjunctive queries have an underlying structure that allows for a direct access to their answers for some lexicographical ordering that takes polylogarithmic time in the size of the database after a polynomial time precomputation. Previous work has precisely characterised the tractable classes and given fine-grained lower bounds on the precomputation time needed depending on the structure of the query. In this paper, we generalise these tractability results to the case of signed conjunctive queries, that is, conjunctive queries that may contain negative atoms. Our technique is based on a class of circuits that can represent relational data. We first show that this class supports tractable direct access after a polynomial time preprocessing. We then give bounds on the size of the circuit needed to represent the answer set of signed conjunctive queries depending on their structure. Both results combined together allow us to prove the tractability of direct access for a large class of conjunctive queries. On the one hand, we recover the known tractable classes from the literature in the case of positive conjunctive queries. On the other hand, we generalise and unify known tractability results about negative conjunctive queries - that is, queries having only negated atoms. In particular, we show that the class of β-acyclic negative conjunctive queries and the class of bounded nest set width negative conjunctive queries admit tractable direct access.

Cite as

Florent Capelli and Oliver Irwin. Direct Access for Conjunctive Queries with Negations. In 27th International Conference on Database Theory (ICDT 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 290, pp. 13:1-13:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)


Copy BibTex To Clipboard

@InProceedings{capelli_et_al:LIPIcs.ICDT.2024.13,
  author =	{Capelli, Florent and Irwin, Oliver},
  title =	{{Direct Access for Conjunctive Queries with Negations}},
  booktitle =	{27th International Conference on Database Theory (ICDT 2024)},
  pages =	{13:1--13:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-312-6},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{290},
  editor =	{Cormode, Graham and Shekelyan, Michael},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICDT.2024.13},
  URN =		{urn:nbn:de:0030-drops-197958},
  doi =		{10.4230/LIPIcs.ICDT.2024.13},
  annote =	{Keywords: Conjunctive queries, factorized databases, direct access, hypertree decomposition}
}
Document
Optimally Rewriting Formulas and Database Queries: A Confluence of Term Rewriting, Structural Decomposition, and Complexity

Authors: Hubie Chen and Stefan Mengel

Published in: LIPIcs, Volume 290, 27th International Conference on Database Theory (ICDT 2024)


Abstract
A central computational task in database theory, finite model theory, and computer science at large is the evaluation of a first-order sentence on a finite structure. In the context of this task, the width of a sentence, defined as the maximum number of free variables over all subformulas, has been established as a crucial measure, where minimizing width of a sentence (while retaining logical equivalence) is considered highly desirable. An undecidability result rules out the possibility of an algorithm that, given a first-order sentence, returns a logically equivalent sentence of minimum width; this result motivates the study of width minimization via syntactic rewriting rules, which is this article’s focus. For a number of common rewriting rules (which are known to preserve logical equivalence), including rules that allow for the movement of quantifiers, we present an algorithm that, given a positive first-order sentence ϕ, outputs the minimum-width sentence obtainable from ϕ via application of these rules. We thus obtain a complete algorithmic understanding of width minimization up to the studied rules; this result is the first one - of which we are aware - that establishes this type of understanding in such a general setting. Our result builds on the theory of term rewriting and establishes an interface among this theory, query evaluation, and structural decomposition theory.

Cite as

Hubie Chen and Stefan Mengel. Optimally Rewriting Formulas and Database Queries: A Confluence of Term Rewriting, Structural Decomposition, and Complexity. In 27th International Conference on Database Theory (ICDT 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 290, pp. 16:1-16:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)


Copy BibTex To Clipboard

@InProceedings{chen_et_al:LIPIcs.ICDT.2024.16,
  author =	{Chen, Hubie and Mengel, Stefan},
  title =	{{Optimally Rewriting Formulas and Database Queries: A Confluence of Term Rewriting, Structural Decomposition, and Complexity}},
  booktitle =	{27th International Conference on Database Theory (ICDT 2024)},
  pages =	{16:1--16:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-312-6},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{290},
  editor =	{Cormode, Graham and Shekelyan, Michael},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICDT.2024.16},
  URN =		{urn:nbn:de:0030-drops-197984},
  doi =		{10.4230/LIPIcs.ICDT.2024.16},
  annote =	{Keywords: width, query rewriting, structural decomposition, term rewriting}
}
Document
A Characterization of Efficiently Compilable Constraint Languages

Authors: Christoph Berkholz, Stefan Mengel, and Hermann Wilhelm

Published in: LIPIcs, Volume 289, 41st International Symposium on Theoretical Aspects of Computer Science (STACS 2024)


Abstract
A central task in knowledge compilation is to compile a CNF-SAT instance into a succinct representation format that allows efficient operations such as testing satisfiability, counting, or enumerating all solutions. Useful representation formats studied in this area range from ordered binary decision diagrams (OBDDs) to circuits in decomposable negation normal form (DNNFs). While it is known that there exist CNF formulas that require exponential size representations, the situation is less well studied for other types of constraints than Boolean disjunctive clauses. The constraint satisfaction problem (CSP) is a powerful framework that generalizes CNF-SAT by allowing arbitrary sets of constraints over any finite domain. The main goal of our work is to understand for which type of constraints (also called the constraint language) it is possible to efficiently compute representations of polynomial size. We answer this question completely and prove two tight characterizations of efficiently compilable constraint languages, depending on whether target format is structured. We first identify the combinatorial property of "strong blockwise decomposability" and show that if a constraint language has this property, we can compute DNNF representations of linear size. For all other constraint languages we construct families of CSP-instances that provably require DNNFs of exponential size. For a subclass of "strong uniformly blockwise decomposable" constraint languages we obtain a similar dichotomy for structured DNNFs. In fact, strong (uniform) blockwise decomposability even allows efficient compilation into multi-valued analogs of OBDDs and FBDDs, respectively. Thus, we get complete characterizations for all knowledge compilation classes between O(B)DDs and DNNFs.

Cite as

Christoph Berkholz, Stefan Mengel, and Hermann Wilhelm. A Characterization of Efficiently Compilable Constraint Languages. In 41st International Symposium on Theoretical Aspects of Computer Science (STACS 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 289, pp. 11:1-11:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)


Copy BibTex To Clipboard

@InProceedings{berkholz_et_al:LIPIcs.STACS.2024.11,
  author =	{Berkholz, Christoph and Mengel, Stefan and Wilhelm, Hermann},
  title =	{{A Characterization of Efficiently Compilable Constraint Languages}},
  booktitle =	{41st International Symposium on Theoretical Aspects of Computer Science (STACS 2024)},
  pages =	{11:1--11:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-311-9},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{289},
  editor =	{Beyersdorff, Olaf and Kant\'{e}, Mamadou Moustapha and Kupferman, Orna and Lokshtanov, Daniel},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2024.11},
  URN =		{urn:nbn:de:0030-drops-197214},
  doi =		{10.4230/LIPIcs.STACS.2024.11},
  annote =	{Keywords: constraint satisfaction, knowledge compilation, dichotomy, DNNF}
}
Document
A Subquadratic Bound for Online Bisection

Authors: Marcin Bienkowski and Stefan Schmid

Published in: LIPIcs, Volume 289, 41st International Symposium on Theoretical Aspects of Computer Science (STACS 2024)


Abstract
The online bisection problem is a natural dynamic variant of the classic optimization problem, where one has to dynamically maintain a partition of n elements into two clusters of cardinality n/2. During runtime, an online algorithm is given a sequence of requests, each being a pair of elements: an inter-cluster request costs one unit while an intra-cluster one is free. The algorithm may change the partition, paying a unit cost for each element that changes its cluster. This natural problem admits a simple deterministic O(n²)-competitive algorithm [Avin et al., DISC 2016]. While several significant improvements over this result have been obtained since the original work, all of them either limit the generality of the input or assume some form of resource augmentation (e.g., larger clusters). Moreover, the algorithm of Avin et al. achieves the best known competitive ratio even if randomization is allowed. In this paper, we present the first randomized online algorithm that breaks this natural quadratic barrier and achieves a competitive ratio of Õ(n^{23/12}) without resource augmentation and for an arbitrary sequence of requests.

Cite as

Marcin Bienkowski and Stefan Schmid. A Subquadratic Bound for Online Bisection. In 41st International Symposium on Theoretical Aspects of Computer Science (STACS 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 289, pp. 14:1-14:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)


Copy BibTex To Clipboard

@InProceedings{bienkowski_et_al:LIPIcs.STACS.2024.14,
  author =	{Bienkowski, Marcin and Schmid, Stefan},
  title =	{{A Subquadratic Bound for Online Bisection}},
  booktitle =	{41st International Symposium on Theoretical Aspects of Computer Science (STACS 2024)},
  pages =	{14:1--14:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-311-9},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{289},
  editor =	{Beyersdorff, Olaf and Kant\'{e}, Mamadou Moustapha and Kupferman, Orna and Lokshtanov, Daniel},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2024.14},
  URN =		{urn:nbn:de:0030-drops-197247},
  doi =		{10.4230/LIPIcs.STACS.2024.14},
  annote =	{Keywords: Bisection, Graph Partitioning, online balanced Repartitioning, online Algorithms, competitive Analysis}
}
Document
The AC⁰-Complexity of Visibly Pushdown Languages

Authors: Stefan Göller and Nathan Grosshans

Published in: LIPIcs, Volume 289, 41st International Symposium on Theoretical Aspects of Computer Science (STACS 2024)


Abstract
We study the question of which visibly pushdown languages (VPLs) are in the complexity class AC⁰ and how to effectively decide this question. Our contribution is to introduce a particular subclass of one-turn VPLs, called intermediate VPLs, for which the raised question is entirely unclear: to the best of our knowledge our research community is unaware of containment or non-containment in AC⁰ for any language in our newly introduced class. Our main result states that there is an algorithm that, given a visibly pushdown automaton, correctly outputs exactly one of the following: that its language L is in AC⁰, some m ≥ 2 such that MODₘ (the words over {0,1} having a number of 1’s divisible by m) is constant-depth reducible to L (implying that L is not in AC⁰), or a finite disjoint union of intermediate VPLs that L is constant-depth equivalent to. In the latter of the three cases one can moreover effectively compute k,l ∈ ℕ_{> 0} with k≠l such that the concrete intermediate VPL L(S → ε ∣ ac^{k-1}Sb₁ ∣ ac^{l-1}Sb₂) is constant-depth reducible to the language L. Due to their particular nature we conjecture that either all intermediate VPLs are in AC⁰ or all are not. As a corollary of our main result we obtain that in case the input language is a visibly counter language our algorithm can effectively determine if it is in AC⁰ - hence our main result generalizes a result by Krebs et al. stating that it is decidable if a given visibly counter language is in AC⁰ (when restricted to well-matched words). For our proofs we revisit so-called Ext-algebras (introduced by Czarnetzki et al.), which are closely related to forest algebras (introduced by Bojańczyk and Walukiewicz), and use Green’s relations.

Cite as

Stefan Göller and Nathan Grosshans. The AC⁰-Complexity of Visibly Pushdown Languages. In 41st International Symposium on Theoretical Aspects of Computer Science (STACS 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 289, pp. 38:1-38:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)


Copy BibTex To Clipboard

@InProceedings{goller_et_al:LIPIcs.STACS.2024.38,
  author =	{G\"{o}ller, Stefan and Grosshans, Nathan},
  title =	{{The AC⁰-Complexity of Visibly Pushdown Languages}},
  booktitle =	{41st International Symposium on Theoretical Aspects of Computer Science (STACS 2024)},
  pages =	{38:1--38:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-311-9},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{289},
  editor =	{Beyersdorff, Olaf and Kant\'{e}, Mamadou Moustapha and Kupferman, Orna and Lokshtanov, Daniel},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2024.38},
  URN =		{urn:nbn:de:0030-drops-197483},
  doi =		{10.4230/LIPIcs.STACS.2024.38},
  annote =	{Keywords: Visibly pushdown languages, Circuit Complexity, AC0}
}
Document
Complete Volume
OASIcs, Volume 117, NG-RES 2024, Complete Volume

Authors: Patrick Meumeu Yomsi and Stefan Wildermann

Published in: OASIcs, Volume 117, Fifth Workshop on Next Generation Real-Time Embedded Systems (NG-RES 2024)


Abstract
OASIcs, Volume 117, NG-RES 2024, Complete Volume

Cite as

Fifth Workshop on Next Generation Real-Time Embedded Systems (NG-RES 2024). Open Access Series in Informatics (OASIcs), Volume 117, pp. 1-62, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)


Copy BibTex To Clipboard

@Proceedings{yomsi_et_al:OASIcs.NG-RES.2024,
  title =	{{OASIcs, Volume 117, NG-RES 2024, Complete Volume}},
  booktitle =	{Fifth Workshop on Next Generation Real-Time Embedded Systems (NG-RES 2024)},
  pages =	{1--62},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-313-3},
  ISSN =	{2190-6807},
  year =	{2024},
  volume =	{117},
  editor =	{Yomsi, Patrick Meumeu and Wildermann, Stefan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/OASIcs.NG-RES.2024},
  URN =		{urn:nbn:de:0030-drops-197028},
  doi =		{10.4230/OASIcs.NG-RES.2024},
  annote =	{Keywords: OASIcs, Volume 117, NG-RES 2024, Complete Volume}
}
Document
Front Matter
Front Matter, Table of Contents, Preface, Conference Organization

Authors: Patrick Meumeu Yomsi and Stefan Wildermann

Published in: OASIcs, Volume 117, Fifth Workshop on Next Generation Real-Time Embedded Systems (NG-RES 2024)


Abstract
Front Matter, Table of Contents, Preface, Conference Organization

Cite as

Fifth Workshop on Next Generation Real-Time Embedded Systems (NG-RES 2024). Open Access Series in Informatics (OASIcs), Volume 117, pp. 0:i-0:x, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)


Copy BibTex To Clipboard

@InProceedings{yomsi_et_al:OASIcs.NG-RES.2024.0,
  author =	{Yomsi, Patrick Meumeu and Wildermann, Stefan},
  title =	{{Front Matter, Table of Contents, Preface, Conference Organization}},
  booktitle =	{Fifth Workshop on Next Generation Real-Time Embedded Systems (NG-RES 2024)},
  pages =	{0:i--0:x},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-313-3},
  ISSN =	{2190-6807},
  year =	{2024},
  volume =	{117},
  editor =	{Yomsi, Patrick Meumeu and Wildermann, Stefan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/OASIcs.NG-RES.2024.0},
  URN =		{urn:nbn:de:0030-drops-197032},
  doi =		{10.4230/OASIcs.NG-RES.2024.0},
  annote =	{Keywords: Front Matter, Table of Contents, Preface, Conference Organization}
}
Document
Invited Paper
HMB: Scheduling PREM-Like Real-Time Tasks at High Memory Bandwidth (Invited Paper)

Authors: Mohammadhassan Gholami Derouei, Paolo Valente, Marco Solieri, and Andrea Marongiu

Published in: OASIcs, Volume 117, Fifth Workshop on Next Generation Real-Time Embedded Systems (NG-RES 2024)


Abstract
Current homogeneous and heterogeneous computing systems reach high performance through parallelization. Yet, parallel execution of tasks entails non-trivial latency-vs-throughput issues when it comes to concurrent accesses to shared memory. In this respect, effective bandwidth regulation solutions do exist, and provide a basic mechanism to control the latency of memory accesses. Such solutions, though, are often cumbersome to deploy and to configure to guarantee both bounded latency and high utilization of the memory bandwidth. The problem is that memory latency varies non-linearly with the number and type of concurrent accesses, and the latter may in turn vary with time, often unpredictably. For this reason, previous attempts at memory regulation in scheduling solutions resulted either in poor real-time execution guarantees, or in severe underutilization of the memory bandwidth. In this paper, we outline High Memory Bandwidth (HMB), a scheduling solution that guarantees bounded response times to real-time task sets through memory regulation, while also reaching a high utilization memory bandwidth. Since the complete solution is complex, just like the problem it addresses, this preliminary work defines in full detail only the core mechanism. This mechanism builds on the notion of memory access slowdown experienced by any processor performing back-to-back memory operations; this slowdown is due to the interference generated by other processors also accessing the memory at the same time. The core mechanism assumes that each processor can tolerate a certain amount of slowdown before the timing behavior of the task(s) it is running is compromised. Each processor has a priority assigned: the higher the priority, the more stringent the timing requirements. The slowdown can be controlled by regulating with precision the maximum amount of system bandwidth each processor is allowed to use, based on its priority. The proposed mechanism finds the maximum bandwidth each processor can use such that the highest number of processors simultaneously accessing memory is found (thus avoiding memory bandwidth underutilization) while guaranteeing that the slowdown of each processor is kept within the tolerated limits.

Cite as

Mohammadhassan Gholami Derouei, Paolo Valente, Marco Solieri, and Andrea Marongiu. HMB: Scheduling PREM-Like Real-Time Tasks at High Memory Bandwidth (Invited Paper). In Fifth Workshop on Next Generation Real-Time Embedded Systems (NG-RES 2024). Open Access Series in Informatics (OASIcs), Volume 117, pp. 1:1-1:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)


Copy BibTex To Clipboard

@InProceedings{gholamiderouei_et_al:OASIcs.NG-RES.2024.1,
  author =	{Gholami Derouei, Mohammadhassan and Valente, Paolo and Solieri, Marco and Marongiu, Andrea},
  title =	{{HMB: Scheduling PREM-Like Real-Time Tasks at High Memory Bandwidth}},
  booktitle =	{Fifth Workshop on Next Generation Real-Time Embedded Systems (NG-RES 2024)},
  pages =	{1:1--1:18},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-313-3},
  ISSN =	{2190-6807},
  year =	{2024},
  volume =	{117},
  editor =	{Yomsi, Patrick Meumeu and Wildermann, Stefan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/OASIcs.NG-RES.2024.1},
  URN =		{urn:nbn:de:0030-drops-197049},
  doi =		{10.4230/OASIcs.NG-RES.2024.1},
  annote =	{Keywords: Heterogenous systems, Parallel execution, Shared memory, Bandwidth regulation, Memory access, Real-time execution, Memory bandwidth utilization, High Memory Bandwidth (HMB), Memory access slowdown, Memory interference, Memory-centric scheduling}
}
Document
Invited Paper
A Multi-Modal Distributed Real-Time IoT System for Urban Traffic Control (Invited Paper)

Authors: Zeba Khanam, Vejey Pradeep Suresh Achari, Issam Boukhennoufa, Anish Jindal, and Amit Kumar Singh

Published in: OASIcs, Volume 117, Fifth Workshop on Next Generation Real-Time Embedded Systems (NG-RES 2024)


Abstract
Traffic congestion is one of the growing urban problem with associated problems like fuel wastage, loss of lives, and slow productivity. The existing traffic system uses programming logic control (PLC) with round-robin scheduling algorithm. Recent works have proposed IoT-based frameworks that use traffic density of each lane to control traffic movement, but they suffer from low accuracy due to lack of emergency vehicle image datasets for training deep neural networks. In this paper, we propose a novel distributed IoT framework that is based on two observations. The first observation is major structural changes to road are rare. This observation is exploited by proposing a novel two stage vehicle detector that is able to achieve 77% vehicle detection accuracy on UA-DETRAC dataset. The second observation is emergency vehicle have distinct siren sound that is detected using a novel acoustic detection algorithm on an edge device. The proposed system is able to detect emergency vehicles with an average accuracy of 99.4%.

Cite as

Zeba Khanam, Vejey Pradeep Suresh Achari, Issam Boukhennoufa, Anish Jindal, and Amit Kumar Singh. A Multi-Modal Distributed Real-Time IoT System for Urban Traffic Control (Invited Paper). In Fifth Workshop on Next Generation Real-Time Embedded Systems (NG-RES 2024). Open Access Series in Informatics (OASIcs), Volume 117, pp. 2:1-2:10, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)


Copy BibTex To Clipboard

@InProceedings{khanam_et_al:OASIcs.NG-RES.2024.2,
  author =	{Khanam, Zeba and Achari, Vejey Pradeep Suresh and Boukhennoufa, Issam and Jindal, Anish and Singh, Amit Kumar},
  title =	{{A Multi-Modal Distributed Real-Time IoT System for Urban Traffic Control}},
  booktitle =	{Fifth Workshop on Next Generation Real-Time Embedded Systems (NG-RES 2024)},
  pages =	{2:1--2:10},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-313-3},
  ISSN =	{2190-6807},
  year =	{2024},
  volume =	{117},
  editor =	{Yomsi, Patrick Meumeu and Wildermann, Stefan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/OASIcs.NG-RES.2024.2},
  URN =		{urn:nbn:de:0030-drops-197057},
  doi =		{10.4230/OASIcs.NG-RES.2024.2},
  annote =	{Keywords: Vehicle Detection, Deep Neural Network, Traffic Control, Edge Computing, Emergency Vehicle Detection, Sliding Window}
}
Document
Invited Paper
DynaVLC - Towards Dynamic GTS Allocation in VLC Networks (Invited Paper)

Authors: Harrison Kurunathan, Miguel Gutiérrez Gaitán, Ramiro Sámano-Robles, and Eduardo Tovar

Published in: OASIcs, Volume 117, Fifth Workshop on Next Generation Real-Time Embedded Systems (NG-RES 2024)


Abstract
Envisioned to deliver superior Quality of Service (QoS) by offering faster data rates and reduced latency in 6G communication scenarios, pioneering communication protocols like the IEEE 802.15.7 are poised to facilitate emerging application trends (e.g. metaverse). The IEEE 802.15.7 standard that supports visible light communication (VLC) provides determinism for time-critical reliable communication through its guaranteed time-slots mechanism of the contention-free period (CFP) while supporting non-time-critical communication through contention-access period (CAP). Nevertheless, the IEEE 802.15.7 MAC structure is fixed and statically defined at the beginning of the network creation. This rigid definition of the network can be detrimental when the traffic characteristics evolve dynamically, for example, due to environmental or user-driven workload conditions. To this purpose, this paper proposes a resource-aware dynamic architecture for IEEE 802.15.7 networks that efficiently adapts the superframe structure to traffic dynamics. Notably, this technique was shown to reduce the overall delay and throughput by up to 45% and 30%, respectively, when compared to the traditional IEEE 802.15.7 protocol performance under the same network conditions.

Cite as

Harrison Kurunathan, Miguel Gutiérrez Gaitán, Ramiro Sámano-Robles, and Eduardo Tovar. DynaVLC - Towards Dynamic GTS Allocation in VLC Networks (Invited Paper). In Fifth Workshop on Next Generation Real-Time Embedded Systems (NG-RES 2024). Open Access Series in Informatics (OASIcs), Volume 117, pp. 3:1-3:11, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)


Copy BibTex To Clipboard

@InProceedings{kurunathan_et_al:OASIcs.NG-RES.2024.3,
  author =	{Kurunathan, Harrison and Gait\'{a}n, Miguel Guti\'{e}rrez and S\'{a}mano-Robles, Ramiro and Tovar, Eduardo},
  title =	{{DynaVLC - Towards Dynamic GTS Allocation in VLC Networks}},
  booktitle =	{Fifth Workshop on Next Generation Real-Time Embedded Systems (NG-RES 2024)},
  pages =	{3:1--3:11},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-313-3},
  ISSN =	{2190-6807},
  year =	{2024},
  volume =	{117},
  editor =	{Yomsi, Patrick Meumeu and Wildermann, Stefan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/OASIcs.NG-RES.2024.3},
  URN =		{urn:nbn:de:0030-drops-197069},
  doi =		{10.4230/OASIcs.NG-RES.2024.3},
  annote =	{Keywords: IEEE 802.15.7, VLC networks, network tuning}
}
Document
History-Based Run-Time Requirement Enforcement of Non-Functional Properties on MPSoCs

Authors: Khalil Esper and Jürgen Teich

Published in: OASIcs, Volume 117, Fifth Workshop on Next Generation Real-Time Embedded Systems (NG-RES 2024)


Abstract
Embedded system applications usually have requirements regarding non-functional properties of their execution like latency or power consumption. Enforcement of such requirements can be implemented by a reactive control loop, where an enforcer determines based on a system response (feedback) how to control the system, e.g., by selecting the number of active cores allocated to a program or by scaling their voltage/frequency mode. It is of a particular interest to design enforcement strategies for which it is possible to provide formal guarantees with respect to requirement violations, especially under a largely varying environmental input (workload) per execution. In this paper, we consider enforcement strategies that are modeled by a finite state machine (FSM) and the environment by a discrete-time Markov chain. Such a formalization enables the formal verification of temporal properties (verification goals) regarding the satisfaction of requirements of a given enforcement strategy. In this paper, we propose history-based enforcement FSMs which compute a reaction not just on the current, but on a fixed history of K previously observed system responses. We then analyze the quality of such enforcement FSMs in terms of the probability of satisfying a given set of verification goals and compare them to enforcement FSMs that react solely on the current system response. As experimental results, we present three use cases while considering requirements on latency and power consumption. The results show that history-based enforcement FSMs outperform enforcement FSMs that only consider the current system response regarding the probability of satisfying a given set of verification goals.

Cite as

Khalil Esper and Jürgen Teich. History-Based Run-Time Requirement Enforcement of Non-Functional Properties on MPSoCs. In Fifth Workshop on Next Generation Real-Time Embedded Systems (NG-RES 2024). Open Access Series in Informatics (OASIcs), Volume 117, pp. 4:1-4:11, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)


Copy BibTex To Clipboard

@InProceedings{esper_et_al:OASIcs.NG-RES.2024.4,
  author =	{Esper, Khalil and Teich, J\"{u}rgen},
  title =	{{History-Based Run-Time Requirement Enforcement of Non-Functional Properties on MPSoCs}},
  booktitle =	{Fifth Workshop on Next Generation Real-Time Embedded Systems (NG-RES 2024)},
  pages =	{4:1--4:11},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-313-3},
  ISSN =	{2190-6807},
  year =	{2024},
  volume =	{117},
  editor =	{Yomsi, Patrick Meumeu and Wildermann, Stefan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/OASIcs.NG-RES.2024.4},
  URN =		{urn:nbn:de:0030-drops-197074},
  doi =		{10.4230/OASIcs.NG-RES.2024.4},
  annote =	{Keywords: Verification, Runtime Requirement Enforcement, History, Latency}
}
Document
SAT Encodings and Beyond (Dagstuhl Seminar 23261)

Authors: Marijn J. H. Heule, Inês Lynce, Stefan Szeider, and Andre Schidler

Published in: Dagstuhl Reports, Volume 13, Issue 6 (2024)


Abstract
This report documents the program and the outcomes of Dagstuhl Seminar 23261 "SAT Encodings and Beyond." The seminar facilitated an intense examination and discussion of current results and challenges related to encodings for SAT and related solving paradigms. The seminar featured presentations and group work that provided theoretical, practical, and industrial viewpoints. The goal was to foster more profound insights and advancements in encoding techniques, which are pivotal in enhancing solvers' efficiency.

Cite as

Marijn J. H. Heule, Inês Lynce, Stefan Szeider, and Andre Schidler. SAT Encodings and Beyond (Dagstuhl Seminar 23261). In Dagstuhl Reports, Volume 13, Issue 6, pp. 106-122, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)


Copy BibTex To Clipboard

@Article{heule_et_al:DagRep.13.6.106,
  author =	{Heule, Marijn J. H. and Lynce, In\^{e}s and Szeider, Stefan and Schidler, Andre},
  title =	{{SAT Encodings and Beyond (Dagstuhl Seminar 23261)}},
  pages =	{106--122},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2024},
  volume =	{13},
  number =	{6},
  editor =	{Heule, Marijn J. H. and Lynce, In\^{e}s and Szeider, Stefan and Schidler, Andre},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagRep.13.6.106},
  URN =		{urn:nbn:de:0030-drops-196409},
  doi =		{10.4230/DagRep.13.6.106},
  annote =	{Keywords: constraint propagation, lower and upper bounds, problem formulation, propositional satisfiability, symmetry breaking}
}
Document
Proving Unsatisfiability with Hitting Formulas

Authors: Yuval Filmus, Edward A. Hirsch, Artur Riazanov, Alexander Smal, and Marc Vinyals

Published in: LIPIcs, Volume 287, 15th Innovations in Theoretical Computer Science Conference (ITCS 2024)


Abstract
A hitting formula is a set of Boolean clauses such that any two of the clauses cannot be simultaneously falsified. Hitting formulas have been studied in many different contexts at least since [Iwama, 1989] and, based on experimental evidence, Peitl and Szeider [Tomás Peitl and Stefan Szeider, 2022] conjectured that unsatisfiable hitting formulas are among the hardest for resolution. Using the fact that hitting formulas are easy to check for satisfiability we make them the foundation of a new static proof system {{rmHitting}}: a refutation of a CNF in {{rmHitting}} is an unsatisfiable hitting formula such that each of its clauses is a weakening of a clause of the refuted CNF. Comparing this system to resolution and other proof systems is equivalent to studying the hardness of hitting formulas. Our first result is that {{rmHitting}} is quasi-polynomially simulated by tree-like resolution, which means that hitting formulas cannot be exponentially hard for resolution and partially refutes the conjecture of Peitl and Szeider. We show that tree-like resolution and {{rmHitting}} are quasi-polynomially separated, while for resolution, this question remains open. For a system that is only quasi-polynomially stronger than tree-like resolution, {{rmHitting}} is surprisingly difficult to polynomially simulate in another proof system. Using the ideas of Raz-Shpilka’s polynomial identity testing for noncommutative circuits [Raz and Shpilka, 2005] we show that {{rmHitting}} is p-simulated by {{rmExtended {{rmFrege}}}}, but we conjecture that much more efficient simulations exist. As a byproduct, we show that a number of static (semi)algebraic systems are verifiable in deterministic polynomial time. We consider multiple extensions of {{rmHitting}}, and in particular a proof system {{{rmHitting}}(⊕)} related to the {{{rmRes}}(⊕)} proof system for which no superpolynomial-size lower bounds are known. {{{rmHitting}}(⊕)} p-simulates the tree-like version of {{{rmRes}}(⊕)} and is at least quasi-polynomially stronger. We show that formulas expressing the non-existence of perfect matchings in the graphs K_{n,n+2} are exponentially hard for {{{rmHitting}}(⊕)} via a reduction to the partition bound for communication complexity. See the full version of the paper for the proofs. They are omitted in this Extended Abstract.

Cite as

Yuval Filmus, Edward A. Hirsch, Artur Riazanov, Alexander Smal, and Marc Vinyals. Proving Unsatisfiability with Hitting Formulas. In 15th Innovations in Theoretical Computer Science Conference (ITCS 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 287, pp. 48:1-48:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)


Copy BibTex To Clipboard

@InProceedings{filmus_et_al:LIPIcs.ITCS.2024.48,
  author =	{Filmus, Yuval and Hirsch, Edward A. and Riazanov, Artur and Smal, Alexander and Vinyals, Marc},
  title =	{{Proving Unsatisfiability with Hitting Formulas}},
  booktitle =	{15th Innovations in Theoretical Computer Science Conference (ITCS 2024)},
  pages =	{48:1--48:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-309-6},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{287},
  editor =	{Guruswami, Venkatesan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITCS.2024.48},
  URN =		{urn:nbn:de:0030-drops-195762},
  doi =		{10.4230/LIPIcs.ITCS.2024.48},
  annote =	{Keywords: hitting formulas, polynomial identity testing, query complexity}
}
Document
On the Convergence Time in Graphical Games: A Locality-Sensitive Approach

Authors: Juho Hirvonen, Laura Schmid, Krishnendu Chatterjee, and Stefan Schmid

Published in: LIPIcs, Volume 286, 27th International Conference on Principles of Distributed Systems (OPODIS 2023)


Abstract
Graphical games are a useful framework for modeling the interactions of (selfish) agents who are connected via an underlying topology and whose behaviors influence each other. They have wide applications ranging from computer science to economics and biology. Yet, even though an agent’s payoff only depends on the actions of their direct neighbors in graphical games, computing the Nash equilibria and making statements about the convergence time of "natural" local dynamics in particular can be highly challenging. In this work, we present a novel approach for classifying complexity of Nash equilibria in graphical games by establishing a connection to local graph algorithms, a subfield of distributed computing. In particular, we make the observation that the equilibria of graphical games are equivalent to locally verifiable labelings (LVL) in graphs; vertex labelings which are verifiable with constant-round local algorithms. This connection allows us to derive novel lower bounds on the convergence time to equilibrium of best-response dynamics in graphical games. Since we establish that distributed convergence can sometimes be provably slow, we also introduce and give bounds on an intuitive notion of "time-constrained" inefficiency of best responses. We exemplify how our results can be used in the implementation of mechanisms that ensure convergence of best responses to a Nash equilibrium. Our results thus also give insight into the convergence of strategy-proof algorithms for graphical games, which is still not well understood.

Cite as

Juho Hirvonen, Laura Schmid, Krishnendu Chatterjee, and Stefan Schmid. On the Convergence Time in Graphical Games: A Locality-Sensitive Approach. In 27th International Conference on Principles of Distributed Systems (OPODIS 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 286, pp. 11:1-11:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)


Copy BibTex To Clipboard

@InProceedings{hirvonen_et_al:LIPIcs.OPODIS.2023.11,
  author =	{Hirvonen, Juho and Schmid, Laura and Chatterjee, Krishnendu and Schmid, Stefan},
  title =	{{On the Convergence Time in Graphical Games: A Locality-Sensitive Approach}},
  booktitle =	{27th International Conference on Principles of Distributed Systems (OPODIS 2023)},
  pages =	{11:1--11:24},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-308-9},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{286},
  editor =	{Bessani, Alysson and D\'{e}fago, Xavier and Nakamura, Junya and Wada, Koichi and Yamauchi, Yukiko},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.OPODIS.2023.11},
  URN =		{urn:nbn:de:0030-drops-195015},
  doi =		{10.4230/LIPIcs.OPODIS.2023.11},
  annote =	{Keywords: distributed computing, Nash equilibria, mechanism design, best-response dynamics}
}
  • Refine by Author
  • 30 Kratsch, Stefan
  • 28 Kiefer, Stefan
  • 27 Schmid, Stefan
  • 23 Szeider, Stefan
  • 22 Milius, Stefan
  • Show More...

  • Refine by Classification
  • 23 Theory of computation → Design and analysis of algorithms
  • 21 Theory of computation → Parameterized complexity and exact algorithms
  • 19 Theory of computation → Logic and verification
  • 16 Theory of computation → Formal languages and automata theory
  • 13 Mathematics of computing → Graph algorithms
  • Show More...

  • Refine by Keyword
  • 15 parameterized complexity
  • 12 Parameterized complexity
  • 9 Preface
  • 9 Table of Contents
  • 8 Markov chains
  • Show More...

  • Refine by Type
  • 602 document

  • Refine by Publication Year
  • 116 2022
  • 42 2012
  • 41 2023
  • 39 2019
  • 37 2020
  • Show More...

Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail