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
- XML-based specification of preferences in a variety of qualitative preference languages -- CP-nets, TCP-nets, CP-Theories
- XML-based specification of preference queries (consistency, dominance) and their results for preferences stated in the above languages
- Preference reasoning via model checking -- by translating a preference specification into a Kripke Structure model and preference queries into temporal logic queries against this model Note: The translation is performed at the higher level of preference rules rather than at the level of the induced preference graph, i.e., it takes as input the preference rules in the preference specification and produces a succinct specification of the Kripke Structure model. Hence, CRISNER never constructs the induced preference graph upfront. For more details, see Dominance Testing via Model Checking
- Provide explanation of the result of preference queries -- proof of dominance, inconsistency (cycles in the induced preference graph)
Reasoning Tasks
- Dominance Testing
- Consistency Checking
- Dominance Performance Test
- *Preference equivalence (subsumption) Checking whether one set of preferences induces the same set (or a subset) of preferences over outcomes as induced by another set of preferences
Platform & Dependencies
CRISNER is implemented in Java. It requires the following dependencies.- Java Runtime Environment (tested with JRE 1.7)
Third party Java libraries used (dependencies): - NuSMV model checker version 2.5.4
Work in Progress
- Support for reasoning with CI-nets
- Handle multiple stakeholders at different levels of authority who may hold possibly conflicting preferences
- Additional reasoning tasks -- Computing an ordering of the outcomes (The next-best solution)
Getting CRISNER
- Please send me an email at gsanthan@iastate.edu or ganeshram.santhanam@gmail.com to get the latest version of 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.Querying using an XML file
CRISNER can accept queries for consistency and dominance via a pre-specified XML format see below. The XML contains the query type (consistency/dominance) and in the case of dominance queries, the dominating (better) and dominated (worse) outcomes are required.-
Querying via the console interface
When running the tool with the "-s" option, CRISNER provides a simple menu via the console interface using which the user can perform consistency, dominance queries against the given preference specification. The console additionally provides a way to perform dominance testing for a given number of randomly generated pairs of outcomes for a preference specification. -
Viewing Query Results
The results of a query contain a boolean result (true/false) and if applicable, a proof of the result, i.e., inconsistency (a cycle of outcomes) or a proof of dominance (a flipping sequence).
Downloadable Examples
Example 1a: Specifying a CP-net with consistent preferences (cycle-free induced preference graph)
Preference Specification
This basic preference specification for a CP-net shows how to declare variables and their domains, e.g., the following (excerpt from the above xml file) declares a preference variable
a
with a binary domain with values 0
and 1
. Note that these valuations can take string values that are combinations of letters and numbers.
<PREFERENCE-VARIABLE> <VARIABLE-NAME>a</VARIABLE-NAME> <DOMAIN-VALUE>0</DOMAIN-VALUE> <DOMAIN-VALUE>1</DOMAIN-VALUE> </PREFERENCE-VARIABLE>The following part of the specification declares a conditional preference over values of the variable
c
conditioned on the variable b
. Note that there can be multiple conditions or no conditions as well. In addition, there can also be multiple preferences for a variable, e.g., if there is a variable with domain of {0,1,TestVal}
then to specify the total order 0 > 1 > TestVal
one would encode 0 > 1
as one preference followed by 1 > TestVal
. The tool requires that the variable names and their assignments match with the preference variable declarations in the file.
<PREFERENCE-STATEMENT> <STATEMENT-ID>p3</STATEMENT-ID> <PREFERENCE-VARIABLE>c</PREFERENCE-VARIABLE> <CONDITION>b=0</CONDITION> <PREFERENCE>0:1</PREFERENCE> </PREFERENCE-STATEMENT>
Graphical Illustration of the CP-net
![Graphical Illustration of the CP-net](CRISNER/samples/nocycle-cpnet/nocycle-cpnet.png)
Induced Preference Graph
![Graphical Illustration of Induced Preference Graph](CRISNER/samples/nocycle-cpnet/nocycle-cpnet-ipg.png)
Translated SMV model
x
is encoded within the next(x)
section. This is how the tool succinctly encodes the preference specification without actually expanding the induced preference graph.
MODULE main VAR a : {0,1}; c : {0,1}; b : {0,1}; gch : {0,1}; FROZENVAR a_0 : {0,1}; b_0 : {0,1}; c_0 : {0,1}; IVAR cha : {0,1}; chb : {0,1}; chc : {0,1}; DEFINE start := a=a_0 & b=b_0 & c=c_0; INIT start=TRUE; TRANS a_0=next(a_0) & b_0=next(b_0) & c_0=next(c_0); ASSIGN next(a) := case a=1 & cha=1 & chb=0 & chc=0 : 0; -- #p1 : null => a=[0:1] >> [] TRUE : a; esac; next(c) := case c=1 & b=0 & cha=0 & chb=0 & chc=1 : 0; -- #p3 : [b=0] => c=[0:1] >> [] TRUE : c; esac; next(b) := case b=0 & c=0 & cha=0 & chb=1 & chc=0 : 1; -- #p2 : [c=0] => b=[1:0] >> [] TRUE : b; esac; next(gch) := case a=1 & cha=1 & chb=0 & chc=0 : 1; c=1 & b=0 & cha=0 & chb=0 & chc=1 : 1; b=0 & c=0 & cha=0 & chb=1 & chc=0 : 1; TRUE: 0; esac;
Example 1b: Reasoning with a CP-net (cycle-free induced preference graph)
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: 3 Consistent Result: TRUE; Query File: samples\nocycle-cpnet\nocycle-cpnet.xml-consistencyquery.xml
Consistency Checking via a query file
(Query) (Result)C:\Users\user>java -jar CRISNER.jar -q samples\nocycle-cpnet\nocycle-cpnet.xml-consistencyquery.xml -m nusmv Parsing query specification ... samples\nocycle-cpnet\nocycle-cpnet.xml-consistencyquery.xml Consistent Result: TRUE; Query File: samples\nocycle-cpnet\nocycle-cpnet.xml-consistencyquery.xml
Dominance Testing
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: 1 Dominating alternative a = ? 0 b = ? 1 c = ? 0 Dominated alternative a = ? 1 b = ? 0 c = ? 1 Please specify a file name to save query (optional): nocycle-cpnet-q1.xml Result: TRUE; Proof: Sequence: [c = 1, a = 1, b = 0] -> [c = 1, a = 1, b = 0] -> [c = 0, a = 1, b = 0] -> [c = 0, b = 1, a = 1] -> [c = 0, b = 1, a = 0]; Query File: samples\nocycle-cpnet\nocycle-cpnet-q1.xml Continue with another dominance test? [Y/N]
Does <0,1,0> dominate <1,1,1>?
(Query) (Result)Continue with another dominance test? [Y/N] y Dominating alternative a = ? 0 b = ? 1 c = ? 0 Dominated alternative a = ? 1 b = ? 1 c = ? 1 Please specify a file name to save query (optional): nocycle-cpnet-q2.xml Result: FALSE; Query File: samples\nocycle-cpnet\nocycle-cpnet-q2.xml Continue with another dominance test? [Y/N]
Example 2: CP-net with inconsistent preferences (cyclic induced preference graph)
Preference Specification
Graphical Illustration of the CP-net
Induced Preference Graph
Translated SMV model
![Graphical Illustration of the CP-net](CRISNER/samples/cycle-cpnet/cycle-cpnet.png)
![Graphical Illustration of the Induced Preference Graph](CRISNER/samples/cycle-cpnet/cycle-cpnet-ipg.png)
MODULE main VAR c : {0,1}; b : {0,1}; a : {0,1}; gch : {0,1}; FROZENVAR a_0 : {0,1}; b_0 : {0,1}; c_0 : {0,1}; IVAR cha : {0,1}; chb : {0,1}; chc : {0,1}; DEFINE start := a=a_0 & b=b_0 & c=c_0; INIT start=TRUE; TRANS a_0=next(a_0) & b_0=next(b_0) & c_0=next(c_0); ASSIGN next(c) := case c=0 & a=0 & cha=0 & chb=0 & chc=1 : 1; -- #p4 : [a=0] => c=[1:0] >> [] c=1 & b=0 & cha=0 & chb=0 & chc=1 : 0; -- #p3 : [b=0] => c=[0:1] >> [] TRUE : c; esac; next(b) := case b=0 & c=0 & cha=0 & chb=1 & chc=0 : 1; -- #p2 : [c=0] => b=[1:0] >> [] TRUE : b; esac; next(a) := case a=1 & cha=1 & chb=0 & chc=0 : 0; -- #p1 : null => a=[0:1] >> [] TRUE : a; esac; next(gch) := case c=0 & a=0 & cha=0 & chb=0 & chc=1 : 1; c=1 & b=0 & cha=0 & chb=0 & chc=1 : 1; b=0 & c=0 & cha=0 & chb=1 & chc=0 : 1; a=1 & cha=1 & chb=0 & chc=0 : 1; TRUE: 0; esac;
Consistency Checking
(Query) (Result)C:\Users\user>java -jar CRISNER.jar -s samples\cycle-cpnet\cycle-cpnet.xml -m nusmv Parsing preference specification ... samples\cycle-cpnet\cycle-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: 3 Cycle found. Sequence: [c = 1, a = 0, b = 0] -> [c = 0, a = 0, b = 0] -> [c = 1, a = 0, b = 0] Result: FALSE; Proof: Sequence: [c = 1, a = 0, b = 0] -> [c = 0, a = 0, b = 0] -> [c = 1, a = 0, b = 0]; Query File: samples\cycle-cpnet\cycle-cpnet.xml-consistencyquery.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:
Example 3: TCP-net with consistent preferences (cycle-free induced preference graph)
Preference Specification
Notice that the relative importance of a over b is specified by stating that the intra-variable PREFERENCE over valuations of a is REGARDLESS-OF b as in the below excerpt.
<PREFERENCE-STATEMENT> <STATEMENT-ID>p1</STATEMENT-ID> <PREFERENCE-VARIABLE>a</PREFERENCE-VARIABLE> <PREFERENCE>0:1</PREFERENCE> <REGARDLESS-OF>b</REGARDLESS-OF> </PREFERENCE-STATEMENT>
Graphical Illustration
![TCP-net graph](CRISNER/samples/nocycle-tcpnet/nocycle-tcpnet.png)
Induced Preference Graph
![TCP-net induced preference graph](CRISNER/samples/nocycle-tcpnet/nocycle-tcpnet-ipg.png)
Translated SMV model
MODULE main VAR b : {0,1}; c : {0,1}; a : {0,1}; gch : {0,1}; FROZENVAR a_0 : {0,1}; b_0 : {0,1}; c_0 : {0,1}; IVAR cha : {0,1}; chb : {0,1}; chc : {0,1}; DEFINE start := a=a_0 & b=b_0 & c=c_0; INIT start=TRUE; TRANS a_0=next(a_0) & b_0=next(b_0) & c_0=next(c_0); ASSIGN next(b) := case a=1 & cha=1 & chb=1 & chc=0 : {0,1}; -- #p1 : [] => a=[0:1] >> [b] b=0 & c=0 & cha=0 & chb=1 & chc=0 : 1; -- #p2 : [c=0] => b=[1:0] >> [] TRUE : b; esac; next(c) := case c=1 & b=0 & cha=0 & chb=0 & chc=1 : 0; -- #p3 : [b=0] => c=[0:1] >> [] TRUE : c; esac; next(a) := case a=1 & cha=1 & chb=1 & chc=0 : 0; -- #p1 : [] => a=[0:1] >> [b] TRUE : a; esac; next(gch) := case a=1 & cha=1 & chb=1 & chc=0 : 1; b=0 & c=0 & cha=0 & chb=1 & chc=0 : 1; c=1 & b=0 & cha=0 & chb=0 & chc=1 : 1; a=1 & cha=1 & chb=1 & chc=0 : 1; TRUE: 0; esac;
Dominance Performance Test
C:\Users\user>java -jar CRISNER.jar -s samples\nocycle-tcpnet\nocycle-tcpnet.xml -m nusmv Parsing preference specification ... samples\nocycle-tcpnet\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: 2 Enter number of specifications to test: 5 QUERY 1 (a=0 & b=0 & c=1) -> EX EF (a=1 & b=0 & c=0) QUERY 2 (a=1 & b=0 & c=1) -> EX EF (a=1 & b=0 & c=0) QUERY 3 (a=0 & b=1 & c=1) -> EX EF (a=0 & b=1 & c=1) QUERY 4 (a=1 & b=1 & c=1) -> EX EF (a=0 & b=0 & c=0) QUERY 5 (a=0 & b=0 & c=0) -> EX EF (a=1 & b=1 & c=0) Dominance does not hold Result: FALSE; Query File: samples\nocycle-tcpnet\nocycle-tcpnet.xml-query1.xml QUERY 1 false 137 ms Dominance does not hold Result: FALSE; Query File: samples\nocycle-tcpnet\nocycle-tcpnet.xml-query2.xml QUERY 2 false 107 ms Dominance does not hold as the outcomes are equal Result: FALSE; Query File: samples\nocycle-tcpnet\nocycle-tcpnet.xml-query3.xml QUERY 3 false 90 ms Dominance does not hold Result: FALSE; Query File: samples\nocycle-tcpnet\nocycle-tcpnet.xml-query4.xml QUERY 4 false 104 ms Dominance holds. Sequence: [c = 0, b = 1, a = 1] -> [] -> [a = 0, b = 0] Sequence: [c = 0, b = 1, a = 1] -> [c = 0, b = 1, a = 1] -> [c = 0, a = 0, b = 0] Proof of dominance: Sequence: [c = 0, b = 1, a = 1] -> [c = 0, b = 1, a = 1] -> [c = 0, a = 0, b = 0] Result: TRUE; Proof: Sequence: [c = 0, b = 1, a = 1] -> [c = 0, b = 1, a = 1] -> [c = 0, a = 0, b = 0]; Query File: samples\nocycle-tcpnet\nocycle-tcpnet.xml-query5.xml QUERY 5 true 119 ms Average time per dominance test: 111 ms
Preference Subsumption and Equivalence Test
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.xmlFor 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
- Dr. Samik Basu Department of Computer Science, Iowa State University
- Dr. Vasant Honavar College of Information Science and Technology, Penn State University