FroCoS 2005 - 5th International Workshop on Frontiers of Combining Systems

Sociable Interfaces
by Luca de Alfaro (Univ. of California, Santa Cruz)

Abstract:
Interface formalisms are able to model both the input requirements and the output behavior of system components; they support both bottom-up component-based design, and top-down design refinement. In this paper, we propose ``sociable'' interface formalisms, endowned with a rich compositional semantics that facilitates their use in design and modeling. Specifically, we introduce interface models that can communicate both via actions and via shared variables, and where communication and synchronization covers the full spectrum, from one-to-one, to one-to-many, many-to-one, and many-to-many. Thanks to the expressive power of interface formalisms, this rich compositional semantics can be realized in an economical way, on the basis of a few basic principles. We show how the algorithms for composing, checking the compatibility, and refining the resulting sociable interfaces can be implemented symbolically, leading to efficient implementations. We describe some applications of the resulting interface models, including their use in the synthesis of schedulers for embedded software.

The talk is based on joint work with Leandro Dias da Silva, Marco Faella, Axel Legay, Pritam Roy, and Maria Sorea.

A Comprehensive Framework for Combined Decision Procedures
by Silvio Ghilardi (Univ. of Milano)

Abstract:
We define a general notion of a fragment within higher order type theory; our fragments can be combined into larger ones and a combined procedure for constraint satisfiability with respect to the intended semantics of such fragments is outlined, following Nelson-Oppen schema. The procedure is in general only sound, but it becomes terminating and complete when the shared fragment enjoys suitable noetherianity conditions and allows an abstract version of a `Keisler-Shelah like' isomorphism theorem. We show that this general decidability transfer result covers as special cases, besides applications which seem to be new, the recent extension of Nelson-Oppen procedure to non-disjoint signatures and the fusion transfer of decidability of consistency of A-Boxes with respect to T-Boxes axioms in local abstract description systems; in addition, it reduces decidability of modal and temporal monodic fragments to their extensional and one-variable components.

The talk is based on joint work with Enrica Nicolini and Daniele Zucchelli.

Matching Classifications via a Bidirectional Integration of SAT and Linguistic Resources
by Fausto Giunchiglia (Univ. of Trento & ITC-IRST)

Abstract: Classifications, often mistakenly called directories, are pervasive: we use them to classify our messages, our favourite Web Pages, our files, ... And many more can be found in the Web; think for instance of the Google and Yahoo's directories. The problem is that all these classifications are very different or more precisely, semantically heterogeneous. The most striking consequence is that they classify documents very differently, making therefore very hard and sometimes impossible to find them.
Matching classifications is the process which allows us to map those nodes of two classifications which, intuitively, correspond semantically to each other. In the first part of the talk I will show how it is possible to encode this problem into a propositional validity problem, thus allowing for the use of SAT reasoners. This is done mainly using linguistic resources (e.g., WordNet) and some amount of Natural Language Processing. However, as shown in the second part of the talk, this turns out to be almost useless. In most cases, in fact, linguistic resources do not contain enough of the axioms needed to prove unsatisfiability. The solution to this problem turns to be that of using SAT as a way to generate the missing axioms.
We have started using linguistic resources to provide SAT with the axioms needed to match classifications, and we have ended up using SAT to generate missing axioms in the linguistic resources. We will argue that this is an example of a more general phenomenon which arises when using commonsense knowledge. This in turns becomes an opportunity for the use of decision procedures for a focused automated generation of the missing knowledge.

Hybrid CSP Solving
by Eric Monfroy (Univ. of Nantes & UTFSM/Chile)

Abstract:
In this paper, we are concerned with the design of a hybrid resolution framework. We develop a theoretical model based on chaotic iterations in which hybrid resolution can be achieved as the computation of a fixpoint of elementary functions. These functions correspond to basic resolution techniques and their applications can easily be parameterized by different search strategies. This framework is used for the hybridization of local search and constraint propagation, and for the integration of genetic algorithms and constraint propagation. Our prototype implementation gave experimental results showing the interest of the model to design such hybridizations.

The talk is based on joint work with Frédéric Saubion and Tony Lambert.