FroCoS 2005 - 5th International Workshop on Frontiers of Combining Systems
Vienna, Austria, September 19-21, 2005
|FroCoS 2005 general info:||home | cfp (txt, pdf) | poster (more) | dates | pc | oc | invited talks | submission | accepted papers | talks | program (txt) | call for participation (txt) | sponsors | abstracts | proceedings|
|FroCoS 2005 local info:||notes (on registration, accomodation, travelling) | registration | accomodation | local information (venue, registration, internet, technical facilities) | social events | local information about Vienna (public transport, restaurants, etc.) | participants | photos|
|FroCoS general info:||FroCoS homepage | FroCoS workshop series | Combination Methods in AR|
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.
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.
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.
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.