Reasoning about Solids Using Constraint Logic Programming

The embedding of constraint satisfaction on the domain of discourse into a rule-based programming paradigm like logic programming provides a powerful reasoning tool. We present an application in spatial reasoning that uses this combination to produce a clear, concise, yet very expressive system through its ability to manipulate partial information. Three-dimensional solid objects in constructive solid geometry representation are manipulated, and their spatial relationship with one another, points, or regions is reasoned about. The language used to develop this application is QUAD-CLP(), an experimental constraint logic programming language of our own design, which is equipped with a solver for quadratic and linear arithmetic constraints over the reals.     

Higher-order communications for concurrent programming

In Pettorossi and Skowron (1983) a recursive-equations language is introduced. Its operational semantics is specified by means of computing agents which communicate and exchange messages. Those communications are, so to speak, zero-order, in the sense that the exchanged messages are values of a data structure, possibly defined by the programmer.

In this paper we extend that approach and we consider also ‘higher-order’ communications by allowing the exchange of agents behaviours, i.e. sets of computations, among computing agents. This extension leads to a new programming methodology which makes use of proofs of computing agents behaviours and their related strategies.     

Towards verification of computation orchestration

Recently, a promising programming model called Orc has been proposed to support a structured way of orchestrating distributed Web Services. Orc is intuitive because it offers concise constructors to manage concurrent communication, time-outs, priorities, failure of Web Services or communication and so forth. The semantics of Orc is precisely defined. However, there is no automatic verification tool available to verify critical properties against Orc programs. Our goal is to verify the orchestration programs (written in Orc language) which invoke web services to achieve certain goals. To investigate this problem and build useful tools, we explore in two directions. Firstly, we define a Timed Automata semantics for the Orc language, which we prove is semantically equivalent to the operational semantics of Orc. Consequently, Timed Automata models are systematically constructed from Orc programs. The practical implication is that existing tool supports for Timed Automata, e.g., Uppaal, can be used to simulate and model check Orc programs. An experimental tool has been implemented to automate this approach. Secondly, we start with encoding the operational semantics of Orc language in Constraint Logic Programming (CLP), which allows a systematic translation from Orc to CLP. Powerful constraint solvers like CLP \({(\mathcal{R})}\) are then used to prove traditional safety properties and beyond, e.g., reachability, deadlock-freeness, lower or upper bound of a time interval, etc. Counterexamples are generated when properties are not satisfied. Furthermore, the stepwise execution traces can be automatically generated as the simulation steps. The two different approaches give an insight into the verification problem of Web Service orchestration. The Timed Automata approach has its merits in visualized simulation and efficient verification supported by the well developed tools. On the other hand, the CPL approach gives better expressiveness in both modeling and verification. The two approaches complement each other, which gives a complete solution for the simulation and verification of Computation Orchestration.     

Intelligent backtracking in CLP(ℜ)

CLP() is a constraint logic programming language in which constraints can be expressed in the domain of real numbers. Computation in this specialized domain gives access to information useful in intelligent backtracking. In this paper, we present an efficient constraint satisfaction algorithm for linear constraints in the real number domain and show that our algorithm directly generates minimal sets of conflicting constraints when failures occur. We demonstrate how information gleaned during constraint satisfaction can be integrated with unification failure analysis. The resulting intelligent backtracking method works in the context of a two-sorted domain, where variables can be bound to either structured terms or real number expressions. We discuss the implementation of backtracking and show examples where the benefit of pruning the search tree outweights the overhead of failure analysis.     

OCL 1.4/5 vs. 2.0 Expressions Formal semantics and expressiveness

A type inference system and a big-step operational semantics for expressions of the Object Constraint Language (OCL), the declarative and navigational constraint language for the Unified Modeling Language (UML), are provided; the account is mainly based on OCL 1.4/5, but also includes the main features of OCL 2.0. The formal systems are parameterised in terms of UML static structures and UML object models, which are treated abstractly. It is proved that the operational semantics satisfies a subject reduction property with respect to the type inference system. Proceeding from the operational semantics and providing a denotational semantics, pure OCL 2.0 expressions are shown to exactly represent the primitive recursive functions, whereas pure OCL 1.4/5 expressions are Turing complete.     

Stochastic Constraint Programming: A Scenario-Based Approach

To model combinatorial decision problems involving uncertainty and probability, we introduce scenario based stochastic constraint programming. Stochastic constraint programs contain both decision variables, which we can set, and stochastic variables, which follow a discrete probability distribution. We provide a semantics for stochastic constraint programs based on scenario trees. Using this semantics, we can compile stochastic constraint programs down into conventional (non-stochastic) constraint programs. This allows us to exploit the full power of existing constraint solvers. We have implemented this framework for decision making under uncertainty in stochastic OPL, a language which is based on the OPL constraint modelling language [Van Hentenryck et al., 1999]. To illustrate the potential of this framework, we model a wide range of problems in areas as diverse as portfolio diversification, agricultural planning and production/inventory management.     

Semantics of OCL specified with QVT

The Object Constraint Language (OCL) has been for many years formalized both in its syntax and semantics in the language standard. While the official definition of OCL’s syntax is already widely accepted and strictly supported by most OCL tools, there is no such agreement on OCL’s semantics, yet. In this paper, we propose an approach based on metamodeling and model transformations for formalizing the semantics of OCL. Similarly to OCL’s official semantics, our semantics formalizes the semantic domain of OCL, i.e. the possible values to which OCL expressions can evaluate, by a metamodel. Contrary to OCL’s official semantics, the evaluation of OCL expressions is formalized in our approach by model transformations written in QVT. Thanks to the chosen format, our semantics definition for OCL can be automatically transformed into a tool, which evaluates OCL expressions in a given context. Our work on the formalization of OCL’s semantics resulted also in the identification and better understanding of important semantic concepts, on which OCL relies. These insights are of great help when OCL has to be tailored as a constraint language of a given DSL. We show on an example, how the semantics of OCL has to be redefined in order to become a constraint language in a database domain.

Modelling agent communication in a first order logic

In the design of information systems, the notion of agent has proven useful. When modelling communication among agents, deontic concepts, such as obligations, permissions, and prohibitions are essential. The dynamics of obligations, i.e. how obligations are created and destroyed, can effectively be described by means of notions from speech act theory. In this paper, we present a language that includes deontic and illocutionary constructs for the modelling of communication between agents. The language is a logic programming language, which gives it a simple semantics and makes it executable. A distinguishing feature of the language is that it is able to represent time explicitly, which is required to give an adequate semantics for deontic constructs.     

Abstract Interpretation for Termination Analysis in Functional Active Databases

An active database consists of a traditional database supplemented by a set of Event-Condition-Action (ECA) rules. One of the key questions for active database designers is that of termination of the ECA rules. The behaviour of the ECA rules may be obscure and their semantics is often not specified formally. Consequently, developing termination analysis algorithms and proving their correctness is a challenging task. In this paper we address this problem for functional active databases by adopting an abstract interpretation approach. By functional active databases we mean active databases whose transaction execution semantics have been expressed in a purely functional language. Although we demonstrate our techniques for a specific active DBMS which supports a functional database programming language interface, these techniques are directly applicable to other active DBMSs whose execution semantics have been specified using a functional or a denotational approach.     

Scheme: A Interpreter for Extended Lambda Calculus

Inspired by ACTORS [7, 17], we have implemented an interpreter for a LISP-like language, SCHEME, based on the lambda calculus [2], but extended for side effects, multiprocessing, and process synchronization. The purpose of this implementation is tutorial. We wish to: 1.alleviate the confusion caused by Micro-PLANNER, CONNIVER, etc., by clarifying the embedding of non-recursive control structures in a recursive host language like LISP. 2.explain how to use these control structures, independent of such issues as pattern matching and data base manipulation. 3.have a simple concrete experimental domain for certain issues of programming semantics and style. This paper is organized into sections. The first section is a short reference manual containing specifications for all the unusual features of SCHEME. Next, we present a sequence of programming examples which illustrate various programming styles, and how to use them. This will raise certain issues of semantics which we will try to clarify with lambda calculus in the third section. In the fourth section we will give a general discussion of the issues facing an implementor of an interpreter for a language based on lambda calculus. Finally, we will present a completely annotated interpreter for SCHEME, written in MacLISP [13], to acquaint programmers with the tricks of the trade of implementing non-recursive control structures in a recursive language like LISP.This report describes research done at the Artificial Intelligence Laboratory of the Massachusetts Institute of Technology. Support for the laboratory's artificial intelligence research is provided in part by the Advanced Research Projects Agency of the Department of Defense under Office of Naval Research contract N00014-75-C-0643.     

MALLET - a multi-agent logic language for encoding teamwork

MALLET, a multi-agent logic language for encoding teamwork, is intended to enable expression of teamwork emulating human teamwork, allowing experimentation with different levels and forms of inferred team intelligence. A consequence of this goal is that the actual teamwork behavior is determined by the level of intelligence built into the underlying system as well as the semantics of the language. In this paper, we give the design objectives, the syntax, and an operational semantics for MALLET in terms of a transition system. We show how the semantics can be used to reason about the behaviors of team-based agents. The semantics can also be used to guide the implementation of various MALLET interpreters emulating different forms of team intelligence, as well as formally study the properties of team-based agents specified in MALLET. We have explored various forms of proactive information exchange behavior embodied in human teamwork using the CAST system, which implements a built-in MALLET interpreter.     

A Fully Abstract Semantics for Concurrent Constraint Programming

A compositional and fully abstract semantics for concurrent constraint programming is developed. It is the first fully abstract semantics which takes into account both non-determinism, infinite computations, and fairness. We present a simple concurrent constraint programming language, whose semantics is given by a set of reduction rules augmented with fairness requirements. In the fully abstract semantics we consider two aspects of a trace, viz. the function computed by the trace (the functionality) and the set of input and output data (the limit of the trace). We then derive the fully abstract semantics from the set of traces using a closure operation. We give two proofs of full abstraction; the first relies on the use of a syntactically infinite context. The second proof requires only a finite context, but assumes as input a representation of the function to be computed by the context. Finally, we examine the algebraic properties of the programming language with respect to the fully abstract semantics. It turns out that the non-deterministic selection operation can be defined using operations derived from parallel composition and the usual set-theoretic operations on sets of traces.     

Semantics for a Quantum Programming Language by Operator Algebras

This paper presents a novel semantics for a quantum programming language by operator algebras, which are known to give a formulation for quantum theory that is alternative to the one by Hilbert spaces. We show that the opposite of the category of W*-algebras and normal completely positive subunital maps is an elementary quantum flow chart category in the sense of Selinger. As a consequence, it gives a denotational semantics for Selinger’s first-order functional quantum programming language. The use of operator algebras allows us to accommodate infinite structures and to handle classical and quantum computations in a unified way.     

Agent通信语言及相关理论的研究

在多代理系统里，为了实现某一目标，Agent需要通信和交互。因此，设计一个理想的Agent通信语言就显得十分重要。Agent通信语言的实现涉及的因素，除了语言本身外，还包括Agent理论、语义、证明和会话策略等。该文就Agent通信语言和相关理论作了简单的分析并指出存在的问题。     

2APL: a practical agent programming language

This article presents a BDI-based agent-oriented programming language, called 2APL (A Practical Agent Programming Language). This programming language facilitates the implementation of multi-agent systems consisting of individual agents that may share and access external environments. It realizes an effective integration of declarative and imperative style programming by introducing and integrating declarative beliefs and goals with events and plans. It also provides practical programming constructs to allow the generation, repair, and (different modes of) execution of plans based on beliefs, goals, and events. The formal syntax and semantics of the programming language are given and its relation with existing BDI-based agent-oriented programming languages is discussed.     

Integrating answer set programming and constraint logic programming

We introduce a knowledge representation language ${\cal AC(C)}$ extending the syntax and semantics of ASP and CR-Prolog, give some examples of its use, and present an algorithm, $\mathcal{AC}\!solver$ , for computing answer sets of ${\cal AC(C)}$ programs. The algorithm does not require full grounding of a program and combines “classical” ASP solving methods with constraint logic programming techniques and CR-Prolog based abduction. The ${\cal AC(C)}$ based approach often allows to solve problems which are impossible to solve by more traditional ASP solving techniques. We believe that further investigation of the language and development of more efficient and reliable solvers for its programs can help to substantially expand the domain of applicability of the answer set programming paradigm.     

基于SOAP协议的Agent通信语言的研究

Agent通信语言是实现多Agent系统交互与合作的基础。SOAP作为一种新的与平台无关的通信协议,可以实现异构多信息的交换,使得各孤立系统的通信变得容易。文中在分析Agent通信语言,XML,SOAP,WebService等技术的基础上,结合KQML语言提出了一种基于SOAP协议的Agent通信实现方法,这种方法的消息结构由三层组成:SOAP层、KQML层和内容层。并分析了这种三层结构的消息表示的优势及其在实际系统中的应用。     

Using agent- and organisation-oriented programming to develop a team of agents for a competitive game

The multi-agent programming contest uses a cow-herding scenario where two teams of cooperative agents compete for resources against each other. We developed such a team of agents using two well-known platforms, one based on a logic-based agent-oriented programming language, called Jason, and the other based on an organisational model, called $\mathcal{M}$ oise. While there is significant research on both agent programming and agent organisations, this was one of the first applications of a combined approach where we can program deliberative agents and organise them using a sophisticated organisational model. In this paper, we describe and discuss our contribution to the multi-agent contest using this combination of agent and organisation programming.