36 Search Results for "Bir�e, Florian"

Document
DOI: 10.4230/DagRep.13.10.1
Automated mathematics: integrating proofs, algorithms and data (Dagstuhl Seminar 23401)

Authors: Andrej Bauer, Katja Berčič, Florian Rabe, Nicolas Thiéry, and Jure Taslak

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

Abstract
This report documents the program and the outcomes of Dagstuhl Seminar 23401 "Automated mathematics: integrating proofs, algorithms and data". The seminar brought together system developers, library authors, and users from key branches of computer-supported mathematics: formalized mathematics, symbolic computation, and mathematical databases. We addressed issues that were common to all areas of computer-supported mathematics: library management, dependencies and interoperability between software components, quality and correctness assurances, searching for information, and usability by end users. Early on in the week, we formed working groups that worked on specific tasks, as described in this report. Each day was divided into a morning talk session and an afternoon period devoted to working in groups. To keep everyone well-informed, we gathered each day before dinner for an informal "show & tell" session.
Cite as

Andrej Bauer, Katja Berčič, Florian Rabe, Nicolas Thiéry, and Jure Taslak. Automated mathematics: integrating proofs, algorithms and data (Dagstuhl Seminar 23401). In Dagstuhl Reports, Volume 13, Issue 10, pp. 1-23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@Article{bauer_et_al:DagRep.13.10.1,
  author =	{Bauer, Andrej and Ber\v{c}i\v{c}, Katja and Rabe, Florian and Thi\'{e}ry, Nicolas and Taslak, Jure},
  title =	{{Automated mathematics: integrating proofs, algorithms and data (Dagstuhl Seminar 23401)}},
  pages =	{1--23},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2024},
  volume =	{13},
  number =	{10},
  editor =	{Bauer, Andrej and Ber\v{c}i\v{c}, Katja and Rabe, Florian and Thi\'{e}ry, Nicolas and Taslak, Jure},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagRep.13.10.1},
  URN =		{urn:nbn:de:0030-drops-198319},
  doi =		{10.4230/DagRep.13.10.1},
  annote =	{Keywords: mathematical knowledge management, mathematical software, formalized mathematics, computer algebra, databases of mathematical structures}
}
Document
DOI: 10.4230/DagRep.13.8.1
Recent Trends in Graph Decomposition (Dagstuhl Seminar 23331)

Authors: George Karypis, Christian Schulz, Darren Strash, Deepak Ajwani, Rob H. Bisseling, Katrin Casel, Ümit V. Çatalyürek, Cédric Chevalier, Florian Chudigiewitsch, Marcelo Fonseca Faraj, Michael Fellows, Lars Gottesbüren, Tobias Heuer, Kamer Kaya, Jakub Lacki, Johannes Langguth, Xiaoye Sherry Li, Ruben Mayer, Johannes Meintrup, Yosuke Mizutani, François Pellegrini, Fabrizio Petrini, Frances Rosamond, Ilya Safro, Sebastian Schlag, Roohani Sharma, Blair D. Sullivan, Bora Uçar, and Albert-Jan Yzelman

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

Abstract
This report documents the program and the outcomes of Dagstuhl Seminar 23331 "Recent Trends in Graph Decomposition", which took place from 13. August to 18. August, 2023. The seminar brought together 33 experts from academia and industry to discuss graph decomposition, a pivotal technique for handling massive graphs in applications such as social networks and scientific simulations. The seminar addressed the challenges posed by contemporary hardware designs, the potential of deep neural networks and reinforcement learning in developing heuristics, the unique optimization requirements of large sparse data, and the need for scalable algorithms suitable for emerging architectures. Through presentations, discussions, and collaborative sessions, the event fostered an exchange of innovative ideas, leading to the creation of community notes highlighting key open problems in the field.
Cite as

George Karypis, Christian Schulz, Darren Strash, Deepak Ajwani, Rob H. Bisseling, Katrin Casel, Ümit V. Çatalyürek, Cédric Chevalier, Florian Chudigiewitsch, Marcelo Fonseca Faraj, Michael Fellows, Lars Gottesbüren, Tobias Heuer, Kamer Kaya, Jakub Lacki, Johannes Langguth, Xiaoye Sherry Li, Ruben Mayer, Johannes Meintrup, Yosuke Mizutani, François Pellegrini, Fabrizio Petrini, Frances Rosamond, Ilya Safro, Sebastian Schlag, Roohani Sharma, Blair D. Sullivan, Bora Uçar, and Albert-Jan Yzelman. Recent Trends in Graph Decomposition (Dagstuhl Seminar 23331). In Dagstuhl Reports, Volume 13, Issue 8, pp. 1-45, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@Article{karypis_et_al:DagRep.13.8.1,
  author =	{Karypis, George and Schulz, Christian and Strash, Darren and Ajwani, Deepak and Bisseling, Rob H. and Casel, Katrin and \c{C}ataly\"{u}rek, \"{U}mit V. and Chevalier, C\'{e}dric and Chudigiewitsch, Florian and Faraj, Marcelo Fonseca and Fellows, Michael and Gottesb\"{u}ren, Lars and Heuer, Tobias and Kaya, Kamer and Lacki, Jakub and Langguth, Johannes and Li, Xiaoye Sherry and Mayer, Ruben and Meintrup, Johannes and Mizutani, Yosuke and Pellegrini, Fran\c{c}ois and Petrini, Fabrizio and Rosamond, Frances and Safro, Ilya and Schlag, Sebastian and Sharma, Roohani and Sullivan, Blair D. and U\c{c}ar, Bora and Yzelman, Albert-Jan},
  title =	{{Recent Trends in Graph Decomposition (Dagstuhl Seminar 23331)}},
  pages =	{1--45},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2024},
  volume =	{13},
  number =	{8},
  editor =	{Karypis, George and Schulz, Christian and Strash, Darren},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagRep.13.8.1},
  URN =		{urn:nbn:de:0030-drops-198114},
  doi =		{10.4230/DagRep.13.8.1},
  annote =	{Keywords: combinatorial optimization, experimental algorithmics, parallel algorithms}
}
Document
DOI: 10.4230/LIPIcs.STACS.2024.8
Faster Graph Algorithms Through DAG Compression

Authors: Max Bannach, Florian Andreas Marwitz, and Till Tantau

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

Abstract
The runtime of graph algorithms such as depth-first search or Dijkstra’s algorithm is dominated by the fact that all edges of the graph need to be processed at least once, leading to prohibitive runtimes for large, dense graphs. We introduce a simple data structure for storing graphs (and more general structures) in a compressed manner using directed acyclic graphs (dags). We then show that numerous standard graph problems can be solved in time linear in the size of the dag compression of a graph, rather than in the number of edges of the graph. Crucially, many dense graphs, including but not limited to graphs of bounded twinwidth, have a dag compression of size linear in the number of vertices rather than edges. This insight allows us to improve the previous best results for the runtime of standard algorithms from quasi-linear to linear for the large class of graphs of bounded twinwidth, which includes all cographs, graphs of bounded treewidth, or graphs of bounded cliquewidth.
Cite as

Max Bannach, Florian Andreas Marwitz, and Till Tantau. Faster Graph Algorithms Through DAG Compression. In 41st International Symposium on Theoretical Aspects of Computer Science (STACS 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 289, pp. 8:1-8:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{bannach_et_al:LIPIcs.STACS.2024.8,
  author =	{Bannach, Max and Marwitz, Florian Andreas and Tantau, Till},
  title =	{{Faster Graph Algorithms Through DAG Compression}},
  booktitle =	{41st International Symposium on Theoretical Aspects of Computer Science (STACS 2024)},
  pages =	{8:1--8: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.8},
  URN =		{urn:nbn:de:0030-drops-197188},
  doi =		{10.4230/LIPIcs.STACS.2024.8},
  annote =	{Keywords: graph compression, graph traversal, twinwidth, parameterized algorithms}
}
Document
DOI: 10.4230/LIPIcs.ISAAC.2023.8
Recognizing Unit Multiple Intervals Is Hard

Authors: Virginia Ardévol Martínez, Romeo Rizzi, Florian Sikora, and Stéphane Vialette

Published in: LIPIcs, Volume 283, 34th International Symposium on Algorithms and Computation (ISAAC 2023)

Abstract
Multiple interval graphs are a well-known generalization of interval graphs introduced in the 1970s to deal with situations arising naturally in scheduling and allocation. A d-interval is the union of d intervals on the real line, and a graph is a d-interval graph if it is the intersection graph of d-intervals. In particular, it is a unit d-interval graph if it admits a d-interval representation where every interval has unit length. Whereas it has been known for a long time that recognizing 2-interval graphs and other related classes such as 2-track interval graphs is NP-complete, the complexity of recognizing unit 2-interval graphs remains open. Here, we settle this question by proving that the recognition of unit 2-interval graphs is also NP-complete. Our proof technique uses a completely different approach from the other hardness results of recognizing related classes. Furthermore, we extend the result for unit d-interval graphs for any d ⩾ 2, which does not follow directly in graph recognition problems -as an example, it took almost 20 years to close the gap between d = 2 and d > 2 for the recognition of d-track interval graphs. Our result has several implications, including that recognizing (x, …, x) d-interval graphs and depth r unit 2-interval graphs is NP-complete for every x ⩾ 11 and every r ⩾ 4.
Cite as

Virginia Ardévol Martínez, Romeo Rizzi, Florian Sikora, and Stéphane Vialette. Recognizing Unit Multiple Intervals Is Hard. In 34th International Symposium on Algorithms and Computation (ISAAC 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 283, pp. 8:1-8:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{ardevolmartinez_et_al:LIPIcs.ISAAC.2023.8,
  author =	{Ard\'{e}vol Mart{\'\i}nez, Virginia and Rizzi, Romeo and Sikora, Florian and Vialette, St\'{e}phane},
  title =	{{Recognizing Unit Multiple Intervals Is Hard}},
  booktitle =	{34th International Symposium on Algorithms and Computation (ISAAC 2023)},
  pages =	{8:1--8:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-289-1},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{283},
  editor =	{Iwata, Satoru and Kakimura, Naonori},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ISAAC.2023.8},
  URN =		{urn:nbn:de:0030-drops-193102},
  doi =		{10.4230/LIPIcs.ISAAC.2023.8},
  annote =	{Keywords: Interval graphs, unit multiple interval graphs, recognition, NP-hardness}
}
Document
DOI: 10.4230/LIPIcs.TIME.2023.2
LTL over Finite Words Can Be Exponentially More Succinct Than Pure-Past LTL, and vice versa

Authors: Alessandro Artale, Luca Geatti, Nicola Gigante, Andrea Mazzullo, and Angelo Montanari

Published in: LIPIcs, Volume 278, 30th International Symposium on Temporal Representation and Reasoning (TIME 2023)

Abstract
Linear Temporal Logic over finite traces (LTL_𝖿) has proved itself to be an important and effective formalism in formal verification as well as in artificial intelligence. Pure past LTL_𝖿 (pLTL) is the logic obtained from LTL_𝖿 by replacing each (future) temporal operator by a corresponding past one, and is naturally interpreted at the end of a finite trace. It is known that each property definable in LTL_𝖿 is also definable in pLTL, and ǐceversa. However, despite being extensively used in practice, to the best of our knowledge, there is no systematic study of their succinctness. In this paper, we investigate the succinctness of LTL_𝖿 and pLTL. First, we prove that pLTL can be exponentially more succinct than LTL_𝖿 by showing that there exists a property definable with a pLTL formula of size n such that the size of all LTL_𝖿 formulas defining it is at least exponential in n. Then, we prove that LTL_𝖿 can be exponentially more succinct than pLTL as well. This result shows that, although being expressively equivalent, LTL_𝖿 and pLTL are incomparable when succinctness is concerned. In addition, we study the succinctness of Safety-LTL (the syntactic safety fragment of LTL over infinite traces) with respect to its canonical form G(pLTL), whose formulas are of the form G(α), G being the globally operator and α a pLTL formula. We prove that G(pLTL) can be exponentially more succinct than Safety-LTL, and that the same holds for the dual cosafety fragment.
Cite as

Alessandro Artale, Luca Geatti, Nicola Gigante, Andrea Mazzullo, and Angelo Montanari. LTL over Finite Words Can Be Exponentially More Succinct Than Pure-Past LTL, and vice versa. In 30th International Symposium on Temporal Representation and Reasoning (TIME 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 278, pp. 2:1-2:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{artale_et_al:LIPIcs.TIME.2023.2,
  author =	{Artale, Alessandro and Geatti, Luca and Gigante, Nicola and Mazzullo, Andrea and Montanari, Angelo},
  title =	{{LTL over Finite Words Can Be Exponentially More Succinct Than Pure-Past LTL, and vice versa}},
  booktitle =	{30th International Symposium on Temporal Representation and Reasoning (TIME 2023)},
  pages =	{2:1--2:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-298-3},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{278},
  editor =	{Artikis, Alexander and Bruse, Florian and Hunsberger, Luke},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2023.2},
  URN =		{urn:nbn:de:0030-drops-190927},
  doi =		{10.4230/LIPIcs.TIME.2023.2},
  annote =	{Keywords: Temporal Logic, Succinctness, LTLf, Finite Traces, Pure past LTL}
}
Document
DOI: 10.4230/LIPIcs.TIME.2023.3
LSCPM: Communities in Massive Real-World Link Streams by Clique Percolation Method

Authors: Alexis Baudin, Lionel Tabourier, and Clémence Magnien

Published in: LIPIcs, Volume 278, 30th International Symposium on Temporal Representation and Reasoning (TIME 2023)

Abstract
Community detection is a popular approach to understand the organization of interactions in static networks. For that purpose, the Clique Percolation Method (CPM), which involves the percolation of k-cliques, is a well-studied technique that offers several advantages. Besides, studying interactions that occur over time is useful in various contexts, which can be modeled by the link stream formalism. The Dynamic Clique Percolation Method (DCPM) has been proposed for extending CPM to temporal networks. However, existing implementations are unable to handle massive datasets. We present a novel algorithm that adapts CPM to link streams, which has the advantage that it allows us to speed up the computation time with respect to the existing DCPM method. We evaluate it experimentally on real datasets and show that it scales to massive link streams. For example, it allows to obtain a complete set of communities in under twenty-five minutes for a dataset with thirty million links, what the state of the art fails to achieve even after a week of computation. We further show that our method provides communities similar to DCPM, but slightly more aggregated. We exhibit the relevance of the obtained communities in real world cases, and show that they provide information on the importance of vertices in the link streams.
Cite as

Alexis Baudin, Lionel Tabourier, and Clémence Magnien. LSCPM: Communities in Massive Real-World Link Streams by Clique Percolation Method. In 30th International Symposium on Temporal Representation and Reasoning (TIME 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 278, pp. 3:1-3:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{baudin_et_al:LIPIcs.TIME.2023.3,
  author =	{Baudin, Alexis and Tabourier, Lionel and Magnien, Cl\'{e}mence},
  title =	{{LSCPM: Communities in Massive Real-World Link Streams by Clique Percolation Method}},
  booktitle =	{30th International Symposium on Temporal Representation and Reasoning (TIME 2023)},
  pages =	{3:1--3:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-298-3},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{278},
  editor =	{Artikis, Alexander and Bruse, Florian and Hunsberger, Luke},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2023.3},
  URN =		{urn:nbn:de:0030-drops-190932},
  doi =		{10.4230/LIPIcs.TIME.2023.3},
  annote =	{Keywords: Temporal network, Link stream, k-clique, Community detection, Clique Percolation Method, Real-world interactions}
}
Document
DOI: 10.4230/LIPIcs.TIME.2023.6
Bounded-Memory Runtime Enforcement of Timed Properties

Authors: Saumya Shankar, Srinivas Pinisetty, and Thierry Jéron

Published in: LIPIcs, Volume 278, 30th International Symposium on Temporal Representation and Reasoning (TIME 2023)

Abstract
Runtime Enforcement (RE) is a monitoring technique aimed at correcting possibly incorrect executions w.r.t. a set of formal requirements (properties) of a system. In this paper, we consider enforcement monitoring of real-time properties. Thus, executions are modelled as timed words and specifications as timed automata. Moreover, we consider that the enforcer has the ability to delay events by storing or buffering them into its internal memory (and releasing them when the property is finally satisfied) and suppressing events when no delaying is appropriate. Practically, in an implementation, the internal memory of the enforcer is finite. In this paper, we propose a new RE paradigm for timed properties, where the memory of the enforcer is bounded/finite, to address practical applications with memory constraints and timed specifications. Bounding the memory presents a number of difficulties, e.g., how to accommodate a timed event into the memory when the memory is full, s.t., regardless of the course of action we choose to handle this situation, the behaviour of the bounded enforcer should not significantly differ from that of the unbounded enforcer. The problem of how to optimally discard events when the buffer is full is significantly more difficult in a timed environment where the progress of time affects the satisfaction or violation of a property. We define the bounded-memory RE problem for timed properties and develop a framework for regular timed properties specified as timed automata. The proposed framework is implemented in Python, and its performance is evaluated. From experiments, we discovered that the enforcer has a reasonable execution time overhead.
Cite as

Saumya Shankar, Srinivas Pinisetty, and Thierry Jéron. Bounded-Memory Runtime Enforcement of Timed Properties. In 30th International Symposium on Temporal Representation and Reasoning (TIME 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 278, pp. 6:1-6:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{shankar_et_al:LIPIcs.TIME.2023.6,
  author =	{Shankar, Saumya and Pinisetty, Srinivas and J\'{e}ron, Thierry},
  title =	{{Bounded-Memory Runtime Enforcement of Timed Properties}},
  booktitle =	{30th International Symposium on Temporal Representation and Reasoning (TIME 2023)},
  pages =	{6:1--6:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-298-3},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{278},
  editor =	{Artikis, Alexander and Bruse, Florian and Hunsberger, Luke},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2023.6},
  URN =		{urn:nbn:de:0030-drops-190962},
  doi =		{10.4230/LIPIcs.TIME.2023.6},
  annote =	{Keywords: Formal methods, Runtime enforcement, Bounded-memory, Timed automata}
}
Document
DOI: 10.4230/LIPIcs.TIME.2023.13
Optimization of Nonsequenced Queries Using Log-Segmented Timestamps

Authors: Curtis E. Dyreson

Published in: LIPIcs, Volume 278, 30th International Symposium on Temporal Representation and Reasoning (TIME 2023)

Abstract
In a period-timestamped, relational temporal database, each tuple is timestamped with a period. The timestamp records when the tuple is "alive" in some temporal dimension. Nonsequenced semantics is a query evaluation semantics that involves adding temporal predicates and constructors to a query. We show how to use log-segmented timestamps to improve the efficiency of temporal, nonsequenced queries evaluated using a non-temporal DBMS, i.e., a DBMS that has no special temporal indexes or query evaluation operators. A log-segmented timestamp divides the time-line into segments of known length. Any temporal period can be represented by a small number of such segments. The segments can be appended to a relation as additional columns. The advantage of log-segmented timestamps is that each segment can be indexed using standard database indexes, e.g., a B^+-tree. A query optimizer can use the indexes to generate a lower cost query evaluation plan. This paper shows how to rewrite a query to use the additional columns and evaluates the time cost benefits and space cost disadvantages.
Cite as

Curtis E. Dyreson. Optimization of Nonsequenced Queries Using Log-Segmented Timestamps. In 30th International Symposium on Temporal Representation and Reasoning (TIME 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 278, pp. 13:1-13:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{dyreson:LIPIcs.TIME.2023.13,
  author =	{Dyreson, Curtis E.},
  title =	{{Optimization of Nonsequenced Queries Using Log-Segmented Timestamps}},
  booktitle =	{30th International Symposium on Temporal Representation and Reasoning (TIME 2023)},
  pages =	{13:1--13:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-298-3},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{278},
  editor =	{Artikis, Alexander and Bruse, Florian and Hunsberger, Luke},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2023.13},
  URN =		{urn:nbn:de:0030-drops-191036},
  doi =		{10.4230/LIPIcs.TIME.2023.13},
  annote =	{Keywords: Temporal databases, nonsequenced semantics, query evaluation, query performance}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2023.20
Expressiveness Results for an Inductive Logic of Separated Relations

Authors: Radu Iosif and Florian Zuleger

Published in: LIPIcs, Volume 279, 34th International Conference on Concurrency Theory (CONCUR 2023)

Abstract
In this paper we study a Separation Logic of Relations (SLR) and compare its expressiveness to (Monadic) Second Order Logic [(M)SO]. SLR is based on the well-known Symbolic Heap fragment of Separation Logic, whose formulæare composed of points-to assertions, inductively defined predicates, with the separating conjunction as the only logical connective. SLR generalizes the Symbolic Heap fragment by supporting general relational atoms, instead of only points-to assertions. In this paper, we restrict ourselves to finite relational structures, and hence only consider Weak (M)SO, where quantification ranges over finite sets. Our main results are that SLR and MSO are incomparable on structures of unbounded treewidth, while SLR can be embedded in SO in general. Furthermore, MSO becomes a strict subset of SLR, when the treewidth of the models is bounded by a parameter and all vertices attached to some hyperedge belong to the interpretation of a fixed unary relation symbol. We also discuss the problem of identifying a fragment of SLR that is equivalent to MSO over models of bounded treewidth.
Cite as

Radu Iosif and Florian Zuleger. Expressiveness Results for an Inductive Logic of Separated Relations. In 34th International Conference on Concurrency Theory (CONCUR 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 279, pp. 20:1-20:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{iosif_et_al:LIPIcs.CONCUR.2023.20,
  author =	{Iosif, Radu and Zuleger, Florian},
  title =	{{Expressiveness Results for an Inductive Logic of Separated Relations}},
  booktitle =	{34th International Conference on Concurrency Theory (CONCUR 2023)},
  pages =	{20:1--20:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-299-0},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{279},
  editor =	{P\'{e}rez, Guillermo A. and Raskin, Jean-Fran\c{c}ois},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2023.20},
  URN =		{urn:nbn:de:0030-drops-190146},
  doi =		{10.4230/LIPIcs.CONCUR.2023.20},
  annote =	{Keywords: Separation Logic, Model Theory, Monadic Second Order Logic, Treewidth}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2023.48
Positive Data Languages

Authors: Florian Frank, Stefan Milius, and Henning Urbat

Published in: LIPIcs, Volume 272, 48th International Symposium on Mathematical Foundations of Computer Science (MFCS 2023)

Abstract
Positive data languages are languages over an infinite alphabet closed under possibly non-injective renamings of data values. Informally, they model properties of data words expressible by assertions about equality, but not inequality, of data values occurring in the word. We investigate the class of positive data languages recognizable by nondeterministic orbit-finite nominal automata, an abstract form of register automata introduced by Bojańczyk, Klin, and Lasota. As our main contribution we provide a number of equivalent characterizations of that class in terms of positive register automata, monadic second-order logic with positive equality tests, and finitely presentable nondeterministic automata in the categories of nominal renaming sets and of presheaves over finite sets.
Cite as

Florian Frank, Stefan Milius, and Henning Urbat. Positive Data Languages. In 48th International Symposium on Mathematical Foundations of Computer Science (MFCS 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 272, pp. 48:1-48:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{frank_et_al:LIPIcs.MFCS.2023.48,
  author =	{Frank, Florian and Milius, Stefan and Urbat, Henning},
  title =	{{Positive Data Languages}},
  booktitle =	{48th International Symposium on Mathematical Foundations of Computer Science (MFCS 2023)},
  pages =	{48:1--48:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-292-1},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{272},
  editor =	{Leroux, J\'{e}r\^{o}me and Lombardy, Sylvain and Peleg, David},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2023.48},
  URN =		{urn:nbn:de:0030-drops-185828},
  doi =		{10.4230/LIPIcs.MFCS.2023.48},
  annote =	{Keywords: Data Languages, Register Automata, MSO, Nominal Sets, Presheaves}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2022.10
Parameter Synthesis for Parametric Probabilistic Dynamical Systems and Prefix-Independent Specifications

Authors: Christel Baier, Florian Funke, Simon Jantsch, Toghrul Karimov, Engel Lefaucheux, Joël Ouaknine, David Purser, Markus A. Whiteland, and James Worrell

Published in: LIPIcs, Volume 243, 33rd International Conference on Concurrency Theory (CONCUR 2022)

Abstract
We consider the model-checking problem for parametric probabilistic dynamical systems, formalised as Markov chains with parametric transition functions, analysed under the distribution-transformer semantics (in which a Markov chain induces a sequence of distributions over states). We examine the problem of synthesising the set of parameter valuations of a parametric Markov chain such that the orbits of induced state distributions satisfy a prefix-independent ω-regular property. Our main result establishes that in all non-degenerate instances, the feasible set of parameters is (up to a null set) semialgebraic, and can moreover be computed (in polynomial time assuming that the ambient dimension, corresponding to the number of states of the Markov chain, is fixed).
Cite as

Christel Baier, Florian Funke, Simon Jantsch, Toghrul Karimov, Engel Lefaucheux, Joël Ouaknine, David Purser, Markus A. Whiteland, and James Worrell. Parameter Synthesis for Parametric Probabilistic Dynamical Systems and Prefix-Independent Specifications. In 33rd International Conference on Concurrency Theory (CONCUR 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 243, pp. 10:1-10:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{baier_et_al:LIPIcs.CONCUR.2022.10,
  author =	{Baier, Christel and Funke, Florian and Jantsch, Simon and Karimov, Toghrul and Lefaucheux, Engel and Ouaknine, Jo\"{e}l and Purser, David and Whiteland, Markus A. and Worrell, James},
  title =	{{Parameter Synthesis for Parametric Probabilistic Dynamical Systems and Prefix-Independent Specifications}},
  booktitle =	{33rd International Conference on Concurrency Theory (CONCUR 2022)},
  pages =	{10:1--10:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-246-4},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{243},
  editor =	{Klin, Bartek and Lasota, S{\l}awomir and Muscholl, Anca},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2022.10},
  URN =		{urn:nbn:de:0030-drops-170732},
  doi =		{10.4230/LIPIcs.CONCUR.2022.10},
  annote =	{Keywords: Model checking, parametric Markov chains, distribution transformer semantics}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2022.20
Skolem Meets Schanuel

Authors: Yuri Bilu, Florian Luca, Joris Nieuwveld, Joël Ouaknine, David Purser, and James Worrell

Published in: LIPIcs, Volume 241, 47th International Symposium on Mathematical Foundations of Computer Science (MFCS 2022)

Abstract
The celebrated Skolem-Mahler-Lech Theorem states that the set of zeros of a linear recurrence sequence is the union of a finite set and finitely many arithmetic progressions. The corresponding computational question, the Skolem Problem, asks to determine whether a given linear recurrence sequence has a zero term. Although the Skolem-Mahler-Lech Theorem is almost 90 years old, decidability of the Skolem Problem remains open. The main contribution of this paper is an algorithm to solve the Skolem Problem for simple linear recurrence sequences (those with simple characteristic roots). Whenever the algorithm terminates, it produces a stand-alone certificate that its output is correct - a set of zeros together with a collection of witnesses that no further zeros exist. We give a proof that the algorithm always terminates assuming two classical number-theoretic conjectures: the Skolem Conjecture (also known as the Exponential Local-Global Principle) and the p-adic Schanuel Conjecture. Preliminary experiments with an implementation of this algorithm within the tool Skolem point to the practical applicability of this method.
Cite as

Yuri Bilu, Florian Luca, Joris Nieuwveld, Joël Ouaknine, David Purser, and James Worrell. Skolem Meets Schanuel. In 47th International Symposium on Mathematical Foundations of Computer Science (MFCS 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 241, pp. 20:1-20:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{bilu_et_al:LIPIcs.MFCS.2022.20,
  author =	{Bilu, Yuri and Luca, Florian and Nieuwveld, Joris and Ouaknine, Jo\"{e}l and Purser, David and Worrell, James},
  title =	{{Skolem Meets Schanuel}},
  booktitle =	{47th International Symposium on Mathematical Foundations of Computer Science (MFCS 2022)},
  pages =	{20:1--20:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-256-3},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{241},
  editor =	{Szeider, Stefan and Ganian, Robert and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2022.20},
  URN =		{urn:nbn:de:0030-drops-168180},
  doi =		{10.4230/LIPIcs.MFCS.2022.20},
  annote =	{Keywords: Skolem Problem, Skolem Conjecture, Exponential Local-Global Principle, p-adic Schanuel Conjecture}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2022.73
A Universal Skolem Set of Positive Lower Density

Authors: Florian Luca, Joël Ouaknine, and James Worrell

Published in: LIPIcs, Volume 241, 47th International Symposium on Mathematical Foundations of Computer Science (MFCS 2022)

Abstract
The Skolem Problem asks to decide whether a given integer linear recurrence sequence (LRS) has a zero term. Decidability of this problem has been open for many decades, with little progress since the 1980s. Recently, a new approach was initiated via the notion of a Skolem set - a set of positive integers relative to which the Skolem Problem is decidable. More precisely, 𝒮 is a Skolem set for a class ℒ of integer LRS if there is an effective procedure that, given an LRS in ℒ, decides whether the sequence has a zero in 𝒮. A recent work exhibited a Skolem set for the class of all LRS that, while infinite, had density zero. In the present work we construct a Skolem set of positive lower density for the class of simple LRS .
Cite as

Florian Luca, Joël Ouaknine, and James Worrell. A Universal Skolem Set of Positive Lower Density. In 47th International Symposium on Mathematical Foundations of Computer Science (MFCS 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 241, pp. 73:1-73:12, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{luca_et_al:LIPIcs.MFCS.2022.73,
  author =	{Luca, Florian and Ouaknine, Jo\"{e}l and Worrell, James},
  title =	{{A Universal Skolem Set of Positive Lower Density}},
  booktitle =	{47th International Symposium on Mathematical Foundations of Computer Science (MFCS 2022)},
  pages =	{73:1--73:12},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-256-3},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{241},
  editor =	{Szeider, Stefan and Ganian, Robert and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2022.73},
  URN =		{urn:nbn:de:0030-drops-168711},
  doi =		{10.4230/LIPIcs.MFCS.2022.73},
  annote =	{Keywords: Linear Recurrence Sequences, Skolem Problem, Exponential Diophantine Equations, Sieve Methods}
}
Document
DOI: 10.4230/LIPIcs.TQC.2022.10
Memory Compression with Quantum Random-Access Gates

Authors: Harry Buhrman, Bruno Loff, Subhasree Patro, and Florian Speelman

Published in: LIPIcs, Volume 232, 17th Conference on the Theory of Quantum Computation, Communication and Cryptography (TQC 2022)

Abstract
In the classical RAM, we have the following useful property. If we have an algorithm that uses M memory cells throughout its execution, and in addition is sparse, in the sense that, at any point in time, only m out of M cells will be non-zero, then we may "compress" it into another algorithm which uses only m log M memory and runs in almost the same time. We may do so by simulating the memory using either a hash table, or a self-balancing tree. We show an analogous result for quantum algorithms equipped with quantum random-access gates. If we have a quantum algorithm that runs in time T and uses M qubits, such that the state of the memory, at any time step, is supported on computational-basis vectors of Hamming weight at most m, then it can be simulated by another algorithm which uses only O(m log M) memory, and runs in time Õ(T). We show how this theorem can be used, in a black-box way, to simplify the presentation in several papers. Broadly speaking, when there exists a need for a space-efficient history-independent quantum data-structure, it is often possible to construct a space-inefficient, yet sparse, quantum data structure, and then appeal to our main theorem. This results in simpler and shorter arguments.
Cite as

Harry Buhrman, Bruno Loff, Subhasree Patro, and Florian Speelman. Memory Compression with Quantum Random-Access Gates. In 17th Conference on the Theory of Quantum Computation, Communication and Cryptography (TQC 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 232, pp. 10:1-10:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{buhrman_et_al:LIPIcs.TQC.2022.10,
  author =	{Buhrman, Harry and Loff, Bruno and Patro, Subhasree and Speelman, Florian},
  title =	{{Memory Compression with Quantum Random-Access Gates}},
  booktitle =	{17th Conference on the Theory of Quantum Computation, Communication and Cryptography (TQC 2022)},
  pages =	{10:1--10:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-237-2},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{232},
  editor =	{Le Gall, Fran\c{c}ois and Morimae, Tomoyuki},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TQC.2022.10},
  URN =		{urn:nbn:de:0030-drops-165177},
  doi =		{10.4230/LIPIcs.TQC.2022.10},
  annote =	{Keywords: complexity theory, data structures, algorithms, quantum walk}
}
Document
CG Challenge
DOI: 10.4230/LIPIcs.SoCG.2022.73
Local Search with Weighting Schemes for the CG:SHOP 2022 Competition (CG Challenge)

Authors: Florian Fontan, Pascal Lafourcade, Luc Libralesso, and Benjamin Momège

Published in: LIPIcs, Volume 224, 38th International Symposium on Computational Geometry (SoCG 2022)

Abstract
This paper describes the heuristics used by the LASAOFOOFUBESTINNRRALLDECA team for the CG:SHOP 2022 challenge. We introduce a new greedy algorithm that exploits information about the challenge instances, and hybridize two classical local-search schemes with weighting schemes. We found 211/225 best-known solutions. Hence, with the algorithms presented in this article, our team was able to reach the 3rd place of the challenge, among 40 participating teams.
Cite as

Florian Fontan, Pascal Lafourcade, Luc Libralesso, and Benjamin Momège. Local Search with Weighting Schemes for the CG:SHOP 2022 Competition (CG Challenge). In 38th International Symposium on Computational Geometry (SoCG 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 224, pp. 73:1-73:6, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{fontan_et_al:LIPIcs.SoCG.2022.73,
  author =	{Fontan, Florian and Lafourcade, Pascal and Libralesso, Luc and Mom\`{e}ge, Benjamin},
  title =	{{Local Search with Weighting Schemes for the CG:SHOP 2022 Competition}},
  booktitle =	{38th International Symposium on Computational Geometry (SoCG 2022)},
  pages =	{73:1--73:6},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-227-3},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{224},
  editor =	{Goaoc, Xavier and Kerber, Michael},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.SoCG.2022.73},
  URN =		{urn:nbn:de:0030-drops-160811},
  doi =		{10.4230/LIPIcs.SoCG.2022.73},
  annote =	{Keywords: heuristics, vertex coloring, digital geometry}
}
  • Refine by Author
  • 7 Sikora, Florian
  • 6 Ouaknine, Joël
  • 5 Worrell, James
  • 4 Bonnet, Édouard
  • 4 Buhrman, Harry
  • Show More...

  • Refine by Classification
  • 6 Theory of computation → Logic and verification
  • 3 Theory of computation → Parameterized complexity and exact algorithms
  • 2 Computing methodologies → Symbolic and algebraic algorithms
  • 2 Mathematics of computing → Graph algorithms
  • 2 Theory of computation → Fixed parameter tractability
  • Show More...

  • Refine by Keyword
  • 2 Skolem Problem
  • 2 Treewidth
  • 2 complexity theory
  • 2 data structures
  • 2 quantum walk
  • Show More...

  • Refine by Type
  • 36 document

  • Refine by Publication Year
  • 7 2023
  • 6 2018
  • 6 2022
  • 4 2015
  • 4 2019
  • 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
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact