FORCES Meetings at Javeriana University. April 13 - April 24 2009.

Detailed Program

Program

Abstracts

Towards a Unified Framework for Declarative Structured Communications

We describe ongoing work on the definition of a formal framework for the declarative analysis of structured communication. By relying on a (timed) concurrent constraint programming language, we show that in addition to the usual behavioral techniques from process calculi, session analysis can elegantly exploit logic based reasoning techniques, all in a single framework. As a preliminary result, we outline a concurrent constraint interpretation of a language for structured communication proposed by Honda, Vasconcelos and Kubo. Distinguishing features of our approach are: the possibility of including partial information (constraints) in the session model; the use of explicit time for reasoning about session duration and expiration; a tight correspondence with logic, which formally relates session execution and linear-time temporal logic formulas.

A Declarative Language for Dynamic Multimedia Interaction Systems

Universal Timed Concurrent Constraint Programming (utcc) is a declarative model for concurrency tied to logic. It aims at specifying mobile reactive systems, i.e., systems that continuously interact with the environment and may change their communication structure. In this paper we argue for utcc as a declarative model for dynamic multimedia interaction systems. Firstly, we show that the notion of constraints as partial information allows us to neatly define temporal relations between interactive agents or events. Secondly, we show that mobility in utcc allows for the specification of more flexible and expressive systems. Thirdly, by relying on the underlying temporal logic in utcc, we show how non-trivial temporal properties of the model can be verified. We give two compelling applications of our approach. We propose a model for dynamic interactive scores where interactive points can be defined to adapt the hierarchical structure of the score depending on the information inferred from the environment. We then broaden the interaction mechanisms available for the composer in previous (more static) models. We also model a music improvisation system based on the factor oracle that scales up to situations involving several players, learners and improvisers.

Representing NTCC with chu spaces

By analyzing some extant models of concurrency and overviewing the most general and important concepts in the NTCC calculus, a timed extension of the CCP model, we explore the possibility of using Chu Spaces Structures, a popular model for representing concurrency, so we can give an adequate semantics for each NTCC construct in a straightforward way. The use of Chu spaces has several advantages as a way of representing NTCC's denotational semantics since it is a more general structure for modeling concurrency and so, it allows NTCC to have a more generally known denotational semantics. Among other benefits we state that one of the most important obtained features is that by means of the Chu spaces adaptability (i.e. they may have different number of valuations for an event. (i.e. binary Chu spaces for representing interleaving, triadic Chu spaces for true concurrency or tetradic Chu spaes for guaranteeing the use of an atomic tell)), different scenarios in NTCC can be represented. Specifically, by borrowing some concepts of transition and cancellation from Pratt, we construct a triadic Chu space to guarantee true concurrency in NTCC. We give complete semantic definitions for each NTCC construct and we demonstrate the accuracy of this semantics by proving several important properties and by ensuring that what is represented by NTCC's own semantics can be represented with our own denotational semantics based on Chu spaces.

Extending CCP for modeling Spatial Behaviour

CCP is a formalism for concurrency for reasoning about agents which interact with each other by telling and asking information represented as logic formulae also known as constraints. This calculus is parametric in a constraint system which is basically an underlying logic theory. An distinctive feature of CCP is that agents can be viewed as both processes and formulas in the underlying logic.

Spatial logic are formalisms that can be used to specify properties of mobile systems. Including hierarchies of named locations restricting the use of certain resources to certain subsystems.

In this talk will be show mi research proposal, an introduction for constraint system defined with spatial logic, a simple example modeled with tcc parametric with this constraint system. Satisfaction rules of these process for the logic formulas and finally showing an introduction about decidibility of deduction system for spatial logics

Cytocomputation

Cytocomputation is a computational paradigm inspired in the processes that are performed inside the cytoplasm of biological cells through the interaction of proteins and enzymes and among these and genes. The model has three parts, all of them concurrent: a linear genotype, which produces resources (proteins and enzymes) on demand; a set of proteins, which hold incoming and temporal data and that are arranged in a regular geometric space, able to perform local computation; and a set of enzymes acting upon proteins to perform transformations. In designing the framework, explicit parameters requiring careful tuning have been avoided. Instead, each part regulates and is regulated by the others, resembling the metabolic pathways and the genetic regulatory networks found in biological cells. The fitness of a given representation is tested according to the patterns presented in the current problem and this establishes if that particular component becomes specialized, generic, or silenced.