arXiv subjects

Jon Haël Brenas

Publications and source records attributed to Jon Haël Brenas.

3 recordsLinked to original sources

arXiv2019

A Surveillance Infrastructure for Malaria Analytics: Provisioning Data Access and Preservation of Interoperability

We propose the Semantics, Interoperability, and Evolution for Malaria Analytics (SIEMA) platform for use in malaria surveillance based on semantic data federation. Using this approach, it is possible to access distributed data, extend and preserve interoperability between multiple dynamic distributed malaria sources, and facilitate detection of system changes that can interrupt mission-critical global surveillance activities. We used Semantic Automated Discovery and Integration (SADI) Semantic Web Services to enable data access and improve interoperability, and the graphical user interface-enabled semantic query engine HYDRA to implement the target queries typical of malaria programs. We implemented a custom algorithm to detect changes to community-developed terminologies, data sources, and services that are core to SIEMA. This algorithm reports to a dashboard. Valet SADI is used to mitigate the impact of changes by rebuilding affected services. We developed a prototype surveillance and change management platform from a combination of third-party tools, community-developed terminologies, and custom algorithms. We illustrated a methodology and core infrastructure to facilitate interoperable access to distributed data sources using SADI Semantic Web services. This degree of access makes it possible to implement complex queries needed by our user community with minimal technical skill. We implemented a dashboard that reports on terminology changes that can render the services inactive, jeopardizing system interoperability. Using this information, end users can control and reactively rebuild services to preserve interoperability and minimize service downtime.

cs.CY↗

arXiv2018

On the Verification of Logically Decorated Graph Transformations

We address the problem of reasoning on graph transformations featuring actions such as \emph{addition} and \emph{deletion} of nodes and edges, node \emph{merging} and \emph{cloning}, node or edge \emph{labelling} and edge \emph{redirection}. First, we introduce the considered graph rewrite systems which are parameterized by a given logic $\mathcal{L}$. Formulas of $\mathcal{L}$ are used to label graph nodes and edges. In a second step, we tackle the problem of formal verification of the considered rewrite systems by using a Hoare-like weakest precondition calculus. It acts on triples of the form $\{\texttt{Pre}\}(\texttt{R},\texttt{strategy}) \{\texttt{Post}\}$ where \texttt{Pre} and \texttt{Post} are conditions specified in the given logic $\mathcal{L}$, \texttt{R} is a graph rewrite system and \texttt{strategy} is an expression stating how rules in \texttt{R} are to be performed. We prove that the calculus we introduce is sound. Moreover, we show how the proposed framework can be instantiated successfully with different logics. We investigate first-order logic and several of its decidable fragments with a particular focus on different dialects of description logic (DL). We also show, by using bisimulation relations, that some DL fragments cannot be used due to their lack of expressive power.

cs.LO↗

arXiv2014

SROIQsigma is decidable

We consider a dynamic extension of the description logic $\mathcal{SROIQ}$. This means that interpretations could evolve thanks to some actions such as addition and/or deletion of an element (respectively, a pair of elements) of a concept (respectively, of a role). The obtained logic is called $\mathcal{SROIQ}$ with explicit substitutions and is written $\mathcal{SROIQ^σ}$. Substitution is not treated as meta-operation that is carried out immediately, but the operation of substitution may be delayed, so that sub-formulae of $\mathcal{SROIQ}^σ$ are of the form $Φσ$, where $Φ$ is a $\mathcal{SROIQ}$ formula and $σ$ is a substitution which encodes changes of concepts and roles. In this paper, we particularly prove that the satisfiability problem of $\mathcal{SROIQ}^σ$ is decidable.

cs.LO↗