|
|
Research Interests
 | Reactive scheduling based on constraint logic programming |
| An efficient and flexible engine for computing fixed points |
| Logic Programming with Preferences |
| Optimization and Implementation of Programming
Languages |
| Parallel
and Distributed Processing |
| Formal
Methods and Software Engineering |
Working Projects
| Reactive scheduling |
We consider how to solve a reactive scheduling problem where the
environment keep changing and evolving. The constraint logic
programming system, with recent advances on efficient incremental
computation, programming with preferences and relaxation, provides a
declarative vehicle for modeling and solving reactive scheduling
problems
| An efficient and flexible engine for computing fixed points:
An efficient and flexible engine for computing fixed points is
critical for many practical applications. In this project, we firstly
investigate a goal-directed fixed point computation strategy in the
logic programming paradigm. The strategy adopts a tabled resolution
(or memorized resolution) to mimic the efficient semi-naive bottom-up
computation. Secondly, there are many situations in which a fixed
point contains a large number or even infinite number of solutions. In
these cases, a fixed point computation engine may not be efficient
enough or feasible at all. We present a mode-declaration scheme which
provides the capabilities to reduce a fixed point from a big solution
set to a preferred small one, or from an infeasible infinite set to a
finite one. The mode declaration scheme can be characterized as a
sequence of meta-level mapping operations over the original fixed
point.
|
| Logic Programming with Preferences:
Traditional constraint programming specifies an optimization problem
by using a set of constraints and minimizing (or maximizing) objective
functions. Unfortunately, general optimization problems may involve
compound objectives whose optima are difficult to be represented by a
simple minimization (or maximization). Even worse, for many
applications, especially those defined over structural domains, it is
difficult to specify any objective functions. In this project we
investigate a declarative method for specifying generalized
optimization problems based on comparison and selection among
alternative solutions. The method introduces a formal
predicate mode declaration for designating certain predicates as
optimization predicates, and uses preference rules for stating the
criteria for determining their optimal solutions. We provide an
implementation on how to extend a tabled Prolog system with declaring
and executing preferences. The execution of logic programs with
preferences is achieved in two steps. First, an automatic
transformation is applied to embed the preferences into the problem
specification to form an executable program. Second, the new program
is then evaluated using tabled resolution, while the mode declaration
provides a selection mechanism among the alternative solutions. We
show that the transformation scheme preserves the semantics for each
optimization predicate. Experimental results have shown that
preferences provide a declarative approach without sacrificing
efficiency.
|
| Implementation of Tabled CLP Systems
Simple techniques for
implementing tabled constraint logic programming systems are being investigated
in this project. Tabled LP systems are crucial for many important
applications of logic programming (model checking, program analysis,
non-monotonic reasoning). Recently, a new technique for implementing
tabling based on dynamic reordering of alternatives has been
proposed by us and implemented on top of the ALS commercial Prolog
systems. Work is in progress to incorporate negation, cuts and
parallelism.
|
| Scalable Parallel Implementation of Constraint Programs on
Distributed Network of SMPs Efficient scalable implementations of
Constraint Logic Programming Systems are being designed. To date, a
model based on stack-splitting has been proposed to realize efficient
distributed implementations of constraint-based system. The
implementation of this model on a distributed network of SMPs on top
of a sequential engine from ALS, Inc., is currently in progress.
|
| Denotation Semantics and Its Applications
The denotational approach developed for specifying semantics of
programming languages is being applied to formally specify software
systems. The role of Horn-logic and Constraints as a notation for
specifying denotations is also being studied. Coupled with partial
evaluation this has numerous applications from building provably
correct efficient compilers (sequential or parallelizing), to
automatic generation of efficient implementations and abstract
interpreters, to checking program correctness, etc.
One of the applications of denotation semantics is to build a
global translation appliance for translating Math Notations. This
projects deals with making mathematics, science, and technology
accessible to blind students. A translator is being developed from
Nemeth Math Braille notation (the Braille based notation for marking
up Mathematics for the blind) to Latex. The Nemeth Math Braille
notation was designed in 1951, and is quite complex. Use of
denotational semantics-based techniques as well as logic programming
has allowed us to develop a translator to Latex, a task that is
extremely hard using traditional compiling technology.
|
| Formal Methods and Software Engineering
A logic-based high-level computational framework is being studied and
applied to model checking and component-based system composition. This
research includes developing an efficient justification tool to
construct evidence automatically supporting XMC model checkers. We
recently proposed a new justification scheme based on program
transformation. With this new scheme, justification of a true literal
is generated as a side-effect of query evaluation on the transformed
program; while justification of a false literal can be obtained by in
the following two steps: (1) generating the dual definition of the
false literal based on its completed semantics, and then (2)
justifying the dual one of the original false literal.
My current research on component-based system composition is mainly on
modeling and constructing reliably hybrid systems. High-level domain
specific languages are being designed to model embedded components,
constraint logic programming adopted for automatic verification, and a
justification tool developed for synthesizing the reliable components
to the hybrid systems.
|
|
| |
|
