26 Search Results for "Hansen, Eric A."

Document
DOI: 10.4230/LIPIcs.STACS.2026.25
Homomorphism Indistinguishability, Multiplicity Automata Equivalence, and Polynomial Identity Testing

Authors: Marek Černý and Tim Seppelt

Published in: LIPIcs, Volume 364, 43rd International Symposium on Theoretical Aspects of Computer Science (STACS 2026)

Abstract
Two graphs G and H are homomorphism indistinguishable over a graph class ℱ if they admit the same number of homomorphisms from every graph F ∈ ℱ. Many graph isomorphism relaxations such as (quantum) isomorphism and cospectrality can be characterised as homomorphism indistinguishability over specific graph classes. Thereby, the problems HomInd(ℱ) of deciding homomorphism indistinguishability over ℱ subsume diverse graph isomorphism relaxations whose complexities range from logspace to undecidable. Establishing the first general result on the complexity of HomInd(ℱ), Seppelt (MFCS 2024) showed that HomInd(ℱ) is in randomised polynomial time for every graph class ℱ of bounded treewidth that can be defined in counting monadic second-order logic CMSO₂. We show that this algorithm is conditionally optimal, i.e. it cannot be derandomised unless polynomial identity testing is in P. For CMSO₂-definable graph classes ℱ of bounded pathwidth, we improve the previous complexity upper bound for HomInd(ℱ) from P to C_ = L and show that this is tight. Secondarily, we establish a connection between homomorphism indistinguishability and multiplicity automata equivalence which allows us to pinpoint the complexity of the latter problem as C_ = L-complete.
Cite as

Marek Černý and Tim Seppelt. Homomorphism Indistinguishability, Multiplicity Automata Equivalence, and Polynomial Identity Testing. In 43rd International Symposium on Theoretical Aspects of Computer Science (STACS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 364, pp. 25:1-25:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{cerny_et_al:LIPIcs.STACS.2026.25,
  author =	{\v{C}ern\'{y}, Marek and Seppelt, Tim},
  title =	{{Homomorphism Indistinguishability, Multiplicity Automata Equivalence, and Polynomial Identity Testing}},
  booktitle =	{43rd International Symposium on Theoretical Aspects of Computer Science (STACS 2026)},
  pages =	{25:1--25:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-412-3},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{364},
  editor =	{Mahajan, Meena and Manea, Florin and McIver, Annabelle and Thắng, Nguy\~{ê}n Kim},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2026.25},
  URN =		{urn:nbn:de:0030-drops-255144},
  doi =		{10.4230/LIPIcs.STACS.2026.25},
  annote =	{Keywords: treewidth, Courcelle’s theorem, logspace, multiplicity automata, polynomial identity testing}
}
Document
Short Paper
DOI: 10.4230/LIPIcs.TIME.2025.20
Temporal Considerations in DJ Mix Information Retrieval and Generation (Short Paper)

Authors: Alexander Williams, Gregor Meehan, Stefan Lattner, Johan Pauwels, and Mathieu Barthet

Published in: LIPIcs, Volume 355, 32nd International Symposium on Temporal Representation and Reasoning (TIME 2025)

Abstract
Music is the art of arranging sounds in time so as to produce a continuous, unified, and evocative composition. Electronic dance music (EDM) is a collection of musical sub-genres produced using computers and electronic instruments and often presented through the medium of DJing, where tracks are curated and mixed sequentially into a continuous stream of music to offer unique listening and dancing experiences over time periods ranging from several minutes to several hours. A DJ’s actions and decisions occur at several levels of temporal granularity, from real-time audio manipulation (e.g. of tempo) for smooth inter-track transitions to long-term planning of track selection and sequencing for mix content and flow. While human DJs can instinctively operate across these different temporal resolutions, replicating this capability in an end-to-end automated DJing system presents significant challenges. In this paper, we analyse existing works in DJ mix information retrieval and generation from this temporal perspective. We first explain the close link between DJing and the temporal notion of musical rhythm, then describe a framework for categorising DJing actions by temporal granularity. Using this framework, we summarise and contrast potential approaches for automating and augmenting sequential DJ decision making, and discuss the unique characteristics of DJ mix track selection as a sequential recommendation task. In doing so, we hope to facilitate the implementation of more robust and complete automated DJing systems in future research.
Cite as

Alexander Williams, Gregor Meehan, Stefan Lattner, Johan Pauwels, and Mathieu Barthet. Temporal Considerations in DJ Mix Information Retrieval and Generation (Short Paper). In 32nd International Symposium on Temporal Representation and Reasoning (TIME 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 355, pp. 20:1-20:8, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{williams_et_al:LIPIcs.TIME.2025.20,
  author =	{Williams, Alexander and Meehan, Gregor and Lattner, Stefan and Pauwels, Johan and Barthet, Mathieu},
  title =	{{Temporal Considerations in DJ Mix Information Retrieval and Generation}},
  booktitle =	{32nd International Symposium on Temporal Representation and Reasoning (TIME 2025)},
  pages =	{20:1--20:8},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-401-7},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{355},
  editor =	{Vidal, Thierry and Wa{\l}\k{e}ga, Przemys{\l}aw Andrzej},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2025.20},
  URN =		{urn:nbn:de:0030-drops-244662},
  doi =		{10.4230/LIPIcs.TIME.2025.20},
  annote =	{Keywords: Music Information Retrieval, Computational Creativity, Recommender Systems, Electronic Dance Music, DJ}
}
Document
DOI: 10.4230/OASIcs.SpaceCHI.2025.20
Navigating Exoplanetary Systems in Augmented Reality: Preliminary Insights on ExoAR

Authors: Bryson Lawton, Frank Maurer, and Daniel Zielasko

Published in: OASIcs, Volume 130, Advancing Human-Computer Interaction for Space Exploration (SpaceCHI 2025)

Abstract
With thousands of exoplanets now confirmed by space missions such as NASA’s Kepler and TESS, scientific interest and public curiosity about these distant worlds continue to grow. However, current visualization tools for exploring exoplanetary systems often lack sufficient scientific accuracy or interactive features, limiting their educational effectiveness and analytical utility. To help address this gap, we developed ExoAR, an augmented reality tool designed to offer immersive, scientifically sound visualizations of all known exoplanetary systems using data directly sourced from NASA’s Exoplanet Archive. By leveraging augmented reality’s strengths, ExoAR enables users to immerse themselves in interactive, dynamic 3D models of these planetary systems with data-driven representations of planets and their host stars. The application also allows users to adjust various visualization scales independently, a capability designed to aid comprehension of comparative astronomical properties such as orbital mechanics, planetary sizes, and stellar classifications. To begin assessing ExoAR’s potential as an educational and analytical tool and inform future iterations, a pilot user study was conducted. Its findings indicate that participants found ExoAR improved user engagement and spatial understanding compared to NASA’s Eyes on Exoplanets application, a non-immersive exoplanetary system visualization tool. This work-in-progress paper presents these early insights, acknowledges current system limitations, and outlines future directions for more rigorously evaluating and further improving ExoAR’s capabilities for both educational and scientific communities.
Cite as

Bryson Lawton, Frank Maurer, and Daniel Zielasko. Navigating Exoplanetary Systems in Augmented Reality: Preliminary Insights on ExoAR. In Advancing Human-Computer Interaction for Space Exploration (SpaceCHI 2025). Open Access Series in Informatics (OASIcs), Volume 130, pp. 20:1-20:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{lawton_et_al:OASIcs.SpaceCHI.2025.20,
  author =	{Lawton, Bryson and Maurer, Frank and Zielasko, Daniel},
  title =	{{Navigating Exoplanetary Systems in Augmented Reality: Preliminary Insights on ExoAR}},
  booktitle =	{Advancing Human-Computer Interaction for Space Exploration (SpaceCHI 2025)},
  pages =	{20:1--20:13},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-384-3},
  ISSN =	{2190-6807},
  year =	{2025},
  volume =	{130},
  editor =	{Bensch, Leonie and Nilsson, Tommy and Nisser, Martin and Pataranutaporn, Pat and Schmidt, Albrecht and Sumini, Valentina},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.SpaceCHI.2025.20},
  URN =		{urn:nbn:de:0030-drops-240106},
  doi =		{10.4230/OASIcs.SpaceCHI.2025.20},
  annote =	{Keywords: Immersive Analytics, Data Visualization, Astronomy, Astrophysics, Exoplanet, Augmented Reality, AR}
}
Document
DOI: 10.4230/OASIcs.SpaceCHI.2025.30
A Research Framework to Develop a Real-Time Synchrony Index to Monitor Team Cohesion and Performance in Long-Duration Space Exploration

Authors: Federico Nemmi, Emma Chabani, Laure Boyer, Charlie Madier, and Daniel Lewkowicz

Published in: OASIcs, Volume 130, Advancing Human-Computer Interaction for Space Exploration (SpaceCHI 2025)

Abstract
As humanity prepares for long-distance space exploration, optimizing group performance, the ability of a group to achieve its goals efficiently, is critical. Astronaut crews will endure isolation, confinement, and operational stress, making group synchrony - the alignment of behaviors, emotions, and physiological states - a key factor in mission success. Synchrony influences team cohesion, performance, and resilience, necessitating effective crew management strategies. This paper proposes a framework for a real-time, unobtrusive index of group synchrony to support astronauts and mission control. Research indicates that team cohesion fluctuates in isolated environments, with reduced communication and interpersonal conflicts emerging over time. A system tracking synchrony could mitigate these issues, providing proactive support and improving remote management. Additionally, it could serve as a cognitive and physiological feedback tool for astronauts and a decision-making aid for mission control, enhancing well-being and efficiency. Our approach integrates behavioral and physiological synchrony measures to assess team cohesion and performance. We propose a multi-modal synchrony index combining movement coordination, communication patterns, and physiological signals such as heart rate, electrodermal activity, and EEG. This index will be validated across different tasks to ensure applicability across diverse mission scenarios. By developing a robust synchrony index, we address a fundamental challenge in space missions: sustaining team effectiveness under extreme conditions. Beyond space exploration, our findings could benefit high-risk, high-isolation teams in submarine crews, polar expeditions, and remote research groups. Our collaboration with the Centre National d'Etudes Spatiales, the Institut de Médecine et de Physiologie Spatiales, and the Toulouse University Hospital marks the first step, with experimental data collection starting this year. Ultimately, this research fosters more adaptive, responsive, and resilient teams for future space missions.
Cite as

Federico Nemmi, Emma Chabani, Laure Boyer, Charlie Madier, and Daniel Lewkowicz. A Research Framework to Develop a Real-Time Synchrony Index to Monitor Team Cohesion and Performance in Long-Duration Space Exploration. In Advancing Human-Computer Interaction for Space Exploration (SpaceCHI 2025). Open Access Series in Informatics (OASIcs), Volume 130, pp. 30:1-30:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{nemmi_et_al:OASIcs.SpaceCHI.2025.30,
  author =	{Nemmi, Federico and Chabani, Emma and Boyer, Laure and Madier, Charlie and Lewkowicz, Daniel},
  title =	{{A Research Framework to Develop a Real-Time Synchrony Index to Monitor Team Cohesion and Performance in Long-Duration Space Exploration}},
  booktitle =	{Advancing Human-Computer Interaction for Space Exploration (SpaceCHI 2025)},
  pages =	{30:1--30:16},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-384-3},
  ISSN =	{2190-6807},
  year =	{2025},
  volume =	{130},
  editor =	{Bensch, Leonie and Nilsson, Tommy and Nisser, Martin and Pataranutaporn, Pat and Schmidt, Albrecht and Sumini, Valentina},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.SpaceCHI.2025.30},
  URN =		{urn:nbn:de:0030-drops-240200},
  doi =		{10.4230/OASIcs.SpaceCHI.2025.30},
  annote =	{Keywords: Performance, Synchronie, Crew monitoring, Cohesion}
}
Document
DOI: 10.4230/OASIcs.SpaceCHI.2025.27
Assessing the Use of Mixed Reality as a Valid Tool for Human-Robot Interaction Studies in the Context of Space Exploration

Authors: Enrico Guerra, Sebastian Thomas Büttner, Alper Beşer, and Michael Prilla

Published in: OASIcs, Volume 130, Advancing Human-Computer Interaction for Space Exploration (SpaceCHI 2025)

Abstract
Mixed Reality (MR) is a technology with strong potential for advancing research in Human-Robot Interaction (HRI) for space exploration. Apart from the efficiency and high flexibility MR can offer, we argue that its benefits for HRI research in space contexts lies particularly in its ability to aid human-in-the-loop development, offer realistic hybrid simulations, and foster broader participation in HRI research in the space exploration context. However, we believe that this is only plausible if MR-based simulations can yield comparable results to fully physical approaches in human-centred studies. In this position paper, we highlight several arguments in favour of MR as a tool for space HRI research, while emphasising the importance of the open question regarding its scientific validity. We believe MR could become a central tool for preparing for future human-robotic space exploration missions and significantly diversify research in this domain.
Cite as

Enrico Guerra, Sebastian Thomas Büttner, Alper Beşer, and Michael Prilla. Assessing the Use of Mixed Reality as a Valid Tool for Human-Robot Interaction Studies in the Context of Space Exploration. In Advancing Human-Computer Interaction for Space Exploration (SpaceCHI 2025). Open Access Series in Informatics (OASIcs), Volume 130, pp. 27:1-27:11, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{guerra_et_al:OASIcs.SpaceCHI.2025.27,
  author =	{Guerra, Enrico and B\"{u}ttner, Sebastian Thomas and Be\c{s}er, Alper and Prilla, Michael},
  title =	{{Assessing the Use of Mixed Reality as a Valid Tool for Human-Robot Interaction Studies in the Context of Space Exploration}},
  booktitle =	{Advancing Human-Computer Interaction for Space Exploration (SpaceCHI 2025)},
  pages =	{27:1--27:11},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-384-3},
  ISSN =	{2190-6807},
  year =	{2025},
  volume =	{130},
  editor =	{Bensch, Leonie and Nilsson, Tommy and Nisser, Martin and Pataranutaporn, Pat and Schmidt, Albrecht and Sumini, Valentina},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.SpaceCHI.2025.27},
  URN =		{urn:nbn:de:0030-drops-240175},
  doi =		{10.4230/OASIcs.SpaceCHI.2025.27},
  annote =	{Keywords: Mixed Reality, Augmented Reality, Human-Robot Interaction, Space Exploration, Validity}
}
Document
DOI: 10.4230/LIPIcs.WABI.2025.22
Design of Worst-Case-Optimal Spaced Seeds

Authors: Jens Zentgraf and Sven Rahmann

Published in: LIPIcs, Volume 344, 25th International Conference on Algorithms for Bioinformatics (WABI 2025)

Abstract
Read mapping (and alignment) is a fundamental problem in biological sequence analysis. For speed and computational efficiency, many popular read mappers tolerate only a few differences between the read and the corresponding part of the reference genome, which leads to reference bias: Reads with too many differences are not guaranteed to be mapped correctly or at all, because to even consider a genomic position, a sufficiently long exact match (seed) must exist. While pangenomes and their graph-based representations provide one way to avoid reference bias by enlarging the reference, we explore an orthogonal approach and consider stronger substitution-tolerant primitives, namely spaced seeds or gapped k-mers. Given two integers k ≤ w, one considers k selected positions, described by a mask, from each length-w window in a sequence. In the existing literature, masks with certain probabilistic guarantees have been designed for small values of k. Here, for the first time, we take a combinatorial approach from a worst-case perspective. For any mask, using integer linear programs, we find least favorable distributions of sequence changes in two different senses: (1) minimizing the number of unchanged windows; (2) minimizing the number of positions covered by unchanged windows. Then, among all masks or all symmetric masks of a given shape (k,w), we find the set of best masks that maximize these minima. As a result, we obtain robust masks, even for large numbers of changes. We illustrate the properties of these masks by constructing a challenging set of reads that contain many approximately equidistributed substitutions (but no indels) that many existing tools cannot map, even though they are in principle easily mappable (apart from the large number of changes) because they originate from selected non-repetitive regions of the human reference genome. We observe that the majority of these reads can be mapped with a simple alignment-free approach using chosen spaced masks, where seeding approaches based on contiguous k-mers fail.
Cite as

Jens Zentgraf and Sven Rahmann. Design of Worst-Case-Optimal Spaced Seeds. In 25th International Conference on Algorithms for Bioinformatics (WABI 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 344, pp. 22:1-22:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{zentgraf_et_al:LIPIcs.WABI.2025.22,
  author =	{Zentgraf, Jens and Rahmann, Sven},
  title =	{{Design of Worst-Case-Optimal Spaced Seeds}},
  booktitle =	{25th International Conference on Algorithms for Bioinformatics (WABI 2025)},
  pages =	{22:1--22:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-386-7},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{344},
  editor =	{Brejov\'{a}, Bro\v{n}a and Patro, Rob},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.WABI.2025.22},
  URN =		{urn:nbn:de:0030-drops-239488},
  doi =		{10.4230/LIPIcs.WABI.2025.22},
  annote =	{Keywords: Spaced seed, Gapped k-mer, Integer linear program (ILP), Worst-case design, Reference bias}
}
Document
DOI: 10.4230/LIPIcs.WABI.2025.20
A k-mer-Based Estimator of the Substitution Rate Between Repetitive Sequences

Authors: Haonan Wu, Antonio Blanca, and Paul Medvedev

Published in: LIPIcs, Volume 344, 25th International Conference on Algorithms for Bioinformatics (WABI 2025)

Abstract
K-mer-based analysis of genomic data is ubiquitous, but the presence of repetitive k-mers continues to pose problems for the accuracy of many methods. For example, the Mash tool (Ondov et al. 2016) can accurately estimate the substitution rate between two low-repetitive sequences from their k-mer sketches; however, it is inaccurate on repetitive sequences such as the centromere of a human chromosome. Follow-up work by Blanca et al. (2021) has attempted to model how mutations affect k-mer sets based on strong assumptions that the sequence is non-repetitive and that mutations do not create spurious k-mer matches. However, the theoretical foundations for extending an estimator like Mash to work in the presence of repeat sequences have been lacking. In this work, we relax the non-repetitive assumption and propose a novel estimator for the mutation rate. We derive theoretical bounds on our estimator’s bias. Our experiments show that it remains accurate for repetitive genomic sequences, such as the alpha satellite higher order repeats in centromeres. We demonstrate our estimator’s robustness across diverse datasets and various ranges of the substitution rate and k-mer size. Finally, we show how sketching can be used to avoid dealing with large k-mer sets while retaining accuracy. Our software is available at https://github.com/medvedevgroup/Repeat-Aware_Substitution_Rate_Estimator.
Cite as

Haonan Wu, Antonio Blanca, and Paul Medvedev. A k-mer-Based Estimator of the Substitution Rate Between Repetitive Sequences. In 25th International Conference on Algorithms for Bioinformatics (WABI 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 344, pp. 20:1-20:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{wu_et_al:LIPIcs.WABI.2025.20,
  author =	{Wu, Haonan and Blanca, Antonio and Medvedev, Paul},
  title =	{{A k-mer-Based Estimator of the Substitution Rate Between Repetitive Sequences}},
  booktitle =	{25th International Conference on Algorithms for Bioinformatics (WABI 2025)},
  pages =	{20:1--20:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-386-7},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{344},
  editor =	{Brejov\'{a}, Bro\v{n}a and Patro, Rob},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.WABI.2025.20},
  URN =		{urn:nbn:de:0030-drops-239465},
  doi =		{10.4230/LIPIcs.WABI.2025.20},
  annote =	{Keywords: k-mers, sketching, mutation rates}
}
Document
Research
DOI: 10.4230/OASIcs.Grossi.7
Conditional Lower Bounds for String Matching in Labelled Graphs

Authors: Massimo Equi

Published in: OASIcs, Volume 132, From Strings to Graphs, and Back Again: A Festschrift for Roberto Grossi's 60th Birthday (2025)

Abstract
The problem of String Matching in Labelled Graphs (SMLG) is one possible generalization of the classic problem of finding a string inside another of greater length. In its most general form, SMLG asks to find a match for a string into a graph, which can be directed or undirected. As for string matching, many different variations are possible. For example, the match could be exact or approximate, and the match could lie on a path or a walk. Some of these variations easily fall into the NP-hard realm, while other variants are solvable in polynomial time. For the latter ones, fine-grained complexity has been a game changer in proving quadratic conditional lower bounds, allowing to finally close the gap with those upper bounds that remained unmatched for almost two decades. If the match is allowed to be approximate, SMLG enjoys the same conditional quadratic lower bounds shown for example for edit distance (Backurs and Indyk, STOC '15). The case that really requires ad hoc conditional lower bounds is the one of finding an exact match that lies on a walk. In this work, we focus on explaining various conditional lower bounds for this version of SMLG, with the goal of giving an overall perspective that could help understand which aspects of the problem make it quadratic. We will introduce the reader to the field of fine-grained complexity and show how it can successfully provide the exact type of lower bounds needed for polynomial problems such as SMLG.
Cite as

Massimo Equi. Conditional Lower Bounds for String Matching in Labelled Graphs. In From Strings to Graphs, and Back Again: A Festschrift for Roberto Grossi's 60th Birthday. Open Access Series in Informatics (OASIcs), Volume 132, pp. 7:1-7:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{equi:OASIcs.Grossi.7,
  author =	{Equi, Massimo},
  title =	{{Conditional Lower Bounds for String Matching in Labelled Graphs}},
  booktitle =	{From Strings to Graphs, and Back Again: A Festschrift for Roberto Grossi's 60th Birthday},
  pages =	{7:1--7:13},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-391-1},
  ISSN =	{2190-6807},
  year =	{2025},
  volume =	{132},
  editor =	{Conte, Alessio and Marino, Andrea and Rosone, Giovanna and Vitter, Jeffrey Scott},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.Grossi.7},
  URN =		{urn:nbn:de:0030-drops-238063},
  doi =		{10.4230/OASIcs.Grossi.7},
  annote =	{Keywords: conditional lower bounds, strong exponential time hypothesis, fine-grained complexity, string matching, graphs}
}
Document
DOI: 10.4230/LIPIcs.CALCO.2025.9
Safety and Strong Completeness via Reducibility for Many-Valued Coalgebraic Dynamic Logics

Authors: Helle Hvid Hansen and Wolfgang Poiger

Published in: LIPIcs, Volume 342, 11th Conference on Algebra and Coalgebra in Computer Science (CALCO 2025)

Abstract
We present a coalgebraic framework for studying generalisations of dynamic modal logics such as PDL and game logic in which both the propositions and the semantic structures can take values in an algebra 𝐀 of truth-degrees. More precisely, we work with coalgebraic modal logic via 𝐀-valued predicate liftings where 𝐀 is an FLew-algebra, and interpret actions (abstracting programs and games) as 𝖥-coalgebras where the functor 𝖥 represents some type of 𝐀-weighted system. We also allow combinations of crisp propositions with 𝐀-weighted systems and vice versa. We introduce coalgebra operations and tests, with a focus on operations which are reducible in the sense that modalities for composed actions can be reduced to compositions of modalities for the constituent actions. We prove that reducible operations are safe for bisimulation and behavioural equivalence, and prove a general strong completeness result, from which we obtain new strong completeness results for 𝟐-valued iteration-free PDL with 𝐀-valued accessibility relations when 𝐀 is a finite chain, and for many-valued iteration-free game logic with many-valued strategies based on finite Lukasiewicz logic.
Cite as

Helle Hvid Hansen and Wolfgang Poiger. Safety and Strong Completeness via Reducibility for Many-Valued Coalgebraic Dynamic Logics. In 11th Conference on Algebra and Coalgebra in Computer Science (CALCO 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 342, pp. 9:1-9:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{hansen_et_al:LIPIcs.CALCO.2025.9,
  author =	{Hansen, Helle Hvid and Poiger, Wolfgang},
  title =	{{Safety and Strong Completeness via Reducibility for Many-Valued Coalgebraic Dynamic Logics}},
  booktitle =	{11th Conference on Algebra and Coalgebra in Computer Science (CALCO 2025)},
  pages =	{9:1--9:23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-383-6},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{342},
  editor =	{C\^{i}rstea, Corina and Knapp, Alexander},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2025.9},
  URN =		{urn:nbn:de:0030-drops-235681},
  doi =		{10.4230/LIPIcs.CALCO.2025.9},
  annote =	{Keywords: dynamic logic, many-valued coalgebraic logic, safety, strong completeness}
}
Document
DOI: 10.4230/LIPIcs.ECRTS.2025.15
Analysis of EDF for Real-Time Multiprocessor Systems with Resource Sharing

Authors: Kunal Agrawal, Sanjoy Baruah, Jeremy T. Fineman, Alberto Marchetti-Spaccamela, and Jinhao Zhao

Published in: LIPIcs, Volume 335, 37th Euromicro Conference on Real-Time Systems (ECRTS 2025)

Abstract
The classic Earliest Deadline First (EDF) algorithm is widely studied and used due to its simplicity and strong theoretical performance, but has not been rigorously analyzed for systems where jobs may execute critical sections protected by shared locks. Analyzing such systems is often challenging due to unpredictable delays caused by contention. In this paper, we propose a straightforward generalization of EDF, called EDF-Block. In this generalization, the critical sections are executed non-preemptively, but scheduling and lock acquisition priorities are based on EDF. We establish lower bounds on the speed augmentation required for any non-clairvoyant scheduler (EDF-Block is an example of non-clairvoyant schedulers) and for EDF-Block, showing that EDF-Block requires at least 4.11× speed augmentation for jobs and 4× for tasks. We then provide an upper bound analysis, demonstrating that EDF-Block requires speedup of at most 6 to schedule all feasible job and task sets.
Cite as

Kunal Agrawal, Sanjoy Baruah, Jeremy T. Fineman, Alberto Marchetti-Spaccamela, and Jinhao Zhao. Analysis of EDF for Real-Time Multiprocessor Systems with Resource Sharing. In 37th Euromicro Conference on Real-Time Systems (ECRTS 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 335, pp. 15:1-15:26, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{agrawal_et_al:LIPIcs.ECRTS.2025.15,
  author =	{Agrawal, Kunal and Baruah, Sanjoy and Fineman, Jeremy T. and Marchetti-Spaccamela, Alberto and Zhao, Jinhao},
  title =	{{Analysis of EDF for Real-Time Multiprocessor Systems with Resource Sharing}},
  booktitle =	{37th Euromicro Conference on Real-Time Systems (ECRTS 2025)},
  pages =	{15:1--15:26},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-377-5},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{335},
  editor =	{Mancuso, Renato},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECRTS.2025.15},
  URN =		{urn:nbn:de:0030-drops-235932},
  doi =		{10.4230/LIPIcs.ECRTS.2025.15},
  annote =	{Keywords: Real-Time Scheduling, Non-Clairvoyant Scheduling, EDF, Competitive Analysis, Shared Resources}
}
Document
Track A: Algorithms, Complexity and Games
DOI: 10.4230/LIPIcs.ICALP.2025.105
NPA Hierarchy for Quantum Isomorphism and Homomorphism Indistinguishability

Authors: Prem Nigam Kar, David E. Roberson, Tim Seppelt, and Peter Zeman

Published in: LIPIcs, Volume 334, 52nd International Colloquium on Automata, Languages, and Programming (ICALP 2025)

Abstract
Mančinska and Roberson [FOCS'20] showed that two graphs are quantum isomorphic if and only if they are homomorphism indistinguishable over the class of planar graphs. Atserias et al. [JCTB'19] proved that quantum isomorphism is undecidable in general. The NPA hierarchy gives a sequence of semidefinite programming relaxations of quantum isomorphism. Recently, Roberson and Seppelt [ICALP'23] obtained a homomorphism indistinguishability characterization of the feasibility of each level of the Lasserre hierarchy of semidefinite programming relaxations of graph isomorphism. We prove a quantum analogue of this result by showing that each level of the NPA hierarchy of SDP relaxations for quantum isomorphism of graphs is equivalent to homomorphism indistinguishability over an appropriate class of planar graphs. By combining the convergence of the NPA hierarchy with the fact that the union of these graph classes is the set of all planar graphs, we are able to give a new proof of the result of Mančinska and Roberson [FOCS'20] that avoids the use of the theory of quantum groups. This homomorphism indistinguishability characterization also allows us to give a randomized polynomial-time algorithm deciding exact feasibility of each fixed level of the NPA hierarchy of SDP relaxations for quantum isomorphism.
Cite as

Prem Nigam Kar, David E. Roberson, Tim Seppelt, and Peter Zeman. NPA Hierarchy for Quantum Isomorphism and Homomorphism Indistinguishability. In 52nd International Colloquium on Automata, Languages, and Programming (ICALP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 334, pp. 105:1-105:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{kar_et_al:LIPIcs.ICALP.2025.105,
  author =	{Kar, Prem Nigam and Roberson, David E. and Seppelt, Tim and Zeman, Peter},
  title =	{{NPA Hierarchy for Quantum Isomorphism and Homomorphism Indistinguishability}},
  booktitle =	{52nd International Colloquium on Automata, Languages, and Programming (ICALP 2025)},
  pages =	{105:1--105:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-372-0},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{334},
  editor =	{Censor-Hillel, Keren and Grandoni, Fabrizio and Ouaknine, Jo\"{e}l and Puppis, Gabriele},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2025.105},
  URN =		{urn:nbn:de:0030-drops-234828},
  doi =		{10.4230/LIPIcs.ICALP.2025.105},
  annote =	{Keywords: Quantum isomorphism, NPA hierarchy, homomorphism indistinguishability}
}
Document
Track B: Automata, Logic, Semantics, and Theory of Programming
DOI: 10.4230/LIPIcs.ICALP.2025.145
Reducing Stochastic Games to Semidefinite Programming

Authors: Manuel Bodirsky, Georg Loho, and Mateusz Skomra

Published in: LIPIcs, Volume 334, 52nd International Colloquium on Automata, Languages, and Programming (ICALP 2025)

Abstract
We present a polynomial-time reduction from max-average constraints to the feasibility problem for semidefinite programs. This shows that Condon’s simple stochastic games, stochastic mean payoff games, and in particular mean payoff games and parity games can all be reduced to semidefinite programming.
Cite as

Manuel Bodirsky, Georg Loho, and Mateusz Skomra. Reducing Stochastic Games to Semidefinite Programming. In 52nd International Colloquium on Automata, Languages, and Programming (ICALP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 334, pp. 145:1-145:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{bodirsky_et_al:LIPIcs.ICALP.2025.145,
  author =	{Bodirsky, Manuel and Loho, Georg and Skomra, Mateusz},
  title =	{{Reducing Stochastic Games to Semidefinite Programming}},
  booktitle =	{52nd International Colloquium on Automata, Languages, and Programming (ICALP 2025)},
  pages =	{145:1--145:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-372-0},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{334},
  editor =	{Censor-Hillel, Keren and Grandoni, Fabrizio and Ouaknine, Jo\"{e}l and Puppis, Gabriele},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2025.145},
  URN =		{urn:nbn:de:0030-drops-235224},
  doi =		{10.4230/LIPIcs.ICALP.2025.145},
  annote =	{Keywords: Mean-payoff games, stochastic games, semidefinite programming, max-average constraints, max-atom problem}
}
Document
Track B: Automata, Logic, Semantics, and Theory of Programming
DOI: 10.4230/LIPIcs.ICALP.2025.146
Saturation Problems for Families of Automata

Authors: León Bohn, Yong Li, Christof Löding, and Sven Schewe

Published in: LIPIcs, Volume 334, 52nd International Colloquium on Automata, Languages, and Programming (ICALP 2025)

Abstract
Families of deterministic finite automata (FDFA) represent regular ω-languages through their ultimately periodic words (UP-words). An FDFA accepts pairs of words, where the first component corresponds to a prefix of the UP-word, and the second component represents a period of that UP-word. An FDFA is termed saturated if, for each UP-word, either all or none of the pairs representing that UP-word are accepted. We demonstrate that determining whether a given FDFA is saturated can be accomplished in polynomial time, thus improving the known PSPACE upper bound by an exponential. We illustrate the application of this result by presenting the first polynomial learning algorithms for representations of the class of all regular ω-languages. Furthermore, we establish that deciding a weaker property, referred to as almost saturation, is PSPACE-complete. Since FDFAs do not necessarily define regular ω-languages when they are not saturated, we also address the regularity problem and show that it is PSPACE-complete. Finally, we explore a variant of FDFAs called families of deterministic weak automata (FDWA), where the semantics for the periodic part of the UP-word considers ω-words instead of finite words. We demonstrate that saturation for FDWAs is also decidable in polynomial time, that FDWAs always define regular ω-languages, and we compare the succinctness of these different models.
Cite as

León Bohn, Yong Li, Christof Löding, and Sven Schewe. Saturation Problems for Families of Automata. In 52nd International Colloquium on Automata, Languages, and Programming (ICALP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 334, pp. 146:1-146:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{bohn_et_al:LIPIcs.ICALP.2025.146,
  author =	{Bohn, Le\'{o}n and Li, Yong and L\"{o}ding, Christof and Schewe, Sven},
  title =	{{Saturation Problems for Families of Automata}},
  booktitle =	{52nd International Colloquium on Automata, Languages, and Programming (ICALP 2025)},
  pages =	{146:1--146:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-372-0},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{334},
  editor =	{Censor-Hillel, Keren and Grandoni, Fabrizio and Ouaknine, Jo\"{e}l and Puppis, Gabriele},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2025.146},
  URN =		{urn:nbn:de:0030-drops-235239},
  doi =		{10.4230/LIPIcs.ICALP.2025.146},
  annote =	{Keywords: Families of Automata, automata learning, FDFAs}
}
Document
Track B: Automata, Logic, Semantics, and Theory of Programming
DOI: 10.4230/LIPIcs.ICALP.2025.152
Tree Algebras and Bisimulation-Invariant MSO on Finite Graphs

Authors: Thomas Colcombet, Amina Doumane, and Denis Kuperberg

Published in: LIPIcs, Volume 334, 52nd International Colloquium on Automata, Languages, and Programming (ICALP 2025)

Abstract
We establish that the bisimulation invariant fragment of MSO over finite transition systems is expressively equivalent over finite transition systems to modal μ-calculus, a question that had remained open for several decades. The proof goes by translating the question to an algebraic framework, and showing that the languages of regular trees that are recognised by finitary tree algebras whose sorts zero and one are finite are the regular ones. This corresponds for trees to a weak form of the key translation of Wilke algebras to omega-semigroup over infinite words, and was also a missing piece in the algebraic theory of regular languages of infinite trees for twenty years.
Cite as

Thomas Colcombet, Amina Doumane, and Denis Kuperberg. Tree Algebras and Bisimulation-Invariant MSO on Finite Graphs. In 52nd International Colloquium on Automata, Languages, and Programming (ICALP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 334, pp. 152:1-152:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{colcombet_et_al:LIPIcs.ICALP.2025.152,
  author =	{Colcombet, Thomas and Doumane, Amina and Kuperberg, Denis},
  title =	{{Tree Algebras and Bisimulation-Invariant MSO on Finite Graphs}},
  booktitle =	{52nd International Colloquium on Automata, Languages, and Programming (ICALP 2025)},
  pages =	{152:1--152:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-372-0},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{334},
  editor =	{Censor-Hillel, Keren and Grandoni, Fabrizio and Ouaknine, Jo\"{e}l and Puppis, Gabriele},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2025.152},
  URN =		{urn:nbn:de:0030-drops-235294},
  doi =		{10.4230/LIPIcs.ICALP.2025.152},
  annote =	{Keywords: MSO, mu-calculus, finite graphs, bisimulation, tree algebra}
}
Document
DOI: 10.4230/LIPIcs.ECOOP.2025.34
Taming and Dissecting Recursions Through Interprocedural Weak Topological Ordering

Authors: Jiawei Yang, Xiao Cheng, Bor-Yuh Evan Chang, Xiapu Luo, and Yulei Sui

Published in: LIPIcs, Volume 333, 39th European Conference on Object-Oriented Programming (ECOOP 2025)

Abstract
Abstract interpretation provides a foundational framework for approximating program semantics by interpreting code through abstract domains using semantic functions over ordered sets along a program’s control flow graph (CFG). To facilitate fixpoint computation in abstract interpretation, weak topological ordering (WTO) is an effective strategy for handling loops, as it identifies strategic control points in the CFG where widening and narrowing operations should be applied. However, existing abstract interpreters still face challenges when extending WTO computation in the presence of recursive programs. Computing a precise whole-program WTO requires full context-sensitive analysis which is not scalable for large programs, while context-insensitive analysis introduces spurious cycles that compromise precision. Current approaches either ignore recursion (resulting in unsoundness) or rely on conservative approximations, sacrificing precision by adopting the greatest elements of abstract domains and applying widening at function boundaries without subsequent narrowing refinements. These can lead to undesired results for downstream tasks, such as bug detection. To address the above limitations, we present RecTopo, a new technique to boost the efficiency of precise abstract interpretation in the presence of recursive programs through interprocedural weak topological ordering (IWTO). Rather than pursuing an expensive whole-program WTO analysis, RecTopo employs an on-demand approach that strategically decomposes programs at recursion boundaries and constructs targeted IWTOs for each recursive component. RecTopo dissects and analyzes (nested) recursions through interleaved widening and narrowing operations. This approach enables precise control over interpretation ordering within recursive structures while eliminating spurious recursions through systematic correlation of control flow and call graphs. We implemented RecTopo and evaluated its effectiveness using an assertion-based checking client focused on buffer overflow detection, comparing it against three popular open-source abstract interpreters (IKOS, Clam, CSA). The experiments on 8312 programs from the NIST dataset demonstrate that, on average, RecTopo is 31.99% more precise and achieves a 17.49% higher recall rate compared to three other tools. Moreover, RecTopo exhibits an average precision improvement of 46.51% and a higher recall rate of 32.98% compared to our baselines across ten large open-source projects. Further ablation studies reveal that IWTO reduces spurious widening operations compared to whole-program WTO, resulting in a 12.83% reduction in analysis time.
Cite as

Jiawei Yang, Xiao Cheng, Bor-Yuh Evan Chang, Xiapu Luo, and Yulei Sui. Taming and Dissecting Recursions Through Interprocedural Weak Topological Ordering. In 39th European Conference on Object-Oriented Programming (ECOOP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 333, pp. 34:1-34:31, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{yang_et_al:LIPIcs.ECOOP.2025.34,
  author =	{Yang, Jiawei and Cheng, Xiao and Chang, Bor-Yuh Evan and Luo, Xiapu and Sui, Yulei},
  title =	{{Taming and Dissecting Recursions Through Interprocedural Weak Topological Ordering}},
  booktitle =	{39th European Conference on Object-Oriented Programming (ECOOP 2025)},
  pages =	{34:1--34:31},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-373-7},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{333},
  editor =	{Aldrich, Jonathan and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2025.34},
  URN =		{urn:nbn:de:0030-drops-233265},
  doi =		{10.4230/LIPIcs.ECOOP.2025.34},
  annote =	{Keywords: Abstract interpretation, recursion, weak topological ordering}
}
  • Refine by Type
  • 26 Document/PDF
  • 22 Document/HTML

  • Refine by Publication Year
  • 1 2026
  • 17 2025
  • 4 2024
  • 1 2023
  • 1 2022
  • Show More...

  • Refine by Author
  • 2 Hansen, Eric A.
  • 2 Seppelt, Tim
  • 1 Agrawal, Kunal
  • 1 Barthet, Mathieu
  • 1 Baruah, Sanjoy
  • Show More...

  • Refine by Series/Journal
  • 13 LIPIcs
  • 6 OASIcs
  • 1 LITES
  • 4 TGDK
  • 2 DagSemProc

  • Refine by Classification
  • 2 Applied computing → Bioinformatics
  • 2 Computing methodologies → Knowledge representation and reasoning
  • 2 Computing methodologies → Ontology engineering
  • 2 Theory of computation → Finite Model Theory
  • 2 Theory of computation → Modal and temporal logics
  • Show More...

  • Refine by Keyword
  • 2 Augmented Reality
  • 2 Knowledge Graphs
  • 1 AI Planning
  • 1 AR
  • 1 Abstract interpretation
  • Show More...

Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact