25 Search Results for "Müller-Olm, Markus"

Volume

Dagstuhl Follow-Ups, Volume 3

Multimodal Music Processing

Editors: Meinard Müller, Masataka Goto, and Markus Schedl

Document
Invited Talk
DOI: 10.4230/LIPIcs.MFCS.2023.4
Algebraic Reasoning for (Un)Solvable Loops (Invited Talk)

Authors: Laura Kovács

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

Abstract
Loop invariants describe valid program properties that hold before and after every loop iteration. As such, loop invariants are the workhorses in formalizing loop semantics and automating the formal analysis and verification of programs with loops. While automatically synthesizing loop invariants is, in general, an uncomputable problem, when considering only single-path loops with linear updates (linear loops), the strongest polynomial invariant is in fact computable [Michael Karr, 1976; Markus Müller-Olm and Helmut Seidl, 2004; Laura Kovács, 2008; Ehud Hrushovski et al., 2018]. Yet, already for loops with "only" polynomial updates, computing the strongest invariant has been an open challenge since 2004 [Markus Müller-Olm and Helmut Seidl, 2004]. In this invited talk, we first present computability results on polynomial invariant synthesis for restricted polynomial loops, called solvable loops [Rodríguez-Carbonell and Kapur, 2004]. Key to solvable loops is that one can automatically compute invariants from closed-form solutions of algebraic recurrence equations that model the loop behaviour [Laura Kovács, 2008; Andreas Humenberger et al., 2017]. We also establish a technique for invariant synthesis for classes of loops that are not solvable, termed unsolvable loops [Daneshvar Amrollahi et al., 2022]. We next study the limits of computability in deriving the (strongest) polynomial invariants for arbitrary polynomial loops. We prove that computing the strongest polynomial invariant of arbitrary, single-path polynomial loops is very hard [Julian Müllner, 2023] - namely, it is at least as hard as the Skolem problem [Graham Everest et al., 2003; Terrence Tao, 2008], a prominent algebraic problem in the theory of linear recurrences. Going beyond single-path loops, we show that the strongest polynomial invariant is uncomputable already for multi-path polynomial loops with arbitrary quadratic polynomial updates [Laura Kovács and Anton Varonka, 2023].
Cite as

Laura Kovács. Algebraic Reasoning for (Un)Solvable Loops (Invited Talk). In 48th International Symposium on Mathematical Foundations of Computer Science (MFCS 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 272, pp. 4:1-4:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{kovacs:LIPIcs.MFCS.2023.4,
  author =	{Kov\'{a}cs, Laura},
  title =	{{Algebraic Reasoning for (Un)Solvable Loops}},
  booktitle =	{48th International Symposium on Mathematical Foundations of Computer Science (MFCS 2023)},
  pages =	{4:1--4:2},
  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.4},
  URN =		{urn:nbn:de:0030-drops-185385},
  doi =		{10.4230/LIPIcs.MFCS.2023.4},
  annote =	{Keywords: Symbolic Computation, Formal Methods, Loop Analysis, Polynomial Invariants}
}
Document
DOI: 10.4230/LIPIcs.STACS.2021.24
Inference and Mutual Information on Random Factor Graphs

Authors: Amin Coja-Oghlan, Max Hahn-Klimroth, Philipp Loick, Noela Müller, Konstantinos Panagiotou, and Matija Pasch

Published in: LIPIcs, Volume 187, 38th International Symposium on Theoretical Aspects of Computer Science (STACS 2021)

Abstract
Random factor graphs provide a powerful framework for the study of inference problems such as decoding problems or the stochastic block model. Information-theoretically the key quantity of interest is the mutual information between the observed factor graph and the underlying ground truth around which the factor graph was created; in the stochastic block model, this would be the planted partition. The mutual information gauges whether and how well the ground truth can be inferred from the observable data. For a very general model of random factor graphs we verify a formula for the mutual information predicted by physics techniques. As an application we prove a conjecture about low-density generator matrix codes from [Montanari: IEEE Transactions on Information Theory 2005]. Further applications include phase transitions of the stochastic block model and the mixed k-spin model from physics.
Cite as

Amin Coja-Oghlan, Max Hahn-Klimroth, Philipp Loick, Noela Müller, Konstantinos Panagiotou, and Matija Pasch. Inference and Mutual Information on Random Factor Graphs. In 38th International Symposium on Theoretical Aspects of Computer Science (STACS 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 187, pp. 24:1-24:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{cojaoghlan_et_al:LIPIcs.STACS.2021.24,
  author =	{Coja-Oghlan, Amin and Hahn-Klimroth, Max and Loick, Philipp and M\"{u}ller, Noela and Panagiotou, Konstantinos and Pasch, Matija},
  title =	{{Inference and Mutual Information on Random Factor Graphs}},
  booktitle =	{38th International Symposium on Theoretical Aspects of Computer Science (STACS 2021)},
  pages =	{24:1--24:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-180-1},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{187},
  editor =	{Bl\"{a}ser, Markus and Monmege, Benjamin},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2021.24},
  URN =		{urn:nbn:de:0030-drops-136692},
  doi =		{10.4230/LIPIcs.STACS.2021.24},
  annote =	{Keywords: Information theory, random factor graphs, inference problems, phase transitions}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2020.50
Propositional Dynamic Logic for Hyperproperties

Authors: Jens Oliver Gutsfeld, Markus Müller-Olm, and Christoph Ohrem

Published in: LIPIcs, Volume 171, 31st International Conference on Concurrency Theory (CONCUR 2020)

Abstract
Information security properties of reactive systems like non-interference often require relating different executions of the system to each other and following them simultaneously. Such hyperproperties can also be useful in other contexts, e.g., when analysing properties of distributed systems like linearizability. Since common logics like LTL, CTL, or the modal μ-calculus cannot express hyperproperties, the hyperlogics HyperLTL and HyperCTL^* were developed to cure this defect. However, these logics are not able to express arbitrary ω-regular properties. In this paper, we introduce HyperPDL-Δ, an adaptation of the Propositional Dynamic Logic of Fischer and Ladner for hyperproperties, in order to remove this limitation. Using an elegant automata-theoretic framework, we show that HyperPDL-Δ model checking is asymptotically not more expensive than HyperCTL^* model checking, despite its vastly increased expressive power. We further investigate fragments of HyperPDL-Δ with regard to satisfiability checking.
Cite as

Jens Oliver Gutsfeld, Markus Müller-Olm, and Christoph Ohrem. Propositional Dynamic Logic for Hyperproperties. In 31st International Conference on Concurrency Theory (CONCUR 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 171, pp. 50:1-50:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{gutsfeld_et_al:LIPIcs.CONCUR.2020.50,
  author =	{Gutsfeld, Jens Oliver and M\"{u}ller-Olm, Markus and Ohrem, Christoph},
  title =	{{Propositional Dynamic Logic for Hyperproperties}},
  booktitle =	{31st International Conference on Concurrency Theory (CONCUR 2020)},
  pages =	{50:1--50:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-160-3},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{171},
  editor =	{Konnov, Igor and Kov\'{a}cs, Laura},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2020.50},
  URN =		{urn:nbn:de:0030-drops-128628},
  doi =		{10.4230/LIPIcs.CONCUR.2020.50},
  annote =	{Keywords: Hyperlogics, Hyperproperties, Model Checking, Automata}
}
Document
DOI: 10.4230/OASIcs.ATMOS.2018.4
Robustness as a Third Dimension for Evaluating Public Transport Plans

Authors: Markus Friedrich, Matthias Müller-Hannemann, Ralf Rückert, Alexander Schiewe, and Anita Schöbel

Published in: OASIcs, Volume 65, 18th Workshop on Algorithmic Approaches for Transportation Modelling, Optimization, and Systems (ATMOS 2018)

Abstract
Providing attractive and efficient public transport services is of crucial importance due to higher demands for mobility and the need to reduce air pollution and to save energy. The classical planning process in public transport tries to achieve a reasonable compromise between service quality for passengers and operating costs. Service quality mostly considers quantities like average travel time and number of transfers. Since daily public transport inevitably suffers from delays caused by random disturbances and disruptions, robustness also plays a crucial role. While there are recent attempts to achieve delay-resistant timetables, comparably little work has been done to systematically assess and to compare the robustness of transport plans from a passenger point of view. We here provide a general and flexible framework for evaluating public transport plans (lines, timetables, and vehicle schedules) in various ways. It enables planners to explore several trade-offs between operating costs, service quality (average perceived travel time of passengers), and robustness against delays. For such an assessment we develop several passenger-oriented robustness tests which can be instantiated with parameterized delay scenarios. Important features of our framework include detailed passenger flow models, delay propagation schemes and disposition strategies, rerouting strategies as well as vehicle capacities. To demonstrate possible use cases, our framework has been applied to a variety of public transport plans which have been created for the same given demand for an artificial urban grid network and to instances for long-distance train networks. As one application we study the impact of different strategies to improve the robustness of timetables by insertion of supplement times. We also show that the framework can be used to optimize waiting strategies in delay management.
Cite as

Markus Friedrich, Matthias Müller-Hannemann, Ralf Rückert, Alexander Schiewe, and Anita Schöbel. Robustness as a Third Dimension for Evaluating Public Transport Plans. In 18th Workshop on Algorithmic Approaches for Transportation Modelling, Optimization, and Systems (ATMOS 2018). Open Access Series in Informatics (OASIcs), Volume 65, pp. 4:1-4:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{friedrich_et_al:OASIcs.ATMOS.2018.4,
  author =	{Friedrich, Markus and M\"{u}ller-Hannemann, Matthias and R\"{u}ckert, Ralf and Schiewe, Alexander and Sch\"{o}bel, Anita},
  title =	{{Robustness as a Third Dimension for Evaluating Public Transport Plans}},
  booktitle =	{18th Workshop on Algorithmic Approaches for Transportation Modelling, Optimization, and Systems (ATMOS 2018)},
  pages =	{4:1--4:17},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-096-5},
  ISSN =	{2190-6807},
  year =	{2018},
  volume =	{65},
  editor =	{Bornd\"{o}rfer, Ralf and Storandt, Sabine},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/OASIcs.ATMOS.2018.4},
  URN =		{urn:nbn:de:0030-drops-97097},
  doi =		{10.4230/OASIcs.ATMOS.2018.4},
  annote =	{Keywords: robustness, timetabling, vehicle schedules, delays}
}
Document
DOI: 10.4230/OASIcs.ATMOS.2017.6
Robustness Tests for Public Transport Planning

Authors: Markus Friedrich, Matthias Müller-Hannemann, Ralf Rückert, Alexander Schiewe, and Anita Schöbel

Published in: OASIcs, Volume 59, 17th Workshop on Algorithmic Approaches for Transportation Modelling, Optimization, and Systems (ATMOS 2017)

Abstract
The classical planning process in public transport planning focuses on the two criteria operating costs and quality for passengers. Quality mostly considers quantities like average travel time and number of transfers. Since public transport often suffers from delays caused by random disturbances, we are interested in adding a third dimension: robustness. We propose passenger-oriented robustness indicators for public transport networks and timetables. These robustness indicators are evaluated for several public transport plans which have been created for an artificial urban network with the same demand. The study shows that these indicators are suitable to measure the robustness of a line plan and a timetable. We explore different trade-offs between operating costs, quality (average travel time of passengers), and robustness against delays. Our results show that the proposed robustness indicators give reasonable results.
Cite as

Markus Friedrich, Matthias Müller-Hannemann, Ralf Rückert, Alexander Schiewe, and Anita Schöbel. Robustness Tests for Public Transport Planning. In 17th Workshop on Algorithmic Approaches for Transportation Modelling, Optimization, and Systems (ATMOS 2017). Open Access Series in Informatics (OASIcs), Volume 59, pp. 6:1-6:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{friedrich_et_al:OASIcs.ATMOS.2017.6,
  author =	{Friedrich, Markus and M\"{u}ller-Hannemann, Matthias and R\"{u}ckert, Ralf and Schiewe, Alexander and Sch\"{o}bel, Anita},
  title =	{{Robustness Tests for Public Transport Planning}},
  booktitle =	{17th Workshop on Algorithmic Approaches for Transportation Modelling, Optimization, and Systems (ATMOS 2017)},
  pages =	{6:1--6:16},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-042-2},
  ISSN =	{2190-6807},
  year =	{2017},
  volume =	{59},
  editor =	{D'Angelo, Gianlorenzo and Dollevoet, Twan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/OASIcs.ATMOS.2017.6},
  URN =		{urn:nbn:de:0030-drops-78904},
  doi =		{10.4230/OASIcs.ATMOS.2017.6},
  annote =	{Keywords: robustness measure, timetabling, line planning, delays, passenger-orientation}
}
Document
Complete Volume
DOI: 10.4230/DFU.Vol3.11041
DFU, Volume 3, Multimodal Music Processing, Complete Volume

Authors: Meinard Müller, Masataka Goto, and Markus Schedl

Published in: Dagstuhl Follow-Ups, Volume 3, Multimodal Music Processing (2012)

Abstract
DFU, Volume 3, Multimodal Music Processing, Complete Volume
Cite as

Multimodal Music Processing. Dagstuhl Follow-Ups, Volume 3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)

Copy BibTex To Clipboard

@Collection{DFU.Vol3.11041,
  title =	{{DFU, Volume 3, Multimodal Music Processing, Complete Volume}},
  booktitle =	{Multimodal Music Processing},
  series =	{Dagstuhl Follow-Ups},
  ISBN =	{978-3-939897-37-8},
  ISSN =	{1868-8977},
  year =	{2012},
  volume =	{3},
  editor =	{M\"{u}ller, Meinard and Goto, Masataka and Schedl, Markus},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DFU.Vol3.11041},
  URN =		{urn:nbn:de:0030-drops-36023},
  doi =		{10.4230/DFU.Vol3.11041},
  annote =	{Keywords: Sound and Music Computing, Arts and Humanities–Music, Multimedia Information Systems}
}
Document
DOI: 10.4230/DFU.Vol3.11041.i
Frontmatter, Table of Contents, Preface, List of Authors

Authors: Meinard Müller, Masataka Goto, and Markus Schedl

Published in: Dagstuhl Follow-Ups, Volume 3, Multimodal Music Processing (2012)

Abstract
Frontmatter, Table of Contents, Preface, List of Authors
Cite as

Multimodal Music Processing. Dagstuhl Follow-Ups, Volume 3, pp. 0:i-0:xii, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)

Copy BibTex To Clipboard

@InCollection{muller_et_al:DFU.Vol3.11041.i,
  author =	{M\"{u}ller, Meinard and Goto, Masataka and Schedl, Markus},
  title =	{{Frontmatter, Table of Contents, Preface, List of Authors}},
  booktitle =	{Multimodal Music Processing},
  pages =	{0:i--0:xii},
  series =	{Dagstuhl Follow-Ups},
  ISBN =	{978-3-939897-37-8},
  ISSN =	{1868-8977},
  year =	{2012},
  volume =	{3},
  editor =	{M\"{u}ller, Meinard and Goto, Masataka and Schedl, Markus},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DFU.Vol3.11041.i},
  URN =		{urn:nbn:de:0030-drops-34621},
  doi =		{10.4230/DFU.Vol3.11041.i},
  annote =	{Keywords: Frontmatter, Table of Contents, Preface, List of Authors}
}
Document
DOI: 10.4230/DFU.Vol3.11041.1
Linking Sheet Music and Audio - Challenges and New Approaches

Authors: Verena Thomas, Christian Fremerey, Meinard Müller, and Michael Clausen

Published in: Dagstuhl Follow-Ups, Volume 3, Multimodal Music Processing (2012)

Abstract
Score and audio files are the two most important ways to represent, convey, record, store, and experience music. While score describes a piece of music on an abstract level using symbols such as notes, keys, and measures, audio files allow for reproducing a specific acoustic realization of the piece. Each of these representations reflects different facets of music yielding insights into aspects ranging from structural elements (e.g., motives, themes, musical form) to specific performance aspects (e.g., artistic shaping, sound). Therefore, the simultaneous access to score and audio representations is of great importance. In this paper, we address the problem of automatically generating musically relevant linking structures between the various data sources that are available for a given piece of music. In particular, we discuss the task of sheet music-audio synchronization with the aim to link regions in images of scanned scores to musically corresponding sections in an audio recording of the same piece. Such linking structures form the basis for novel interfaces that allow users to access and explore multimodal sources of music within a single framework. As our main contributions, we give an overview of the state-of-the-art for this kind of synchronization task, we present some novel approaches, and indicate future research directions. In particular, we address problems that arise in the presence of structural differences and discuss challenges when applying optical music recognition to complex orchestral scores. Finally, potential applications of the synchronization results are presented.
Cite as

Verena Thomas, Christian Fremerey, Meinard Müller, and Michael Clausen. Linking Sheet Music and Audio - Challenges and New Approaches. In Multimodal Music Processing. Dagstuhl Follow-Ups, Volume 3, pp. 1-22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)

Copy BibTex To Clipboard

@InCollection{thomas_et_al:DFU.Vol3.11041.1,
  author =	{Thomas, Verena and Fremerey, Christian and M\"{u}ller, Meinard and Clausen, Michael},
  title =	{{Linking Sheet Music and Audio - Challenges and New Approaches}},
  booktitle =	{Multimodal Music Processing},
  pages =	{1--22},
  series =	{Dagstuhl Follow-Ups},
  ISBN =	{978-3-939897-37-8},
  ISSN =	{1868-8977},
  year =	{2012},
  volume =	{3},
  editor =	{M\"{u}ller, Meinard and Goto, Masataka and Schedl, Markus},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DFU.Vol3.11041.1},
  URN =		{urn:nbn:de:0030-drops-34637},
  doi =		{10.4230/DFU.Vol3.11041.1},
  annote =	{Keywords: Music signals, audio, sheet music, music synchronization, alignment, optical music recognition, user interfaces, multimodality}
}
Document
DOI: 10.4230/DFU.Vol3.11041.53
A Cross-Version Approach for Harmonic Analysis of Music Recordings

Authors: Verena Konz and Meinard Müller

Published in: Dagstuhl Follow-Ups, Volume 3, Multimodal Music Processing (2012)

Abstract
The automated extraction of chord labels from audio recordings is a central task in music information retrieval. Here, the chord labeling is typically performed on a specific audio version of a piece of music, produced under certain recording conditions, played on specific instruments and characterized by individual styles of the musicians. As a consequence, the obtained chord labeling results are strongly influenced by version-dependent characteristics. In this chapter, we show that analyzing the harmonic properties of several audio versions synchronously stabilizes the chord labeling result in the sense that inconsistencies indicate version-dependent characteristics, whereas consistencies across several versions indicate harmonically stable passages in the piece of music. In particular, we show that consistently labeled passages often correspond to correctly labeled passages. Our experiments show that the cross-version labeling procedure significantly increases the precision of the result while keeping the recall at a relatively high level. Furthermore, we introduce a powerful visualization which reveals the harmonically stable passages on a musical time axis specified in bars. Finally, we demonstrate how this visualization facilitates a better understanding of classification errors and may be used by music experts as a helpful tool for exploring harmonic structures.
Cite as

Verena Konz and Meinard Müller. A Cross-Version Approach for Harmonic Analysis of Music Recordings. In Multimodal Music Processing. Dagstuhl Follow-Ups, Volume 3, pp. 53-72, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)

Copy BibTex To Clipboard

@InCollection{konz_et_al:DFU.Vol3.11041.53,
  author =	{Konz, Verena and M\"{u}ller, Meinard},
  title =	{{A Cross-Version Approach for Harmonic Analysis of Music Recordings}},
  booktitle =	{Multimodal Music Processing},
  pages =	{53--72},
  series =	{Dagstuhl Follow-Ups},
  ISBN =	{978-3-939897-37-8},
  ISSN =	{1868-8977},
  year =	{2012},
  volume =	{3},
  editor =	{M\"{u}ller, Meinard and Goto, Masataka and Schedl, Markus},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DFU.Vol3.11041.53},
  URN =		{urn:nbn:de:0030-drops-34665},
  doi =		{10.4230/DFU.Vol3.11041.53},
  annote =	{Keywords: Harmonic analysis, chord labeling, audio, music, music synchronization, audio alignment}
}
Document
DOI: 10.4230/DFU.Vol3.11041.73
Score-Informed Source Separation for Music Signals

Authors: Sebastian Ewert and Meinard Müller

Published in: Dagstuhl Follow-Ups, Volume 3, Multimodal Music Processing (2012)

Abstract
In recent years, the processing of audio recordings by exploiting additional musical knowledge has turned out to be a promising research direction. In particular, additional note information as specified by a musical score or a MIDI file has been employed to support various audio processing tasks such as source separation, audio parameterization, performance analysis, or instrument equalization. In this contribution, we provide an overview of approaches for score-informed source separation and illustrate their potential by discussing innovative applications and interfaces. Additionally, to illustrate some basic principles behind these approaches, we demonstrate how score information can be integrated into the well-known non-negative matrix factorization (NMF) framework. Finally, we compare this approach to advanced methods based on parametric models.
Cite as

Sebastian Ewert and Meinard Müller. Score-Informed Source Separation for Music Signals. In Multimodal Music Processing. Dagstuhl Follow-Ups, Volume 3, pp. 73-94, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)

Copy BibTex To Clipboard

@InCollection{ewert_et_al:DFU.Vol3.11041.73,
  author =	{Ewert, Sebastian and M\"{u}ller, Meinard},
  title =	{{Score-Informed Source Separation for Music Signals}},
  booktitle =	{Multimodal Music Processing},
  pages =	{73--94},
  series =	{Dagstuhl Follow-Ups},
  ISBN =	{978-3-939897-37-8},
  ISSN =	{1868-8977},
  year =	{2012},
  volume =	{3},
  editor =	{M\"{u}ller, Meinard and Goto, Masataka and Schedl, Markus},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DFU.Vol3.11041.73},
  URN =		{urn:nbn:de:0030-drops-34670},
  doi =		{10.4230/DFU.Vol3.11041.73},
  annote =	{Keywords: Audio processing, music signals, source separation, musical score, alignment, music synchronization, non-negative matrix factorization, parametric mod}
}
Document
DOI: 10.4230/DFU.Vol3.11041.157
Audio Content-Based Music Retrieval

Authors: Peter Grosche, Meinard Müller, and Joan Serrà

Published in: Dagstuhl Follow-Ups, Volume 3, Multimodal Music Processing (2012)

Abstract
The rapidly growing corpus of digital audio material requires novel retrieval strategies for exploring large music collections. Traditional retrieval strategies rely on metadata that describe the actual audio content in words. In the case that such textual descriptions are not available, one requires content-based retrieval strategies which only utilize the raw audio material. In this contribution, we discuss content-based retrieval strategies that follow the query-by-example paradigm: given an audio query, the task is to retrieve all documents that are somehow similar or related to the query from a music collection. Such strategies can be loosely classified according to their "specificity", which refers to the degree of similarity between the query and the database documents. Here, high specificity refers to a strict notion of similarity, whereas low specificity to a rather vague one. Furthermore, we introduce a second classification principle based on "granularity", where one distinguishes between fragment-level and document-level retrieval. Using a classification scheme based on specificity and granularity, we identify various classes of retrieval scenarios, which comprise "audio identification", "audio matching", and "version identification". For these three important classes, we give an overview of representative state-of-the-art approaches, which also illustrate the sometimes subtle but crucial differences between the retrieval scenarios. Finally, we give an outlook on a user-oriented retrieval system, which combines the various retrieval strategies in a unified framework.
Cite as

Peter Grosche, Meinard Müller, and Joan Serrà. Audio Content-Based Music Retrieval. In Multimodal Music Processing. Dagstuhl Follow-Ups, Volume 3, pp. 157-174, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)

Copy BibTex To Clipboard

@InCollection{grosche_et_al:DFU.Vol3.11041.157,
  author =	{Grosche, Peter and M\"{u}ller, Meinard and Serr\`{a}, Joan},
  title =	{{Audio Content-Based Music Retrieval}},
  booktitle =	{Multimodal Music Processing},
  pages =	{157--174},
  series =	{Dagstuhl Follow-Ups},
  ISBN =	{978-3-939897-37-8},
  ISSN =	{1868-8977},
  year =	{2012},
  volume =	{3},
  editor =	{M\"{u}ller, Meinard and Goto, Masataka and Schedl, Markus},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DFU.Vol3.11041.157},
  URN =		{urn:nbn:de:0030-drops-34711},
  doi =		{10.4230/DFU.Vol3.11041.157},
  annote =	{Keywords: music retrieval, content-based, query-by-example, audio identification, audio matching, cover song identification}
}
Document
DOI: 10.4230/DFU.Vol3.11041.175
Data-Driven Sound Track Generation

Authors: Meinard Müller and Jonathan Driedger

Published in: Dagstuhl Follow-Ups, Volume 3, Multimodal Music Processing (2012)

Abstract
Background music is often used to generate a specific atmosphere or to draw our attention to specific events. For example in movies or computer games it is often the accompanying music that conveys the emotional state of a scene and plays an important role for immersing the viewer or player into the virtual environment. In view of home-made videos, slide shows, and other consumer-generated visual media streams, there is a need for computer-assisted tools that allow users to generate aesthetically appealing music tracks in an easy and intuitive way. In this contribution, we consider a data-driven scenario where the musical raw material is given in form of a database containing a variety of audio recordings. Then, for a given visual media stream, the task consists in identifying, manipulating, overlaying, concatenating, and blending suitable music clips to generate a music stream that satisfies certain constraints imposed by the visual data stream and by user specifications. It is our main goal to give an overview of various content-based music processing and retrieval techniques that become important in data-driven sound track generation. In particular, we sketch a general pipeline that highlights how the various techniques act together and come into play when generating musically plausible transitions between subsequent music clips.
Cite as

Meinard Müller and Jonathan Driedger. Data-Driven Sound Track Generation. In Multimodal Music Processing. Dagstuhl Follow-Ups, Volume 3, pp. 175-194, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)

Copy BibTex To Clipboard

@InCollection{muller_et_al:DFU.Vol3.11041.175,
  author =	{M\"{u}ller, Meinard and Driedger, Jonathan},
  title =	{{Data-Driven Sound Track Generation}},
  booktitle =	{Multimodal Music Processing},
  pages =	{175--194},
  series =	{Dagstuhl Follow-Ups},
  ISBN =	{978-3-939897-37-8},
  ISSN =	{1868-8977},
  year =	{2012},
  volume =	{3},
  editor =	{M\"{u}ller, Meinard and Goto, Masataka and Schedl, Markus},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DFU.Vol3.11041.175},
  URN =		{urn:nbn:de:0030-drops-34725},
  doi =		{10.4230/DFU.Vol3.11041.175},
  annote =	{Keywords: Sound track, content-based retrieval, audio matching, time-scale modification, warping, tempo, beat tracking, harmony}
}
Document
DOI: 10.4230/DagSemProc.09461.4
Solving hard instances in QF-BV combining Boolean reasoning with computer algebra

Authors: Markus Wedler, Evgeny Pavlenko, Alexander Dreyer, Frank Seelisch, Dominik Stoffel, Gert-Martin Greuel, and Wolfgang Kunz

Published in: Dagstuhl Seminar Proceedings, Volume 9461, Algorithms and Applications for Next Generation SAT Solvers (2010)

Abstract
This paper describes our new satisfyability (SAT) modulo theory (SMT) solver STABLE for the quantifier-free logic over fixed size bit vectors. Our main application domain is formal verification of system-on-chip (SoC) modules designed for complex computational tasks, for example, in signal processing applications. Ensuring proper functional behavior for such modules, including arithmetic correctness of the data paths, is considered a very difficult problem. We show how methods from computer algebra can be integrated into an SMT solver such that instances can be handled where the arithmetic problem parts are specified mixing various levels of abstraction from the plain gate level for small highly optimized components up to the pure word level used in high-level specifications. If the arithmetic problem parts include multiplications such mixed problem descriptions quickly drive current SMT solvers towards their capacity limits. High performance data paths are often designed at a level of abstraction that we call the arithmetic bit level (ABL). We show how ABL information, if available in an SMT instance, can be used to transform the decision problem into an equivalent set of variety subset problems. These problems can be solved efficiently with techniques from computer algebra based on Gröbner basis theory over finite rings Z/2^n . Sometimes, instances contain problem parts at a level below the ABL using gate-level operations. These problem parts, e.g., originate from custom-designed arithmetic components that are highly optimized using the gate-level constructs of a hardware description language (HDL). For such cases we integrate a local ABL extraction technique based on local Reed-Muller forms.
Cite as

Markus Wedler, Evgeny Pavlenko, Alexander Dreyer, Frank Seelisch, Dominik Stoffel, Gert-Martin Greuel, and Wolfgang Kunz. Solving hard instances in QF-BV combining Boolean reasoning with computer algebra. In Algorithms and Applications for Next Generation SAT Solvers. Dagstuhl Seminar Proceedings, Volume 9461, pp. 1-20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)

Copy BibTex To Clipboard

@InProceedings{wedler_et_al:DagSemProc.09461.4,
  author =	{Wedler, Markus and Pavlenko, Evgeny and Dreyer, Alexander and Seelisch, Frank and Stoffel, Dominik and Greuel, Gert-Martin and Kunz, Wolfgang},
  title =	{{Solving hard instances in QF-BV combining Boolean reasoning with computer algebra}},
  booktitle =	{Algorithms and Applications for Next Generation SAT Solvers},
  pages =	{1--20},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2010},
  volume =	{9461},
  editor =	{Bernd Becker and Valeria Bertacoo and Rolf Drechsler and Masahiro Fujita},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagSemProc.09461.4},
  URN =		{urn:nbn:de:0030-drops-25096},
  doi =		{10.4230/DagSemProc.09461.4},
  annote =	{Keywords: SAT modulo Theory, Quantifier Free logic over fixed sized bitvectors; Computer Algebra}
}
Document
DOI: 10.4230/DagSemProc.07171.1
07171 Abstracts Collection – Visual Computing – Convergence of Computer Graphics and Computer Vision

Authors: Markus Gross, Heinrich Müller, Hans-Peter Seidel, and Harry Shum

Published in: Dagstuhl Seminar Proceedings, Volume 7171, Visual Computing - Convergence of Computer Graphics and Computer Vision (2008)

Abstract
From 22.04. to 27.04.2007, the Dagstuhl Seminar 07171 ``Visual Computing - Convergence of Computer Graphics and Computer Vision'' was held in the International Conference and Research Center (IBFI), Schloss Dagstuhl. During the seminar, several participants presented their current research, and ongoing work and open problems were discussed. Abstracts of the presentations given during the seminar as well as abstracts of seminar results and ideas are put together in this paper. The first section describes the seminar topics and goals in general. Links to extended abstracts or full papers are provided, if available.
Cite as

Markus Gross, Heinrich Müller, Hans-Peter Seidel, and Harry Shum. 07171 Abstracts Collection – Visual Computing – Convergence of Computer Graphics and Computer Vision. In Visual Computing - Convergence of Computer Graphics and Computer Vision. Dagstuhl Seminar Proceedings, Volume 7171, pp. 1-18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2008)

Copy BibTex To Clipboard

@InProceedings{gross_et_al:DagSemProc.07171.1,
  author =	{Gross, Markus and M\"{u}ller, Heinrich and Seidel, Hans-Peter and Shum, Harry},
  title =	{{07171 Abstracts Collection – Visual Computing – Convergence of Computer Graphics and Computer Vision}},
  booktitle =	{Visual Computing - Convergence of Computer Graphics and Computer Vision},
  pages =	{1--18},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2008},
  volume =	{7171},
  editor =	{Markus Gross and Heinrich M\"{u}ller and Hans-Peter Seidel and Harry Shum},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagSemProc.07171.1},
  URN =		{urn:nbn:de:0030-drops-15044},
  doi =		{10.4230/DagSemProc.07171.1},
  annote =	{Keywords: Image- and video-based modeling and rendering, perception-guided modeling and rendering, texture synthesis, scattering and reflectance measurement rendering, capturing reality (appearance, motion) from images, 3D acquisition and display, 3D reconstruction, image and model compression, computation}
}
  • Refine by Author
  • 7 Müller, Meinard
  • 4 Gross, Markus
  • 4 Müller, Heinrich
  • 4 Müller-Olm, Markus
  • 4 Seidel, Hans-Peter
  • Show More...

  • Refine by Classification
  • 1 Applied computing → Transportation
  • 1 Mathematics of computing → Graph algorithms
  • 1 Mathematics of computing → Probabilistic inference problems
  • 1 Theory of computation → Algebraic semantics
  • 1 Theory of computation → Automata over infinite objects
  • Show More...

  • Refine by Keyword
  • 3 music synchronization
  • 2 3D acquisition and display
  • 2 3D reconstruction
  • 2 Image- and video-based modeling and rendering
  • 2 alignment
  • Show More...

  • Refine by Type
  • 24 document
  • 1 volume

  • Refine by Publication Year
  • 8 2012
  • 6 2006
  • 2 2003
  • 2 2008
  • 1 1998
  • 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