NEW Slides for AAAI 2014 Tutorial on Representing and Reasoning with Qualitative Preferences: Tools and Applications (pdf)

About

CRISNER is a practical reasoner tool for preferences expressed in qualitative preference languages. CRISNER is founded on decision theory, formal methods and software engineering.

Supported Features

Reasoning Tasks

* The functionalities for equivalence and subsumption checking is currently being integrated into CRISNER and tested. It will be available for download shortly.

Platform & Dependencies

CRISNER is implemented in Java. It requires the following dependencies.

Work in Progress

Getting CRISNER

Running CRISNER

To run CRISNER, ensure that NuSMV is installed and use one of the following commands, depending on whether you are starting with a preference specification or a query specification. The CRISNER.jar includes the needed java library dependencies listed above. If starting with a preference specification file (more about it below), then use the option "-s".
C:\Users\user>java -jar CRISNER.jar -s <"path to preference specification xml file"> -m <"path to NuSMV executable">
If starting with a query specification file (more about it below), then use the option "-q".
C:\Users\user>java -jar CRISNER.jar -q <"path to query specification xml file"> -m <"path to NuSMV executable">
In either case, the command line option should include the path to the NuSMV model checker executable, or an error will be reported.
USAGE:
 Please specify the model checker command to use AND the path to either:  (1) a preference specification file OR (2) query specification file.
 Example: "java -jar CRISNER.jar -m C:\Program files\NuSMV\bin\2.5.4\NuSMV.exe -s C:\Data\prefspec.xml" or "java -jar CRISNER.jar -m NuSMV -q query.xml"
For more on preference and query specification files, see examples below.

XML Syntax

Specifying preferences via an XML file

CRISNER accepts a preference specification for one of the above languages in a pre-specified XML format. The preference specification consists of a declaration of the preference variables, their domains and a set of preference statements each of which expresses a preference relation over the domain of that variable. There are examples below.

CRISNER then parses the XML to extract the preference rules and builds a corresponding SMV model (saved as a .smv file) suitable for model checking by the NuSMV model checker (version 2.5.4). This translation is based on our AAAI 2010 paper Dominance Testing via Model Checking and as presented in the AAAI 2014 tutorial.

Querying a preference specification

CRISNER allows querying a preference specification via either an XML file that specifies the reference preference specification, the query and its parameters, or via a reasoning menu served via the console interface when the tool is run with the "-s" option. Currently the tool supports dominance and consistency. In the future we plan to add anytime computation of an ordering of all outcomes (sequence of next-preferred outcomes respecting the preference rules); this is work in progress. If you are in need of this immediately, please send an email to get the latest working version for this functionality.

Downloadable Examples

  • Preference Subsumption and Equivalence Test

  • This menu option allows the user to check if the already specified preference specification induces preferences subsumed by those induced by another preference specification.
    C:\Users\user>java -jar CRISNER.jar -s samples\nocycle-cpnet\nocycle-cpnet.xml -m nusmv
    
    Parsing preference specification ... samples\nocycle-cpnet\nocycle-cpnet.xml
    
    Reasoning options:
    [1] Test Dominance
    [2] Test Dominance Performance
    [3] Test Consistency
    [4] Test Subsumption*
    [5] Test Equivalence*
    [9] Exit
    (* - For subsumption and equivalence, we currently require both specifications to have the same set of preference variables and respective domains.)
    Enter option: 4
    Please enter another XML preference specification to test subsumption: 
    Enter the location of the XML file: samples\nocycle-tcpnet\nocycle-tcpnet.xml
    Is nocycle-cpnet.xml subsumed by nocycle-tcpnet.xml ?
    Subsumption holds.
    true; nocycle-cpnet.xml is subsumed by nocycle-tcpnet.xml
    
    Reasoning options:
    [1] Test Dominance
    [2] Test Dominance Performance
    [3] Test Consistency
    [4] Test Subsumption*
    [5] Test Equivalence*
    [9] Exit
    (* - For subsumption and equivalence, we currently require both specifications to have the same set of preference variables and respective domains.)
    Enter option: 5
    Please enter another XML preference specification to test equivalence: 
    Enter the location of the XML file: samples\nocycle-tcpnet\nocycle-tcpnet.xml
    Is nocycle-cpnet.xml subsumed by nocycle-tcpnet.xml ?
    Subsumption holds.
    Is nocycle-tcpnet.xml subsumed by nocycle-cpnet.xml ?
    Subsumption does not hold.
    false; nocycle-cpnet.xml is not equivalent to nocycle-tcpnet.xml
    
    
    
    For further details regarding the usage of CRISNER or for help integrating CRISNER into your project, please contact me at the address on top of this page.
    Please cite the following paper which contains the theoretical foundations of the tool Dominance Testing via Model Checking by Santhanam et al. (AAAI 2010).
    Other publications related to preference reasoning

    Funding and Support

    The research activities of the project were supported in parts by US National Science Foundation grants CCF 1143734 and CCF 0702758.

    Collaborators