| Selected Projects
A
World View Solver for Epistemic Logic Programs
The world view semantics for epistemic logic program was proposed by Gelfond in his 1994
paper "Logic programming and reasoning with incomplete information" (Annals of
Mathematics and Artificial Intelligence, 12 (1994) 98-116). It extends the answer set
semantics for disjunctive logic programs and allows the reasoning with the agent's beliefs
and knowledge.
We have implemented a prototype called Wviews that computes the world views for a given
epistemic logic program. Wviews works in the following way: it takes an epistemic logic
program as input, then guesses an epistemic valuation for all subjective literals
occurring in the program and transform the input program to an extended disjunctiv logic
program. Finally, by calling dlv, Wviews computes all answer sets of this extended
disjunctive logic program and verify whether the collection of these answer sets is a
world view of the input epistemic logic program. Many detailed optimization methods have
been implmented in order to prune the search space.
Wviews now can be downloaded from:
http://www.scm.uws.edu.au/~yan/Wviews.html
[Back to Top]
Theory of
Forgetting in Logic Programs
In this project, we consider how to forget a set of atoms in a logic program. Intuitively,
when a set of atoms is forgotten from a logic program, all atoms in the set should be
eliminated from this program in some way, and other atoms related to them in the program
might also be affected. We define notions of strong and weak forgettings in logic programs
to capture such intuition, reveal their close connections to the notion of forgetting in
classical propositional theories, and provide a precise semantic characterization for
them. Based on these notions, we then develop a general framework for conflict solving in
logic programs. We investigate various semantic properties and features in relation to
strong and weak forgettings and conflict solving in the proposed framework. We argue that
many important conflict solving problems can be represented within this framework. In
particular, we show that all major logic program update approaches can be transformed into
our framework, under which each approach becomes a specific conflict solving case with
certain constraints.
Relevant publications are as follows:
- Y. Zhang and N.Y. Foo, Solving logic program conflict through strong and weak
forgettings. Artificial Intelligence (AIJ). 170 (2006) 739-778.
- Y. Zhang and N.Y. Foo, A unified framework for representing logic program updates. In
Proceedings of the 20th National Conference on Artificial Intelligence (AAAI 2005), pp
707-712. AAAI Press 2005.
- Y. Zhang, N.Y. Foo and K. Wang, Solving logic program conflicts through strong and weak
forgettings. In Proceedings of the 19th International Joint Conference on Artificial
Intelligence (IJCAI 2005), pp 627-632. Morgan Kaufmann Publishers, Inc. 2005.
[Back to Top]
Bargaining Theory and Automated
Negotiation
Bargaining is a traditional research topic in economics initiated by John Nash in 1950. We
explore the theme from AI point of view by modelling reasoning behind bargaining
processes. We express bargaining situations in logical form and model bargaining games
with a combinatorial form of belief revision and game theory. We have proposed a logic
solution to the bargaining problem, which has a sound and complete axiomatic
characterization. Such an axiomatization is a combination of belief revision postulates
and game theoretic axioms. We have also proposed a set of other logic-based solutions to
deal with ordinal bargaining and bargaining with mixed deals. The whole framework
initiates a new methodology of bargaining analysis and would help us to identify the
logical reasoning behind bargaining processes
Relevant publications are as follows:
- D. Zhang, Reasoning about bargaining situations. In Proceedings of the 22nd AAAI
Conference on Artificial Intelligence (AAAI-07), 154-159, 2007.
- Jin, M. Thielscher and D. Zhang, Mutual belief revision: semantics and computation. In
Proceedings of the 22nd AAAI Conference on Artificial Intelligence (AAAI-07), 440-445,
2007.
- D. Zhang and Y. Zhang, A computational model of logic-based negotiation. In Proceedings
of the 21st National Conference on Artificial Intelligence (AAAI-06), 728-733, 2006.
- D. Zhang, A logical model for Nash bargaining solution. In Proceedings of the Nineteenth
International Joint Conference on Artificial Intelligence (IJCAI-05), 983-988, 2005.
[Back to Top]
Jackaroo Trading
Agent System
Trading agent design and analysis has been one of the main research interests in ISL since
2003. We have built a trading agent system, named jackaroo, which participated in the
International Trading Agent Competitions (TAC) in last five years. The agent is built upon
the economic model of TAC markets and initiated the approach of equilibrium analysis to
strategic trading agents. Jackaroo agent has achieved significant results in previous TAC
games: the 4th place in TAC-07 CAT final, the 11th in TAC-06 SCM final, the 2nd place in
TAC-05 SCM qualifying, the 1st place in TAC-05 SCM qualifying and the 3rd place in TAC-03
SCM qualifying.
Relevant publications are as follows:
- M. Furuhata and D. Zhang, Capacity allocation with competitive retailers. In Proceedings
of the Eighth International Conference on Electronic Commerce (ICEC-06), 31-37, 2006.
- D. Zhang, Negotiation mechanism for TAC SCM component market. In Proceedings of the 4th
International Conference on Autonomous Agent and Multiagent Systems(AAMAS-05), 288-295,
2005.
- D. Zhang, K. Zhao, C-M. Liang, G. Begum, and T-H. Huang, Strategic trading agents via
market modelling, ACM SIGecom Exchange,4(3), 46-55, 2004.
[Back to Top]
Model
Update for System Modifications
Model checking is a promising technology, which has been applied for verification of many
hardware and software systems. In this paper, we introduce the concept of model update
towards the development of an automatic system modification tool that extends model
checking functions. We define primitive update operations on the models of Computation
Tree Logic (CTL) and formalize the principle of minimal change for CTL model update. These
primitive update operations, together with the underlying minimal change principle, serve
as the foundation for CTL model update. Essential semantic and computational
characterizations are provided for our CTL model update approach. We then describe a
formal algorithm that implements this approach. We also illustrate two case studies of CTL
model updates for the well-known microwave oven example and the Andrew File System 1, from
which we further propose a method to optimize the update results in complex system
modifications.
Relevant publications are as follows:
- Y. Zhang and Y. Ding, CTL model update for system modifications. Journal of Artificial
Intelligence Research (JAIR) 31 (2008) 113-155.
- Y. Ding and Y. Zhang, CTL model update: Semantics, computations and implementation. In
Proceedings of the 17th Europen Conference on Artificial Intelligence (ECAI 2006), pp
362-366. IOS Press 2006.
- Y. Ding and Y. Zhang, A case study for CTL model update. In Proceedings of the 1st
International Conference on Knowledge Systems, Engineering and Management (KSEM 2006), pp
88-101. Springer 2006.
[Back to Top]
Object
Tracking in Video Sequences
Tracking an object of a non-rigid body shape in a video sequence is an exciting and yet
very challenging task, especially under the non-ideal environment such as illumination
variation, shape deformation, partial occlusion, shade occurrence, clutter and moving
background, as well as camouflages by the background. The effective techniques can be as
intuitive as geometric explorations, or as advanced as in-depth mathematical and
statistical models. We have already explored a number of strategies and methodologies
including weighted region consolidation, refinement via confidence voting, positioning via
dominant features, color kernel densities, as well as the Bayesian propagation of
contours. Accuracy and efficiency are the two major objectives of such object tracking,
although a tradeoff of these two is often required.
[Back to Top]
Image
Watermarking, Compression, and Indexing
Watermarking and compression for images or videos can be considered either together or
independently. A watermarking scheme provides a mechanism to embed or hide such as
copyright information into a piece of multimedia without causing visible quality
degradation, while the compression scheme aims to represent a multimedia object such as an
image with a much smaller storage, with or without losing any degree of fidelity.
We proposed several wavelet-based watermarking schemes to better defend against image
rescaling, illumination change, cropping and some other potential watermark attacks. Some
new bi-orthogonal wavelet filters have also been derived in this connection. In terms of
image compression, we developed a generalised scheme based on weighted finite automata
which characterise the similarities among the subimages. On image indexing, on the other
hand, semantic classification of web images have been investigated to unify keywords and
visual contents in image retrieval.
References
- Target positioning with dominant feature elements, by Huang Z and Jiang Z, Computer
Analysis of Images and Patterns, 12th International Conference on Computer Analysis of
Images and Patterns (CAIP), Vienna, Lecture Notes in Computer Science 4673, (2007)69-76.
- An object tracking scheme based on local density, by Huang Z and Jiang Z, International
MultiMedia Modeling Conference (MMM), Lecture Notes in Computer Science 4351,
(2007)166-175.
- Image Watermarking via Sequencing Wavelet Filters, by Huang Z and Jiang Z, International
Conference on Communications, Circuits and Systems, to appear, May 2008.
- Semantic classification of web images for efficient image retrieval, by Jayaratne
K L, Ginige A and Jiang Z, International Conference on Computational Intelligence for
Modelling, Control and Automation and International Conference on Intelligent Agents, Web
Technologies and Internet Commerce Vol-1 (CIMCA-IAWTIC'06) Vienna, Austria, IEEE Computer
Society (2005)464-470.
- Unification and extension of weighted finite automata applicable to image compression,
by Jiang Z, O de Vel and Litow B, Theoretical Computer Science A, vol 302/1-3,
(2003)275-294.
[Back to Top] |
