Dominance Testing via Model Checking

Authors

  • Ganesh Ram Santhanam Iowa State University
  • Samik Basu Iowa State University
  • Vasant Honavar Iowa State University

DOI:

https://doi.org/10.1609/aaai.v24i1.7599

Keywords:

Dominance, Qualitative Preferences, Preference Reasoning, Model Checking, Temporal Logic, Kripke Structure

Abstract

Dominance testing, the problem of determining whether an outcome is preferred over another, is of fundamental importance in many applications. Hence, there is a need for algorithms and tools for dominance testing. CP-nets and TCP-nets are some of the widely studied languages for representing and reasoning with preferences. We reduce dominance testing in TCP-nets to reachability analysis in a graph of outcomes. We provide an encoding of TCP-nets in the form of a Kripke structure for CTL. We show how to compute dominance using NuSMV, a model checker for CTL. We present results of experiments that demonstrate the feasibility of our approach to dominance testing.

Downloads

Published

2010-07-03

How to Cite

Santhanam, G. R., Basu, S., & Honavar, V. (2010). Dominance Testing via Model Checking. Proceedings of the AAAI Conference on Artificial Intelligence, 24(1), 357-362. https://doi.org/10.1609/aaai.v24i1.7599