Publications

Effectively selling products online is a challenging task. Today's product domains often contain a dizzying variety of brands and models with highly complex sets of characteristics. This paper addresses the problem of supporting product search and selection in domains containing large numbers of alternatives with complex sets of features. A number of online shopping websites provide product choice assistance by making direct use of Multi-Attribute Utility Theory (MAUT). While the MAUT approach is appealing due to its solid theoretical foundations, there are several reasons that it does not fit well with people's decision making behavior.This paper presents an approach designed to better fit with people's natural decision making process. The system is called VMAP for Visualizing Multi-Attribute Preferences. VMAP provides on one screen both a multi-attribute preference tool (MAP-tool) and a product visualization tool (V-tool). The product visualization tool displays the set of available products, with each product displayed as a point in a 3D attribute space. By viewing the product space, users can gain an overview of the range of available products, as well as an understanding of the relationships between their attributes. The MAP-tool integrates expression of preferences and filter conditions, which are then immediately reflected in the V-tool display. In this way, the user can immediately see the consequences of his expressed preferences on the product space.The VMAP system is evaluated on a number of factors by comparing users' subjective ratings of the system to those of a more traditional MAUT product selection tool. The results show that while VMAP is somewhat more difficult to use than a traditional MAUT product selection tool, it provides better flexibility, provides the ability to more effectively explore the product domain, and produces more confidence in the selected product.

 This report aims at developing a technique for verifying if a timed automaton satisfies a linear duration constraint on the automaton states. The constraints are represented in the form of linear duration invariants - a simple class of Chop-free Duration Calculus (DC) formulas. We prove that linear duration invariants of a timed automaton are discretisable, and reduce checking if a timed automaton satisfies a linear duration invariant to checking if the integer timed region graph of the original automaton satisfies the same linear duration invariant. The latter can be done with exhausted search on graphs. In comparison to the techniques in the literatures, our one is more powerful; it works for the standard semantics of DC and general form of timed automata while the others cannot be applied.

 This Report shows the application of model checking techniques over formal specifications expressed in RSL using the FRD2 refinement checker, for which we have developed a first version of a translator from RSL to CSPM. We give an overview of the semantic and syntactic differences between these two languages, then we define a translation subset and finally we show the strategy used to find the respective equivalences in order to make the translation possible; we also briefly describe the development of the translator and show the use of this translator with some typical concurrent examples.