191 Search Results for "Liu-Zhang, Chen-Da"

Document
DOI: 10.4230/LIPIcs.DNA.30.1
Geometric Enumeration of Localized DNA Strand Displacement Reaction Networks

Authors: Matthew R. Lakin and Sarika Kumar

Published in: LIPIcs, Volume 314, 30th International Conference on DNA Computing and Molecular Programming (DNA 30) (2024)

Abstract
Localized molecular devices are a powerful tool for engineering complex information-processing circuits and molecular robots. Their practical advantages include speed and scalability of interactions between components tethered near to each other on an underlying nanostructure, and the ability to restrict interactions between more distant components. The latter is a critical feature that must be factored into computational tools for the design and simulation of localized molecular devices: unlike in solution-phase systems, the geometries of molecular interactions must be accounted for when attempting to determine the network of possible reactions in a tethered molecular system. This work aims to address that challenge by integrating, for the first time, automated approaches to analysis of molecular geometry with reaction enumeration algorithms for DNA strand displacement reaction networks that can be applied to tethered molecular systems. By adapting a simple approach to solving the biophysical constraints inherent in molecular interactions to be applicable to tethered systems, we produce a localized reaction enumeration system that enhances previous approaches to reaction enumeration in tethered system by not requiring users to explicitly specify the subsets of components that are capable of interacting. This greatly simplifies the user’s task and could also be used as the basis of future systems for automated placement or routing of signal-transmission and logical processing in molecular devices. We apply this system to several published example systems from the literature, including both tethered molecular logic systems and molecular robots.
Cite as

Matthew R. Lakin and Sarika Kumar. Geometric Enumeration of Localized DNA Strand Displacement Reaction Networks. In 30th International Conference on DNA Computing and Molecular Programming (DNA 30). Leibniz International Proceedings in Informatics (LIPIcs), Volume 314, pp. 1:1-1:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{lakin_et_al:LIPIcs.DNA.30.1,
  author =	{Lakin, Matthew R. and Kumar, Sarika},
  title =	{{Geometric Enumeration of Localized DNA Strand Displacement Reaction Networks}},
  booktitle =	{30th International Conference on DNA Computing and Molecular Programming (DNA 30)},
  pages =	{1:1--1:24},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-344-7},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{314},
  editor =	{Seki, Shinnosuke and Stewart, Jaimie Marie},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.DNA.30.1},
  URN =		{urn:nbn:de:0030-drops-209294},
  doi =		{10.4230/LIPIcs.DNA.30.1},
  annote =	{Keywords: Localized circuits, reaction enumeration, DNA strand displacement, geometry, molecular computing}
}
Document
DOI: 10.4230/LIPIcs.DNA.30.2
Domain-Based Nucleic-Acid Minimum Free Energy: Algorithmic Hardness and Parameterized Bounds

Authors: Erik D. Demaine, Timothy Gomez, Elise Grizzell, Markus Hecher, Jayson Lynch, Robert Schweller, Ahmed Shalaby, and Damien Woods

Published in: LIPIcs, Volume 314, 30th International Conference on DNA Computing and Molecular Programming (DNA 30) (2024)

Abstract
Molecular programmers and nanostructure engineers use domain-level design to abstract away messy DNA/RNA sequence, chemical and geometric details. Such domain-level abstractions are enforced by sequence design principles and provide a key principle that allows scaling up of complex multistranded DNA/RNA programs and structures. Determining the most favoured secondary structure, or Minimum Free Energy (MFE), of a set of strands, is typically studied at the sequence level but has seen limited domain-level work. We analyse the computational complexity of MFE for multistranded systems in a simple setting were we allow only 1 or 2 domains per strand. On the one hand, with 2-domain strands, we find that the MFE decision problem is NP-complete, even without pseudoknots, and requires exponential time algorithms assuming SAT does. On the other hand, in the simplest case of 1-domain strands there are efficient MFE algorithms for various binding modes. However, even in this single-domain case, MFE is P-hard for promiscuous binding, where one domain may bind to multiple as experimentally used by Nikitin [Nat Chem., 2023], which in turn implies that strands consisting of a single domain efficiently implement arbitrary Boolean circuits.
Cite as

Erik D. Demaine, Timothy Gomez, Elise Grizzell, Markus Hecher, Jayson Lynch, Robert Schweller, Ahmed Shalaby, and Damien Woods. Domain-Based Nucleic-Acid Minimum Free Energy: Algorithmic Hardness and Parameterized Bounds. In 30th International Conference on DNA Computing and Molecular Programming (DNA 30). Leibniz International Proceedings in Informatics (LIPIcs), Volume 314, pp. 2:1-2:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{demaine_et_al:LIPIcs.DNA.30.2,
  author =	{Demaine, Erik D. and Gomez, Timothy and Grizzell, Elise and Hecher, Markus and Lynch, Jayson and Schweller, Robert and Shalaby, Ahmed and Woods, Damien},
  title =	{{Domain-Based Nucleic-Acid Minimum Free Energy: Algorithmic Hardness and Parameterized Bounds}},
  booktitle =	{30th International Conference on DNA Computing and Molecular Programming (DNA 30)},
  pages =	{2:1--2:24},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-344-7},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{314},
  editor =	{Seki, Shinnosuke and Stewart, Jaimie Marie},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.DNA.30.2},
  URN =		{urn:nbn:de:0030-drops-209304},
  doi =		{10.4230/LIPIcs.DNA.30.2},
  annote =	{Keywords: Domain-based DNA designs, minimum free energy, efficient algorithms, NP-hard, P-hard, NC, fixed-parameter tractable}
}
Document
DOI: 10.4230/LIPIcs.DNA.30.3
Simulation of the Abstract Tile Assembly Model Using Crisscross Slats

Authors: Phillip Drake, Daniel Hader, and Matthew J. Patitz

Published in: LIPIcs, Volume 314, 30th International Conference on DNA Computing and Molecular Programming (DNA 30) (2024)

Abstract
The abstract Tile Assembly Model (aTAM) provides an excellent foundation for the mathematical study of DNA-tile-based self-assembling systems, especially those wherein logic is embedded within the designs of the tiles so that they follow prescribed algorithms. While such algorithmic self-assembling systems are theoretically powerful, being computationally universal and capable of building complex shapes using information-theoretically optimal numbers of tiles, physical DNA-based implementations of these systems still encounter formidable error rates and undesired nucleation that hinder this theoretical potential. Slat-based self-assembly is a recent development wherein DNA forms long slats that combine together in 2 layers, rather than square tiles in a plane. In this approach, the length of the slats is key; while tiles typically only bind to 2 neighboring tiles at a time, slats may bind to dozens of other slats. This increased coordination between slats means that several mismatched slats must coincidentally meet in just the right way for errors to persist, unlike tiles where only a few are required. Consequently, while still a novel technology, large slat-based DNA constructions have been successfully implemented in the lab with resilience to many tile-based construction problems. These improved error characteristics come at a cost however, as slat-based systems are often more difficult to design and simulate than tile-based ones. Moreover, it has not been clear whether slats, with their larger sizes and different geometries, have the same theoretical capabilities as tiles. In this paper, we show that slats are capable of doing anything that tiles can, at least at scale. We demonstrate that any aTAM system may be converted to and simulated by an effectively equivalent system of slats. Furthermore, we show that these simulating slat systems can be made more efficiently, using shorter slats and a smaller scale factor, if the simulated tile system avoids certain uncommon growth patterns. Specifically, we consider 5 classes of aTAM systems with increasing complexity, from zig-zag systems which grow in a rigid pattern to the full class of all aTAM systems, and show how they may be converted to equivalent slat systems. We show that the simplest class may be simulated by slats at only a 2c × 2c scale, where c is the freely chosen coordination number of the slats, and further show that the full class of aTAM systems can be simulated at only a 5c × 5c scale. These results prove that slats have the full theoretical power of aTAM tiles while also providing constructions that are compact enough for potential DNA-based implementations of slat systems that are both capable of powerful algorithmic self-assembly and possessing of the strong error resilience of slats.
Cite as

Phillip Drake, Daniel Hader, and Matthew J. Patitz. Simulation of the Abstract Tile Assembly Model Using Crisscross Slats. In 30th International Conference on DNA Computing and Molecular Programming (DNA 30). Leibniz International Proceedings in Informatics (LIPIcs), Volume 314, pp. 3:1-3:25, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{drake_et_al:LIPIcs.DNA.30.3,
  author =	{Drake, Phillip and Hader, Daniel and Patitz, Matthew J.},
  title =	{{Simulation of the Abstract Tile Assembly Model Using Crisscross Slats}},
  booktitle =	{30th International Conference on DNA Computing and Molecular Programming (DNA 30)},
  pages =	{3:1--3:25},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-344-7},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{314},
  editor =	{Seki, Shinnosuke and Stewart, Jaimie Marie},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.DNA.30.3},
  URN =		{urn:nbn:de:0030-drops-209315},
  doi =		{10.4230/LIPIcs.DNA.30.3},
  annote =	{Keywords: DNA origami, tile-assembly, self-assembly, aTAM, kinetic modeling, computational modeling}
}
Document
DOI: 10.4230/LIPIcs.DNA.30.4
Designing 3D RNA Origami Nanostructures with a Minimum Number of Kissing Loops

Authors: Antti Elonen and Pekka Orponen

Published in: LIPIcs, Volume 314, 30th International Conference on DNA Computing and Molecular Programming (DNA 30) (2024)

Abstract
We present a general design technique for rendering any 3D wireframe model, that is any connected graph linearly embedded in 3D space, as an RNA origami nanostructure with a minimum number of kissing loops. The design algorithm, which applies some ideas and methods from topological graph theory, produces renderings that contain at most one kissing-loop pair for many interesting model families, including for instance all fully triangulated wireframes and the wireframes of all Platonic solids. The design method is already implemented and available for use in the design tool DNAforge (https://dnaforge.org).
Cite as

Antti Elonen and Pekka Orponen. Designing 3D RNA Origami Nanostructures with a Minimum Number of Kissing Loops. In 30th International Conference on DNA Computing and Molecular Programming (DNA 30). Leibniz International Proceedings in Informatics (LIPIcs), Volume 314, pp. 4:1-4:12, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{elonen_et_al:LIPIcs.DNA.30.4,
  author =	{Elonen, Antti and Orponen, Pekka},
  title =	{{Designing 3D RNA Origami Nanostructures with a Minimum Number of Kissing Loops}},
  booktitle =	{30th International Conference on DNA Computing and Molecular Programming (DNA 30)},
  pages =	{4:1--4:12},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-344-7},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{314},
  editor =	{Seki, Shinnosuke and Stewart, Jaimie Marie},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.DNA.30.4},
  URN =		{urn:nbn:de:0030-drops-209325},
  doi =		{10.4230/LIPIcs.DNA.30.4},
  annote =	{Keywords: RNA origami, wireframe nanostructures, polyhedra, kissing loops, topological graph embeddings, self-assembly}
}
Document
DOI: 10.4230/LIPIcs.COSIT.2024.1
Wayfinding Stages: The Role of Familiarity, Gaze Events, and Visual Attention

Authors: Negar Alinaghi and Ioannis Giannopoulos

Published in: LIPIcs, Volume 315, 16th International Conference on Spatial Information Theory (COSIT 2024)

Abstract
Understanding the cognitive processes involved in wayfinding is crucial for both theoretical advances and practical applications in navigation systems development. This study explores how gaze behavior and visual attention contribute to our understanding of cognitive states during wayfinding. Based on the model proposed by Downs and Stea, which segments wayfinding into four distinct stages: self-localization, route planning, monitoring, and goal recognition, we conducted an outdoor wayfinding experiment with 56 participants. Given the significant role of spatial familiarity in wayfinding behavior, each participant navigated six different routes in both familiar and unfamiliar environments, with their eye movements being recorded. We provide a detailed examination of participants' gaze behavior and the actual objects of focus. Our findings reveal distinct gaze behavior patterns and visual attention, differentiating wayfinding stages while emphasizing the impact of spatial familiarity. This examination of visual engagement during wayfinding explains adaptive cognitive processes, demonstrating how familiarity influences navigation strategies. The results enhance our theoretical understanding of wayfinding and offer practical insights for developing navigation aids capable of predicting different wayfinding stages.
Cite as

Negar Alinaghi and Ioannis Giannopoulos. Wayfinding Stages: The Role of Familiarity, Gaze Events, and Visual Attention. In 16th International Conference on Spatial Information Theory (COSIT 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 315, pp. 1:1-1:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{alinaghi_et_al:LIPIcs.COSIT.2024.1,
  author =	{Alinaghi, Negar and Giannopoulos, Ioannis},
  title =	{{Wayfinding Stages: The Role of Familiarity, Gaze Events, and Visual Attention}},
  booktitle =	{16th International Conference on Spatial Information Theory (COSIT 2024)},
  pages =	{1:1--1:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-330-0},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{315},
  editor =	{Adams, Benjamin and Griffin, Amy L. and Scheider, Simon and McKenzie, Grant},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.COSIT.2024.1},
  URN =		{urn:nbn:de:0030-drops-208161},
  doi =		{10.4230/LIPIcs.COSIT.2024.1},
  annote =	{Keywords: Eye-tracking, Wayfinding, Spatial Familiarity, Visual Attention, Gaze Behavior}
}
Document
DOI: 10.4230/LIPIcs.COSIT.2024.4
Qualitative Formalization of a Curve on a Two-Dimensional Plane

Authors: Kazuko Takahashi

Published in: LIPIcs, Volume 315, 16th International Conference on Spatial Information Theory (COSIT 2024)

Abstract
We propose a theoretical framework for qualitative spatial representation and reasoning about curves on a two-dimensional plane. We regard a curve as a sequence of segments, each of which has its own direction and convexity, and give a symbolic expression to it. We propose a reasoning method on this symbolic expression; when only a few segments of a curve are visible, we find missing segments by connecting them to create a global smooth continuous curve. In addition, we discuss whether the shape of the created curve can represent that of a real object; if the curve forms a spiral, such a curve is sometimes not appropriate as a border of an object. We show a method that judges the appropriateness of a curve, by considering the orientations of the segments.
Cite as

Kazuko Takahashi. Qualitative Formalization of a Curve on a Two-Dimensional Plane. In 16th International Conference on Spatial Information Theory (COSIT 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 315, pp. 4:1-4:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{takahashi:LIPIcs.COSIT.2024.4,
  author =	{Takahashi, Kazuko},
  title =	{{Qualitative Formalization of a Curve on a Two-Dimensional Plane}},
  booktitle =	{16th International Conference on Spatial Information Theory (COSIT 2024)},
  pages =	{4:1--4:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-330-0},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{315},
  editor =	{Adams, Benjamin and Griffin, Amy L. and Scheider, Simon and McKenzie, Grant},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.COSIT.2024.4},
  URN =		{urn:nbn:de:0030-drops-208193},
  doi =		{10.4230/LIPIcs.COSIT.2024.4},
  annote =	{Keywords: qualitative spatial reasoning, knowledge representation, logical reasoning, shape information}
}
Document
DOI: 10.4230/LIPIcs.COSIT.2024.6
Is Familiarity Reflected in the Spatial Knowledge Revealed by Sketch Maps?

Authors: Markus Kattenbeck, Daniel R. Montello, Martin Raubal, and Ioannis Giannopoulos

Published in: LIPIcs, Volume 315, 16th International Conference on Spatial Information Theory (COSIT 2024)

Abstract
Despite the frequent use of sketch maps in assessing environmental knowledge, it remains unclear how and to what degree familiarity impacts sketch map content. In the present study, we assess whether different levels of familiarity relate to differences in the content and spatial accuracy of environmental knowledge depicted in sketch maps drawn for the purpose of route instructions. To this end, we conduct a real-world wayfinding study with 91 participants, all of whom have to walk along a pre-defined route of approximately 2.3km length. Prior to the walk, we collect self-report familiarity ratings from participants for both a set of 15 landmarks and a set of areas we define as hexagons along the route. Once participants finished walking the route, they were asked to sketch a map of the route, specifically a sketch that would enable a person who had never walked the route to follow it. We found that participants unfamiliar with the areas along the route sketched fewer features than familiar people did. Contrary to our expectations, however, we found that landmarks were sketched or not regardless of participants' level of familiarity with the landmarks. We were also surprised that the level of familiarity was not correlated to the accuracy of the sketched order of features along the route, of the position of sketched features in relation to the route, nor to the metric locational accuracy of feature placement on the sketches. These results lead us to conclude that different aspects of feature salience influence whether the features are included on sketch maps, independent of familiarity. They also point to the influence of task context on the content of sketch maps, again independent of familiarity. We propose further studies to more fully explore these ideas.
Cite as

Markus Kattenbeck, Daniel R. Montello, Martin Raubal, and Ioannis Giannopoulos. Is Familiarity Reflected in the Spatial Knowledge Revealed by Sketch Maps?. In 16th International Conference on Spatial Information Theory (COSIT 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 315, pp. 6:1-6:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{kattenbeck_et_al:LIPIcs.COSIT.2024.6,
  author =	{Kattenbeck, Markus and Montello, Daniel R. and Raubal, Martin and Giannopoulos, Ioannis},
  title =	{{Is Familiarity Reflected in the Spatial Knowledge Revealed by Sketch Maps?}},
  booktitle =	{16th International Conference on Spatial Information Theory (COSIT 2024)},
  pages =	{6:1--6:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-330-0},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{315},
  editor =	{Adams, Benjamin and Griffin, Amy L. and Scheider, Simon and McKenzie, Grant},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.COSIT.2024.6},
  URN =		{urn:nbn:de:0030-drops-208215},
  doi =		{10.4230/LIPIcs.COSIT.2024.6},
  annote =	{Keywords: Familiarity, Spatial Knowledge, Sketch Maps}
}
Document
DOI: 10.4230/LIPIcs.COSIT.2024.10
Revealing Differences in Public Transport Share Through District-Wise Comparison and Relating Them to Network Properties

Authors: Manuela Canestrini, Ioanna Gogousou, Dimitrios Michail, and Ioannis Giannopoulos

Published in: LIPIcs, Volume 315, 16th International Conference on Spatial Information Theory (COSIT 2024)

Abstract
Sustainable transport is becoming an increasingly pressing issue, with two major pillars being the reduction of car usage and the promotion of public transport. One way to approach both of these pillars is through the large number of daily commute trips in urban areas, and their modal split. Previous research gathered knowledge on influencing factors on the modal split mainly through travel surveys. We take a different approach by analysing the "raw" network and the time-optimised trips on a multi-modal graph. For the case study of Vienna, Austria we investigate how the option to use a private car influences the modal split of routes towards the city centre. Additionally, we compare the modal split across seven inner districts and we relate properties of the public transport network to the respective share of public transport. The results suggest that different districts have varying options of public transport connections towards the city centre, with a share of public transport between about 5% up to a share of 45%. This reveals areas where investments in public transport could reduce commute times to the city centre. Regarding network properties, our findings suggest, that it is not sufficient to analyse the joint public transport network. Instead, individual public transport modalities should be examined. We show that the network length and the direction of the lines towards the city centre influence the proportion of subway and tram in the modal split.
Cite as

Manuela Canestrini, Ioanna Gogousou, Dimitrios Michail, and Ioannis Giannopoulos. Revealing Differences in Public Transport Share Through District-Wise Comparison and Relating Them to Network Properties. In 16th International Conference on Spatial Information Theory (COSIT 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 315, pp. 10:1-10:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{canestrini_et_al:LIPIcs.COSIT.2024.10,
  author =	{Canestrini, Manuela and Gogousou, Ioanna and Michail, Dimitrios and Giannopoulos, Ioannis},
  title =	{{Revealing Differences in Public Transport Share Through District-Wise Comparison and Relating Them to Network Properties}},
  booktitle =	{16th International Conference on Spatial Information Theory (COSIT 2024)},
  pages =	{10:1--10:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-330-0},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{315},
  editor =	{Adams, Benjamin and Griffin, Amy L. and Scheider, Simon and McKenzie, Grant},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.COSIT.2024.10},
  URN =		{urn:nbn:de:0030-drops-208255},
  doi =		{10.4230/LIPIcs.COSIT.2024.10},
  annote =	{Keywords: Mobility, Modal Split, Transportation Networks}
}
Document
DOI: 10.4230/LIPIcs.COSIT.2024.11
Semantic Perspectives on the Lake District Writing: Spatial Ontology Modeling and Relation Extraction for Deeper Insights

Authors: Erum Haris, Anthony G. Cohn, and John G. Stell

Published in: LIPIcs, Volume 315, 16th International Conference on Spatial Information Theory (COSIT 2024)

Abstract
Extracting spatial details from historical texts can be difficult, hindering our understanding of past landscapes. The study addresses this challenge by analyzing the Corpus of the Lake District Writing, focusing on the English Lake District region. We systematically link the theoretical notions from the core concepts of spatial information to provide basis for the problem domain. The conceptual foundation is further complemented with a spatial ontology and a custom gazetteer, allowing a formal and insightful semantic exploration of the massive unstructured corpus. The other contrasting side of the framework is the usage of LLMs for spatial relation extraction. We formulate prompts leveraging understanding of the LLMs of the intended task, curate a list of spatial relations representing the most recurring proximity or vicinity relations terms and extract semantic triples for the top five place names appearing in the corpus. We compare the extraction capabilities of three benchmark LLMs for a scholarly significant historical archive, representing their potential in a challenging and interdisciplinary research problem. Finally, the network comprising the semantic triples is enhanced by incorporating a gazetteer-based classification of the objects involved thus improving their spatial profiling.
Cite as

Erum Haris, Anthony G. Cohn, and John G. Stell. Semantic Perspectives on the Lake District Writing: Spatial Ontology Modeling and Relation Extraction for Deeper Insights. In 16th International Conference on Spatial Information Theory (COSIT 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 315, pp. 11:1-11:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{haris_et_al:LIPIcs.COSIT.2024.11,
  author =	{Haris, Erum and Cohn, Anthony G. and Stell, John G.},
  title =	{{Semantic Perspectives on the Lake District Writing: Spatial Ontology Modeling and Relation Extraction for Deeper Insights}},
  booktitle =	{16th International Conference on Spatial Information Theory (COSIT 2024)},
  pages =	{11:1--11:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-330-0},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{315},
  editor =	{Adams, Benjamin and Griffin, Amy L. and Scheider, Simon and McKenzie, Grant},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.COSIT.2024.11},
  URN =		{urn:nbn:de:0030-drops-208268},
  doi =		{10.4230/LIPIcs.COSIT.2024.11},
  annote =	{Keywords: spatial humanities, spatial narratives, ontology, large language models}
}
Document
Short Paper
DOI: 10.4230/LIPIcs.COSIT.2024.23
Towards Formalizing Concept Drift and Its Variants: A Case Study Using Past COSIT Proceedings (Short Paper)

Authors: Meilin Shi, Krzysztof Janowicz, Zilong Liu, and Kitty Currier

Published in: LIPIcs, Volume 315, 16th International Conference on Spatial Information Theory (COSIT 2024)

Abstract
In the classic Philosophical Investigations, Ludwig Wittgenstein suggests that the meaning of words is rooted in their use in ordinary language, challenging the idea of fixed rules determining the meaning of words. Likewise, we believe that the meaning of keywords and concepts in academic papers is shaped by their usage within the articles and evolves as research progresses. For example, the terms natural hazards and natural disasters were once used interchangeably, but this is rarely the case today. When searching for archived documents, such as those related to disaster relief, choosing the appropriate keyword is crucial and requires a deeper understanding of the historical context. To improve interoperability and promote reusability from a Research Data Management (RDM) perspective, we examine the dynamic nature of concepts, providing formal definitions of concept drift and its variants. By employing a case study of past COSIT (Conference on Spatial Information Theory) proceedings to support these definitions, we argue that a quantitative formalization can help systematically detect subsequent changes and enhance the overall interpretation of concepts.
Cite as

Meilin Shi, Krzysztof Janowicz, Zilong Liu, and Kitty Currier. Towards Formalizing Concept Drift and Its Variants: A Case Study Using Past COSIT Proceedings (Short Paper). In 16th International Conference on Spatial Information Theory (COSIT 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 315, pp. 23:1-23:8, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{shi_et_al:LIPIcs.COSIT.2024.23,
  author =	{Shi, Meilin and Janowicz, Krzysztof and Liu, Zilong and Currier, Kitty},
  title =	{{Towards Formalizing Concept Drift and Its Variants: A Case Study Using Past COSIT Proceedings}},
  booktitle =	{16th International Conference on Spatial Information Theory (COSIT 2024)},
  pages =	{23:1--23:8},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-330-0},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{315},
  editor =	{Adams, Benjamin and Griffin, Amy L. and Scheider, Simon and McKenzie, Grant},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.COSIT.2024.23},
  URN =		{urn:nbn:de:0030-drops-208386},
  doi =		{10.4230/LIPIcs.COSIT.2024.23},
  annote =	{Keywords: Concept Drift, Semantic Aging, Research Data Management}
}
Document
Short Paper
DOI: 10.4230/LIPIcs.COSIT.2024.28
Evaluating the Ability of Large Language Models to Reason About Cardinal Directions (Short Paper)

Authors: Anthony G Cohn and Robert E Blackwell

Published in: LIPIcs, Volume 315, 16th International Conference on Spatial Information Theory (COSIT 2024)

Abstract
We investigate the abilities of a representative set of Large language Models (LLMs) to reason about cardinal directions (CDs). To do so, we create two datasets: the first, co-created with ChatGPT, focuses largely on recall of world knowledge about CDs; the second is generated from a set of templates, comprehensively testing an LLM’s ability to determine the correct CD given a particular scenario. The templates allow for a number of degrees of variation such as means of locomotion of the agent involved, and whether set in the first , second or third person. Even with a temperature setting of zero, Our experiments show that although LLMs are able to perform well in the simpler dataset, in the second more complex dataset no LLM is able to reliably determine the correct CD, even with a temperature setting of zero.
Cite as

Anthony G Cohn and Robert E Blackwell. Evaluating the Ability of Large Language Models to Reason About Cardinal Directions (Short Paper). In 16th International Conference on Spatial Information Theory (COSIT 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 315, pp. 28:1-28:9, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{cohn_et_al:LIPIcs.COSIT.2024.28,
  author =	{Cohn, Anthony G and Blackwell, Robert E},
  title =	{{Evaluating the Ability of Large Language Models to Reason About Cardinal Directions}},
  booktitle =	{16th International Conference on Spatial Information Theory (COSIT 2024)},
  pages =	{28:1--28:9},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-330-0},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{315},
  editor =	{Adams, Benjamin and Griffin, Amy L. and Scheider, Simon and McKenzie, Grant},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.COSIT.2024.28},
  URN =		{urn:nbn:de:0030-drops-208432},
  doi =		{10.4230/LIPIcs.COSIT.2024.28},
  annote =	{Keywords: Large Language Models, Spatial Reasoning, Cardinal Directions}
}
Document
Short Paper
DOI: 10.4230/LIPIcs.COSIT.2024.31
Large Language Models: Testing Their Capabilities to Understand and Explain Spatial Concepts (Short Paper)

Authors: Majid Hojati and Rob Feick

Published in: LIPIcs, Volume 315, 16th International Conference on Spatial Information Theory (COSIT 2024)

Abstract
Interest in applying Large Language Models (LLMs), which use natural language processing (NLP) to provide human-like responses to text-based questions, to geospatial tasks has grown rapidly. Research shows that LLMs can help generate software code and answer some types of geographic questions to varying degrees even without fine-tuning. However, further research is required to explore the types of spatial questions they answer correctly, their abilities to apply spatial reasoning, and the variability between models. In this paper we examine the ability of four LLM models (GPT3.5 and 4, LLAma2.0, Falcon40B) to answer spatial questions that range from basic calculations to more advanced geographic concepts. The intent of this comparison is twofold. First, we demonstrate an extensible method for evaluating LLM’s limitations to supporting spatial data science through correct calculations and code generation. Relatedly, we also consider how these models can aid geospatial learning by providing text-based explanations of spatial concepts and operations. Our research shows common strengths in more basic types of questions, and mixed results for questions relating to more advanced spatial concepts. These results provide insights that may be used to inform strategies for testing and fine-tuning these models to increase their understanding of key spatial concepts.
Cite as

Majid Hojati and Rob Feick. Large Language Models: Testing Their Capabilities to Understand and Explain Spatial Concepts (Short Paper). In 16th International Conference on Spatial Information Theory (COSIT 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 315, pp. 31:1-31:9, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{hojati_et_al:LIPIcs.COSIT.2024.31,
  author =	{Hojati, Majid and Feick, Rob},
  title =	{{Large Language Models: Testing Their Capabilities to Understand and Explain Spatial Concepts}},
  booktitle =	{16th International Conference on Spatial Information Theory (COSIT 2024)},
  pages =	{31:1--31:9},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-330-0},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{315},
  editor =	{Adams, Benjamin and Griffin, Amy L. and Scheider, Simon and McKenzie, Grant},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.COSIT.2024.31},
  URN =		{urn:nbn:de:0030-drops-208460},
  doi =		{10.4230/LIPIcs.COSIT.2024.31},
  annote =	{Keywords: Geospatial concepts, Large Language Models, LLM, GPT, Llama, Falcon}
}
Document
DOI: 10.4230/LIPIcs.ITP.2024.7
An Operational Semantics in Isabelle/HOL-CSP

Authors: Benoît Ballenghien and Burkhart Wolff

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

Abstract
The theory of Communicating Sequential Processes going back to Hoare and Roscoe is still today a reference model for concurrency. In the fairly rich literature, several versions of operational semantics have been discussed, which should be consistent with the denotational one. This work is based on Isabelle/HOL-CSP 2.0, a shallow embedding of the failure-divergence model of denotational semantics proposed by Hoare, Roscoe and Brookes in the eighties. In several ways, HOL-CSP is actually an extension of the original setting in the sense that it admits higher-order processes and infinite alphabets. In this paper, we present a construction and formal equivalence proofs between operational CSP semantics and the underlying denotational failure-divergence semantics. The construction is based on a definition of the operational transition operator P ⇝e P’ basically via the After operator and the classical failure-divergence refinement. Several choices are discussed to formally derive the operational semantics leading to subtle differences. The derived operational semantics for symbolic Labelled Transition Systems (LTSs) can be potentially used for certifications of model-checker logs as well as combined proof techniques.
Cite as

Benoît Ballenghien and Burkhart Wolff. An Operational Semantics in Isabelle/HOL-CSP. In 15th International Conference on Interactive Theorem Proving (ITP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 309, pp. 7:1-7:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{ballenghien_et_al:LIPIcs.ITP.2024.7,
  author =	{Ballenghien, Beno\^{i}t and Wolff, Burkhart},
  title =	{{An Operational Semantics in Isabelle/HOL-CSP}},
  booktitle =	{15th International Conference on Interactive Theorem Proving (ITP 2024)},
  pages =	{7:1--7:18},
  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.7},
  URN =		{urn:nbn:de:0030-drops-207355},
  doi =		{10.4230/LIPIcs.ITP.2024.7},
  annote =	{Keywords: Process-Algebra, Semantics, Concurrency, Computational Models, Theorem Proving, Isabelle/HOL}
}
Document
DOI: 10.4230/LIPIcs.ITP.2024.17
Verifying Software Emulation of an Unsupported Hardware Instruction

Authors: Samuel Gruetter, Thomas Bourgeat, and Adam Chlipala

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

Abstract
Some processors, especially embedded ones, do not implement all instructions in hardware. Instead, if the processor encounters an unimplemented instruction, an unsupported-instruction exception is raised, and an exception handler is run that implements the missing instruction in software. Getting such a system to work correctly is tricky: The exception-handler code must not destroy any state of the user program and must use the control and status registers (CSRs) of the processor correctly. Moreover, parts of the handler are typically implemented in assembly, while other parts are implemented in a language like C, and one must make sure that when jumping from the user program into the handler assembly, from the handler assembly into C, back to assembly and finally back to the user program, all the assumptions made by the different pieces of code, hardware, and the compiler are satisfied. Despite all these tricky details, there is a concise and intuitive way of stating the correctness of such a system: User programs running on a system where some instructions are implemented in software behave the same as if they were running on a system where all instructions are implemented in hardware. We formalize and prove such a statement in the Coq proof assistant, for the case of a simple exception handler implementing the multiplication instruction on a RISC-V processor.
Cite as

Samuel Gruetter, Thomas Bourgeat, and Adam Chlipala. Verifying Software Emulation of an Unsupported Hardware Instruction. In 15th International Conference on Interactive Theorem Proving (ITP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 309, pp. 17:1-17:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{gruetter_et_al:LIPIcs.ITP.2024.17,
  author =	{Gruetter, Samuel and Bourgeat, Thomas and Chlipala, Adam},
  title =	{{Verifying Software Emulation of an Unsupported Hardware Instruction}},
  booktitle =	{15th International Conference on Interactive Theorem Proving (ITP 2024)},
  pages =	{17:1--17: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.17},
  URN =		{urn:nbn:de:0030-drops-207452},
  doi =		{10.4230/LIPIcs.ITP.2024.17},
  annote =	{Keywords: Software verification, Software-hardware boundary, Coq}
}
Document
DOI: 10.4230/LIPIcs.ITP.2024.25
Formalizing the Cholesky Factorization Theorem

Authors: Carl Kwan and Warren A. Hunt Jr.

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

Abstract
We present a formal proof of the Cholesky Factorization Theorem, a fundamental result in numerical linear algebra, by verifying formally a Cholesky decomposition algorithm in ACL2. Our mechanical proof of correctness is largely automatic for two main reasons: (1) we employ a derivation which involves partitioning the matrix to obtain the desired result; and (2) we provide an inductive invariant for the Cholesky decomposition algorithm. To formalize (1), we build support for reasoning about partitioned matrices. This is a departure from how typical numerical linear algebra algorithms are presented, i.e. via excessive indexing. To enable (2), we build a new recursive recognizer for a matrix to be Cholesky decomposable and mathematically prove that the recognizer is indeed necessary and sufficient. Guided by the recognizer, ACL2 automatically inducts and verifies the Cholesky decomposition algorithm. We also present our ACL2-based formalization of the decomposition algorithm itself, and discuss how to bridge the gap between verifying a decomposition algorithm and proving the Cholesky Factorization Theorem. To our knowledge, this is the first formalization of the Cholesky Factorization Theorem.
Cite as

Carl Kwan and Warren A. Hunt Jr.. Formalizing the Cholesky Factorization Theorem. In 15th International Conference on Interactive Theorem Proving (ITP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 309, pp. 25:1-25:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{kwan_et_al:LIPIcs.ITP.2024.25,
  author =	{Kwan, Carl and Hunt Jr., Warren A.},
  title =	{{Formalizing the Cholesky Factorization Theorem}},
  booktitle =	{15th International Conference on Interactive Theorem Proving (ITP 2024)},
  pages =	{25:1--25: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.25},
  URN =		{urn:nbn:de:0030-drops-207532},
  doi =		{10.4230/LIPIcs.ITP.2024.25},
  annote =	{Keywords: Numerical linear algebra, Cholesky factorization theorem, Matrix decomposition, Automated reasoning, ACL2}
}
  • Refine by Author
  • 9 Liu-Zhang, Chen-Da
  • 4 Chen, Lin
  • 4 Zhang, Guochuan
  • 4 Zheng, Da Wei
  • 3 Cai, Shaowei
  • Show More...

  • Refine by Classification
  • 10 Theory of computation → Graph algorithms analysis
  • 8 Theory of computation → Approximation algorithms analysis
  • 8 Theory of computation → Constraint and logic programming
  • 8 Theory of computation → Parameterized complexity and exact algorithms
  • 7 Computer systems organization → Real-time systems
  • Show More...

  • Refine by Keyword
  • 6 broadcast
  • 5 Scheduling
  • 4 Approximate counting
  • 4 Large Language Models
  • 3 Constraint Programming
  • Show More...

  • Refine by Type
  • 191 document

  • Refine by Publication Year
  • 130 2024
  • 21 2023
  • 8 2021
  • 8 2022
  • 6 2020
  • Show More...

© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact