7 Search Results for "Möller, Ralf"

Document
DOI: 10.4230/LIPIcs.ITP.2025.15
Certified Implementability of Global Multiparty Protocols

Authors: Elaine Li and Thomas Wies

Published in: LIPIcs, Volume 352, 16th International Conference on Interactive Theorem Proving (ITP 2025)

Abstract
Implementability is the decision problem at the heart of top-down approaches to protocol verification. In this paper, we present a mechanization of a recently proposed precise implementability characterization by Li et al. for a large class of protocols that subsumes many existing formalisms in the literature. Our protocols and implementations model asynchronous commmunication, and can exhibit infinite behavior. We improve upon their pen-and-paper results by unifying distinct formalisms, simplifying existing proof arguments, elaborating on the construction of canonical implementations, and even uncovering a subtle bug in the semantics for infinite words. As a corollary of our mechanization, we show that the original characterization of implementability applies even to protocols with infinitely many participants. We also contribute a reusable library for reasoning about generic communicating state machines. Our mechanization consists of about 15k lines of Rocq code. We believe that our mechanization can provide the foundation for deductively proving the implementability of protocols beyond the reach of prior work, extracting certified implementations for finite protocols, and investigating implementability under alternative asynchronous communication models.
Cite as

Elaine Li and Thomas Wies. Certified Implementability of Global Multiparty Protocols. In 16th International Conference on Interactive Theorem Proving (ITP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 352, pp. 15:1-15:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{li_et_al:LIPIcs.ITP.2025.15,
  author =	{Li, Elaine and Wies, Thomas},
  title =	{{Certified Implementability of Global Multiparty Protocols}},
  booktitle =	{16th International Conference on Interactive Theorem Proving (ITP 2025)},
  pages =	{15:1--15:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-396-6},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{352},
  editor =	{Forster, Yannick and Keller, Chantal},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2025.15},
  URN =		{urn:nbn:de:0030-drops-246139},
  doi =		{10.4230/LIPIcs.ITP.2025.15},
  annote =	{Keywords: Asynchronous protocols, communicating state machines, labeled transition systems, infinite semantics, realizability, multiparty session types, choreographies, deadlock freedom}
}
Document
DOI: 10.4230/OASIcs.FMBC.2025.10
Program Logics for Ledgers

Authors: Orestis Melkonian, Wouter Swierstra, and James Chapman

Published in: OASIcs, Volume 129, 6th International Workshop on Formal Methods for Blockchains (FMBC 2025)

Abstract
Distributed ledgers nowadays manage substantial monetary funds in the form of cryptocurrencies such as Bitcoin, Ethereum, and Cardano. For such ledgers to be safe, operations that add new entries must be cryptographically sound - but it is less clear how to reason effectively about such ever-growing linear data structures. This paper demonstrates how distributed ledgers may be viewed as computer programs, that, when executed, transfer funds between various parties. As a result, familiar program logics, such as Hoare logic, are applied in a novel setting. Borrowing ideas from concurrent separation logic, this enables modular reasoning principles over arbitrary fragments of any ledger. All of our results have been mechanised in the Agda proof assistant.
Cite as

Orestis Melkonian, Wouter Swierstra, and James Chapman. Program Logics for Ledgers. In 6th International Workshop on Formal Methods for Blockchains (FMBC 2025). Open Access Series in Informatics (OASIcs), Volume 129, pp. 10:1-10:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{melkonian_et_al:OASIcs.FMBC.2025.10,
  author =	{Melkonian, Orestis and Swierstra, Wouter and Chapman, James},
  title =	{{Program Logics for Ledgers}},
  booktitle =	{6th International Workshop on Formal Methods for Blockchains (FMBC 2025)},
  pages =	{10:1--10:22},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-371-3},
  ISSN =	{2190-6807},
  year =	{2025},
  volume =	{129},
  editor =	{Marmsoler, Diego and Xu, Meng},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.FMBC.2025.10},
  URN =		{urn:nbn:de:0030-drops-230370},
  doi =		{10.4230/OASIcs.FMBC.2025.10},
  annote =	{Keywords: blockchain, distributed ledgers, UTxO separation logic, program semantics, formal verification, Agda}
}
Document
Position
DOI: 10.4230/TGDK.2.1.2
Grounding Stream Reasoning Research

Authors: Pieter Bonte, Jean-Paul Calbimonte, Daniel de Leng, Daniele Dell'Aglio, Emanuele Della Valle, Thomas Eiter, Federico Giannini, Fredrik Heintz, Konstantin Schekotihin, Danh Le-Phuoc, Alessandra Mileo, Patrik Schneider, Riccardo Tommasini, Jacopo Urbani, and Giacomo Ziffer

Published in: TGDK, Volume 2, Issue 1 (2024): Special Issue on Trends in Graph Data and Knowledge - Part 2. Transactions on Graph Data and Knowledge, Volume 2, Issue 1

Abstract
In the last decade, there has been a growing interest in applying AI technologies to implement complex data analytics over data streams. To this end, researchers in various fields have been organising a yearly event called the "Stream Reasoning Workshop" to share perspectives, challenges, and experiences around this topic. In this paper, the previous organisers of the workshops and other community members provide a summary of the main research results that have been discussed during the first six editions of the event. These results can be categorised into four main research areas: The first is concerned with the technological challenges related to handling large data streams. The second area aims at adapting and extending existing semantic technologies to data streams. The third and fourth areas focus on how to implement reasoning techniques, either considering deductive or inductive techniques, to extract new and valuable knowledge from the data in the stream. This summary is written not only to provide a crystallisation of the field, but also to point out distinctive traits of the stream reasoning community. Moreover, it also provides a foundation for future research by enumerating a list of use cases and open challenges, to stimulate others to join this exciting research area.
Cite as

Pieter Bonte, Jean-Paul Calbimonte, Daniel de Leng, Daniele Dell'Aglio, Emanuele Della Valle, Thomas Eiter, Federico Giannini, Fredrik Heintz, Konstantin Schekotihin, Danh Le-Phuoc, Alessandra Mileo, Patrik Schneider, Riccardo Tommasini, Jacopo Urbani, and Giacomo Ziffer. Grounding Stream Reasoning Research. In Special Issue on Trends in Graph Data and Knowledge - Part 2. Transactions on Graph Data and Knowledge (TGDK), Volume 2, Issue 1, pp. 2:1-2:47, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@Article{bonte_et_al:TGDK.2.1.2,
  author =	{Bonte, Pieter and Calbimonte, Jean-Paul and de Leng, Daniel and Dell'Aglio, Daniele and Della Valle, Emanuele and Eiter, Thomas and Giannini, Federico and Heintz, Fredrik and Schekotihin, Konstantin and Le-Phuoc, Danh and Mileo, Alessandra and Schneider, Patrik and Tommasini, Riccardo and Urbani, Jacopo and Ziffer, Giacomo},
  title =	{{Grounding Stream Reasoning Research}},
  journal =	{Transactions on Graph Data and Knowledge},
  pages =	{2:1--2:47},
  ISSN =	{2942-7517},
  year =	{2024},
  volume =	{2},
  number =	{1},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/TGDK.2.1.2},
  URN =		{urn:nbn:de:0030-drops-198597},
  doi =		{10.4230/TGDK.2.1.2},
  annote =	{Keywords: Stream Reasoning, Stream Processing, RDF streams, Streaming Linked Data, Continuous query processing, Temporal Logics, High-performance computing, Databases}
}
Document
Survey
DOI: 10.4230/TGDK.2.1.4
Logics for Conceptual Data Modelling: A Review

Authors: Pablo R. Fillottrani and C. Maria Keet

Published in: TGDK, Volume 2, Issue 1 (2024): Special Issue on Trends in Graph Data and Knowledge - Part 2. Transactions on Graph Data and Knowledge, Volume 2, Issue 1

Abstract
Information modelling for databases and object-oriented information systems avails of conceptual data modelling languages such as EER and UML Class Diagrams. Many attempts exist to add logical rigour to them, for various reasons and with disparate strengths. In this paper we aim to provide a structured overview of the many efforts. We focus on aims, approaches to the formalisation, including key dimensions of choice points, popular logics used, and the main relevant reasoning services. We close with current challenges and research directions.
Cite as

Pablo R. Fillottrani and C. Maria Keet. Logics for Conceptual Data Modelling: A Review. In Special Issue on Trends in Graph Data and Knowledge - Part 2. Transactions on Graph Data and Knowledge (TGDK), Volume 2, Issue 1, pp. 4:1-4:30, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@Article{fillottrani_et_al:TGDK.2.1.4,
  author =	{Fillottrani, Pablo R. and Keet, C. Maria},
  title =	{{Logics for Conceptual Data Modelling: A Review}},
  journal =	{Transactions on Graph Data and Knowledge},
  pages =	{4:1--4:30},
  ISSN =	{2942-7517},
  year =	{2024},
  volume =	{2},
  number =	{1},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/TGDK.2.1.4},
  URN =		{urn:nbn:de:0030-drops-198616},
  doi =		{10.4230/TGDK.2.1.4},
  annote =	{Keywords: Conceptual Data Modelling, EER, UML, Description Logics, OWL}
}
Document
DOI: 10.4230/DagSemProc.08091.1
08091 Abstracts Collection – Logic and Probability for Scene Interpretation

Authors: Bernd Neumann, Anthony C. Cohn, David C. Hogg, and Ralf Möller

Published in: Dagstuhl Seminar Proceedings, Volume 8091, Logic and Probability for Scene Interpretation (2008)

Abstract
From 25.2.2008 to Friday 29.2.2008, the Dagstuhl Seminar 08091 ``Logic and Probability for Scene Interpretation'' 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.
Cite as

Bernd Neumann, Anthony C. Cohn, David C. Hogg, and Ralf Möller. 08091 Abstracts Collection – Logic and Probability for Scene Interpretation. In Logic and Probability for Scene Interpretation. Dagstuhl Seminar Proceedings, Volume 8091, pp. 1-17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2008)

Copy BibTex To Clipboard

@InProceedings{neumann_et_al:DagSemProc.08091.1,
  author =	{Neumann, Bernd and Cohn, Anthony C. and Hogg, David C. and M\"{o}ller, Ralf},
  title =	{{08091 Abstracts Collection – Logic and Probability for Scene Interpretation}},
  booktitle =	{Logic and Probability for Scene Interpretation},
  pages =	{1--17},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2008},
  volume =	{8091},
  editor =	{Anthony G. Cohn and David C. Hogg and Ralf M\"{o}ller and Bernd Neumann},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.08091.1},
  URN =		{urn:nbn:de:0030-drops-16480},
  doi =		{10.4230/DagSemProc.08091.1},
  annote =	{Keywords: Logic, probabilities, scene interpretation}
}
Document
DOI: 10.4230/DagSemProc.08091.8
Implementing probabilistic description logics: An application to image interpretation

Authors: Ralf Möller and Tobias H. Näth

Published in: Dagstuhl Seminar Proceedings, Volume 8091, Logic and Probability for Scene Interpretation (2008)

Abstract
This paper presents an application of an optimized implementation of a probabilistic description logic defined by Giugno and Lukasiewicz [9] to the domain of image interpretation. This approach extends a description logic with so-called probabilistic constraints to allow for automated reasoning over formal ontologies in combination with probabilistic knowledge. We analyze the performance of current algorithms and investigate new optimization techniques.
Cite as

Ralf Möller and Tobias H. Näth. Implementing probabilistic description logics: An application to image interpretation. In Logic and Probability for Scene Interpretation. Dagstuhl Seminar Proceedings, Volume 8091, pp. 1-6, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2008)

Copy BibTex To Clipboard

@InProceedings{moller_et_al:DagSemProc.08091.8,
  author =	{M\"{o}ller, Ralf and N\"{a}th, Tobias H.},
  title =	{{Implementing probabilistic description logics: An application to image interpretation}},
  booktitle =	{Logic and Probability for Scene Interpretation},
  pages =	{1--6},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2008},
  volume =	{8091},
  editor =	{Anthony G. Cohn and David C. Hogg and Ralf M\"{o}ller and Bernd Neumann},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.08091.8},
  URN =		{urn:nbn:de:0030-drops-16186},
  doi =		{10.4230/DagSemProc.08091.8},
  annote =	{Keywords: Probabilistic description logics, image interpretation probabilistic lexicographic entailment}
}
Document
DOI: 10.4230/DagSemProc.08091.16
Towards a Media Interpretation Framework for the Semantic Web

Authors: S. Espinosa Peraldi, A. Kaya, S. Melzer, Ralf Möller, and M. Wessel

Published in: Dagstuhl Seminar Proceedings, Volume 8091, Logic and Probability for Scene Interpretation (2008)

Abstract
We present a framework for media interpretation that leverages low-level information extraction to a higher level of abstraction in order to support semantics-based information retrieval for the Semantic Web. The overall goal of the framework is to provide high-level content descriptions of documents for maximizing precision and recall of semantics-based information retrieval.
Cite as

S. Espinosa Peraldi, A. Kaya, S. Melzer, Ralf Möller, and M. Wessel. Towards a Media Interpretation Framework for the Semantic Web. In Logic and Probability for Scene Interpretation. Dagstuhl Seminar Proceedings, Volume 8091, pp. 1-7, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2008)

Copy BibTex To Clipboard

@InProceedings{espinosaperaldi_et_al:DagSemProc.08091.16,
  author =	{Espinosa Peraldi, S. and Kaya, A. and Melzer, S. and M\"{o}ller, Ralf and Wessel, M.},
  title =	{{Towards a Media Interpretation Framework for the Semantic Web}},
  booktitle =	{Logic and Probability for Scene Interpretation},
  pages =	{1--7},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2008},
  volume =	{8091},
  editor =	{Anthony G. Cohn and David C. Hogg and Ralf M\"{o}ller and Bernd Neumann},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.08091.16},
  URN =		{urn:nbn:de:0030-drops-16190},
  doi =		{10.4230/DagSemProc.08091.16},
  annote =	{Keywords: }
}
  • Refine by Type
  • 7 Document/PDF
  • 4 Document/HTML

  • Refine by Publication Year
  • 2 2025
  • 2 2024
  • 3 2008

  • Refine by Author
  • 3 Möller, Ralf
  • 1 Bonte, Pieter
  • 1 Calbimonte, Jean-Paul
  • 1 Chapman, James
  • 1 Cohn, Anthony C.
  • Show More...

  • Refine by Series/Journal
  • 1 LIPIcs
  • 1 OASIcs
  • 2 TGDK
  • 3 DagSemProc

  • Refine by Classification
  • 2 Computing methodologies → Description logics
  • 1 Computing methodologies → Temporal reasoning
  • 1 Information systems → Data streams
  • 1 Information systems → Database design and models
  • 1 Information systems → Graph-based database models
  • Show More...

  • Refine by Keyword
  • 1 Agda
  • 1 Asynchronous protocols
  • 1 Conceptual Data Modelling
  • 1 Continuous query processing
  • 1 Databases
  • Show More...

Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

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