16 Search Results for "Müller, Daniel"

Document
DOI: 10.4230/LIPIcs.ITP.2024.23
A Generalised Union of Rely-Guarantee and Separation Logic Using Permission Algebras

Authors: Vincent Jackson, Toby Murray, and Christine Rizkallah

Published in: LIPIcs, Volume 309, 15th International Conference on Interactive Theorem Proving (ITP 2024)

Abstract
This paper describes GenRGSep, an Isabelle/HOL library for the development of RGSep logics using a general algebraic state model. In particular, we develop an algebraic state models based on resource algebras that assume neither the presence of unit resources or the cancellativity law. If a new resource model is required, its components need only be proven an instance of a permission algebra, and then they can be composed together using tuples and functions. The proof of soundness is performed by Vafeiadis' operational soundness method. This method was originally formulated with respect to a concrete heap model. This paper adapts it to account for the absence of both units as well as the cancellativity law.
Cite as

Vincent Jackson, Toby Murray, and Christine Rizkallah. A Generalised Union of Rely-Guarantee and Separation Logic Using Permission Algebras. In 15th International Conference on Interactive Theorem Proving (ITP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 309, pp. 23:1-23:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{jackson_et_al:LIPIcs.ITP.2024.23,
  author =	{Jackson, Vincent and Murray, Toby and Rizkallah, Christine},
  title =	{{A Generalised Union of Rely-Guarantee and Separation Logic Using Permission Algebras}},
  booktitle =	{15th International Conference on Interactive Theorem Proving (ITP 2024)},
  pages =	{23:1--23:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-337-9},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{309},
  editor =	{Bertot, Yves and Kutsia, Temur and Norrish, Michael},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2024.23},
  URN =		{urn:nbn:de:0030-drops-207510},
  doi =		{10.4230/LIPIcs.ITP.2024.23},
  annote =	{Keywords: verification, concurrency, rely-guarantee, separation logic, resource algebras}
}
Document
DOI: 10.4230/LIPIcs.CP.2024.19
An Efficient Local Search Solver for Mixed Integer Programming

Authors: Peng Lin, Mengchuan Zou, and Shaowei Cai

Published in: LIPIcs, Volume 307, 30th International Conference on Principles and Practice of Constraint Programming (CP 2024)

Abstract
Mixed integer programming (MIP) is a fundamental model in operations research. Local search is a powerful method for solving hard problems, but the development of local search solvers for MIP still needs to be explored. This work develops an efficient local search solver for solving MIP, called Local-MIP. We propose two new operators for MIP to adaptively modify variables for optimizing the objective function and satisfying constraints, respectively. Furthermore, we design a new weighting scheme to dynamically balance the priority between the objective function and each constraint, and propose a two-level scoring function structure to hierarchically guide the search for high-quality feasible solutions. Experiments are conducted on seven public benchmarks to compare Local-MIP with state-of-the-art MIP solvers, which demonstrate that Local-MIP significantly outperforms CPLEX, HiGHS, SCIP and Feasibility Jump, and is competitive with the most powerful commercial solver Gurobi. Moreover, Local-MIP establishes 4 new records for MIPLIB open instances.
Cite as

Peng Lin, Mengchuan Zou, and Shaowei Cai. An Efficient Local Search Solver for Mixed Integer Programming. In 30th International Conference on Principles and Practice of Constraint Programming (CP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 307, pp. 19:1-19:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{lin_et_al:LIPIcs.CP.2024.19,
  author =	{Lin, Peng and Zou, Mengchuan and Cai, Shaowei},
  title =	{{An Efficient Local Search Solver for Mixed Integer Programming}},
  booktitle =	{30th International Conference on Principles and Practice of Constraint Programming (CP 2024)},
  pages =	{19:1--19:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-336-2},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{307},
  editor =	{Shaw, Paul},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2024.19},
  URN =		{urn:nbn:de:0030-drops-207041},
  doi =		{10.4230/LIPIcs.CP.2024.19},
  annote =	{Keywords: Mixed Integer Programming, Local Search, Operator, Scoring Function}
}
Document
DOI: 10.4230/LIPIcs.CP.2024.10
Anytime Weighted Model Counting with Approximation Guarantees for Probabilistic Inference

Authors: Alexandre Dubray, Pierre Schaus, and Siegfried Nijssen

Published in: LIPIcs, Volume 307, 30th International Conference on Principles and Practice of Constraint Programming (CP 2024)

Abstract
Weighted model counting (WMC) plays a central role in probabilistic reasoning. Given that this problem is #P-hard, harder instances can generally only be addressed using approximate techniques based on sampling, which provide statistical convergence guarantees: the longer a sampling process runs, the more accurate the WMC is likely to be. In this work, we propose a deterministic search-based approach that can also be stopped at any time and provides hard lower- and upper-bound guarantees on the true WMC. This approach uses a value heuristic that guides exploration first towards models with a high weight and leverages Limited Discrepancy Search to make the bounds converge faster. The validity, scalability, and convergence of our approach are tested and compared with state-of-the-art baseline methods on the problem of computing marginal probabilities in Bayesian networks and reliability estimation in probabilistic graphs.
Cite as

Alexandre Dubray, Pierre Schaus, and Siegfried Nijssen. Anytime Weighted Model Counting with Approximation Guarantees for Probabilistic Inference. In 30th International Conference on Principles and Practice of Constraint Programming (CP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 307, pp. 10:1-10:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{dubray_et_al:LIPIcs.CP.2024.10,
  author =	{Dubray, Alexandre and Schaus, Pierre and Nijssen, Siegfried},
  title =	{{Anytime Weighted Model Counting with Approximation Guarantees for Probabilistic Inference}},
  booktitle =	{30th International Conference on Principles and Practice of Constraint Programming (CP 2024)},
  pages =	{10:1--10:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-336-2},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{307},
  editor =	{Shaw, Paul},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2024.10},
  URN =		{urn:nbn:de:0030-drops-206956},
  doi =		{10.4230/LIPIcs.CP.2024.10},
  annote =	{Keywords: Projected Weighted Model Counting, Limited Discrepancy Search, Approximate Method, Probabilistic Inference}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2024.12
Generalizing Roberts' Characterization of Unit Interval Graphs

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

Published in: LIPIcs, Volume 306, 49th International Symposium on Mathematical Foundations of Computer Science (MFCS 2024)

Abstract
For any natural number d, a graph G is a (disjoint) d-interval graph if it is the intersection graph of (disjoint) d-intervals, the union of d (disjoint) intervals on the real line. Two important subclasses of d-interval graphs are unit and balanced d-interval graphs (where every interval has unit length or all the intervals associated to a same vertex have the same length, respectively). A celebrated result by Roberts gives a simple characterization of unit interval graphs being exactly claw-free interval graphs. Here, we study the generalization of this characterization for d-interval graphs. In particular, we prove that for any d ⩾ 2, if G is a K_{1,2d+1}-free interval graph, then G is a unit d-interval graph. However, somehow surprisingly, under the same assumptions, G is not always a disjoint unit d-interval graph. This implies that the class of disjoint unit d-interval graphs is strictly included in the class of unit d-interval graphs. Finally, we study the relationships between the classes obtained under disjoint and non-disjoint d-intervals in the balanced case and show that the classes of disjoint balanced 2-intervals and balanced 2-intervals coincide, but this is no longer true for d > 2.
Cite as

Virginia Ardévol Martínez, Romeo Rizzi, Abdallah Saffidine, Florian Sikora, and Stéphane Vialette. Generalizing Roberts' Characterization of Unit Interval Graphs. In 49th International Symposium on Mathematical Foundations of Computer Science (MFCS 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 306, pp. 12:1-12:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{ardevolmartinez_et_al:LIPIcs.MFCS.2024.12,
  author =	{Ard\'{e}vol Mart{\'\i}nez, Virginia and Rizzi, Romeo and Saffidine, Abdallah and Sikora, Florian and Vialette, St\'{e}phane},
  title =	{{Generalizing Roberts' Characterization of Unit Interval Graphs}},
  booktitle =	{49th International Symposium on Mathematical Foundations of Computer Science (MFCS 2024)},
  pages =	{12:1--12:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-335-5},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{306},
  editor =	{Kr\'{a}lovi\v{c}, Rastislav and Ku\v{c}era, Anton{\'\i}n},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2024.12},
  URN =		{urn:nbn:de:0030-drops-205687},
  doi =		{10.4230/LIPIcs.MFCS.2024.12},
  annote =	{Keywords: Interval graphs, Multiple Interval Graphs, Unit Interval Graphs, Characterization}
}
Document
DOI: 10.4230/OASIcs.FMBC.2024.2
Formal Specification of the Cardano Blockchain Ledger, Mechanized in Agda

Authors: Andre Knispel, Orestis Melkonian, James Chapman, Alasdair Hill, Joosep Jääger, William DeMeo, and Ulf Norell

Published in: OASIcs, Volume 118, 5th International Workshop on Formal Methods for Blockchains (FMBC 2024)

Abstract
Blockchain systems comprise critical software that handle substantial monetary funds, rendering them excellent candidates for formal verification. One of their core components is the underlying ledger that does all the accounting: keeping track of transactions and their validity, etc. Unfortunately, previous theoretical studies are typically confined to an idealized setting, while specifications for real implementations are scarce; either the functionality is directly implemented without a proper specification, or at best an informal specification is written on paper. The present work expands beyond prior meta-theoretical investigations of the EUTxO model to encompass the full scale of the Cardano blockchain: our formal specification describes a hierarchy of modular transitions that covers all the intricacies of a realistic blockchain, such as fully expressive smart contracts and decentralized governance. It is mechanized in a proof assistant, thus enjoys a higher standard of rigor: type-checking prevents minor oversights that were frequent in previous informal approaches; key meta-theoretical properties can now be formally proven; it is an executable specification against which the implementation in production is being tested for conformance; and it provides firm foundations for smart contract verification. Apart from a safety net to keep us in check, the formalization also provides a guideline for the ledger design: one informs the other in a symbiotic way, especially in the case of state-of-the-art features like decentralized governance, which is an emerging sub-field of blockchain research that however mandates a more exploratory approach. All the results presented in this paper have been mechanized in the Agda proof assistant and are publicly available. In fact, this document is itself a literate Agda script and all rendered code has been successfully type-checked.
Cite as

Andre Knispel, Orestis Melkonian, James Chapman, Alasdair Hill, Joosep Jääger, William DeMeo, and Ulf Norell. Formal Specification of the Cardano Blockchain Ledger, Mechanized in Agda. In 5th International Workshop on Formal Methods for Blockchains (FMBC 2024). Open Access Series in Informatics (OASIcs), Volume 118, pp. 2:1-2:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{knispel_et_al:OASIcs.FMBC.2024.2,
  author =	{Knispel, Andre and Melkonian, Orestis and Chapman, James and Hill, Alasdair and J\"{a}\"{a}ger, Joosep and DeMeo, William and Norell, Ulf},
  title =	{{Formal Specification of the Cardano Blockchain Ledger, Mechanized in Agda}},
  booktitle =	{5th International Workshop on Formal Methods for Blockchains (FMBC 2024)},
  pages =	{2:1--2:18},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-317-1},
  ISSN =	{2190-6807},
  year =	{2024},
  volume =	{118},
  editor =	{Bernardo, Bruno and Marmsoler, Diego},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.FMBC.2024.2},
  URN =		{urn:nbn:de:0030-drops-198673},
  doi =		{10.4230/OASIcs.FMBC.2024.2},
  annote =	{Keywords: blockchain, distributed ledgers, UTxO, Cardano, formal verification, Agda}
}
Document
DOI: 10.4230/OASIcs.iPMVM.2020.7
Influence of Flank Face Structuring on Cooling, Tool Lifetime and Borehole Quality When Drilling Inconel 718: Physical Simulations and Experimental Validation

Authors: Daniel Müller, Benjamin Kirsch, and Jan C. Aurich

Published in: OASIcs, Volume 89, 2nd International Conference of the DFG International Research Training Group 2057 – Physical Modeling for Virtual Manufacturing (iPMVM 2020)

Abstract
When drilling difficult-to-cut materials such as Inconel 718, the drills are exposed to high thermomechanical loads. Due to the low thermal conductivity of the workpiece material, a large amount of the generated heat has to be dissipated by the metal working fluid (MWF). However, the cutting zone is located inside the workpiece, which makes it challenging to provide sufficient MWF to the cutting zone. To solve this, drills with internal cooling channels are commonly used. In this work, the influence of differently structured flank faces on cooling efficiency, tool life, process forces and borehole quality is investigated. The influence of the structures on the cooling was investigated by Computational-Fluid-Dynamics (CFD) simulations. These simulations allow a detailed analysis of the flow conditions inside the borehole and showed that the structuring improved flow conditions, especially near the thermally highly loaded main cutting edge. The improved flow conditions resulted in an extension of the tool life by up to 22 % compared to unstructured drills in experimental investigations.
Cite as

Daniel Müller, Benjamin Kirsch, and Jan C. Aurich. Influence of Flank Face Structuring on Cooling, Tool Lifetime and Borehole Quality When Drilling Inconel 718: Physical Simulations and Experimental Validation. In 2nd International Conference of the DFG International Research Training Group 2057 – Physical Modeling for Virtual Manufacturing (iPMVM 2020). Open Access Series in Informatics (OASIcs), Volume 89, pp. 7:1-7:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{muller_et_al:OASIcs.iPMVM.2020.7,
  author =	{M\"{u}ller, Daniel and Kirsch, Benjamin and Aurich, Jan C.},
  title =	{{Influence of Flank Face Structuring on Cooling, Tool Lifetime and Borehole Quality When Drilling Inconel 718: Physical Simulations and Experimental Validation}},
  booktitle =	{2nd International Conference of the DFG International Research Training Group 2057 – Physical Modeling for Virtual Manufacturing (iPMVM 2020)},
  pages =	{7:1--7:17},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-183-2},
  ISSN =	{2190-6807},
  year =	{2021},
  volume =	{89},
  editor =	{Garth, Christoph and Aurich, Jan C. and Linke, Barbara and M\"{u}ller, Ralf and Ravani, Bahram and Weber, Gunther H. and Kirsch, Benjamin},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.iPMVM.2020.7},
  URN =		{urn:nbn:de:0030-drops-137562},
  doi =		{10.4230/OASIcs.iPMVM.2020.7},
  annote =	{Keywords: drilling, cooling, CFD}
}
Document
DOI: 10.4230/LIPIcs.AofA.2018.23
Refined Asymptotics for the Number of Leaves of Random Point Quadtrees

Authors: Michael Fuchs, Noela S. Müller, and Henning Sulzbach

Published in: LIPIcs, Volume 110, 29th International Conference on Probabilistic, Combinatorial and Asymptotic Methods for the Analysis of Algorithms (AofA 2018)

Abstract
In the early 2000s, several phase change results from distributional convergence to distributional non-convergence have been obtained for shape parameters of random discrete structures. Recently, for those random structures which admit a natural martingale process, these results have been considerably improved by obtaining refined asymptotics for the limit behavior. In this work, we propose a new approach which is also applicable to random discrete structures which do not admit a natural martingale process. As an example, we obtain refined asymptotics for the number of leaves in random point quadtrees. More applications, for example to shape parameters in generalized m-ary search trees and random gridtrees, will be discussed in the journal version of this extended abstract.
Cite as

Michael Fuchs, Noela S. Müller, and Henning Sulzbach. Refined Asymptotics for the Number of Leaves of Random Point Quadtrees. In 29th International Conference on Probabilistic, Combinatorial and Asymptotic Methods for the Analysis of Algorithms (AofA 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 110, pp. 23:1-23:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{fuchs_et_al:LIPIcs.AofA.2018.23,
  author =	{Fuchs, Michael and M\"{u}ller, Noela S. and Sulzbach, Henning},
  title =	{{Refined Asymptotics for the Number of Leaves of Random Point Quadtrees}},
  booktitle =	{29th International Conference on Probabilistic, Combinatorial and Asymptotic Methods for the Analysis of Algorithms (AofA 2018)},
  pages =	{23:1--23:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-078-1},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{110},
  editor =	{Fill, James Allen and Ward, Mark Daniel},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.AofA.2018.23},
  URN =		{urn:nbn:de:0030-drops-89165},
  doi =		{10.4230/LIPIcs.AofA.2018.23},
  annote =	{Keywords: Quadtree, number of leaves, phase change, stochastic fixed-point equation, central limit theorem, positivity of variance, contraction method}
}
Document
DOI: 10.4230/OASIcs.ATMOS.2009.2148
Accelerating Time-Dependent Multi-Criteria Timetable Information is Harder Than Expected

Authors: Annabell Berger, Daniel Delling, Andreas Gebhardt, and Matthias Müller-Hannemann

Published in: OASIcs, Volume 12, 9th Workshop on Algorithmic Approaches for Transportation Modeling, Optimization, and Systems (ATMOS'09) (2009)

Abstract
Speeding up multi-criteria search in real timetable information systems remains a challenge in spite of impressive progress achieved in recent years for related problems in road networks. Our goal is to perform multi-criteria range queries, that is, to find all Pareto-optimal connections with respect to travel time and number of transfers within a given start time interval. This problem can be modeled as a path search problem in a time- and event-dependent graph. In this paper, we investigate two key speed-up techniques for a multi-criteria variant of \textsc{Dijkstra}'s algorithm --- arc flags and contraction --- which seem to be strong candidates for railway networks, too. We describe in detail how these two techniques have to be adapted for a multi-criteria scenario and explain why we can expect only marginal speed-ups (compared to observations in road networks) from a direct implementation. Based on these insights we extend traditional arc-flags to \emph{time-period flags} and introduce \emph{route contraction} as a substitute for node contraction. A computational study on real queries demonstrates that these techniques combined with goal-directed search lead to a speed-up of factor 13.08 over the baseline variant for range queries for a full day.
Cite as

Annabell Berger, Daniel Delling, Andreas Gebhardt, and Matthias Müller-Hannemann. Accelerating Time-Dependent Multi-Criteria Timetable Information is Harder Than Expected. In 9th Workshop on Algorithmic Approaches for Transportation Modeling, Optimization, and Systems (ATMOS'09). Open Access Series in Informatics (OASIcs), Volume 12, pp. 1-21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2009)

Copy BibTex To Clipboard

@InProceedings{berger_et_al:OASIcs.ATMOS.2009.2148,
  author =	{Berger, Annabell and Delling, Daniel and Gebhardt, Andreas and M\"{u}ller-Hannemann, Matthias},
  title =	{{Accelerating Time-Dependent Multi-Criteria Timetable Information is Harder Than Expected}},
  booktitle =	{9th Workshop on Algorithmic Approaches for Transportation Modeling, Optimization, and Systems (ATMOS'09)},
  pages =	{1--21},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-11-8},
  ISSN =	{2190-6807},
  year =	{2009},
  volume =	{12},
  editor =	{Clausen, Jens and Di Stefano, Gabriele},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.ATMOS.2009.2148},
  URN =		{urn:nbn:de:0030-drops-21481},
  doi =		{10.4230/OASIcs.ATMOS.2009.2148},
  annote =	{Keywords: Timetable information, multi-criteria search, time-dependent networks, arc flags, contraction Timetable information, multi-criteria search, time-dependent networks, arc flags, contraction}
}
Document
DOI: 10.4230/DagSemProc.09211.3
Accounting system for heterogeneous IP-networks (IPNA) implemented at Kaiserslautern University

Authors: Brian Worden, Claudia Baltes, Inga Scheler, Paul Müller, and Hans Hagen

Published in: Dagstuhl Seminar Proceedings, Volume 9211, Visualization and Monitoring of Network Traffic (2009)

Abstract
This paper describes an accounting system (IPNA) for heterogenous IP-networks with arbitrary topologies implemented at the university of Kaiserslautern. The produced data volume per unit is numerated. The collected data is stored in a database and offers different analysis possibilities. The results can be visualized and adapted to the users requirements. The main effort was to build a data traffic quota system for single units as well as groups of devices that also report exceeded quotas. The system itself only observes the network traffic. Interfaces offer tools to interact with the network. The IPNA consists of a back-end for the data- acquisition and -preparation and a front-end for configuration and visualization tasks including quality control.
Cite as

Brian Worden, Claudia Baltes, Inga Scheler, Paul Müller, and Hans Hagen. Accounting system for heterogeneous IP-networks (IPNA) implemented at Kaiserslautern University. In Visualization and Monitoring of Network Traffic. Dagstuhl Seminar Proceedings, Volume 9211, pp. 1-7, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2009)

Copy BibTex To Clipboard

@InProceedings{worden_et_al:DagSemProc.09211.3,
  author =	{Worden, Brian and Baltes, Claudia and Scheler, Inga and M\"{u}ller, Paul and Hagen, Hans},
  title =	{{Accounting system for heterogeneous IP-networks (IPNA) implemented at Kaiserslautern University}},
  booktitle =	{Visualization and Monitoring of Network Traffic},
  pages =	{1--7},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2009},
  volume =	{9211},
  editor =	{Daniel A. Keim and Aiko Pras and J\"{u}rgen Sch\"{o}nw\"{a}lder and Pak Chung Wong},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.09211.3},
  URN =		{urn:nbn:de:0030-drops-21557},
  doi =		{10.4230/DagSemProc.09211.3},
  annote =	{Keywords: Accounting system, IP-network, Communication, informa- tion visualization, online quality control}
}
Document
DOI: 10.4230/DagSemProc.09051.3
Case Study ``Beatles Songs'' – What can be Learned from Unreliable Music Alignments?

Authors: Sebastian Ewert, Meinard Müller, Daniel Müllensiefen, Michael Clausen, and Geraint A. Wiggins

Published in: Dagstuhl Seminar Proceedings, Volume 9051, Knowledge representation for intelligent music processing (2009)

Abstract
As a result of massive digitization efforts and the world wide web, there is an exploding amount of available digital data describing and representing music at various semantic levels and in diverse formats. For example, in the case of the Beatles songs, there are numerous recordings including an increasing number of cover songs and arrangements as well as MIDI data and other symbolic music representations. The general goal of music synchronization is to align the multiple information sources related to a given piece of music. This becomes a difficult problem when the various representations reveal significant differences in structure and polyphony, while exhibiting various types of artifacts. In this paper, we address the issue of how music synchronization techniques are useful for automatically revealing critical passages with significant difference between the two versions to be aligned. Using the corpus of the Beatles songs as test bed, we analyze the kind of differences occurring in audio and MIDI versions available for the songs.
Cite as

Sebastian Ewert, Meinard Müller, Daniel Müllensiefen, Michael Clausen, and Geraint A. Wiggins. Case Study ``Beatles Songs'' – What can be Learned from Unreliable Music Alignments?. In Knowledge representation for intelligent music processing. Dagstuhl Seminar Proceedings, Volume 9051, pp. 1-16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2009)

Copy BibTex To Clipboard

@InProceedings{ewert_et_al:DagSemProc.09051.3,
  author =	{Ewert, Sebastian and M\"{u}ller, Meinard and M\"{u}llensiefen, Daniel and Clausen, Michael and Wiggins, Geraint A.},
  title =	{{Case Study ``Beatles Songs'' – What can be Learned from Unreliable Music Alignments?}},
  booktitle =	{Knowledge representation for intelligent music processing},
  pages =	{1--16},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2009},
  volume =	{9051},
  editor =	{Eleanor Selfridge-Field and Frans Wiering and Geraint A. Wiggins},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.09051.3},
  URN =		{urn:nbn:de:0030-drops-19640},
  doi =		{10.4230/DagSemProc.09051.3},
  annote =	{Keywords: MIDI, audio, music synchronization, multimodal, music collections, Beatles songs}
}
Document
DOI: 10.4230/DagSemProc.07281.3
Approximating Solution Structure

Authors: Iris van Rooij, Matthew Hamilton, Moritz Müller, and Todd Wareham

Published in: Dagstuhl Seminar Proceedings, Volume 7281, Structure Theory and FPT Algorithmics for Graphs, Digraphs and Hypergraphs (2007)

Abstract
hen it is hard to compute an optimal solution $y in optsol(x)$ to an instance $x$ of a problem, one may be willing to settle for an efficient algorithm $A$ that computes an approximate solution $A(x)$. The most popular type of approximation algorithm in Computer Science (and indeed many other applications) computes solutions whose value is within some multiplicative factor of the optimal solution value, {em e.g.}, $max(frac{val(A(x))}{optval(x)}, frac{optval(x)}{val(A(x))}) leq h(|x|)$ for some function $h()$. However, an algorithm might also produce a solution whose structure is ``close'' to the structure of an optimal solution relative to a specified solution-distance function $d$, {em i.e.}, $d(A(x), y) leq h(|x|)$ for some $y in optsol(x)$. Such structure-approximation algorithms have applications within Cognitive Science and other areas. Though there is an extensive literature dating back over 30 years on value-approximation, there is to our knowledge no work on general techniques for assessing the structure-(in)approximability of a given problem. In this talk, we describe a framework for investigating the polynomial-time and fixed-parameter structure-(in)approximability of combinatorial optimization problems relative to metric solution-distance functions, {em e.g.}, Hamming distance. We motivate this framework by (1) describing a particular application within Cognitive Science and (2) showing that value-approximability does not necessarily imply structure-approximability (and vice versa). This framework includes definitions of several types of structure approximation algorithms analogous to those studied in value-approximation, as well as structure-approximation problem classes and a structure-approximability-preserving reducibility. We describe a set of techniques for proving the degree of structure-(in)approximability of a given problem, and summarize all known results derived using these techniques. We also list 11 open questions summarizing particularly promising directions for future research within this framework. vspace*{0.15in} oindent (co-presented with Todd Wareham) vspace*{0.15in} jointwork{Hamilton, Matthew; M"{u}ller, Moritz; van Rooij, Iris; Wareham, Todd}
Cite as

Iris van Rooij, Matthew Hamilton, Moritz Müller, and Todd Wareham. Approximating Solution Structure. In Structure Theory and FPT Algorithmics for Graphs, Digraphs and Hypergraphs. Dagstuhl Seminar Proceedings, Volume 7281, pp. 1-24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2007)

Copy BibTex To Clipboard

@InProceedings{vanrooij_et_al:DagSemProc.07281.3,
  author =	{van Rooij, Iris and Hamilton, Matthew and M\"{u}ller, Moritz and Wareham, Todd},
  title =	{{Approximating Solution Structure}},
  booktitle =	{Structure Theory and FPT Algorithmics for Graphs, Digraphs and Hypergraphs},
  pages =	{1--24},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2007},
  volume =	{7281},
  editor =	{Erik Demaine and Gregory Z. Gutin and Daniel Marx and Ulrike Stege},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.07281.3},
  URN =		{urn:nbn:de:0030-drops-12345},
  doi =		{10.4230/DagSemProc.07281.3},
  annote =	{Keywords: Approximation Algorithms, Solution Structure}
}
Document
DOI: 10.4230/DagSemProc.05011.1
05011 Abstracts Collection – Computing and Markets

Authors: Daniel Lehmann, Rudolf Müller, and Tuomas Sandholm

Published in: Dagstuhl Seminar Proceedings, Volume 5011, Computing and Markets (2005)

Abstract
From 03.01.05 to 07.01.05, the Dagstuhl Seminar 05011``Computing and Markets'' 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

Daniel Lehmann, Rudolf Müller, and Tuomas Sandholm. 05011 Abstracts Collection – Computing and Markets. In Computing and Markets. Dagstuhl Seminar Proceedings, Volume 5011, pp. 1-26, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2005)

Copy BibTex To Clipboard

@InProceedings{lehmann_et_al:DagSemProc.05011.1,
  author =	{Lehmann, Daniel and M\"{u}ller, Rudolf and Sandholm, Tuomas},
  title =	{{05011 Abstracts Collection – Computing and Markets}},
  booktitle =	{Computing and Markets},
  pages =	{1--26},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2005},
  volume =	{5011},
  editor =	{Daniel Lehmann and Rudolf M\"{u}ller and Tuomas Sandholm},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.05011.1},
  URN =		{urn:nbn:de:0030-drops-2250},
  doi =		{10.4230/DagSemProc.05011.1},
  annote =	{Keywords: Algorithms, complexity, game theory, social choice, auctions, equilibrium}
}
Document
DOI: 10.4230/DagSemProc.05011.2
05011 Executive Summary – Computing and Markets

Authors: Daniel Lehmann, Rudolf Müller, and Tuomas Sandholm

Published in: Dagstuhl Seminar Proceedings, Volume 5011, Computing and Markets (2005)

Abstract
The seminar Computing and Markets facilitated a very fruitful interaction between economists and computer scientists, which intensified the understanding of the other disciplines' tool sets. The seminar helped to pave the way to a unified theory of markets that takes into account both the economic and the computational issues---and their deep interaction.
Cite as

Daniel Lehmann, Rudolf Müller, and Tuomas Sandholm. 05011 Executive Summary – Computing and Markets. In Computing and Markets. Dagstuhl Seminar Proceedings, Volume 5011, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2005)

Copy BibTex To Clipboard

@InProceedings{lehmann_et_al:DagSemProc.05011.2,
  author =	{Lehmann, Daniel and M\"{u}ller, Rudolf and Sandholm, Tuomas},
  title =	{{05011 Executive Summary – Computing and Markets}},
  booktitle =	{Computing and Markets},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2005},
  volume =	{5011},
  editor =	{Daniel Lehmann and Rudolf M\"{u}ller and Tuomas Sandholm},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.05011.2},
  URN =		{urn:nbn:de:0030-drops-2248},
  doi =		{10.4230/DagSemProc.05011.2},
  annote =	{Keywords: Algorithms, complexity, game theory, social choice, auctions, equilibrium}
}
Document
DOI: 10.4230/DagSemProc.05011.4
A Network Approach to Bayes-Nash Incentive Compatible Mechanisms

Authors: Rudolf Müller, Andres Perea, and Sascha Wolf

Published in: Dagstuhl Seminar Proceedings, Volume 5011, Computing and Markets (2005)

Abstract
This paper provides a characterization of Bayes-Nash incentive compatible mechanisms in settings where agents have one-dimensional or multi-dimensional types, quasi-linear utility functions and interdependent valuations. The characterization is derived in terms of conditions for the underlying allocation function. We do this by making a link to network theory and building complete directed graphs for agents type spaces. We show that an allocation rule is Bayes-Nash incentive compatible if and only if these graphs have no negative, finite cycles. In the case of one-dimensional types and given certain properties for agents valuation functions, we show that this condition reduces to the absence of negative 2-cycles. In the case of multi-dimensional types and given a linearity requirement on the valuation functions, we show that this condition reduces to the absence of negative 2-cycles and an integratebility condition on the valuation functions.
Cite as

Rudolf Müller, Andres Perea, and Sascha Wolf. A Network Approach to Bayes-Nash Incentive Compatible Mechanisms. In Computing and Markets. Dagstuhl Seminar Proceedings, Volume 5011, pp. 1-10, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2005)

Copy BibTex To Clipboard

@InProceedings{muller_et_al:DagSemProc.05011.4,
  author =	{M\"{u}ller, Rudolf and Perea, Andres and Wolf, Sascha},
  title =	{{A Network Approach to Bayes-Nash Incentive Compatible Mechanisms}},
  booktitle =	{Computing and Markets},
  pages =	{1--10},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2005},
  volume =	{5011},
  editor =	{Daniel Lehmann and Rudolf M\"{u}ller and Tuomas Sandholm},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.05011.4},
  URN =		{urn:nbn:de:0030-drops-2056},
  doi =		{10.4230/DagSemProc.05011.4},
  annote =	{Keywords: compact representation of games, congestion games, local-effect games, action-graph gamescomputational markets; auctions; bidding strategiesNegotiatio}
}
Document
DOI: 10.4230/DagSemProc.05011.8
Dominant Strategy Mechanisms with Multidimensional Types

Authors: Hongwei Gui, Rudolf Müller, and Rakesh V. Vohra

Published in: Dagstuhl Seminar Proceedings, Volume 5011, Computing and Markets (2005)

Abstract
This paper provides a characterization of dominant strategy mechanisms with quasi-linear utilities and multi-dimensional types for a variety of preference domains. These characterizations are in terms of a monotonicity property on the underlying allocation rule.
Cite as

Hongwei Gui, Rudolf Müller, and Rakesh V. Vohra. Dominant Strategy Mechanisms with Multidimensional Types. In Computing and Markets. Dagstuhl Seminar Proceedings, Volume 5011, pp. 1-23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2005)

Copy BibTex To Clipboard

@InProceedings{hongweigui_et_al:DagSemProc.05011.8,
  author =	{Hongwei Gui and M\"{u}ller, Rudolf and Vohra, Rakesh V.},
  title =	{{Dominant Strategy Mechanisms with Multidimensional Types}},
  booktitle =	{Computing and Markets},
  pages =	{1--23},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2005},
  volume =	{5011},
  editor =	{Daniel Lehmann and Rudolf M\"{u}ller and Tuomas Sandholm},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.05011.8},
  URN =		{urn:nbn:de:0030-drops-2107},
  doi =		{10.4230/DagSemProc.05011.8},
  annote =	{Keywords: Dominant Strategy, Farkas Lemma,}
}
  • Refine by Author
  • 5 Müller, Rudolf
  • 3 Lehmann, Daniel
  • 3 Sandholm, Tuomas
  • 2 Vohra, Rakesh V.
  • 1 Ardévol Martínez, Virginia
  • Show More...

  • Refine by Classification

  • Refine by Keyword
  • 2 Algorithms
  • 2 auctions
  • 2 complexity
  • 2 equilibrium
  • 2 game theory
  • Show More...

  • Refine by Type
  • 16 document

  • Refine by Publication Year
  • 5 2024
  • 4 2005
  • 3 2009
  • 1 2002
  • 1 2007
  • 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 About DROPS Imprint Privacy Contact