21 Search Results for "Martin, Jos"


Document
Window-Slicing Techniques Extended to Spanning-Event Streams

Authors: Aurélie Suzanne, Guillaume Raschia, José Martinez, and Damien Tassetti

Published in: LIPIcs, Volume 178, 27th International Symposium on Temporal Representation and Reasoning (TIME 2020)


Abstract
Streaming systems often use slices to share computation costs among overlapping windows. However they are limited to instantaneous events where only one point represents the event. Here, we extend streams to events that come with a duration, denoted as spanning events. After a short review of the new constraints ensued by event lifespan in a temporal sliding-window context, we propose a new structure for dealing with slices in such an environment, and prove that our technique is both correct and effective to deal with such spanning events.

Cite as

Aurélie Suzanne, Guillaume Raschia, José Martinez, and Damien Tassetti. Window-Slicing Techniques Extended to Spanning-Event Streams. In 27th International Symposium on Temporal Representation and Reasoning (TIME 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 178, pp. 10:1-10:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)


Copy BibTex To Clipboard

@InProceedings{suzanne_et_al:LIPIcs.TIME.2020.10,
  author =	{Suzanne, Aur\'{e}lie and Raschia, Guillaume and Martinez, Jos\'{e} and Tassetti, Damien},
  title =	{{Window-Slicing Techniques Extended to Spanning-Event Streams}},
  booktitle =	{27th International Symposium on Temporal Representation and Reasoning (TIME 2020)},
  pages =	{10:1--10:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-167-2},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{178},
  editor =	{Mu\~{n}oz-Velasco, Emilio and Ozaki, Ana and Theobald, Martin},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2020.10},
  URN =		{urn:nbn:de:0030-drops-129783},
  doi =		{10.4230/LIPIcs.TIME.2020.10},
  annote =	{Keywords: Data Stream, Spanning-events, Temporal Aggregates, Sliding Windows}
}
Document
Martin Hofmann’s Case for Non-Strictly Positive Data Types

Authors: Ulrich Berger, Ralph Matthes, and Anton Setzer

Published in: LIPIcs, Volume 130, 24th International Conference on Types for Proofs and Programs (TYPES 2018)


Abstract
We describe the breadth-first traversal algorithm by Martin Hofmann that uses a non-strictly positive data type and carry out a simple verification in an extensional setting. Termination is shown by implementing the algorithm in the strongly normalising extension of system F by Mendler-style recursion. We then analyze the same algorithm by alternative verifications first in an intensional setting using a non-strictly positive inductive definition (not just a non-strictly positive data type), and subsequently by two different algebraic reductions. The verification approaches are compared in terms of notions of simulation and should elucidate the somewhat mysterious algorithm and thus make a case for other uses of non-strictly positive data types. Except for the termination proof, which cannot be formalised in Coq, all proofs were formalised in Coq and some of the algorithms were implemented in Agda and Haskell.

Cite as

Ulrich Berger, Ralph Matthes, and Anton Setzer. Martin Hofmann’s Case for Non-Strictly Positive Data Types. In 24th International Conference on Types for Proofs and Programs (TYPES 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 130, pp. 1:1-1:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)


Copy BibTex To Clipboard

@InProceedings{berger_et_al:LIPIcs.TYPES.2018.1,
  author =	{Berger, Ulrich and Matthes, Ralph and Setzer, Anton},
  title =	{{Martin Hofmann’s Case for Non-Strictly Positive Data Types}},
  booktitle =	{24th International Conference on Types for Proofs and Programs (TYPES 2018)},
  pages =	{1:1--1:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-106-1},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{130},
  editor =	{Dybjer, Peter and Esp{\'\i}rito Santo, Jos\'{e} and Pinto, Lu{\'\i}s},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2018.1},
  URN =		{urn:nbn:de:0030-drops-114052},
  doi =		{10.4230/LIPIcs.TYPES.2018.1},
  annote =	{Keywords: non strictly-positive data types, breadth-first traversal, program verification, Mendler-style recursion, System F, theorem proving, Coq, Agda, Haskell}
}
Document
Dependent Sums and Dependent Products in Bishop’s Set Theory

Authors: Iosif Petrakis

Published in: LIPIcs, Volume 130, 24th International Conference on Types for Proofs and Programs (TYPES 2018)


Abstract
According to the standard, non type-theoretic accounts of Bishop’s constructivism (BISH), dependent functions are not necessary to BISH. Dependent functions though, are explicitly used by Bishop in his definition of the intersection of a family of subsets, and they are necessary to the definition of arbitrary products. In this paper we present the basic notions and principles of CSFT, a semi-formal constructive theory of sets and functions intended to be a minimal, adequate and faithful, in Feferman’s sense, semi-formalisation of Bishop’s set theory (BST). We define the notions of dependent sum (or exterior union) and dependent product of set-indexed families of sets within CSFT, and we prove the distributivity of prod over sum i.e., the translation of the type-theoretic axiom of choice within CSFT. We also define the notions of dependent sum (or interior union) and dependent product of set-indexed families of subsets within CSFT. For these definitions we extend BST with the universe of sets #1 V_0 and the universe of functions #1 V_1.

Cite as

Iosif Petrakis. Dependent Sums and Dependent Products in Bishop’s Set Theory. In 24th International Conference on Types for Proofs and Programs (TYPES 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 130, pp. 3:1-3:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)


Copy BibTex To Clipboard

@InProceedings{petrakis:LIPIcs.TYPES.2018.3,
  author =	{Petrakis, Iosif},
  title =	{{Dependent Sums and Dependent Products in Bishop’s Set Theory}},
  booktitle =	{24th International Conference on Types for Proofs and Programs (TYPES 2018)},
  pages =	{3:1--3:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-106-1},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{130},
  editor =	{Dybjer, Peter and Esp{\'\i}rito Santo, Jos\'{e} and Pinto, Lu{\'\i}s},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2018.3},
  URN =		{urn:nbn:de:0030-drops-114070},
  doi =		{10.4230/LIPIcs.TYPES.2018.3},
  annote =	{Keywords: Bishop’s constructive mathematics, Martin-L\"{o}f’s type theory, dependent sums, dependent products, type-theoretic axiom of choice}
}
Document
Normalization by Evaluation for Typed Weak lambda-Reduction

Authors: Filippo Sestini

Published in: LIPIcs, Volume 130, 24th International Conference on Types for Proofs and Programs (TYPES 2018)


Abstract
Weak reduction relations in the lambda-calculus are characterized by the rejection of the so-called xi-rule, which allows arbitrary reductions under abstractions. A notable instance of weak reduction can be found in the literature under the name restricted reduction or weak lambda-reduction. In this work, we attack the problem of algorithmically computing normal forms for lambda-wk, the lambda-calculus with weak lambda-reduction. We do so by first contrasting it with other weak systems, arguing that their notion of reduction is not strong enough to compute lambda-wk-normal forms. We observe that some aspects of weak lambda-reduction prevent us from normalizing lambda-wk directly, thus devise a new, better-behaved weak calculus lambda-ex, and reduce the normalization problem for lambda-w to that of lambda-ex. We finally define type systems for both calculi and apply Normalization by Evaluation to lambda-ex, obtaining a normalization proof for lambda-wk as a corollary. We formalize all our results in Agda, a proof-assistant based on intensional Martin-Löf Type Theory.

Cite as

Filippo Sestini. Normalization by Evaluation for Typed Weak lambda-Reduction. In 24th International Conference on Types for Proofs and Programs (TYPES 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 130, pp. 6:1-6:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)


Copy BibTex To Clipboard

@InProceedings{sestini:LIPIcs.TYPES.2018.6,
  author =	{Sestini, Filippo},
  title =	{{Normalization by Evaluation for Typed Weak lambda-Reduction}},
  booktitle =	{24th International Conference on Types for Proofs and Programs (TYPES 2018)},
  pages =	{6:1--6:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-106-1},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{130},
  editor =	{Dybjer, Peter and Esp{\'\i}rito Santo, Jos\'{e} and Pinto, Lu{\'\i}s},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2018.6},
  URN =		{urn:nbn:de:0030-drops-114101},
  doi =		{10.4230/LIPIcs.TYPES.2018.6},
  annote =	{Keywords: normalization, lambda-calculus, reduction, term-rewriting, Agda}
}
Document
The Second Order Traffic Fine: Temporal Reasoning in European Transport Regulations

Authors: Ana de Almeida Borges, Juan José Conejero Rodríguez, David Fernández-Duque, Mireia González Bedmar, and Joost J. Joosten

Published in: LIPIcs, Volume 147, 26th International Symposium on Temporal Representation and Reasoning (TIME 2019)


Abstract
We argue that European transport regulations can be formalized within the Sigma^1_1 fragment of monadic second order logic, and possibly weaker fragments including linear temporal logic. We consider several articles in the regulation to verify these claims.

Cite as

Ana de Almeida Borges, Juan José Conejero Rodríguez, David Fernández-Duque, Mireia González Bedmar, and Joost J. Joosten. The Second Order Traffic Fine: Temporal Reasoning in European Transport Regulations. In 26th International Symposium on Temporal Representation and Reasoning (TIME 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 147, pp. 6:1-6:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)


Copy BibTex To Clipboard

@InProceedings{dealmeidaborges_et_al:LIPIcs.TIME.2019.6,
  author =	{de Almeida Borges, Ana and Conejero Rodr{\'\i}guez, Juan Jos\'{e} and Fern\'{a}ndez-Duque, David and Gonz\'{a}lez Bedmar, Mireia and Joosten, Joost J.},
  title =	{{The Second Order Traffic Fine: Temporal Reasoning in European Transport Regulations}},
  booktitle =	{26th International Symposium on Temporal Representation and Reasoning (TIME 2019)},
  pages =	{6:1--6:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-127-6},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{147},
  editor =	{Gamper, Johann and Pinchinat, Sophie and Sciavicco, Guido},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2019.6},
  URN =		{urn:nbn:de:0030-drops-113649},
  doi =		{10.4230/LIPIcs.TIME.2019.6},
  annote =	{Keywords: linear temporal logic, monadic second order logic, formalized law, transport regulations}
}
Document
A Local-Search Algorithm for Steiner Forest

Authors: Martin Groß, Anupam Gupta, Amit Kumar, Jannik Matuschke, Daniel R. Schmidt, Melanie Schmidt, and José Verschae

Published in: LIPIcs, Volume 94, 9th Innovations in Theoretical Computer Science Conference (ITCS 2018)


Abstract
In the Steiner Forest problem, we are given a graph and a collection of source-sink pairs, and the goal is to find a subgraph of minimum total length such that all pairs are connected. The problem is APX-Hard and can be 2-approximated by, e.g., the elegant primal-dual algorithm of Agrawal, Klein, and Ravi from 1995. We give a local-search-based constant-factor approximation for the problem. Local search brings in new techniques to an area that has for long not seen any improvements and might be a step towards a combinatorial algorithm for the more general survivable network design problem. Moreover, local search was an essential tool to tackle the dynamic MST/Steiner Tree problem, whereas dynamic Steiner Forest is still wide open. It is easy to see that any constant factor local search algorithm requires steps that add/drop many edges together. We propose natural local moves which, at each step, either (a) add a shortest path in the current graph and then drop a bunch of inessential edges, or (b) add a set of edges to the current solution. This second type of moves is motivated by the potential function we use to measure progress, combining the cost of the solution with a penalty for each connected component. Our carefully-chosen local moves and potential function work in tandem to eliminate bad local minima that arise when using more traditional local moves. Our analysis first considers the case where the local optimum is a single tree, and shows optimality w.r.t. moves that add a single edge (and drop a set of edges) is enough to bound the locality gap. For the general case, we show how to "project" the optimal solution onto the different trees of the local optimum without incurring too much cost (and this argument uses optimality w.r.t. both kinds of moves), followed by a tree-by-tree argument. We hope both the potential function, and our analysis techniques will be useful to develop and analyze local-search algorithms in other contexts.

Cite as

Martin Groß, Anupam Gupta, Amit Kumar, Jannik Matuschke, Daniel R. Schmidt, Melanie Schmidt, and José Verschae. A Local-Search Algorithm for Steiner Forest. In 9th Innovations in Theoretical Computer Science Conference (ITCS 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 94, pp. 31:1-31:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)


Copy BibTex To Clipboard

@InProceedings{gro_et_al:LIPIcs.ITCS.2018.31,
  author =	{Gro{\ss}, Martin and Gupta, Anupam and Kumar, Amit and Matuschke, Jannik and Schmidt, Daniel R. and Schmidt, Melanie and Verschae, Jos\'{e}},
  title =	{{A Local-Search Algorithm for Steiner Forest}},
  booktitle =	{9th Innovations in Theoretical Computer Science Conference (ITCS 2018)},
  pages =	{31:1--31:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-060-6},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{94},
  editor =	{Karlin, Anna R.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ITCS.2018.31},
  URN =		{urn:nbn:de:0030-drops-83134},
  doi =		{10.4230/LIPIcs.ITCS.2018.31},
  annote =	{Keywords: Local Search, Steiner Forest, Approximation Algorithms, Network Design}
}
Document
Scheduling Problems over Network of Machines

Authors: Zachary Friggstad, Arnoosh Golestanian, Kamyar Khodamoradi, Christopher Martin, Mirmahdi Rahgoshay, Mohsen Rezapour, Mohammad R. Salavatipour, and Yifeng Zhang

Published in: LIPIcs, Volume 81, Approximation, Randomization, and Combinatorial Optimization. Algorithms and Techniques (APPROX/RANDOM 2017)


Abstract
We consider scheduling problems in which jobs need to be processed through a (shared) network of machines. The network is given in the form of a graph the edges of which represent the machines. We are also given a set of jobs, each specified by its processing time and a path in the graph. Every job needs to be processed in the order of edges specified by its path. We assume that jobs can wait between machines and preemption is not allowed; that is, once a job is started being processed on a machine, it must be completed without interruption. Every machine can only process one job at a time. The makespan of a schedule is the earliest time by which all the jobs have finished processing. The flow time (a.k.a. the completion time) of a job in a schedule is the difference in time between when it finishes processing on its last machine and when the it begins processing on its first machine. The total flow time (or the sum of completion times) is the sum of flow times (or completion times) of all jobs. Our focus is on finding schedules with the minimum sum of completion times or minimum makespan. In this paper, we develop several algorithms (both approximate and exact) for the problem both on general graphs and when the underlying graph of machines is a tree. Even in the very special case when the underlying network is a simple star, the problem is very interesting as it models a biprocessor scheduling with applications to data migration.

Cite as

Zachary Friggstad, Arnoosh Golestanian, Kamyar Khodamoradi, Christopher Martin, Mirmahdi Rahgoshay, Mohsen Rezapour, Mohammad R. Salavatipour, and Yifeng Zhang. Scheduling Problems over Network of Machines. In Approximation, Randomization, and Combinatorial Optimization. Algorithms and Techniques (APPROX/RANDOM 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 81, pp. 5:1-5:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)


Copy BibTex To Clipboard

@InProceedings{friggstad_et_al:LIPIcs.APPROX-RANDOM.2017.5,
  author =	{Friggstad, Zachary and Golestanian, Arnoosh and Khodamoradi, Kamyar and Martin, Christopher and Rahgoshay, Mirmahdi and Rezapour, Mohsen and Salavatipour, Mohammad R. and Zhang, Yifeng},
  title =	{{Scheduling Problems over Network of Machines}},
  booktitle =	{Approximation, Randomization, and Combinatorial Optimization. Algorithms and Techniques (APPROX/RANDOM 2017)},
  pages =	{5:1--5:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-044-6},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{81},
  editor =	{Jansen, Klaus and Rolim, Jos\'{e} D. P. and Williamson, David P. and Vempala, Santosh S.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.APPROX-RANDOM.2017.5},
  URN =		{urn:nbn:de:0030-drops-75547},
  doi =		{10.4230/LIPIcs.APPROX-RANDOM.2017.5},
  annote =	{Keywords: approximation algorithms, job-shop scheduling, min-sum edge coloring, minimum latency}
}
Document
Dynamic Traffic Models in Transportation Science (Dagstuhl Seminar 15412)

Authors: José R. Correa, Tobias Harks, Kai Nagel, Britta Peis, and Martin Skutella

Published in: Dagstuhl Reports, Volume 5, Issue 10 (2016)


Abstract
Traffic assignment models are crucial for traffic planners to be able to predict traffic distributions, especially, in light of possible changes of the infrastructure, e.g., road constructions, traffic light controls, etc. The starting point of the seminar was the observation that there is a trend in the transportation community (science as well as industry) to base such predictions on complex computer-based simulations that are capable of resolving many elements of a real transportation system. On the other hand, within the past few years, the theory of dynamic traffic assignments in terms of equilibrium existence and equilibrium computation has not matured to the point matching the model complexity inherent in simulations. In view of the above, this interdisciplinary seminar brought together leading scientists in the areas traffic simulations, algorithmic game theory and dynamic traffic assignment as well as people from industry with strong scientific background who identified possible ways to bridge the described gap.

Cite as

José R. Correa, Tobias Harks, Kai Nagel, Britta Peis, and Martin Skutella. Dynamic Traffic Models in Transportation Science (Dagstuhl Seminar 15412). In Dagstuhl Reports, Volume 5, Issue 10, pp. 19-34, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)


Copy BibTex To Clipboard

@Article{correa_et_al:DagRep.5.10.19,
  author =	{Correa, Jos\'{e} R. and Harks, Tobias and Nagel, Kai and Peis, Britta and Skutella, Martin},
  title =	{{Dynamic Traffic Models in Transportation Science (Dagstuhl Seminar 15412)}},
  pages =	{19--34},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2016},
  volume =	{5},
  number =	{10},
  editor =	{Correa, Jos\'{e} R. and Harks, Tobias and Nagel, Kai and Peis, Britta and Skutella, Martin},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagRep.5.10.19},
  URN =		{urn:nbn:de:0030-drops-56938},
  doi =		{10.4230/DagRep.5.10.19},
  annote =	{Keywords: Dynamic traffic equilibria, Complexity of equilibrium computation, Simulation, Dynamic network flow theory, Network optimization}
}
Document
Complexity and Approximation of the Continuous Network Design Problem

Authors: Martin Gairing, Tobias Harks, and Max Klimm

Published in: LIPIcs, Volume 28, Approximation, Randomization, and Combinatorial Optimization. Algorithms and Techniques (APPROX/RANDOM 2014)


Abstract
We revisit a classical problem in transportation, known as the continuous (bilevel) network design problem, CNDP for short. Given a graph for which the latency of each edge depends on the ratio of the edge flow and the capacity installed, the goal is to find an optimal investment in edge capacities so as to minimize the sum of the routing cost of the induced Wardrop equilibrium and the investment cost for installing the capacity. While this problem is considered as challenging in the literature, its complexity status was still unknown. We close this gap showing that CNDP is strongly NP-complete and APX-hard, both on directed and undirected networks and even for instances with affine latencies. As for the approximation of the problem, we first provide a detailed analysis for a heuristic studied by Marcotte for the special case of monomial latency functions (Math. Program., Vol. 34, 1986). We derive a closed form expression of its approximation guarantee for arbitrary sets of latency functions. We then propose a different approximation algorithm and show that it has the same approximation guarantee. However, we show that using the better of the two approximation algorithms results in a strictly improved approximation guarantee for which we derive a closed form expression. For affine latencies, e.g., this algorithm achieves a 49/41-approximation which improves on the 5/4 that has been shown before by Marcotte. We finally discuss the case of hard budget constraints on the capacity investment.

Cite as

Martin Gairing, Tobias Harks, and Max Klimm. Complexity and Approximation of the Continuous Network Design Problem. In Approximation, Randomization, and Combinatorial Optimization. Algorithms and Techniques (APPROX/RANDOM 2014). Leibniz International Proceedings in Informatics (LIPIcs), Volume 28, pp. 226-241, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)


Copy BibTex To Clipboard

@InProceedings{gairing_et_al:LIPIcs.APPROX-RANDOM.2014.226,
  author =	{Gairing, Martin and Harks, Tobias and Klimm, Max},
  title =	{{Complexity and Approximation of the Continuous Network Design Problem}},
  booktitle =	{Approximation, Randomization, and Combinatorial Optimization. Algorithms and Techniques (APPROX/RANDOM 2014)},
  pages =	{226--241},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-74-3},
  ISSN =	{1868-8969},
  year =	{2014},
  volume =	{28},
  editor =	{Jansen, Klaus and Rolim, Jos\'{e} and Devanur, Nikhil R. and Moore, Cristopher},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.APPROX-RANDOM.2014.226},
  URN =		{urn:nbn:de:0030-drops-46998},
  doi =		{10.4230/LIPIcs.APPROX-RANDOM.2014.226},
  annote =	{Keywords: Bilevel optimization, Optimization under equilibrium constraints, Network design, Wardrop equilibrium, Computational complexity, Approximation algorit}
}
Document
The complexity of positive first-order logic without equality II: The four-element case

Authors: Barnaby Martin and Jos Martin

Published in: Dagstuhl Seminar Proceedings, Volume 9441, The Constraint Satisfaction Problem: Complexity and Approximability (2010)


Abstract
We study the complexity of evaluating positive equality-free sentences of first-order (FO) logic over fixed, finite structures B. This may be seen as a natural generalisation of the non-uniform quantified constraint satisfaction problem QCSP(B). Extending the algebraic methods of a previous paper, we derive a complete complexity classification for these problems as B ranges over structures of domain size 4. Specifically, each problem is either in Logspace, is NP-complete, is co-NP-complete or is Pspace-complete.

Cite as

Barnaby Martin and Jos Martin. The complexity of positive first-order logic without equality II: The four-element case. In The Constraint Satisfaction Problem: Complexity and Approximability. Dagstuhl Seminar Proceedings, Volume 9441, pp. 1-12, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)


Copy BibTex To Clipboard

@InProceedings{martin_et_al:DagSemProc.09441.5,
  author =	{Martin, Barnaby and Martin, Jos},
  title =	{{The complexity of positive first-order logic without equality II: The four-element case}},
  booktitle =	{The Constraint Satisfaction Problem: Complexity and Approximability},
  pages =	{1--12},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2010},
  volume =	{9441},
  editor =	{Andrei A. Bulatov and Martin Grohe and Phokion G. Kolaitis and Andrei Krokhin},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagSemProc.09441.5},
  URN =		{urn:nbn:de:0030-drops-23670},
  doi =		{10.4230/DagSemProc.09441.5},
  annote =	{Keywords: Quantified constraints, Galois connection}
}
Document
09041 Working Group on MCDM for Robust Multiobjective Optimization (1st Round)

Authors: Jos Figueira, Martin Geiger, Salvatore Greco, Johannes Jahn, Kathrin Klamroth, Masahiro Inuiguchi, Vincent Mousseau, Sayin Serpil, Roman Slowinski, Margaret M. Wiecek, and Witting Katrin

Published in: Dagstuhl Seminar Proceedings, Volume 9041, Hybrid and Robust Approaches to Multiobjective Optimization (2009)


Abstract
This group explored MCDM techniques for robust multiobjective optimization.

Cite as

Jos Figueira, Martin Geiger, Salvatore Greco, Johannes Jahn, Kathrin Klamroth, Masahiro Inuiguchi, Vincent Mousseau, Sayin Serpil, Roman Slowinski, Margaret M. Wiecek, and Witting Katrin. 09041 Working Group on MCDM for Robust Multiobjective Optimization (1st Round). In Hybrid and Robust Approaches to Multiobjective Optimization. Dagstuhl Seminar Proceedings, Volume 9041, pp. 1-2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2009)


Copy BibTex To Clipboard

@InProceedings{figueira_et_al:DagSemProc.09041.6,
  author =	{Figueira, Jos and Geiger, Martin and Greco, Salvatore and Jahn, Johannes and Klamroth, Kathrin and Inuiguchi, Masahiro and Mousseau, Vincent and Sayin Serpil and Slowinski, Roman and Wiecek, Margaret M. and Witting Katrin},
  title =	{{09041 Working Group on MCDM for Robust Multiobjective Optimization (1st Round)}},
  booktitle =	{Hybrid and Robust Approaches to Multiobjective Optimization},
  pages =	{1--2},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2009},
  volume =	{9041},
  editor =	{Kalyanmoy Deb and Salvatore Greco and Kaisa Miettinen and Eckart Zitzler},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagSemProc.09041.6},
  URN =		{urn:nbn:de:0030-drops-20025},
  doi =		{10.4230/DagSemProc.09041.6},
  annote =	{Keywords: Robust multiobjective optimization}
}
Document
05081 Abstracts Collection – Foundations of Global Computing

Authors: José Luiz Fiadeiro, Ugo Montanari, and Martin Wirsing

Published in: Dagstuhl Seminar Proceedings, Volume 5081, Foundations of Global Computing (2006)


Abstract
From 20.02.05 to 25.02.05, the Dagstuhl Seminar 05081 on ``Foundations of Global Computing'' 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

José Luiz Fiadeiro, Ugo Montanari, and Martin Wirsing. 05081 Abstracts Collection – Foundations of Global Computing. In Foundations of Global Computing. Dagstuhl Seminar Proceedings, Volume 5081, pp. 1-16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2006)


Copy BibTex To Clipboard

@InProceedings{fiadeiro_et_al:DagSemProc.05081.1,
  author =	{Fiadeiro, Jos\'{e} Luiz and Montanari, Ugo and Wirsing, Martin},
  title =	{{05081 Abstracts Collection – Foundations of Global Computing}},
  booktitle =	{Foundations of Global Computing},
  pages =	{1--16},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2006},
  volume =	{5081},
  editor =	{Jos\'{e} Luiz Fiadeiro and Ugo Montanari and Martin Wirsing},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagSemProc.05081.1},
  URN =		{urn:nbn:de:0030-drops-4590},
  doi =		{10.4230/DagSemProc.05081.1},
  annote =	{Keywords: Global Computing}
}
Document
Architectural Views for CommUnity

Authors: Cristóvão Oliveira and Michel Wermelinger

Published in: Dagstuhl Seminar Proceedings, Volume 5081, Foundations of Global Computing (2006)


Abstract
CommUnity and its categorical foundations provide a formal approach to Software Architecture (SA). Several concepts such as (re) configuration and (higher-order) connector have been given precise definitions in this setting. One of the cornerstones of the approach is the separation between computation, coordination and distribution. In this paper, we take this separation one step further and define explicit architectural views, one for each concern. They will be used to help to detect errors made while building the architecture. Moreover they will be a support to improve the design of the system by focusing on one concern at a time and/or by combining them with each other.

Cite as

Cristóvão Oliveira and Michel Wermelinger. Architectural Views for CommUnity. In Foundations of Global Computing. Dagstuhl Seminar Proceedings, Volume 5081, pp. 1-3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2006)


Copy BibTex To Clipboard

@InProceedings{oliveira_et_al:DagSemProc.05081.2,
  author =	{Oliveira, Crist\'{o}v\~{a}o and Wermelinger, Michel},
  title =	{{Architectural Views for CommUnity}},
  booktitle =	{Foundations of Global Computing},
  pages =	{1--3},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2006},
  volume =	{5081},
  editor =	{Jos\'{e} Luiz Fiadeiro and Ugo Montanari and Martin Wirsing},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagSemProc.05081.2},
  URN =		{urn:nbn:de:0030-drops-2967},
  doi =		{10.4230/DagSemProc.05081.2},
  annote =	{Keywords: Software Architecture, views, computation, coordination, distribution}
}
Document
Data Handover: Reconciling Message Passing and Shared Memory

Authors: Jens Gustedt

Published in: Dagstuhl Seminar Proceedings, Volume 5081, Foundations of Global Computing (2006)


Abstract
Data Handover (DHO) is a programming paradigm and interface that aims to handle data between parallel or distributed processes that mixes aspects of message passing and shared memory. It is designed to overcome the potential problems in terms of efficiency of both: (1) memory blowup and forced copies for message passing and (2) data consistency and latency problems for shared memory. Our approach attempts to be simple and easy to understand. It contents itself with just a handful of functions to cover the main aspects of coarse grained inter-operation upon data.

Cite as

Jens Gustedt. Data Handover: Reconciling Message Passing and Shared Memory. In Foundations of Global Computing. Dagstuhl Seminar Proceedings, Volume 5081, pp. 1-13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2006)


Copy BibTex To Clipboard

@InProceedings{gustedt:DagSemProc.05081.3,
  author =	{Gustedt, Jens},
  title =	{{Data Handover: Reconciling Message Passing and Shared Memory}},
  booktitle =	{Foundations of Global Computing},
  pages =	{1--13},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2006},
  volume =	{5081},
  editor =	{Jos\'{e} Luiz Fiadeiro and Ugo Montanari and Martin Wirsing},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagSemProc.05081.3},
  URN =		{urn:nbn:de:0030-drops-2977},
  doi =		{10.4230/DagSemProc.05081.3},
  annote =	{Keywords: Efficient data management, message passing, shared memory}
}
Document
Injecting Distribution in CASL

Authors: Maura Cerioli and Matteo Dell'Amico

Published in: Dagstuhl Seminar Proceedings, Volume 5081, Foundations of Global Computing (2006)


Abstract
We present a first attempt at the development of a library in the specification language Casl providing primitives to represent connectivity and communication in a distributed system. The focus, in particular, is on peer-to-peer, which presents more challanges than the client-server paradigm, because of the higher degree of anarchy and the large amount of middleware providing similar but different features in support of it. From our experience on the definition of this library, we draw some methodological lessons on how to deal with the capture of complex software systems, as opposite to classical libraries representing standard or mathematical datatypes.

Cite as

Maura Cerioli and Matteo Dell'Amico. Injecting Distribution in CASL. In Foundations of Global Computing. Dagstuhl Seminar Proceedings, Volume 5081, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2006)


Copy BibTex To Clipboard

@InProceedings{cerioli_et_al:DagSemProc.05081.4,
  author =	{Cerioli, Maura and Dell'Amico, Matteo},
  title =	{{Injecting Distribution in CASL}},
  booktitle =	{Foundations of Global Computing},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2006},
  volume =	{5081},
  editor =	{Jos\'{e} Luiz Fiadeiro and Ugo Montanari and Martin Wirsing},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagSemProc.05081.4},
  URN =		{urn:nbn:de:0030-drops-2981},
  doi =		{10.4230/DagSemProc.05081.4},
  annote =	{Keywords: P2P, CASL, algebraic specification language, specification library}
}
  • Refine by Author
  • 3 Wirsing, Martin
  • 2 Ehrig, Hartmut
  • 2 Harks, Tobias
  • 2 Meseguer, José
  • 2 Montanari, Ugo
  • Show More...

  • Refine by Classification
  • 1 Applied computing → Law
  • 1 Information systems → Stream management
  • 1 Software and its engineering → Abstract data types
  • 1 Software and its engineering → Coroutines
  • 1 Software and its engineering → Recursion
  • Show More...

  • Refine by Keyword
  • 2 Agda
  • 1 Anonymity
  • 1 Approximation Algorithms
  • 1 Approximation algorit
  • 1 Bilevel optimization
  • Show More...

  • Refine by Type
  • 21 document

  • Refine by Publication Year
  • 8 2006
  • 4 2019
  • 1 1994
  • 1 1996
  • 1 2009
  • 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