Possible Hyperworlds: representing Kripke models in RDF

Tracking #: 3701-4915

This paper is currently under review
Christopher Leturc
Fabien Gandon
Maxime Lefrançois

Responsible editor: 
Stefano Borgo

Submission type: 
Full Paper
Modal logic extends propositional logic by adding modal operators, and enables us to reason with concepts such as necessity, possibility, knowledge, belief, obligation, or consequences of actions. The most common way to interpret modal logic formulas is to apply the possible worlds semantics and to formally represent it with a Kripke model. Kripke models consist of a set of possible worlds, accessibility relations between possible worlds, and a valuation function that assigns to propositional atoms a truth value relative to those worlds. Existing work explored the connection between modal logic and Description Logics, including Modal Description Logics, and consider the inclusion of a Kripke model in their semantics. We are interested in considering a novel perspective, where we aim to represent in RDF a Kripke model, formulas from a modal logic language, and in which possible worlds such formulas are verified. Such a representation could have several applications: 1. contributing to a standard exchange format for modal logic applications, including reasoners; 2. facilitating the Open Science initiative in the modal logic research community; 3. supporting the representation and management of uncertainty or other modalities; and 4. facilitating interoperability between heterogeneous systems. As a starting point, our intuition is that a set of triples could be translated to a formula, and one could explicit in what possible worlds a formula is verified using metadata about this set of triples. Following that intuition, the main contribution of this article is to provide an RDF representation of normal Kripke models, applying the linked data principles and standards, focusing on identifying possible worlds and expressing the (N+1)-ary accessibility relations between them. We call possible hyperworld the result of this hypermedia approach to representing possible worlds. We discuss the different modeling alternatives for linking sets of triples to possible worlds, and for representing accessibility relations. We motivate one modeling choice, and compile our design rationale in a formal vocabulary for describing Kripke models: the Possible Worlds and Kripke Structures Ontology (PWKSO). Adopting a simple and generic usage pattern, we illustrate PWKSO with examples from epistemic multi-modal logic, dyadic deontic logic, and the dynamic logic of mental attitudes and joint actions (DL-MA). Perspectives and future work include 1. defining a translation, in the context of an RDF dataset, of sets of triples to modal logic formulas; 2. querying, instantiating, reasoning with possible hyperworlds; 3. nesting possible worlds or Kripke structures as a way to model Dynamic Epistemic Logics (DEL) or Propositional Dynamic Logics (PDL); 4. potential applications that leverage existing modal logic formalisms for example to merge knowledge graphs, represent the knowledge or beliefs of agents, represent the effects of actions or norms, or develop model checking applications.
Full PDF Version: 
Under Review