5 Search Results for "Schneider, Daniel"


Document
Possible and Certain Answers for Queries over Order-Incomplete Data

Authors: Antoine Amarilli, Mouhamadou Lamine Ba, Daniel Deutch, and Pierre Senellart

Published in: LIPIcs, Volume 90, 24th International Symposium on Temporal Representation and Reasoning (TIME 2017)


Abstract
To combine and query ordered data from multiple sources, one needs to handle uncertainty about the possible orderings. Examples of such "order-incomplete" data include integrated event sequences such as log entries; lists of properties (e.g., hotels and restaurants) ranked by an unknown function reflecting relevance or customer ratings; and documents edited concurrently with an uncertain order on edits. This paper introduces a query language for order-incomplete data, based on the positive relational algebra with order-aware accumulation. We use partial orders to represent order-incomplete data, and study possible and certain answers for queries in this context. We show that these problems are respectively NP-complete and coNP-complete, but identify many tractable cases depending on the query operators or input partial orders.

Cite as

Antoine Amarilli, Mouhamadou Lamine Ba, Daniel Deutch, and Pierre Senellart. Possible and Certain Answers for Queries over Order-Incomplete Data. In 24th International Symposium on Temporal Representation and Reasoning (TIME 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 90, pp. 4:1-4:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)


Copy BibTex To Clipboard

@InProceedings{amarilli_et_al:LIPIcs.TIME.2017.4,
  author =	{Amarilli, Antoine and Ba, Mouhamadou Lamine and Deutch, Daniel and Senellart, Pierre},
  title =	{{Possible and Certain Answers for Queries over Order-Incomplete Data}},
  booktitle =	{24th International Symposium on Temporal Representation and Reasoning (TIME 2017)},
  pages =	{4:1--4:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-052-1},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{90},
  editor =	{Schewe, Sven and Schneider, Thomas and Wijsen, Jef},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2017.4},
  URN =		{urn:nbn:de:0030-drops-79311},
  doi =		{10.4230/LIPIcs.TIME.2017.4},
  annote =	{Keywords: certain answer, possible answer, partial order, uncertain data}
}
Document
The Fully Hybrid mu-Calculus

Authors: Daniel Kernberger and Martin Lange

Published in: LIPIcs, Volume 90, 24th International Symposium on Temporal Representation and Reasoning (TIME 2017)


Abstract
We consider the hybridisation of the mu-calculus through the addition of nominals, binder and jump. Especially the use of the binder differentiates our approach from earlier hybridisations of the mu-calculus and also results in a more involved formal semantics. We then investigate the model checking problem and obtain ExpTime-completeness for the full logic and the same complexity as the modal mu-calculus for a fixed number of variables. We also show that this logic is invariant under hybrid bisimulation and use this result to show that - contrary to the non-hybrid case - the hybrid extension of the full branching time logic CTL* is not a fragment of the fully hybrid mu-calculus.

Cite as

Daniel Kernberger and Martin Lange. The Fully Hybrid mu-Calculus. In 24th International Symposium on Temporal Representation and Reasoning (TIME 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 90, pp. 17:1-17:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)


Copy BibTex To Clipboard

@InProceedings{kernberger_et_al:LIPIcs.TIME.2017.17,
  author =	{Kernberger, Daniel and Lange, Martin},
  title =	{{The Fully Hybrid mu-Calculus}},
  booktitle =	{24th International Symposium on Temporal Representation and Reasoning (TIME 2017)},
  pages =	{17:1--17:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-052-1},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{90},
  editor =	{Schewe, Sven and Schneider, Thomas and Wijsen, Jef},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2017.17},
  URN =		{urn:nbn:de:0030-drops-79244},
  doi =		{10.4230/LIPIcs.TIME.2017.17},
  annote =	{Keywords: mu-calculus, hybrid logics, model checking, bisimulation invariance}
}
Document
CakES: Cake Metaphor for Analyzing Safety Issues of Embedded Systems

Authors: Yasmin I. Al-Zokari, Taimur Khan, Daniel Schneider, Dirk Zeckzer, and Hans Hagen

Published in: Dagstuhl Follow-Ups, Volume 2, Scientific Visualization: Interactions, Features, Metaphors (2011)


Abstract
Embedded systems are used everywhere. They are complex systems whose failure may cause death or injury to people or may damage the environment are required to be safety safe. Therefore, these systems need to be analyzed. Fault tree analysis is a common way for performing safety analysis. It generates a large amount of interconnected data that itself needs to be analyzed to help different domain experts (e.g., engineers and safety analysts) in their decisions for improving the system’s safety. Additional difficulties occur for the experts in communication and in linking the data (e.g., information of basic events or minimal cut sets) to the actual parts of the system (model). Therefore, a large amount of time and effort is being spent on discussions, searching,and navigating through the data. To overcome this, we present a new metaphor called "CakES" consisting of multiple views visualizing the data generated by fault tree analysis and linking them to the actual parts of the model by intuitive interaction. Using the interaction techniques of CakES the user can directly explore the safety related data without navigating through the fault tree while retaining an overview of all critical aspects in the model.

Cite as

Yasmin I. Al-Zokari, Taimur Khan, Daniel Schneider, Dirk Zeckzer, and Hans Hagen. CakES: Cake Metaphor for Analyzing Safety Issues of Embedded Systems. In Scientific Visualization: Interactions, Features, Metaphors. Dagstuhl Follow-Ups, Volume 2, pp. 1-16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)


Copy BibTex To Clipboard

@InCollection{alzokari_et_al:DFU.Vol2.SciViz.2011.1,
  author =	{Al-Zokari, Yasmin I. and Khan, Taimur and Schneider, Daniel and Zeckzer, Dirk and Hagen, Hans},
  title =	{{CakES: Cake Metaphor for Analyzing Safety Issues of Embedded Systems}},
  booktitle =	{Scientific Visualization: Interactions, Features, Metaphors},
  pages =	{1--16},
  series =	{Dagstuhl Follow-Ups},
  ISBN =	{978-3-939897-26-2},
  ISSN =	{1868-8977},
  year =	{2011},
  volume =	{2},
  editor =	{Hagen, Hans},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DFU.Vol2.SciViz.2011.1},
  URN =		{urn:nbn:de:0030-drops-32844},
  doi =		{10.4230/DFU.Vol2.SciViz.2011.1},
  annote =	{Keywords: Fault Tree Analysis, minimal cut sets, basic events, information visualization, scientific visualization, engineering, tiled-wall, multiple monitor sy}
}
Document
Framework for Comprehensive Size and Resolution Utilization of Arbitrary Displays

Authors: Taimur Khan, Daniel Schneider, Yasmin Al-Zokari, Dirk Zeckzer, and Hans Hagen

Published in: Dagstuhl Follow-Ups, Volume 2, Scientific Visualization: Interactions, Features, Metaphors (2011)


Abstract
Scalable large high-resolution displays such as tiled displays are imperative for the visualization of large and complex datasets. In recent times, the relatively low costs for setting up large display systems have led to an highly increased usage of such devices. However, it is equally vital to optimally utilize their size and resolution to effectively explore such data through a combination of diverse visualizations, views, and interaction mechanisms. In this paper, we present a lightweight dispatcher framework which facilitates input management, focus management, and the execution of several interrelated yet independent visualizations. The approach is deliberately kept flexible to not only tackle different hardware configurations but also the amount of visualization applications to be implemented. This is demonstrated through a scenario that executes four interrelated visualizations equally well on both a 5 PC tiled-wall and a single desktop. The key contribution of this work is the ability to extend the tiled-wall to work with multiple applications for enhanced size and resolution utilization of such displays.

Cite as

Taimur Khan, Daniel Schneider, Yasmin Al-Zokari, Dirk Zeckzer, and Hans Hagen. Framework for Comprehensive Size and Resolution Utilization of Arbitrary Displays. In Scientific Visualization: Interactions, Features, Metaphors. Dagstuhl Follow-Ups, Volume 2, pp. 144-159, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)


Copy BibTex To Clipboard

@InCollection{khan_et_al:DFU.Vol2.SciViz.2011.144,
  author =	{Khan, Taimur and Schneider, Daniel and Al-Zokari, Yasmin and Zeckzer, Dirk and Hagen, Hans},
  title =	{{Framework for Comprehensive Size and Resolution Utilization of Arbitrary Displays}},
  booktitle =	{Scientific Visualization: Interactions, Features, Metaphors},
  pages =	{144--159},
  series =	{Dagstuhl Follow-Ups},
  ISBN =	{978-3-939897-26-2},
  ISSN =	{1868-8977},
  year =	{2011},
  volume =	{2},
  editor =	{Hagen, Hans},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DFU.Vol2.SciViz.2011.144},
  URN =		{urn:nbn:de:0030-drops-32916},
  doi =		{10.4230/DFU.Vol2.SciViz.2011.144},
  annote =	{Keywords: Large and High-res Displays, Coordinated and Multiple Views, Human Computer Interaction}
}
Document
Termination of Programs using Term Rewriting and SAT Solving

Authors: Jürgen Giesl, Peter Schneider-Kamp, René Thiemann, Stephan Swiderski, Manh Thang Nguyen, Daniel De Schreye, and Alexander Serebrenik

Published in: Dagstuhl Seminar Proceedings, Volume 7401, Deduction and Decision Procedures (2007)


Abstract
There are many powerful techniques for automated termination analysis of term rewrite systems (TRSs). However, up to now they have hardly been used for real programming languages. In this talk, we describe recent results which permit the application of existing techniques from term rewriting in order to prove termination of programs. We discuss two possible approaches: 1. One could translate programs into TRSs and then use existing tools to verify termination of the resulting TRSs. 2. One could adapt TRS-techniques to the respective programming languages in order to analyze programs directly. We present such approaches for the functional language Haskell and the logic language Prolog. Our results have been implemented in the termination provers AProVE and Polytool. In order to handle termination problems resulting from real programs, these provers had to be coupled with modern SAT solvers, since the automation of the TRS-termination techniques had to improve significantly. Our resulting termination analyzers are currently the most powerful ones for Haskell and Prolog.

Cite as

Jürgen Giesl, Peter Schneider-Kamp, René Thiemann, Stephan Swiderski, Manh Thang Nguyen, Daniel De Schreye, and Alexander Serebrenik. Termination of Programs using Term Rewriting and SAT Solving. In Deduction and Decision Procedures. Dagstuhl Seminar Proceedings, Volume 7401, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2007)


Copy BibTex To Clipboard

@InProceedings{giesl_et_al:DagSemProc.07401.7,
  author =	{Giesl, J\"{u}rgen and Schneider-Kamp, Peter and Thiemann, Ren\'{e} and Swiderski, Stephan and Nguyen, Manh Thang and De Schreye, Daniel and Serebrenik, Alexander},
  title =	{{Termination of Programs using Term Rewriting and SAT Solving}},
  booktitle =	{Deduction and Decision Procedures},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2007},
  volume =	{7401},
  editor =	{Franz Baader and Byron Cook and J\"{u}rgen Giesl and Robert Nieuwenhuis},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagSemProc.07401.7},
  URN =		{urn:nbn:de:0030-drops-12481},
  doi =		{10.4230/DagSemProc.07401.7},
  annote =	{Keywords: Termination, Term Rewriting, Haskell, Prolog, SAT Solving}
}
  • Refine by Author
  • 2 Hagen, Hans
  • 2 Khan, Taimur
  • 2 Schneider, Daniel
  • 2 Zeckzer, Dirk
  • 1 Al-Zokari, Yasmin
  • Show More...

  • Refine by Classification

  • Refine by Keyword
  • 1 Coordinated and Multiple Views
  • 1 Fault Tree Analysis
  • 1 Haskell
  • 1 Human Computer Interaction
  • 1 Large and High-res Displays
  • Show More...

  • Refine by Type
  • 5 document

  • Refine by Publication Year
  • 2 2011
  • 2 2017
  • 1 2007

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