Search Results

Documents authored by Mossakowski, Till

Document
DOI: 10.4230/LIPIcs.CALCO.2017.15
UML Interactions Meet State Machines - An Institutional Approach

Authors: Alexander Knapp and Till Mossakowski

Published in: LIPIcs, Volume 72, 7th Conference on Algebra and Coalgebra in Computer Science (CALCO 2017)

Abstract
UML allows the multi-viewpoint modelling of systems. One important question is whether an interaction as specified by a sequence diagram can be actually realised in the system. Here, the latter is specified as a combination of several state machines (one for each lifeline in the interaction) by a composite structure diagram. In order to tackle this question, we formalise the involved UML diagram types as institutions, and their relations as institution (co)morphisms.
Cite as

Alexander Knapp and Till Mossakowski. UML Interactions Meet State Machines - An Institutional Approach. In 7th Conference on Algebra and Coalgebra in Computer Science (CALCO 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 72, pp. 15:1-15:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{knapp_et_al:LIPIcs.CALCO.2017.15,
  author =	{Knapp, Alexander and Mossakowski, Till},
  title =	{{UML Interactions Meet State Machines - An Institutional Approach}},
  booktitle =	{7th Conference on Algebra and Coalgebra in Computer Science (CALCO 2017)},
  pages =	{15:1--15:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-033-0},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{72},
  editor =	{Bonchi, Filippo and K\"{o}nig, Barbara},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2017.15},
  URN =		{urn:nbn:de:0030-drops-80346},
  doi =		{10.4230/LIPIcs.CALCO.2017.15},
  annote =	{Keywords: UML, state machines, interactions, composite structure diagrams, institutions, multi-view consistency}
}
Document
DOI: 10.4230/DagSemProc.05491.9
Qualitative Constraint Calculi: Heterogeneous Verification of Composition Tables

Authors: Stefan Wölfl, Till Mossakowski, and Lutz Schröder

Published in: Dagstuhl Seminar Proceedings, Volume 5491, Spatial Cognition: Specialization and Integration (2007)

Abstract
In the domain of qualitative constraint reasoning, a subfield of AI which has evolved in the past 25 years, a large number of calculi for efficient reasoning about spatial and temporal entities has been developed. Reasoning techniques developed for these constraint calculi typically rely on so-called composition tables of the calculus at hand, which allow for replacing semantic reasoning by symbolic operations. Often these composition tables are developed in a quite informal, pictorial manner and hence composition tables are prone to errors. In view of possible safety critical applications of qualitative calculi, however, it is desirable to formally verify these composition tables. In general, the verification of composition tables is a tedious task, in particular in cases where the semantics of the calculus depends on higher-order constructs such as sets. In this paper we address this problem by presenting a heterogeneous proof method that allows for combining a higher-order proof assistance system (such as Isabelle) with an automatic (first order) reasoner (such as SPASS or VAMPIRE). The benefit of this method is that the number of proof obligations that is to be proven interactively with a semi-automatic reasoner can be minimized to an acceptable level.
Cite as

Stefan Wölfl, Till Mossakowski, and Lutz Schröder. Qualitative Constraint Calculi: Heterogeneous Verification of Composition Tables. In Spatial Cognition: Specialization and Integration. Dagstuhl Seminar Proceedings, Volume 5491, pp. 1-12, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2007)

Copy BibTex To Clipboard

@InProceedings{wolfl_et_al:DagSemProc.05491.9,
  author =	{W\"{o}lfl, Stefan and Mossakowski, Till and Schr\"{o}der, Lutz},
  title =	{{Qualitative Constraint Calculi: Heterogeneous Verification of Composition Tables}},
  booktitle =	{Spatial Cognition: Specialization and Integration},
  pages =	{1--12},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2007},
  volume =	{5491},
  editor =	{Anthony G. Cohn and Christian Freksa and Bernhard Nebel},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.05491.9},
  URN =		{urn:nbn:de:0030-drops-9798},
  doi =		{10.4230/DagSemProc.05491.9},
  annote =	{Keywords: Knowledge representation and reasoning, geometric and spatial reasoning, qualitative reasoning, automated versus interaction proving, heterogeneous}
}
Document
DOI: 10.4230/DagSemProc.04391.7
Heterogeneous Theories and the Heterogeneous Tool Set

Authors: Till Mossakowski

Published in: Dagstuhl Seminar Proceedings, Volume 4391, Semantic Interoperability and Integration (2005)

Abstract
Heterogeneous multi-logic theories arise in different contexts: they are needed for the specification of large software systems, as well as for mediating between different ontologies. This is because large theories typically involve different aspects that are best specified in different logics (like equational logics, description logics, first-order logics, higher-order logics, modal logics), but also because different formalisms are in practical use (like RDF, OWL, EML). Using heterogeneous theories, different formalims being developed at different sites can be related, i.e. there is a formal interoperability among languages and tools. In many cases, specialized languages and tools have their strengths in particular aspects. Using heterogeneous theories, these strengths can be combined with comparably small effort. By contrast, a true combination of all the involved logics into a single logic would be too complex (or even inconsistent) in many cases. We propose to use \emph{institutions} as a formalization of the notion of logical system. Institutions can be related by so-called institution morphsims and comorphisms. Any graph of institutions and (co)morphisms can be flattened to a so-called \emph{Grothendieck institution}, which is kind of disjoint union of all the logics, enriched with connections via the (co)morphisms. This semantic basis for heterogeneous theories is complemented by the heterogeneous tool set, which provides tool support. Based on an object-oriented interface for institutions (using type classes in Haskell), it implements the Grothendieck institution and provides a heterogeneous parser, static analysis and proof support for heterogeneous theories. This is based on parsers, static analysers and proof support for the individual institutions, and on a heterogeneous proof calculus for theories in the Grothendieck institution. See also the Hets web page: http://www.tzi.de/cofi/hets
Cite as

Till Mossakowski. Heterogeneous Theories and the Heterogeneous Tool Set. In Semantic Interoperability and Integration. Dagstuhl Seminar Proceedings, Volume 4391, pp. 1-9, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2005)

Copy BibTex To Clipboard

@InProceedings{mossakowski:DagSemProc.04391.7,
  author =	{Mossakowski, Till},
  title =	{{Heterogeneous Theories and the Heterogeneous Tool Set}},
  booktitle =	{Semantic Interoperability and Integration},
  pages =	{1--9},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2005},
  volume =	{4391},
  editor =	{Y. Kalfoglou and M. Schorlemmer and A. Sheth and S. Staab and M. Uschold},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.04391.7},
  URN =		{urn:nbn:de:0030-drops-437},
  doi =		{10.4230/DagSemProc.04391.7},
  annote =	{Keywords: Heterogeneity , logic , theory mediation , tool integration}
}
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

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