CRISNER: A Qualitative Preference Reasoner for CP-nets, TCP-nets, CP-Theories

CRISNER stands for Conditional and Relative Importance Statement Network PrEference Reasoner. It can reason about ceteris paribus preference languages such as CP-nets, TCP-nets and CP-theories. Given a preference specification (a set of preference statements) in one of these languages, CRISNER succinctly encodes its induced preference graph (IPG) into a Kripke structure model in the language of the NuSMV model checker. This Kripke model is reachability-equivalent to the induced preference graph. CRISNER generates the model only once, and then translates each query posed against this preference specification into a temporal logic formula in computation-tree temporal logic (CTL) such that the formula is verified in the Kripke model if and only if the query holds true according to the ceteris paribus semantics of the preference language. The model checker either affirms the query or returns with a counterexample. For answering queries related to equivalence and subsumption checking of two sets of preferences, CRISNER constructs a combined IPG and uses temporal queries in CTL to identify whether every dominance that holds in one also holds in the other, and vice-versa.

Versions and History

Justification of Answers to Preference Queries

CRISNER's reasoning is exact and provably correct for dominance, consistency, equivalence and subsumption queries. Because CRISNER uses a model checker for answering queries, CRISNER is also able to provide proofs or justifications to dominance of one outcome over another, inconsistency of a preference specifications, etc. CRISNER automatically builds proofs by collecting and examining the model checker output and producing a (flipping) sequence of preference statements.

Architecture

CRISNER is developed in pure Java and is domain-agnostic in the sense that any set of variables with any domain can be included in a preference specification, although it is optimized for variables with binary domains (due to the use of BDDs by the model checker). It accepts preference specifications and queries in a XML format, which provides a common and generic syntax using which users can specify preferences for CP-languages. The results (answers and proofs) for the corresponding queries are also saved in the form XML, so that the results can be further transformed into vocabulary that is more easily understandable by domain users.

Required Citations

nsmattei{at}gmail{dot}com
GitHub Logo   GitHub
s.j.rey{at}uva{dot}nl