Possible Hyperworlds: representing Kripke models in RDF

This submission proposes to represent Kripke models in RDF. The authors show different
representations depending on the wanted notation, and propose a general terminology to
deal with the specific elements of Kripke models.

Let me start with the obvious: Kripke models are, essentially, labelled graphs. RDF triples
represent, essentially, labelled graphs. So it is not surprising that RDF can be used to
represent Kripke models. I also do not believe that a special insight is required to reach
this conclusion. On the positive side, the translations proposed by the authors are correct,
and indeed can represent the relevant information of a Kripke model.

What I do not understand is the motivation and application of this representation. I believe
that it is based on a misunderstanding by the authors. The authors claim that when dealing
with modal logic, the Kripke models of interest need to be given explicitly. I have never
encountered a scenario of this kind, and in fact that goes counter to my experience in
modal logic, where the main place is taken by the formula, and the interest is in the properties
of all models (or, dually, the existence of a model with some properties). If the "world" is
already decided (and fixed), then most of the interest in modalities is lost.

Then, even if the specific Kripke model is of interest, its RDF representation does not
provide any advantage. One cannot even check complex entailment in it.

I get the general impression that the authors have an important idea behind their interest
in this representation, but they do not make it explicit, and as it stands the general
framework seems unnecessary. In particular, making the 5 possible representations explicit
seems like an excess; one should suffice to provide the idea, and it can be translated to
others when needed.

The submission needs also quite some work starting from the preliminaries. The ideas are not
very well presented, and this could be the source of confusion. The authors jump from
"classical" modal logics, to those with multiple modalities, to those with n-ary modalities,
and back in a way that is very difficult to follow. Even their example of the binary modality
O does not fit with the semantics of n-ary modalities given later.

For all this reasons, I believe that this submission is still in need of some deep
improvements before being ready for publication.

REVIEW Paper ID 3701

1. Summary

The article illustrate an approach for the representation of Kripke models for propositional modal logic into RDF.

After providing a motivating introduction to their work, the authors present a running example based on a scenario involving reasoning in presence of heterogeneous data sources.

Then, after the (polyadic) modal logic preliminaries and the positioning of their approach with respect to others in the literature, the core encoding of Kripke structures and models into RDF is presented. Here, the fundamental idea is to represent that an atom is true at some world by stating that an RDF triple (expressing the propositional atom) is in turn in the "verifiedIn" or "noVerifiedIn" relation with a Possible Hyper-world. Several RDF notations are considered and discussed.

Subsequently, the authors show how to represent N-ary accessibility relations in their RDF framework, again comparing different modelling possibilities (lists and classes for relation instances).

In the following section, they present a small ontology that formalises the constructors and their properties presented so far.

Finally, the authors focus on discussing alternatives for functions that map RDF graphs into logical statements, and provide examples of SPARQL queries using the introduced RDF features. Some paragraphs on potential applications and a conclusive summary close the paper.

2. Evaluation

# Novelty and significance

In terms of novelty and significance, the contribution -- in its current state -- is definitely not groundbreaking. The core idea, to represent Kripke structures and models using RDFs triples, is quite natural and easy to grasp, and over the whole paper very little modelling techniques and remarks seem to stand out as extremely significant. FInally, the references should be significantly extended to include relevant literature on automated theorem proving in modal logic, description logics, modal description logics, and ontology-based data management. The applications are vague and sketchy, and much more should be said about positioning, related work, and concrete problems that such a proposal could address and solve.

# Technical quality and rigour

Technically, the paper is quite shallow as well. Again, most of the encodings regarding Kripke models (and related notions) in RDF are straightforward, and do not require neither particular hacks over the RDF capabilities, nor a deep understanding on the modal logic side (other than the very basic definitions). Some of the definitions here provided could benefit from better explanations on the RDF technicalities involved. The connections with other strictly frameworks, such as modal/temporal description logics or other many-dimensional formalisms, are only superficially mentioned, but no deeper analysis is provided (for instance, if an RDF triple is a logical statement that can actually be expressed as an assertional axiom of a description logic, I would expect that by relativising these statements to possible worlds one would get a natural fragment of a modal description logic).

# Clarity of presentation

The paper is quite easy to follow, although it could be significantly improved with respect to motivations and examples. With respect to the former, a wider and more concrete set of potential applications should be devised. With respect to the latter, a toy scenario involving a more complex formula evaluation would greatly improve the paper. Last but not least, many phrases are too vague and several claims are too generic to be properly evaluated (see "Detailed feedback" below). A thorough rewriting of these parts is definitely needed.

# General evaluation

Overall, I believe that the article in its current form requires a thorough round of major revision before being considered for publication in this venue.

3. Detailed feedback

- P. 2, LL. 24-32
This paragraph seems quite unsuccessful in explaining the "limitations of modal logic". What does it mean that the the models "must be given a priori"? To which reasoning problem(s) are the authors referring here, exactly? The subsequent sentences are equally obscure. Given that the claimed limitations of modal logic are not stated very clearly, the usefulness of Semantic Web technologies to overcome these supposed difficulties remains unconvincing. I suggest to rephrase the sentences of this paragraph so to be less vague.

- P. 2, LL. 33-40
This paragraph falls quite short in providing an overview of the integration of modalities in Semantic Web technologies. The mentioned references are actually taken from the modal and description logic literature. Rather than providing a simple example, I suggest the authors to widen the connections with the broad literature on automated reasoning and modal logics, description logics, ontology-based data management (with the inconsistency-handling literature as a particularly interesting case), etc.

- P. 2, LL. 41-51
Similarly to what mentioned above, I found this motivation paragraph quite vague and unconvincing. First, it would be helpful to provide some references associated with each of the mentioned applications, in order to allow the reader to find support in the literature regarding the problems that this contribution is supposed to address. Secondly, "enabling different families of motivating scenarios" sounds like a weak formulation: is it possible to strengthen it, and to actually show more concrete examples where the approach suggested by the authors could be of concrete help? Last but not least (and related to the above observations), please rephrase or make more precise very vague (albeit very common) claims such as "facilitate interoperability between heterogeneous systems".

- PP. 3-4
The Section "Running Example" (admittedly) contains a very simplistic example, and some of the elements involved in the figure do not seem to be even covered in detail by the contribution (for instance, the provenance of the data seems orthogonal to the content of the article). I suggest the authors to provide some more details on this topic in the remainder of the paper (possibly even as future work?), or to remove from the example (and the picture) some unnecessary elements that do not play any actual role.

- P. 3, L. 5
The title "State of the art" for this section, as well as the choice of the content, seems a bit inappropriate. I would suggest "Preliminaries" for a section that contains the actual technical preliminaries, and to split in a separate section the "Related Work and Positioning" parts.

- P. 10, L. 3
Regarding the phrase "Property :verifiedIn is then used to map a rdf:Statement to a :PossibleWorld", I believe it would be appropriate to briefly discuss how map a statement to a set of possible worlds, instead (as one would expect from the semantics). Did you devise an RDF encoding to explicitly allow for this? Or is it just a matter of repeating a property, e.g. by suitably adding triples that state in which other worlds a statement is true?

- P. 12, LL. 35-36
Are ", " here a shorthand of any kind? Is there any connection with RDF Containers or Collection (such as the lists used later on) that is worth mentioning already at this point? Please clarify this aspects, also with respect to the above observation of associating a statement to a set of worlds, rather than a single one.

-P. 20, LL. 43 and ffw.
The title "Discussing the function f" could be improved by explicitly mentioning what is the role played by f (e.g., "Mapping RDF triples into logical statements").

Overall, this section appears also quite preliminary (as indeed admitted by the authors themselves). I understand that the authors would like to keep open the choice of the mapping f, depending on applications, but it is unclear which properties this translation should respect in order to be considered satisfactory. For instance, focusing on the proposed example that maps the merge of RDF graphs into a conjunction, how should it behave with respect to negation? Is there even a way to represent operations on RDF graphs that can "mimic" all the boolean operators on formulas? Is there such a way at least for a positive/Horn fragment of modal logic (e.g., in the description logic notation, the logic EL)? Are there ontologies of logical expressions that can be modified and integrated in the proposed framework?

- P. 20, LL. 48-51
The remainder of the grammar for modal formulas at this point is completely unnecessary. I suggest to remove it.

- P. 21, LL. 10-11
It is unclear in which sense the authors claim that "some reasoner should treat such situations as violating the definition of Kripke models".

- P. 21, L. 14 & fwd.
What is the connection with Assertional axioms in modalised description logics and the RDF triples that you consider in this setting? Can something more be said about the connection between this formalisms, here and elsewhere in the paper?

- P. 21, LL. 32 & fwd.
The subsection on the representation of negation (and the subsequent on conjunction) deserves some more discussion. For instance, the RDF approach by the authors does not seem to provide any mechanism to connect the behaviour of "isNotVerifiedIn" with that of "isVerifiedIn" by using "isNegationOf". More in general, "isNotVerifiedIn" with that of "isVerifiedIn" (from above) do not seem to ever be stated as to represent mutually exclusive and jointly exhaustive occurrences.

- P. 24, L. 25
I would suggest to move the content of the footnote into the main text, and to expand the discussion on this, to make it easier for the reader to follow the example. Moreover, the content of the whole subsection should be greatly expanded: as it is now, the tile "Reasoning with PWKSO and SPARQL" seems a massive overstatement, given that the paragraph only claim to shows how to make the representation of an accessibility relation symmetric. What else can be done, and how? Is this section about frame conditions, or about reasoning? What is the impact of the former over the latter, and how do you envisage the integration of reasoning services within your framework? These question remain relatively unanswered.

P. 24, L. 42 & fwd.
The title could be shortened by removing what follows after the colon.

The whole paragraph, however, is too vague and unclear. At the beginning, are the authors also referring to modal description logics, and in general many-dimensional modal logic formalisms, in which one associates to states in one dimension a relational structure that represents states of another dimension (e.g., temporal description logics, with one dimension representing time points and the precedence relation between them, and the other dimension modelling objects and relations between them that evolve over time points)?

Moreover, what exactly is the connection with PDL and DEL? How are, for instance, the operators of PDL represented with this "nesting" trick? The content of the paragraph is too high-level to be properly understood and evaluated. It should be completely revised, expanded, and made more precise.

- P. 25, LL. 35 & fwd.
The overall "large panel of applications" (an expression that I suggest to revise anyway) is also quite vague and unsatisfactory. For instance, to justify the applicability of the proposed framework to knowledge graph merging and inconsistency handling, one would require a much stronger example than the toy scenario given at the beginning, or -- at least -- a detailed analysis of the problems that can be actually covered, and how such framework is better in dealing with them, compared to other approaches from the literature. How does this setting position with respect to modal description logics? Can the provided representation be somehow "embedded" in more expressive formalisms, and how? Many more references and details could be added to this conclusive part of the paper.

# Typos

- P. 3, L. 48: is "differed processing" intended? what does it mean?

- P. 6, L. 45: "modilizing" -> "modalizing"

- P. 13, L. 28: "This need to qualify" -> It should be "needs", but the whole sentence is not very clear? What is "This" referring to?

- P. 20, L. 37: "kripke" -> "Kripke"

- P. 21, L. 45: "isPresidentOf" -> "isNotPresidentOf"?

- P. 22, L. 36: "postulate." -> "postulate:"

The paper introduces a vocabulary, the Possible Worlds and Kripke Structures Ontology (PWKSO), for the representation of Kripke models in RDF Knowledge Graphs.

The authors first introduce their modelling idea and a motivating example. Then, basic definitions of Kripke models are provided, followed by a short summary of the current related approaches for the representation of modal concepts in Semantic Web languages. In what follows, the authors propose different solutions for representing possible worlds and accessibility relations in RDF and then present the final definition of the PWKSO ontology. The paper concludes with a discussion of the properties of the representation and its possible extensions for future work.

In general, the topics of enabling modal extensions of interpretations of Semantic Web languages and providing their representation in standard languages are clearly in the scope of the journal and useful for the KG community.

However, the work in its current state has several limitations with respect to the intended use of Kripke models, the relations with standard semantics, significance of the contribution for the PWKSO model and its evaluation.

In particular, the goal of the paper and the intended use of the ontology is not entirely clear. It appears that the final goal of the work is to enable the use of modal semantics in Semantic Web languages: however, what is presented is in fact a syntactic representation of a semantic structure.

The motivating example (Sec.2) is also unclear to me from a modal logic perspective: I would expect that modal operators (thus syntactic constructs) could be used to express the proposed knowledge scenario, instead of modelling and using for knowledge exchange a (minimal?) semantic model that verifies the intended interpretation.
Also, the motivating scenarios proposed in the introduction are not really motivated by some actual representation problem, but possible uses of the ontology.

What is not considered in the paper (while allowed by the provided definition of Kripke model) is that a Kripke structure can possibly be non-finite (which can be used to verify, for example, some temporal properties, as you mention in the possible applications).
No mention is given if it is possible to consider the PWKSO instances as "pre-models" for non-finite models.
Thus, the provided solution does not appear to be general enough: I suggest to restrict the kind of logics that the authors are interested to consider and prove that such representation can capture their semantics.
One of the possible uses (not mentioned) for the need to communicate a specific Kripke model is the recognition of a counter example (e.g. in a proof of a property of a system).
I also note that only the concept of validity in a model is defined in Sec.3, but the authors do not consider consequence (what can be verified by all models of a KB) and queries.

Also, it is not clear the relation with the semantics of complex formulas: the statements that are considered in the :verifiedIn statement appear to be only atomic statements.
Use of logical operators is just sketched in the interpretation of negation in Sec.4.1 and recognized as a needed extension in the final discussion: this needs to be better studied and the relation with the Kripke interpretations should be proved formally.

As noted above, no evaluation of the contributions is provided: for example, use in real use cases and implementation of specific modal logics could be studied.
Considering a specific Kripke based logic, correctness of the representation could be given as a proof showing that the representation is correct with respect to the definition of Kripke models for such logic.

Methods for modal extensions of DLs are discussed and the reference language for the ontology is OWL (thus with a DL based semantics): however, it is not clear how the proposed ontology can be used in combination with such semantics or, in general, by combining (OWL) knowledge from other ontology-based KBs.
Relation of the representation with the OWL semantics should be provided precisely: for example, it is mentioned the closed world assumption (CWA) as an option for reasoning with negation, but CWA is not standard in DLs and OWL (and in modal logics).

The presented representation methods in RDF are quite standard, thus from the point of view of the RDF representation, the novelty of the work is limited.
I suggest to consider also methods for representing contexts/modules in RDF/OWL for the representation of different points of view (like in the proposed example), which can be also globally inconsistent.

Given the problems noted above, the contributions of the paper are lacking in originality (with respect to the RDF representation) and the significance is not justified by a clear evaluation of the resource.

With respect to the writing and organization of the paper, there are some aspects that can be enhanced. For example, In Sec.3, in addition to the definition of Kripke models and representation methods, it would be useful to provide some example of the Kripke based semantics that could be represented with your model.
In Sec.3.2, the authors provide a short summary of modal extensions of DLs, but this is not then clearly used in the formalization and the positioning with respect to such semantics remains unclear.
Sec.3.3 could be enhanced by using some example of the presented modelling methods: however, this section can be reduced to a discussion of the alternative methods and presented after the actual formalization of the PWKSO model (and so, Sec.4.1 would be redundant).
Similarly for Sec.5, when explaining the possible ways of modelling accessibility relations.
In Sec.6, the complete listing of the PWKSO ontology is redundant (since the ontology is provided as an external resource): having an explanation of its elements is sufficient.

With respect to the data under "Long-term stable URL for resources":
- the organization of files is not supported by a README explaining their contents (the ontology documentation is an OwlDocGen generated HTML file).
- the complete ontology is provided as a single TTL file.
- the repository is a standard Zenodo repository, thus appropriate for long-term archival.
- the contents of the repository are complete, but more contents (like an implementation of the examples in the paper as a demonstration of the ontology use) could be included.