Didier Buchs

Sahar Aljalbout, Gilles Falquet, Didier Buchs

Wikidata is a knowledge graph increasingly adopted by many communities for diverse applications. Wikidata statements are annotated with qualifier-value pairs that are used to depict information, such as the validity context of the statement, its causality, provenances, etc. Handling the qualifiers in reasoning is a challenging problem. When defining inference rules (in particular, rules on ontological properties (x subclass of y, z instance of x, etc.)), one must consider the qualifiers, as most of them participate in the semantics of the statements. This poses a complex problem because a) there is a massive number of qualifiers, and b) the qualifiers of the inferred statement are often a combination of the qualifiers in the rule condition. In this work, we propose to address this problem by a) defining a categorization of the qualifiers b) formalizing the Wikidata model with a many-sorted logical language; the sorts of this language are the qualifier categories. We couple this logic with an algebraic specification that provides a means for effectively handling qualifiers in inference rules. Using Wikidata ontological properties, we show how to use the MSL and specification to reason on qualifiers. Finally, we discuss the methodology for practically implementing the work and present a prototype implementation. The work can be naturally extended, thanks to the extensibility of the many-sorted algebraic specification, to cover more qualifiers in the specification, such as uncertain time, recurring events, geographic locations, and others.

Fabrice Kordon, Alban Linard, Marco Beccuti et al.

This document presents the results of the Model Checking Contest held at Petri Nets 2013 in Milano. This contest aimed at a fair and experimental evaluation of the performances of model checking techniques applied to Petri nets. This is the third edition after two successful editions in 2011 and 2012. The participating tools were compared on several examinations (state space generation and evaluation of several types of formulæ -- reachability, LTL, CTL for various classes of atomic propositions) run on a set of common models (Place/Transition and Symmetric Petri nets). After a short overview of the contest, this paper provides the raw results from the contest, model per model and examination per examination. An HTML version of this report is also provided (http://mcc.lip6.fr).

F. Kordon, A. Linard, D. Buchs et al.

This article presents the results of the Model Checking Contest held at Petri Nets 2012 in Hambourg. This contest aimed at a fair and experimental evaluation of the performances of model checking techniques applied to Petri nets. This is the second edition after a successful one in 2011. The participating tools were compared on several examinations (state space generation and evaluation of several types of formulae - structural, reachability, LTL, CTL) run on a set of common models (Place/Transition and Symmetric Petri nets). After a short overview of the contest, this paper provides the raw results from the context, model per model and examination per examination.