You can also check this list of publications without abstracts, or get the full bibtex file. Return to the AVISPA Research Group page.

**Copyright Notice.** The documents distributed have been provided by the contributing authors as a means to ensure timely dissemination of technical work on a noncommercial basis. Copyright and all rights therein are maintained by the authors or by other copyright holders, not withstanding that they have offered their works here electronically. It is understood that all persons copying this information will adhere to the terms and constraints invoked by each author's copyright. These works may not be reposted without the explicit permission of the copyright holder.

[CR10] |
N. Catano, and C. Rueda.
Matelas: A Predicate Calculus Common Formal Definition for Social Networking.
LNCS, Vol. 5977, Feb. 2010. [ bib | .pdf ] This paper presents Matelas, a B predicate calculus deﬁnition for social networking, modeling social-network content, privacy policies, social-networks friendship relations, and how these relations eﬀect users’ policies. The work presented in this paper is part of an ongoing work that aims at using several formal methods tools and techniques to develop a full-ﬂedged social-network service implementing stipulated policies. Although we employed Atelier B to write Matelas, plans are to port it to Event B and to use Rodin to implement the social-network application. |

[AP09] |
J. Aranda, and J. A.Perez.
Languages for Concurrency Featuring Quantitative Information: An Overview and New Perspectives.
The ALP Newsletter. Association for Logic Programming (ALP). Vol. 22, No. 1. Mar. 2009. [ bib | .pdf ] The study of quantitative information within languages for concurrency has recently gained a lot of momentum. In many applications, quantitative information becomes crucial when refining models with empirical data, and is of the essence for verification purposes. In this paper we survey some of the existing languages for concurrency that feature quantitative information, with a special interest in those proposed for biological applications. This survey is then used as a context to motivate a novel approach for analyzing systems exhibiting stochastic behavior, in the form of a discrete-timed concurrent constraint process calculus. Some design decisions involved in the definition of an operational semantics for such a calculus are discussed. |

[MP09] |
J. A. Munoz, and H. A. Perez.
Aplicacion de la Programacion Concurrente por Restricciones en el Modelado de Procesos en la Membrana Celular.
BSc Thesis - Engineering Degree in Computer Science, Pontificia
Universidad Javeriana - Cali (Colombia)., 2009. [ bib | .pdf ] The functional behavior of biological systems has become a task of increasing interest to the scientic community of biologists, who constantly search to infer this behavior from biological data, in order to analyze, to forecast some situations and to do detailed studies about some behaviors which occur at biological level. This fact has also led to the exploration of computational tools that complement this study, inspiring new programming paradigms to describe and model the operation of these biological systems. Computationally one of the alternatives in the current time is the use of Process Caluli based on a concurrent constraint programming model (CCP), where it is possible to model abstractions between the components of the systems and the basics elements of the calculus, allowing to model partial information through formalisms based on constraints in a store where all information about the system is kept. Particularly in this dissertation the Utcc Calculus (Universal Timed Concurrent Constraint) will be used as a language derived from TCC (extension of CCP) by adding new constructions like the abstraction of processes allowing the calculus to represent the notion of mobility. This work is mainly focused on the "Mobile Computing with membranes", one of the main problems in bioinformatics, where the mechanisms which the cell communicates with the outside through the cell membrane are studied. The document outlines two calculi focused on the modeling of these kinds of biological processes based on the interaction between membranes, the first one is BioAmbients derived from Ambient Calculus, allowing the creation of local processes within environments, thus defining the basic configuration of a membrane. The second one is "Brane calculi"which defines a set of biologically inspired primitives in the interaction between membranes, with a fidelity to the biological reality modeled in the calculus. Then a detailed approach to the syntax, functionality and reactions modeled in Brane Calculi will be presented and then an interpretation of the processes in Brane Calculi to Utcc, generating an encoding which allows to translate processes in Brane Calculi to equivalent processes in Utcc. Finally the results obtained are presented, with an analysis of the most important points of this work and establishing a set of conclusions that describe the main advantages and disadvantages to dene an interpretation of the calculi, and also to suggest some guidelines for future work. The main contributions of Utcc to modeling biological membrane systems will be analyzed. The last part is intended to work through the findings and results, motivate and encourage the study and analysis of programming models based on CCP to model more complex biological systems. |

[LPSS09] |
I. Lanese, J. A. Perez, D. Sangiorgi, and A. Schmitt.
On the Expressiveness of Polyadicity in Higher-Order Communication.
In Proceedings of the 11th Italian Conference on Theoretical Computer Science (ICTCS09), September 2009.[ bib | .pdf ] In higher-order process calculi the values exchanged in communications may contain processes. We describe a study of the expressive power of strictly higher-order process calculi, i.e. calculi in which only process passing is allowed and no name-passing is present. In this setting, the polyadicity (i.e. the number of parameters) allowed in communications is shown to induce a hierarchy of calculi of strictly increasing expressiveness: a higher-order calculus with n-adic communication cannot be encoded into a calculus with n - 1-adic communication. In this note we outline this result, and discuss on how it relies on a notion of encoding that takes a rather fine standpoint with respect to internal behavior. |

[GPZ09] |
C. Di Giusto, J. A. Perez, and G. Zavattaro.
On the Expressiveness of Forwarding in Higher-Order Communication.
In Proceedings of the 6th International Colloquium on Theoretical Aspects of Computing (ICTAC09), volume 5684 of Lecture Notes in Computer Science, pages 155-169, Springer, August 2009.[ bib | .pdf ] In higher-order process calculi the values exchanged in communications may contain processes. There are only two capabilities for received processes: execution and forwarding. Here we propose a limited form of forwarding: output actions can only communicate the parallel composition of statically known closed processes and processes received through previously executed input actions. We study the expressiveness of a higher-order process calculus featuring this style of communication. Our main result shows that in this calculus termination is decidable while convergence is undecidable. |

[CBG+09] |
N. Catano, F. Barraza, D. Garcia, P. Ortega, and C. Rueda.
A Case Study in JML-Assisted Software Development.
Electronic Notes in Theoretical Computer Science (ENTCS), 240:5-21, 2009.[ bib | .pdf ] {This paper presents a case study in formal software development of a plugin for a Java Desktop project management application using JML. Our goals for the case study include determining how JML-based formal methods can be incorporated in traditional software engineering practices used in the software industry and how the use of JML for modeling software requirements can enforce the programming of correct Java code. We demonstrate how JML-based formal methods can be used so as to effectively contribute to the making of decisions within a software development team. /font> Keywords: Java, Java Modeling Language (JML), Formal Methods, Software Development, International Center for Tropical Agriculture (CIAT) |

[CR09] |
N. Cataño, and C. Rueda.
Teaching Formal Methods for the Unconquered Territory.
In Proceedings of the 2nd International FME Conference on Teaching Formal Methods (TFM2009), volume 5846/2009 of Lecture Notes in Computer Science, pages 2-19, Springer, November 2009.[ bib | .pdf ] We summarise our experiences in teaching two formal methods courses at Pontificia Universidad Javeriana. The first course is a JML-based software engineering course. The second course is a modeldriven software engineering course realised in the B method for software development. We explain how formal methods are promoted in Pontificia Universidad Javeriana, how we motivate students to embrace formal methods techniques, and how they are promoted through the presentation of motivating examples. |

[Ara09] |
J. Aranda.
On the Expressivity of Infinite and Local Behaviour in Fragments of the Pi-calculus.
PhD Thesis, l'X, Ecole Polytechnique (France) and Universidad del Valle (Colombia), 2009. [ bib | .pdf ] The pi-calculus is one the most influential formalisms for modelling and analyzing the behaviour of concurrent systems. This calculus provides a language in which the structure of terms represents the structure of processes together with an operational semantics to represent computational steps. For example, the parallel composition term P | Q, which is built from the terms P and Q, represents the process that results from the parallel execution of the processes P and Q. Similarly, the restriction (\nu x)P represents a process P with local resource x. The replication !P can be thought of as abbreviating the parallel composition P | P | P .... of an unbounded number of P processes. As for other language-based formalisms (e.g., logic, formal grammars and the lambda-calculus) a fundamental part of the research in process calculi involves the study of the expressiveness of fragments or variants of a given process calculus. In this dissertation we shall study the expressiveness of some variants of the pi-calculus focusing on the role of the terms used to represent local and infinite behaviour, namely restriction and replication. The first part of this dissertation is devoted to the expressiveness of the zero-adic variant of the (polyadic) pi-calculus, i.e., CCS with replication (CCS!). Busi et al show that CCS! is Turing powerful. The result is obtained by encoding Random Access Machines (RAMs) in CCS!. The encoding is said to be non-faithful because it may move from a state which can lead to termination into a divergent one which do not correspond to any configuration of the encoded RAM. I.e., the encoding is not termination preserving. In this dissertation we shall study the existence of faithful encodings into CCS! of models of computability strictly less expressive than Turing Machines. Namely, grammars of Types 1 (Context Sensitive Languages), 2 (Context Free Languages) and 3 (Regular Languages) in the Chomsky Hierarchy. We provide faithful encodings of Type 3 grammars. We show that it is impossible to provide a faithful encoding of Type 2 grammars and that termination-preserving CCS! processes can generate languages which are not Type 2. We finally conjecture that the languages generated by termination-preserving CCS! processes are Type 1 . We also observe that the encoding of RAMs and several encoding of Turing-powerful formalisms in pi-calculus variants may generate an unbounded number of restrictions during the simulation of a given machine. This unboundedness arises from having restrictions under the scope of replication (or recursion) as in e.g., $!(nu x)P$ or $\mu X.(\nu x)(P | X)$. This suggests that such an interplay between these operators is fundamental for Turing completeness. We shall also study the expressive power of restriction and its interplay with replication. We do this by considering several syntactic variants of CCS! which differ from each other in the use of restriction with respect to replication. We consider three syntactic variations of CCS! which do not allow the generation of unbounded number of restrictions: C1 is the fragment of CCS! not allowing restrictions under the scope of a replication, C2 is the restriction-free fragment of CCS!. The third variant is C3 which extends C1 with Phillips' priority guards. We shall show that the use of an unboundedly many restrictions in CCS! is necessary for obtaining Turing expressiveness in the sense of Busi et al. We do this by showing that there is no encoding of RAMs into C1 which preserves and reflects convergence. We also prove that up to failures equivalence, there is no encoding from CCS! into C1 nor from C1 into C2 . Thus up to failures equivalence, we cannot encode a process with an unbounded number of restrictions into one with a bounded number of restrictions, nor one with a bounded number of restrictions into a restriction-free process. As lemmata for the above results we prove that convergence is decidable for C1 and that language equivalence is decidable for C2 but undecidable for C1. As corollary it follows that convergence is decidable for restriction-free CCS. Finally, we show the expressive power of priorities by providing a faithful encoding of RAMs in C3. Thus bearing witness to the expressive power of Phillips' priority guards. The second part of this dissertation is devoted to expressiveness of the asynchronous monadic pi-calculus, Api. In [C. Palamidessi, V. Saraswat, F. Valencia and B. Victor. On the Expressiveness of Linearity vs Persistence in the Asynchronous Pi Calculus. LICS 2006:59-68, 2006] the authors studied the expressiveness of persistence in Api wrt weak barbed congruence. The study is incomplete because it ignores divergence. We shall present an expressiveness study of persistence in Api wrt De Nicola and Hennessy's testing scenario which is sensitive to divergence. Following [C. Palamidessi, V. Saraswat, F. Valencia and B. Victor. On the Expressiveness of Linearity vs Persistence in the Asynchronous Pi Calculus. LICS 2006:59-68, 2006], we consider Api and three sub-languages of it, each capturing one source of persistence: the persistent-input Api-calculus (PIpi), the persistent-output Api-calculus (POpi) and the persistent Api-calculus (Ppi). In [C. Palamidessi, V. Saraswat, F. Valencia and B. Victor. On the Expressiveness of Linearity vs Persistence in the Asynchronous Pi Calculus. LICS 2006:59-68, 2006] the authors showed encodings from Api into the semi-persistent calculi (i.e., POpi and PIpi) correct wrt weak barbed congruence. We show that, under some general conditions related to compositionality of the encoding and preservation of the infinite behaviour, there cannot be an encoding from Api into a (semi)-persistent calculus preserving the must testing semantics. We also prove that convergence and divergence are decidable for POpi (and Ppi). As a consequence there is no encoding preserving and reflecting divergence or convergence from Api into POpi (and Ppi). This study fills a gap on the expressiveness study of persistence in Api in [C. Palamidessi, V. Saraswat, F. Valencia and B. Victor. On the Expressiveness of Linearity vs Persistence in the Asynchronous Pi Calculus. LICS 2006:59-68, 2006]. |

[FOP09] |
M. Falaschi, C. Olarte, and C. Palamidessi.
A framework for abstract interpretation of timed concurrent constraint programs.
In Antonio Porto and Francisco Javier Lopez-Fraguas, editors, Proceedings of the 11th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming (PPDP09), pages 207-218, ACM, September 2009.[ bib | .pdf ] Timed Concurrent Constraint Programming (tcc) is a declarative model for concurrency offering a logic for specifying reactive systems, i.e. systems that continuously interact with the environment. The universal tcc formalism (utcc) is an extension of tcc with the ability to express mobility. Here mobility is understood as communication of private names as typically done for mobile systems and security protocols. In this paper we consider the denotational semantics for tcc, and we extend it to a "collecting" semantics for utcc based on closure operators over sequences of constraints. Relying on this semantics, we formalize the first general framework for data flow analyses of tcc and utcc programs by abstract interpretation techniques. The concrete and abstract semantics we propose are compositional, thus allowing us to reduce the complexity of data flow analyses. We show that our method is sound and parametric w.r.t. the abstract domain. Thus, different analyses can be performed by instantiating the framework. We illustrate how it is possible to reuse abstract domains previously defined for logic programming, e.g., to perform a groundness analysis for tcc programs. We show the applicability of this analysis in the context of reactive systems. Furthermore, we make also use of the abstract semantics to exhibit a secrecy flaw in a security protocol. We have developed a prototypical implementation of our methodology and we have implemented the abstract domain for security to perform automatically the secrecy analysis. |

[LOP09] |
Hugo A. López, Carlos Olarte and Jorge A. Pérez.
Towards a Unified Framework for Declarative Structured Communications.
Proc. of PLACES'09. To appear in Electronic Proceedings in theoretical Computer Science, 2009. [ bib | .pdf ] We describe a uniﬁed framework for the declarative analysis of structured communications. By relying on a (timed) concurrent constraint programming language, we show that in addition to the usual operational techniques from process calculi, the analysis of structured communications can elegantly exploit logic-based reasoning techniques. In this work, we present a concurrent constraint interpretation of the language for structured communications 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. |

[AAO+09] |
J Aranda, G Assayag, C Olarte, J P{\'e}rez, C Rueda, M Toro, and F D. Valencia
An Overview of FORCES: An INRIA Project on Declarative Formalisms for Emergent Systems.
In Patricia M. Hill and David Scott Warren, editors, Proc of the 25th International Conference on Logic Programming (ICLP 2009), volume 5649 of Lecture Notes in Computer Science, pages 509-513, Springer, July 2009.[ bib | .pdf ] The FORCES project aims at providing robust and declarative formalisms for analyzing systems in the emerging areas of Security Protocols, Biological Systems and Multimedia Semantic Interaction. This short paper describes FORCES's motivations, results and future research directions. |

[PS09] |
S. Perchy, and G. Sarria.
Dissonances: Brief Description and its Computational Representation in the RTCC Calculus.
In Proc of the 6th Sound and Music Computing Conference, SMC2009. 2009.[ bib | .pdf ] Dissonances in music have had a long evolution history dating back to days of strictly prohibition to times of enricheness of musical motives and forms. Nowadays, dissonances account for most of the musical expressiveness and contain a full application theory supporting their use making them a frequently adopted resource of composition. This work partially describes their theoretical background as well as their evolution in music and finally proposing a new model for their computational use. |

[Ola09] |
C. Olarte.
Universal Temporal Concurrent Constraint Programming.
PhD Thesis, l'X, Ecole Polytechnique, France, 2009. [ bib | .pdf ] Concurrent Constraint Programming (CCP) [Saraswat 1993] is a formalism for concurrency in which agents (processes) interact with one another by telling (adding) and asking (reading) information represented as constraints in a shared medium (the store). Temporal Concurrent Constraint Programming (tcc) extends CCP by allowing agents to be constrained by time conditions. This dissertation studies temporal CCP as a model of concurrency for mobile, timed reactive systems. The study is conducted by developing a process calculus called utcc, Universal Temporal CCP. The thesis is that utcc is a model for concurrency where behavioral and declarative reasoning techniques coexist coherently, thus allowing for the specification and verification of mobile reactive systems in emergent application areas. The utcc calculus generalizes tcc [Saraswat 1994], a temporal CCP model of reactive synchronous programming, with the ability to express mobility. Here mobility is understood as communication of private names as typically done for mobile systems and security protocols. The utcc calculus introduces parametric ask operations called abstractions that behave as persistent parametric asks during a time-interval but may disappear afterwards. The applicability of the calculus is shown in several domains of Computer Science. Namely, decidability of Pnueli's First-order Temporal Logic, closure-operator semantic characterization of security protocols, semantics of a Service-Oriented Computing language, and modeling of Dynamic Multimedia-Interaction systems. The utcc calculus is endowed with an operational semantics and then with a symbolic semantics to deal with problematic operational aspects involving infinitely many substitutions and divergent internal computations. The novelty of the symbolic semantics is to use temporal constraints to represent finitely infinitely-many substitutions. In the tradition of CCP-based languages, utcc is a declarative model for concurrency. It is shown that utcc processes can be seen, at the same time, as computing agents and as logic formulae in the Pnueli's First-order Linear-time Temporal Logic (FLTL) [Manna 1991]. More precisely, the outputs of a process correspond to the formulae entailed by its FLTL representation. The above-mentioned FLTL characterization is here used to prove an insightful (un)decidability result for Monadic FLTL. To do this it is proven that in contrast to tcc, utcc is Turing-powerful by encoding Minsky machines [Minsky 1967]. The encoding uses a simple decidable constraint system involving only monadic predicates and no equality nor function symbols. The importance of using such a constraint system is that it allows for using the underlying theory of utcc to prove the undecidability of the validity problem for monadic FLTL without function symbols nor equality. In fact, it is shown that this fragment of FLTL is strongly incomplete. This result refutes a decidability conjecture for FLTL from a previous work. It also justifies the restriction imposed in previous decidability results on the quantification of flexible-variables. This dissertation then fills a gap on the decidability study of monadic FLTL. Similarly to tcc, utcc processes can be semantically characterized as partial closure operators. Because of additional technical difficulties posed by utcc, the codomain of the closure operators is more involved than that for tcc. Namely, processes are mapped into sequences of future-free temporal formulae rather than sequences of basic constraints as in tcc. This representation is shown to be fully abstract with respect to the input-output behavior of processes for a meaningful fragment of the calculus. This shows that mobility can be captured as closure operators over an underlying constraint system. As a compelling application of the semantic study of utcc, this dissertation gives a closure operator semantics to a language for security protocols. This language arises as a specialization of utcc with a particular cryptographic constraint systems. This brings new semantic insights into the modeling and verification of security protocols. The utcc calculus is also used in this dissertation to give an alternative interpretation of the pi-based language defined by Honda, Vasconcelos and Kubo (HVK) for structuring communications [Honda 1998]. The encoding of HVK into utcc is straightforwardly extended to explicitly model information on session duration, allows for declarative preconditions within session establishment constructs, and features a construct for session abortion. Then, a richer language for the analysis of sessions is defined where time can be explicitly modeled. Additionally, relying on the above-mentioned interpretation of utcc processes as FLTL formulae, reachability analysis of sessions can be characterized as FLTL entailment. It is also illustrated that the utcc calculus allows for the modeling of dynamic multimedia interaction systems. The notion of constraints as partial information neatly defines temporal relations between interactive agents or events. Furthermore, mobility in utcc allows for the specification of more flexible and expressive systems in this setting, thus broadening the interaction mechanisms available in previous models. Finally, this dissertation proposes a general semantic framework for the data flow analysis of utcc and tcc programs by abstract interpretation techniques [Cousot 1979]. The concrete and abstract semantics are compositional reducing the complexity of data flow analyses. Furthermore, the abstract semantics is parametric with respect to the abstract domain and allows for reusing the most popular abstract domains previously defined for logic programming. Particularly, a groundness analysis is developed and used in the verification of a simple reactive systems. The abstract semantics allows also to efficiently exhibit a secrecy flaw in a security protocol modeled in utcc. Keywords: Concurrent Constraint Based Calculi, Denotational Semantics, Symbolic Semantics, Security Protocols, Temporal Logic. |

[ORV09] |
C. Olarte, C. Rueda, and F. D. Valencia.
Concurrent Constraints Calculi: A Declarative Paradigm for Modeling Music Systems.
In in New Computational Paradigms for Computer Music. Editions Latour, Paris, 2009.[ bib | .pdf ] Concurrent constraint programming (CCP) [25] has emerged as a simple but powerful paradigm for concurrent systems ; i.e., systems of multiple agents that interact with each other as for example in a collection of music processes (musicians) performing a particular piece. A fundamental issue in CCP is the speciﬁcation of concurrent systems by means of constraints. A constraint (e.g., note > 60) represents partial information about certain system variables. During the computation, the current state of the system is speciﬁed by a set of constraints (store). Processes can change the state of the system by tel ling (adding) information to the store and synchronize by asking information to the store. The ntcc calculus [14] is a CCP formalism for modeling temporal reactive systems. The calculus is built upon a small number of basic ideas that capture several aspects of temporal nondeterministic behavior. In ntcc, processes can also be constrained by temporal requirements such as delays, time-outs and pre-emptions. Thus, the calculus integrates two dimensions of computation: a horizontal dimension dealing with partial information (e.g., note > 60) and a vertical one in which temporal requirements come into play (e.g., a process must be executed at any time within the next ten time units). The above integration is remarkably useful for modeling complex musical processes, in particular for music improvisation. For example, for the vertical dimension one can specify that a given process can nondeterministically choose any note satisfying a given constraint. For the horizontal dimension one can specify that the process can nonde- terministically choose the time to play the note sub ject to a given time upper bound. This nondeterministic view is particularly suitable for processes representing a musi- cian’s choices when improvising. Similarly, the horizontal dimension may supply partial information on a rhythmic pattern that leaves room for variation while keeping a basic control, as in one of the examples given below. We shall also illustrate how implementing a weaker ntcc model of a musical process may greatly simplify the formal veriﬁcation of its properties. We argue that this modeling strategy provides a “runnable speciﬁcation” for music problems that eases the task of formally reasoning about them. Furthermore, ntcc is provided with a linear temporal process logic for verifying spec- iﬁcations of ntcc processes. We shall show how this logic gives a very expressive setting for formally proving the existence of interesting musical properties of a process. We shall also give examples of musical speciﬁcations in ntcc and use the linear temporal logic for proving properties of a realistic musical problem. |

[Tor09c] |
M. Toro.
Towards a correct and eﬃcient implementation of simulation
and veriﬁcation tools for Probabilistic ntcc
, Tech. Report, Pontificia
Universidad Javeriana - Cali (Colombia)., 2009. [ bib | .pdf ] Using process calculi one can verify properties of a system and simulate the system as well. One should be able to do these operations at least semi-automatically. There is a tool to simulate the Non-deterministic Timed Concurrent Constraint (ntcc) calculus in the Ntccrt framework, but there are not tools for veriﬁcation. We present a new simulation tool for Probabilistic ntcc (pntcc) and a prototype for veriﬁcation of pntcc models. We include these tools in the Ntccrt framework. We also show the formal basis for correctness of the ntcc simulation tool and we show that the execution times of the simulation are still acceptable for real-time interaction using pntcc. |

[TRAA09] |
M. Toro-Bermudez, C. Rueda, C. Agon, and G. Assayag.
NTCCRT: A Concurrent Constraint Framework for Real-Time Interaction.
In Proc of the International Computer Music Conference, ICMC 2009. 2009.[ bib | .pdf ] Writing multimedia interaction systems is not easy. Their concurrent processes usually access shared resources in a non-deterministic order, often leading to unpredictable be- havior. Using Pure Data (Pd) and Max/MSP is possible to program concurrency, however, it is difﬁcult to synchronize processes based on multiple criteria. Process calculi such as the Non-deterministic Timed Concurrent Constraint (ntcc) calculus, overcome that problem by representing multiple criteria as constraints. We propose using our framework Ntccrt to manage concurrency in Pd and Max. Ntccrt is a real-time capable interpreter for ntcc. Using Ntccrt exter- nals (binary plugins) in Pd we ran models for machine im- provisation and signal processing. |

[AVV09] |
J. Aranda, F. D.Valencia, and C. Versari.
On the Expressive Power of Restriction and Priorities in CCS with Replication.
In Proc of Foundations of Software Science and Computational Structures, 12th International Conference, FOSSACS 2009, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2009, volume 5504 of Lecture Notes in Computer Science, pages 242-256. Springer, March 2009.[ bib | .pdf ] We study the expressive power of restriction and its interplay with replication. We do this by considering several syntactic variants of CCS_{!} (CCS with replication instead of recursion) which differ from each other in the use of restriction with respect to replication. We consider three syntactic variations of CCS_{!} which do not allow the use of an unbounded number of restrictions: CCS_{!}^{-!v} is the fragment of CCS_{!} not allowing restrictions under the scope of a replication. CCS_{!}^{-v} is the restriction-free fragment of CCS_{!}. The third variant is CCS_{!+pr}^{-!v} which extends CCS_{!}^{-!v} with Phillips' priority guards. We show that the use of unboundedly many restrictions in CCS_{!} is necessary for obtaining Turing expressiveness in the sense of Busi et al [N. Busi, M. Gabbrielli, and G. Zavattaro. Comparing recursion, replication, and iteration in process calculi. In ICALP'04, volume 3142 of LNCS, pages 307-319. Springer-Verlag, 2004]. We do this by showing that there is no encoding of RAMs into CCS_{!}^{-!v} which preserves and reflects convergence. We also prove that up to failures equivalence, there is no encoding from CCS_{!} into CCS_{!}^{-!v} nor from CCS_{!}^{-!v} into CCS_{!}^{-v}. As lemmata for the above results we prove that convergence is decidable for CCS_{!}^{-!v} and that language equivalence is decidable for CCS_{!}^{-v}. As corollary it follows that convergence is decidable for restriction-free CCS. Finally, we show the expressive power of priorities by providing an encoding of RAMs in CCS_{!+pr}^{-!v}. |

[LMO+09] |
D. Lesaint, D. Mehta, B. O'Sullivan, L.O. Quesada, and N. Wilson.
A Soft Global Precedence Constraint.
In IJCAI '09: Proceedings of the Twenty-first International Joint Conference on Artificial Intelligence., 2009.[ bib | .pdf ] Hard and soft precedence constraints play a key role in many application domains. In telecommunications, one application is the configuration of callcontrol feature subscriptions where the task is to sequence a set of user-selected features subject to a set of hard (catalogue) precedence constraints and a set of soft (user-selected) precedence constraints. When no such consistent sequence exists, the task is to find an optimal relaxation by discarding some features or user precedences. For this purpose, we present the global constraint SOFTPREC. Enforcing Generalized Arc Consistency (GAC) on SOFTPREC is NP-complete. Therefore, we approximate GAC based on domain pruning rules that follow from the semantics of SOFTPREC; this pruning is polynomial. Empirical results demonstrate that the search effort required by SOFTPREC is up to one order of magnitude less than the previously known best CP approach for the feature subscription problem. SOFTPREC is also applicable to other problem domains including minimum cutset problems for which initial experiments confirm the interest. |

[Tor09] |
M. Toro.
Probabilistic Extension to the Concurrent Constraint Factor Oracle model for Music Improvisation.
BSc Thesis - Engineering Degree in Computer Science, Pontificia
Universidad Javeriana - Cali (Colombia)., 2009. [ bib | .pdf ] We can program a Real-Time (RT) music improvisation system in C++ without a formal semantic or we can model it with process calculi such as the Non-deterministic Timed Concurrent Constraint (ntcc) calculus. "Concurrent Constraints Factor Oracle (FO) model for Music Improvisation" (Ccfomi) is an improvisation model specified on ntcc. Since Ccfomi improvises non-deterministically, there is no control on choices and therefore little control over the sequence variation during the improvisation. To avoid this, we extended Ccfomi using the Probabilistic Non-deterministic Timed Concurrent Constraint calculus. Our extension to Ccfomi does not change the time and space complexity of building the FO, thus making our extension compatible with RT. However, there was not a ntcc interpreter capable of RT to execute Ccfomi. We developed Ntccrt -a RT capable interpreter for ntcc- and we executed Ccfomi on Ntccrt. In the future, we plan to extend Ntccrt to execute our extension to Ccfomi. |

[PR08] |
J. A. Perez, and C. Rueda.
Non-determinism and Probabilities in Timed Concurrent Constraint Programming.
In Maria Garcia de la Banda and Enrico Pontelli, editors, Proc of the 24th International Conference on Logic Programming (ICLP 2008). volume 5366 of Lecture Notes in Computer Science, pages 677-681. Springer, 2008.[ bib | .pdf ] A timed concurrent constraint process calculus with probabilistic and non-deterministic choices is proposed. We outline the rationale of an operational semantics for the calculus. The semantics ensures consistent interactions between both kinds of choices and is indispensable for the definition of logic-based verification capabilities over system specifications. |

[LPSS08] |
I. Lanese, J. A.Perez, D. Sangiorgi, and A. Schmitt.
On the Expressiveness and Decidability of Higher-Order Process Calculi .
In Proc. of the Twenty-Third Annual IEEE Symposium on Logic in Computer Science, LICS 2008, pages 145-155. IEEE, 2008.[ bib | .pdf ] In higher-order process calculi the values exchanged in communications may contain processes. A core calculus of higher-order concurrency is studied; it has only the operators necessary to express higher-order communications: input prefix, process output, and parallel composition. By exhibiting a nearly deterministic encoding of Minsky Machines, the calculus is shown to be Turing Complete andtherefore its termination problem is undecidable. Strong bisimilarity, however, is proved to be decidable. Further, the main forms of strong bisimilarity for higher-order processes (higher-order bisimilarity, context bisimilarity, normal bisimilarity, barbed congruence) coincide. They also coincide with their asynchronous versions. A sound and complete axiomatization of bisimilarity is given. Finally, bisimilarity is shown to become undecidable if at least four static (i.e., top-level) restrictions are added to the calculus. |

[BPV08] |
R. Beauxis, C. Palamidessi, C. Rueda, and F. D. Valencia.
On the Asynchronous Nature of the Asynchronous pi-Calculus.
In Pierpaolo Degano and Rocco De Nicola and Jos{\'e} Meseguer, editors, Concurrency, Graphs and Models, Essays Dedicated to Ugo Montanari on the Occasion of His 65th Birthday. volume 5065 of Lecture Notes in Computer Science, pages 473-492. Springer, 2008.[ bib | .pdf ] We address the question of what kind of asynchronous communication is exactly modeled by the asynchronous $\pi$-calculus ($\pi_{a}$). To this purpose we define a calculus $\pi_{\mathcal{B}}$ where channels are represented explicitly as special buffer processes. The base language for $\pi_{\mathcal{B}}$ is the (synchronous) $\pi$-calculus, except that ordinary processes communicate only via buffers. Then we compare this calculus with $\pi_{a}$. It turns out that there is a strong correspondence between $\pi_{a}$ and $\pi_{\mathcal{B}}$ in the case that buffers are bags: we can indeed encode each a process into $\pi_{a}$ strongly asynchronous bisimilar $\pi_{\mathcal{B}}$ process, and each $\pi_{\mathcal{B}}$ process into a weakly asynchronous bisimilar $\pi_{a}$ process. In case the buffers are queues or stacks, on the contrary, the correspondence does not hold. We show indeed that it is not possible to translate a stack or a queue into a weakly asynchronous bisimilar $\pi_{a}$ process. Actually, for stacks we show an even stronger result, namely that they cannot be encoded into weakly (asynchronous) bisimilar processes in a $\pi$-calculus without mixed choice. |

[APRV08] |
J. Aranda, J. Perez, C. Rueda, and F. D. Valencia.
Stochastic Behavior and Explicit Discrete Time in Concurrent Constraint Programming.
In Proc. of 24th International Conference on Logic Programming (ICLP 2008). volume 5366 of Lecture Notes in Computer Science, pages 682-686. Springer-Verlag, 2008.[ bib | .pdf ] We address the inclusion of stochastic information into an explicitly timed concurrent constraint process language. An operational semantics is proposed as a preliminary result. Our approach finds applications in biology, among other areas. |

[CCAV08] |
D. Cacciagrano, F. Corradini, J. Aranda, and F. D. Valencia.
Linearity, Persistence and Testing Semantics in the Asynchronous Pi-Calculus.
Electronic Notes in Theoretical Computer Science (ENTCS), 194(2):59-84, 2008.[ bib | .pdf ] In [C. Palamidessi, V. Saraswat, F. Valencia and B. Victor. On the Expressiveness of Linearity vs Persistence in the Asynchronous Pi Calculus. LICS 2006:59-68, 2006] the authors studied the expressiveness of persistence in the asynchronous $\pi$-calculus (A$\pi$) wrt weak barbed congruence. The study is incomplete because it ignores the issue of divergence. In this paper, we present an expressiveness study of persistence in the asynchronous $\pi$-calculus (A$\pi$) wrt De Nicola and Hennessy's testing scenario which is sensitive to divergence. Following [C. Palamidessi, V. Saraswat, F. Valencia and B. Victor. On the Expressiveness of Linearity vs Persistence in the Asynchronous Pi Calculus. LICS 2006:59-68, 2006], we consider A$\pi$ and three sub-languages of it, each capturing one source of persistence: the persistent-input calculus (PIA$\pi$), the persistent-output calculus (POA$\pi$) and persistent calculus (PA$\pi$). In [C. Palamidessi, V. Saraswat, F. Valencia and B. Victor. On the Expressiveness of Linearity vs Persistence in the Asynchronous Pi Calculus. LICS 2006:59-68, 2006] the authors showed encodings from A$\pi$ into the semi-persistent calculi (i.e., POA$\pi$ and PIA$\pi$) correct wrt weak barbed congruence. In this paper we prove that, under some general conditions, there cannot be an encoding from A$\pi$ into a (semi)-persistent calculus preserving the must testing semantics. Keywords: Asynchronous Pi-Calculus, Linearity, Persistence, Testing Semantics. |

[OV08b] |
C. Olarte, and F. D. Valencia.
The Expressivity of Universal Timed CCP: Undecidability of Monadic FLTL and Closure operators for Security
In Proc. of PPDP’ 08. 2008.[ bib | .pdf ] The timed concurrent constraint programing model (tcc) is a declarative framework, closely related to First-Order Linear Temporal Logic (FLTL), for modeling reactive systems. The universal tcc formalism (utcc) is an extension of tcc with the ability to express mobility. Here mobility is understood as communication of private names as typically done for mobile systems and security protocols. This paper is devoted to the study of 1) the expressiveness of utcc and 2) its semantic foundations. As applications of this study, we also state 3) a noteworthy decidability result for the well-established framework of FLTL and 4) bring new semantic insights into the modeling of security protocols. More precisely, we show that in contrast to tcc, utcc is Turingpowerful by encoding Minsky machines. The encoding uses a monadic constraint system allowing us to prove a new result for a fragment of FLTL: The undecidability of the validity problem for monadic FLTL without equality and function symbols. This result refutes a decidability conjecture for FLTL from a previous paper. It also justifies the restriction imposed in previous decidability results on the quantification of flexible-variables. We shall also show that as in tcc, utcc processes can be semantically represented as partial closure operators. The representation is fully abstract wrt the input-output behavior of processes for a meaningful fragment of the utcc. This shows that mobility can be captured as closure operators over an underlying constraint system. As an application we identify a language for security protocols that can be represented as closure operators over a cryptographic constraint system. Keywords: Concurrent Constraint Programming, First-order Linear Temporal Logic, Closure Operators, Security Protocols |

[OV08a] |
C. Olarte, and F. D. Valencia.
Universal Concurrent Constraint Programming: Symbolic Semantics and Applications to Security.
In Proc. of SAC'08. ACM Press. 2008.[ bib | .pdf ] We introduce the Universal Timed Concurrent Constraint Programming (utcc) process calculus; a generalisation of Timed Concurrent Constraint Programming. The utcc calculus allows for the specication of mobile behaviours in the sense of Milner's pi-calculus: Generation and communication of private channels or links. We first endow utcc with an operational semantics and then with a symbolic semantics to deal with problematic operational aspects involving infinitely many substitutions and divergent internal computations. The novelty of the symbolic semantics is to use temporal constraints to represent finitely infinitely-many substitutions. We also show that utcc has a strong connection with Pnueli's Temporal Logic. This connection can be used to prove reachability properties of utcc processes. As a compelling example, we use utcc to exhibit the secrecy flaw of the Needham-Schroeder security protocol. Keywords: Concurrent Constraint Programming, Symbolic Semantics, Security, Mobility. |

[ORV08] |
C. Olarte, C. Rueda, and F. D. Valencia.
Universal Timed CCP: Expressivity and Applications to Musical Improvisation.
In Proc. of CLEI2008. Santa Fe, Argentina, 2008.[ bib | .pdf ] Universal timed concurrent constraint programming (utcc) is an extension of temporal CCP (tcc) aimed at modeling mobile reactive systems. The language counts with several reasoning techniques such as a symbolic semantics and a compositional semantics based on closure operators. Additionally, utcc processes can be regarded as formulae in first-order linear temporal logic (FLTL). In this paper we first show how the abstraction operator introduced in utcc can neatly express arbitrary recursion which is not possible in tcc. Second, we present an encoding of the lambda-calculus into utcc. Although utcc has been previously proved to be Turing powerful encoding Minsky machines in it, the encoding we present here is compositional unlike that of Minsky machines. Compositionality is an important property of an encoding as it may allow structural analysis in utcc of the source terms; i.e., functional programs. Finally, as compelling application, making use of the recursive definitions in utcc, we model a music improvisation system composed of interactive agents learning a musical style and generating on the fly new material in the same style. |

[SR08] |
G. Sarria, and C. Rueda.
Real-Time Concurrent Constraint Programming.
In Proc. of CLEI2008. Santa Fe, Argentina, 2008.[ bib | .pdf ] The ntcc calculus is a model of temporal concurrent constraint programming with the capability of expressing asynchronous and non-deterministic timed behaviour. We propose a model of real-time concurrent constraint programming, which adds to ntcc the means for specifying and modelling real-time behaviour. We provide a new construct for strong preemption, an operational semantics supporting resources and limited time and a denotational semantics based on CHU spaces. We argue that the resultant calculus has a natural application in various fields such as multimedia interaction. Keywords: ntcc, rtcc, real-time, process calculus |

[HLM+08] |
H. Hadzic, D. Lesaint, D. Mehta, B. O'Sullivan, L.O. Quesada, and N. Wilson.
A BDD Approach to the Feature Subscription Problem.
In ECAI 2008: Proceedings of the 18th European Conference on Artificial Intelligence., volume 178 of Frontiers in Artificial Intelligence and Applications, pages 698-702. IOS Press, July 2008.[ bib | .pdf ] Modern feature-rich telecommunications services offer significant opportunities to human users. To make these services more usable, facilitating personalisation is very important since it enhances the users' experience considerably. However, regardless how service providers organise their catalogues of features, they cannot achieve complete configurability due to the existence of feature interactions. Distributed Feature Composition (DFC) provides a comprehensive methodology, underpinned by a formal architecture model to address this issue. In this paper we present an approach based on using Binary Decision Diagrams (BDD) to find optimal reconfigurations of features when a user's preferences violate the technical constraints defined by a set of DFC rules. In particular, we propose hybridizing constraint programming and standard BDD compilation techniques in order to scale the construction of a BDD for larger size catalogues. Our approach outperforms the standard BDD techniques by reducing the memory requirements by as much as five orders-of-magnitude and compiles the catalogues for which the standard techniques ran out of memory. |

[LMO+08c] |
D. Lesaint, D. Mehta, B. O'Sullivan, L.O. Quesada, and N. Wilson.
Personalisation of Telecommunications Services as Combinatorial Optimisation.
In AAAI 2008: Proceedings of the Twenty-Third AAAI Conference on Artificial Intelligence, pages 1693-1698. AAAI Press, 2008.[ bib | .pdf ] Modern feature-rich telecommunications services offer significant opportunities to human users. To make these services more usable, facilitating personalisation is very important. Such personalisation enhances the users' experience considerably. The Session Initiation Protocol and Distributed Feature Composition architecture allow users to select and compose telecommunications network applications or features. In this paper we view feature composition as a configuration problem. We model feature composition using a variety of combinatorial optimisation paradigms. In particular, we present and evaluate an approach to finding optimal reconfigurations of network features when the user's preferences violate the technical constraints defined by a set of DFC rules. |

[LMO+08b] |
D. Lesaint, D. Mehta, B. O'Sullivan, L.O. Quesada, and N. Wilson.
Solving a Telecommunications Feature Subscription Configuration Problem.
Consistency Techniques for Finding an Optimal Relaxation of a Feature Subscription.
In ICTAI '08: Proceedings of the 2008 20th IEEE International Conference on Tools with Artificial Intelligence., volume 1, pages 283-290. IEEE Computer Society, 2008.[ bib | .pdf ] Telecommunication services are playing an increasing and potentially disruptive role in our lives. As a result, service providers seek to develop personalisation solutions that put customers in charge of controlling and enriching their services. In this context, the personalisation approach consists of exposing a catalogue of call control features (e.g., call-divert, voice-mail) to end-users and letting them subscribe to a subset of features subject to a set of precedence and exclusion constraints. When a subscription is inconsistent, the problem is to find an optimal relaxation. We present a constraint programming formulation to find an optimal reconfiguration of features. We investigate the performance of maintaining arc consistency within branch and bound search. We also study the impact of maintaining mixed consistency, that is maintaining different levels of consistency on different sets of variables. We further present a global constraint and a set of filtering rules that exploit the structure of our problem. We theoretically and experimentally compare all approaches. Our results demonstrate that the filtering rules of the global constraint outperform all other approaches when a catalogue is dense, and mixed consistency pays off when a catalogue is sparse. Keywords: constraint handling, personal computing, telecommunication services, tree searchingbranch and bound search, consistency techniques, constraint programming, feature subscription, optimal relaxation, personalisation solutions, telecommunication services. |

[LMO+08a] |
D. Lesaint, D. Mehta, B. O'Sullivan, L.O. Quesada, and N. Wilson.
Solving a Telecommunications Feature Subscription Configuration Problem.
In CP '08: Proceedings of the 14th international conference on Principles and Practice of Constraint Programming., volume 5202 of Lecture Notes in Computer Science, pages 67-81. Springer, 2008.[ bib | .pdf ] Call control features (e.g., call-divert, voice-mail) are primitive options to which users can subscribe off-line to personalise their service. The configuration of a feature subscription involves choosing and sequencing features from a catalogue and is subject to constraints that prevent undesirable feature interactions at run-time. When the subscription requested by a user is inconsistent, one problem is to find an optimal relaxation. In this paper, we show that this problem is NP-hard and we present a constraint programming formulation using the variable weighted constraint satisfaction problem framework. We also present simple formulations using partial weighted maximum satisfiability and integer linear programming. We experimentally compare our formulations of the different approaches; the results suggest that our constraint programming approach is the best of the three overall. |

[TOR08] |
M. Toro.
Exploring the possibilities and limitations of Concurrent Constraint Programming for Multimedia Interaction and Visual Programming for Musical Constraint Satisfaaction Problems.
Technical report, AVISPA Research Group, IRCAM and Pontificia Universidad
Javeriana, December 2008. [ bib | .pdf ] Multimedia interaction systems are inherently concurrent. Developing correct concurrent systems is diﬃcult because we need to consider all the possible interactions between processes. To reason formally about concurrent systems, there are several concurrent process calculi. We developed multiple prototypes for real-time capable interpreters for both, Concurrent Constraint Program- ming (CCP) and Non-deterministic Timed Concurrent Constraint (ntcc). We found out that using lightweight threads to implement these interpreters is not appropriate for real-time (RT) interac- tion. Instead, we recommend using event-driven programming. Using this model of concurrency, we developed Ntccrt, an interpreter for ntcc capable of RT interaction. Ntccrt is based on encoding ntcc processes as Gecode propagators. Using Ntccrt, we executed some models in Pure Data. Due to our success using Gecode, we upgraded Gelisp, providing a graphical interface to solve musical Constraint Satisfaction Problems (CSP) in OpenMusic based on Gecode. In Gelisp, constraints, search heuristics, and optimization criteria can be represented graphically. Using Gelisp, we suc- cessfully solved a CSP proposed by compositor Michael Jarrell. Keywords: concurrent constraint programming, constraint satisfaction problem, constraints, ntcc, gelisp, csp, interpreter, ccp, ntccrt, openmusic, real-time, gecol, gecode. |

[SAR08] |
G. Sarria.
Formal Models of Timed Musical Processes
PhD thesis, Universidad del Valle, 2008.
PhD thesis. xii+150.[ bib | .pdf ] In the last decades several formal models have been proposed to formalize various musical applications, to solve musical and improvisation problems and to prove properties in music. In this document we briefly describe some of those formal models, their applications and we give some considerations about them. We focus on the CCP calculi and specially on the ntcc calculus, a model of temporal concurrent constraint programming with the capability of expressing asynchronous and non-deterministic timed behaviour. This calculus has been used as a convenient formalism for expressing temporal musical processes. Additionally, in this thesis we propose a model of real-time concurrent constraint programming, called rtcc, which adds to ntcc the means for specifying and modeling real-time behaviour. This calculus is provided with a new construct for modeling strong preemption and another one for defining delays within the same time unit. Together with these new features we provide an operational semantics supporting resources, limited time and true concurrency. A denotational semantics based on Chu spaces is also provided. The lack of monotonicity derived from the new constructs and the inclusion of resources and time in the operational semantics precludes defining the denotations of processes in terms of quiescent points as is usual in CCP calculi such as ntcc. This dissertation also introduces a real-time logic for expressing temporal specifications of rtcc processes. An inference system is defined to prove that a process in the calculus satisfies a formula in the logic. Finally, we show the applicability of the rtcc calculus in music and multimedia interaction. We formalize the notion of OpenMusic Maquette as the main application. Keywords: Concurrent Constraint Programming, ntcc, rtcc, Music, Semantics of Programming Languages |

[AGPV07] |
J. Aranda, C. Di Giusto, C. Palamidessi, and F. D. Valencia.
On Recursion, Replication and Scope Mechanisms in Process Calculi.
In Proc. of Formal Methods for Components and Objects, 5th International
Symposium, FMCO 2006. volume 4709 of Lecture Notes in Computer Science, pages 185-206, Springer, November 2007.[ bib | .pdf ] This paper we shall survey and discuss in detail the work on the relative expressiveness of Recursion and Replication in various process calculi. Namely, CCS, the $\pi$-calculus, the Ambient calculus, Concurrent Constraint Programming and calculi for Cryptographic Protocols. We shall see that often the ability of expressing recursive behaviours via replication depends on the scoping mechanisms of the given calculus which compensate for the restriction of replication. |

[AGNV07] |
J. Aranda, C. Di Giusto, M. Nielsen, and F. D. Valencia.
CCS with Replication in the Chomsky Hierarchy: The Expressive Power of Divergence.
In Proc. of Programming Languages and Systems, 5th Asian Symposium, APLAS 2007. volume 4807 of Lecture Notes in Computer Science, pages 383-398, Springer, 2007.[ bib | .pdf ] A remarkable result in [N. Busi, M. Gabbrielli, and G. Zavattaro. Comparing recursion, replication, and iteration in process calculi. In ICALP'04, volume 3142 of Lecture Notes in Computer Science, pages 307-319. Springer-Verlag, 2004] shows that in spite of its being less expressive than CCS w.r.t. weak bisimilarity, CCS_{!} (a CCS variant where infinite behavior is specified by using replication rather than recursion) is Turing powerful. This is done by encoding Random Access Machines (RAM) in CCS_{!}. The encoding is said to be \emph{non-faithful} because it may move from a state which can lead to termination into a divergent one which do not correspond to any configuration of the encoded RAM. I.e., the encoding is not termination preserving. In this paper we study the existence of faithful encodings into CCS_{!} of models of computability \emph{strictly less} expressive than Turing Machines. Namely, grammars of Types 1 (Context Sensitive Languages), 2 (Context Free Languages) and 3 (Regular Languages) in the Chomsky Hierarchy. We provide faithful encodings of Type 3 grammars. We show that it is impossible to provide a faithful encoding of Type 2 grammars and that termination-preserving CCS_{!} processes can generate languages which are not Type 2. We finally show that the languages generated by termination-preserving CCS_{!} processes are Type 1. |

[OPV07] |
C. Olarte, C. Palamidessi, and F. D. Valencia.
Universal Timed Concurrent Constraint Programming.
In Proc. of ICLP 2007. 2007.[ bib | .pdf ] In this doctoral work we aim at developing a rich timed concurrent constraint (tcc) based language with strong ties to logic. The new calculus called Universal Timed Concurrent Constraint (utcc) increases the expressiveness of tcc languages allowing infinite behaviour and mobility. We introduce a constructor of the form (abs x; c)P (Abstraction in P) that can be viewed as a dual operator of the hidden operator local x in P. i.e. the later can be viewed as an existential quantication on the variable x and the former as an universal quantication of x, executing P[t=x] for all t s.t. the current store entails c[t=x]. As a compelling application, we applied this calculus to verify security protocols. |

[FOPV07] |
M. Falaschi, C. Olarte, C. Palamidessi, and F. D. Valencia.
Declarative Diagnosis of Temporal Concurrent Constraint Programs.
In Proc. of ICLP 2007. 2007.[ bib | .pdf ] We present a framework for the declarative diagnosis of nondeterministic timed concurrent constraint programs. We present a denotational semantics based on a (continuous) immediate consequence operator, TD, which models the process behaviour associated with a program D given in terms of sequences of constraints. Then, we show that, given the intended specication of D, it is possible to check the correctness of D by a single step of TD. In order to develop an eective debugging method, we approximate the denotational semantics of D. We formalize this method by abstract interpretation techniques, and we derive a finitely terminating abstract diagnosis method, which can be used statically. We define an abstract domain which allows us to approximate the infinite sequences by a finite `cut'. As a further development we show how to use a specific linear temporal logic for deriving automatically the debugging sequences. Our debugging framework does not require the user to either provide error symptoms in advance or answer questions concerning program correctness. Our method is compositional, that may allow to master the complexity of the debugging methodology. Keywords: Timed concurrent constraint programs, (modular) declarative debugging, denotational semantics, specification logic |

[MOR07] |
E. Monfroy, C. Olarte, and C. Rueda.
Process Calculi for Adaptive Enumeration Strategies in Constraint Programming.
Research in Computing Science, 2007.[ bib | .pdf ] Constraint programming (CP) has been extensively used to solve a wide variety of problems. Solving a constraint problem mainly consists in two phases: propagation to prune the search space, and enumeration to choose a variable and one of its values for branching. Enumeration strategies are crucial for resolution performances. We propose a framework to model adaptive enumeration strategies using a stochastic, non-deterministic timed concurrent constraint calculus. Using the reactivity of the calculus we can design enumeration strategies that adapt themselves according to information issued from the resolution process and from external solvers such as an incomplete solver. The experimental results show the effectiveness of our approach. |

[GPRV07] |
J. Gutierrez, J. Perez, C. Rueda, and F. D. Valencia.
Timed Concurrent Constraint Programming for Analysing Biological Systems
Electronic Notes in Theoretical Computer Science. Elsevier,
171(2):117-137. 2007.[ bib | .pdf ] In this paper we present our first approach to model and verify biological systems using ntcc, a concurrent constraint process calculus. We argue that the partial information constructs in ntcc can provide a suitable language for such systems. We also illustrate how ntcc may provide a unified framework for the analysis of biological systems, as they can be described, simulated and verified using the elements available in the calculus. Keywords: Process Calculi, Verification of Biological Systems, Partial Information, Concurrent Constraint Programming (CCP) |

[AAG+07] |
A. Arbelaez, A. Aristizabal, J. Gutierrez, H. Lopez, J. A. Perez, C. Rueda, and F. D. Valencia.
Process Calculi to Analyze Emerging Applications in Concurrency.
Matemáticas: Enseñanza Universitaria, 2007.[ bib | .pdf ] The notion of computation has significantly evolved in the last ten years or so. Modern computing systems (e.g., Internet) now exhibit infinite behavior, usually in the context of decentralized networks where interactions are inherently concurrent. The ubiquitous presence of this new kind of systems has led to the urgent need of counting with techniques for designing them in a reliable way. Process calculi are formal specification languages of concurrent systems in which the notions of process and interaction prevail. They are endowed with reasoning techniques that allow to rigorously determine whether a system exhibits some desirable properties. The generic nature of process calculi has made possible their successful application in very diverse areas. Based on recent work by the authors, this paper illustrates the use of process calculi in two emerging application areas: biology and security protocols. Basic notions of process calculi are introduced, real systems in the two areas are modeled and their properties are verified. Keywords: Computer Science, Concurrency Theory, Verification of Concurrent Systems, Process Calculi |

[OR06] |
C. Olarte, and C. Rueda.
A Stochastic Concurrent Constraint Based Framework to Model and Verify Biological Systems.
CLEI Electronic Journal, 9(2), 2006.[ bib | .pdf ] Concurrent process calculi are powerful formalisms for modelling concurrent systems. The mathematical style underlying process calculi allow to both model and verify properties of a system, thus providing a concrete design methodology for complex systems. ntcc, a constraints-based calculus for modeling temporal non-deterministic and asynchronous behaviour of processes has been proposed recently. Process interactions in ntcc can be determined by partial information (i.e. constraints) accumulated in a global store. ntcc has also an associated temporal logic with a proof system that can be conveniently used to formally verify temporal properties of processes. We are interested in using ntcc to model the activity of genes in biological systems. In order to account for issues such as the basal rate of reactions or binding affinities of molecular components, we believe that stochastic features must be added to the calculus. In this paper we propose an extension of ntcc with various stochastic constructs. We describe the syntax and semantics of this extension together with the new temporal logic and proof system associated with it. We show the relevance of the added features by modelling a non trivial biological system: the gene expression mechanisms of the lambda virus. We argue that this model is both more elaborate and compact than the stochastic pi calculus model proposed recently for the same system. |

[AAD+06] |
A. Allombert, G. Assayag, M. Desainte-Catherine, and C. Rueda.
Concurrent Constraint Models for Specifying Interactive
Scores.
In Proc. of the Third Sound and Music Computing
Conference (SMC'06)., May 2006.[ bib | .pdf ] We propose a formalism for the construction and performance of musical pieces composed of temporal structures involving discrete interactive events. The occurrence in time of these structures and events is partially defined according to constraints, such as Allen temporal relations. We represent the temporal structures using two constraint models. A constraints propagation model is used for the score composition stage, while a non deterministic temporal concurrent constraint calculus (NTCC) is used for the performance phase. The models are tested with examples of temporal structures computed with the GECODE constraint system library and run with a NTCC interpreter. Keywords: Concurrent Constraint Programming, Formal Languages for Computer Music, Interactive Scores |

[OMR06] |
C. Olarte, E. Monfroy, and C. Rueda.
Exploring Process Calculi as a Mechanism to Define Dynamic
Enumeration Strategies in Constraint Programming.
In Proc. of CLEI 2006 (32nd Latinamerican Conference on
Informatics), August 2006.[ bib | .pdf ] Constraint programming (CP) has been extensively used to solve a wide variety of problems. Its declarative flavor makes possible to state conditions over variables and the solver finds solutions by applying generic and complete techniques. The process of computing a solution in CP consists mainly in two phases: propagation in which values that are not consistent w.r.t. the constraints are eliminated, and enumeration that chooses a variable and a value for this variable to continue the search when no further propagation is possible. Constraint based languages offer a set of static enumeration strategies. The strategy chosen may affect drastically the time required to find a solution. In this paper we propose a framework to model dynamic enumeration strategies using a stochastic, non-deterministic timed concurrent constraint calculus. Thanks to the reactivity of the calculus, we are able to express strategies that dynamically change according to results observed. Additionally, the compositional approach of the calculus enables us to integrate external knowledge to adapt the strategy. Keywords: sntcc (stochastic, non-deterministic, timed concurrent constraint programming), Constraint programming, Dynamic enumeration strategies |

[PSV+06] |
C. Palamidessi, V. A. Saraswat, F. D. Valencia, and B. Victor.
On the expressiveness of linearity vs persistence in the asychronous
pi-calculus.
In Proc. of the 21th IEEE Symposium on Logic in Computer Science
(LICS 2006), pages 59-68. IEEE Computer Society, 2006.[ bib | .pdf ] We present an expressiveness study of linearity and persistence of processes. We choose the pi-calculus, one of the main representatives of process calculi, as a framework to conduct our study. We consider four fragments of the pi-calculus. Each one singles out a natural source of linearity/ persistence also present in other frameworks such as Concurrent Constraint Programming (CCP), Linear CCP, and several calculi for security. The study is presented by providing (or proving the non-existence of) encodings among the fragments, a processes-as-formulae interpretation and a reduction from Minsky machines. Keywords: Persistence/Linearity in process calculi, asynchronous pi-calculus, expresiveness of process calculi |

[GPR+06] |
J. Gutierrez, J. A. Perez, C. Rueda, and F. D. Valencia.
Timed Concurrent Constraint Programming for Analysing
Biological Systems.
To appear in the ENTCS (Electronic Notes in Theoretical Computer
Science) series, 2006.
Presented in the Workshop on Membrane Computing and Biologically
Inspired Process Calculi (MeCBIC 06), part of ICALP'06.[ bib | .pdf ] In this paper we present our first approach to model and verify biological systems using ntcc, a concurrent constraint process calculus. We argue that the partial information constructs in ntcc can provide a suitable language for such systems. We also illustrate how ntcc may provide a unified framework for the analysis of biological systems, as they can be described, simulated and verified using the elements provided by the calculus. Keywords: Process Calculi, Verification of Biological Systems, Partial Information, Concurrent Constraint Programming (CCP) |

[AG06] |
A. Arbelaez and J. E. Gutierrez.
Estudio Exploratorio de la Aplicacion de la Programacion
Concurrente por Restricciones en Bioinformatica.
BSc Thesis - Engineering Degree in Computer Science, Pontificia
Universidad Javeriana - Cali (Colombia)., 2006. [ bib | .pdf ] Keywords: Programacion Concurrente por Restricciones, Calculos de Procesos, Biologia Sistemica, Mozart, ntcc, Redes de Regulacion Genetica |

[AL06] |
A. A. Aristizabal and H. A. Lopez.
Using Process Calculi to Model and Verify Security
Properties in Real Communication Protocols.
BSc Thesis - Engineering Degree in Computer Science, Pontificia
Universidad Javeriana - Cali (Colombia)., 2006. [ bib | .pdf ] Keywords: Process Calculi, Verification of Security Protocols, SPL (Secure Protocol Language) |

[Rod06] |
J. Rodriguez.
Diseño e Implementación de un Sistema de Restricciones de Armonía Musical para Mozart.
BSc Thesis - Engineering Degree in Computer Science,
Universidad del Valle - Cali (Colombia)., 2006. [ bib | .pdf ] |

[Vil06] |
A. Villota Gómez.
Diseño e Implementación de un Sistema de Restricciones para Búsqueda de Patrones en Secuencias de ADN para Mozart.
BSc Thesis - Engineering Degree in Computer Science,
Universidad del Valle - Cali (Colombia)., 2006. [ bib | .pdf ] |

[ALR+06] |
A. Aristizabal, H. A. Lopez, C. Rueda, and F. D. Valencia.
Formally Reasoning About Security Issues in P2P Protocols: A Case
Study.
In S. Cruz-Lara and Y.K. Tsay, editors, Proc. of the Third
Taiwanese-French Conference on Information Technology (TFIT), March 2006.[ bib | .pdf ] Peer-to-Peer (P2P) systems can be seen as highly dynamic distributed systems designed for very specific purposes, such as resources sharing in collaborative settings. Because of their ubiquity, it is fundamental to provide techniques for formally proving properties of the communication protocols underlying those systems. In this paper we present a formal specification of MUTE, a protocol for P2P systems, modelled in the SPL process calculus. Furthermore, we use the SPL reasoning techniques to show how the protocol enjoys a secrecy property against outsider attacks. By formally modeling and analyzing a real-world, yet informally specified protocol, we bear witness to the applicability of SPL as a formalism to specify security protocols as well as the flexibility of its reasoning techniques. This paper represents our first approach towards the use of process calculi, in particular SPL, for the specification and reasoning of P2P protocols. Keywords: Verification of Security Protocols, SPL (Securiy Protocol Language), Peer-to-Peer (P2P) Systems, Process calculi |

[LPP+06] |
H. A. Lopez, C. Palamidessi, J. A. Perez, C. Rueda, and F. D. Valencia.
A Declarative Framework for Security: Secure Concurrent
Constraint Programming (Short Abstract).
In S. Etalle and M. Truszczynski, editors, Proc. of the 22nd
International Conference in Logic Programming (ICLP 2006), volume 4079 of
Lecture Notes in Computer Science, pages 449-450. Springer, 2006.[ bib | .pdf ] Due to technological advances, Security has become a serious challenge involving several disciplines of Computer Science. In recent years, there has been a growing interest in the analysis of security protocols and one promising approach is the development of formalisms that model communicating processes, in particular Process Calculi. The results are so far encouraging although most remains to be done. Concurrent Constraint Programming (CCP) is a well-established formalism which generalizes Logic Programming. One of the most appealing and distinct features of CCP is that it combines the traditional operational view of processes calculi with a declarative one of processes based upon logic. This combination allows CCP to benefit from the large body of techniques of both process calculi and logic. Our project Secure CCP (SCCP) aims at advancing both the theory and tools of CCP for analyzing and programming security protocols. The main goal is to develop a CCP-based framework for security protocols. Keywords: Process Calculi, Concurrent Constraint Programming (CCP), Verification of Security Protocols |

[AGO+06] |
A. Arbelaez, J. Gutierrez, C. Olarte, and C. Rueda.
A Generic Framework to Model, Simulate and Verify Genetic
Regulatory Networks (Poster).
In Proc. of CLEI 2006 (32nd Latinamerican Conference on
Informatics), 2006.[ bib | .pdf ] Process calculi are formalisms to model concurrent systems. Their mathematical basis and compositional style make possible to decompose a system into simple and well dened processes. Interaction among them is formally dened by the semantic of the calculi. These characteristics allow to study systems coming from dierent areas such as arts, engineering and sciences. In this paper we propose a generic framework to model, simulate and verify genetic regulatory networks based on a non-deterministic timed concurrent constraint calculus. This framework provides a set of process denitions to model generic/parametric components in a biological context, a simulator to observe the system evolution in time and some insights to perform formal proofs to verify and make inferences over the systems. An instantiation of the framework is presented by modeling the lactose operon. Keywords: Process calculi, Concurrent Constraint Programming, ntcc, Genetic Regulatory Networks, Lac Operon |

[AGP06] |
A. Arbelaez, J. Gutierrez, and J. A.Perez.
ATimed CCP in Systems Biology.
The ALP Newsletter. Association for Logic Programming (ALP). Vol. 19, No. 4. Nov-Dec. 2006. [ bib | .pdf ] Systems biology aims at getting a higher-level understanding of living matter, building on the available data at the molecular level. In this field, theories and methods from computer science have proven very useful, mainly for system modeling and simulation. Here we argue that languages based on timed concurrent constraint programming (timed ccp) - a well-established model for concurrency based on the idea of partial information - have a place in systems biology. We summarize some works in which our group has tried to assess the possibilities/limitations of one such formalisms in this domain. Our base language is ntcc, a non-deterministic, timed ccp process calculus that provides a unified framework for modeling, simulating and verifying several kinds of biological systems. We discuss how the interplay of the operational and logic perspectives that ntcc integrates greatly favors biological systems analysis. |

[ALR05] |
A. Aristizabal, H. A. Lopez, and C. Rueda.
Tiempo, Listas negras y Seguridad en SPL.
Technical report, AVISPA Research Group, Pontificia Universidad
Javeriana, February 2005. [ bib | .pdf ] Diversos avances concernientes a la seguridad dentro de las comunicaciones han utilizado nociones que permiten denotar tanto caducidad en los mensajes para sortear de manera efectiva una amplia gama de ataques, como el manejo del concepto de listas negras utilizadas para ubicar aquellos agentes de reputacion dudosa con los cuales no se debe establecer ningun contacto para evitar contratiempos. Debido a la relevancia intrinseca de la inclusion de esta clase de elementos frente a temas de seguridad, se introduciran nociones de este tipo dentro de un calculo de procesos de seguridad bien establecido denominado SPL, sin realizar cambios intrusivos dentro del lenguaje. De esta forma se permitiria modelar nuevos protocolos de comunicacion seguros, posibilitando el razonamiento de propiedades de seguridad a traves de las tecnicas inherentes a SPL. Por ultimo, se presentaran modelos especificados en este lenguaje de dos conocidos protocolos que hagan uso de las citadas nociones, de forma que se pueda verificar la validez de la inclusion de estos nuevos componentes. Keywords: Process Calculi, SPL (Security Protocol Language), Verification of Security Protocols, Peer-to-Peer (P2P) Systems, |

[ALR+05] |
A. Aristizabal, H. A. Lopez, C. Rueda, and F. D. Valencia.
Process Calculi for the Verification of Security Properties of
Communication Protocols for Peer-to-Peer systems.
Technical report, AVISPA Research Group, Pontificia Universidad
Javeriana, February 2005. [ bib | .pdf ] Recent advances in communication have made the use of dynamic and reconfigurable network topologies a mandatory requirement in scenarios where the participants must actively collaborate to each other to achieve a common, specific goal. A particular case of those scenarios are the Peer-to-Peer (P2P) systems. The wide applicability of P2P-based applications and its pervasive presence in corporate applications are two important factors that suggest a careful study of the communication protocols underlying these systems. Surprisingly, little effort has been invested in giving formal foundations that support both protocols and its security properties. This paper is intended to be a step towards such a research strand, using a process calculus as main resource to build such foundations. In particular, we focus on the reconfiguration problem in P2P-based applications. We propose two protocols for modeling this problem: while the first one is inspired on an existing protocol (known as the Friends Troubleshooting Network or FTN), the second constitutes an original proposal based on a multi-layered encryption system. We show how SPL (the process calculi in which both models are given) is well-suited to model and to proof certain security properties of the protocols. Keywords: Process Calculi, SPL (Security Protocol Language), Verification of Security Protocols, Peer-to-Peer (P2P) Systems, |

[DV05] |
S. S. Dantchev and F. D. Valencia.
On the computational limits of infinite satisfaction.
In Proceedings of the 2005 ACM Symposium on Applied
Computing (SAC), pages 393-397, 2005.[ bib | .pdf ] We study the computational limits of Constraint Satisfaction Problems (CSP's) allowing infinitely, or unboundedly, many indexed variables as in, e.g., xi > xi+2 for each i = 1, 2,.... We refer to these CSP's as Infinite CSP's (ICSP's). These problems arise in contexts in which the number of variables is unknown a priori as well as in optimization problems wrt the number of variables satisfying a given finite set of constraints.In particular, we investigate the decidability of the satisfiability problem for ICSP's wrt (a) the first-order theory specifying the indices of variables and (b) the dimension of the indices. We first show that (1) if the indices are one-dimensional and specified in the theory of the natural numbers with linear order (the theory of (N, 0, succ, <)) then the satisfiability problem is decidable. We then prove that, in contrast to (1), (2) if we move to the two-dimensional case then the satisfiability problem is undecidable for indices specified in (N, 0, succ, <) and even in (N, 0, succ). Finally, we show that, in contrast to (1) and (2), already in the one-dimensional case (3) if we also allow addition, we get undecidability. I.e., if the one-dimensional indices are specified in Presburger arithmetic (i.e., the theory of (N, 0, succ, <, +)) then satisfiability is undecidable |

[GPR05] |
J. Gutierrez, J. A. Perez, and C. Rueda.
Modelamiento de Sistemas Biologicos usando Calculos de
Procesos Concurrentes (Modelling Biological Systems using Process
Calculi).
Epiciclos, 4(1):79-101, 2005.[ bib | .pdf ] ENGLISH: Process calculi are formalisms that have been proposed to model concurrent systems in a wide variety of areas. Their mathematical foundations allow to define abstractions between the components of real systems and the constructions of a calculus. This is particularly convenient when verifying essential properties of the modelled systems. These features make process calculi an interesting approach to describe and verify biological systems. This article offers a survey of the process calculi proposed in the biological context. A particular class of calculi, those based on the notion of constraint, is thoroughly described. Those calculi provide, among other useful features, the transparent inclusion of quantitative and partial information into formal models. SPANISH: Los calculos de procesos son formalismos propuestos para modelar sistemas concurrentes en diversos ambitos. Su fundamentacion matematica permite establecer abstracciones entre los elementos reales de los sistemas y los componentes basicos del calculo, lo que facilita la verificacion de propiedades interesantes de los sistemas modelados. Estas caracteristicas perfilan a los calculos de procesos como una alternativa interesante para especificar y verificar propiedades esenciales de sistemas biologicos. Este articulo presenta un analisis de los calculos de procesos mas importantes propuestos recientemente en el contexto biologico. Especial atencion es dada a los calculos basados en restricciones, que permiten, entre otras cosas, el manejo transparente de informacion parcial y cuantitativa. Keywords: Process Calculi, Concurrent Constraint Programming (CCP), Molecular Biology. |

[ALR05b] |
A. Aristizabal, H. A. Lopez, and C. Rueda.
Using a Declarative Process Language for P2P Protocols.
ALP Newsletter, November 2005.
More info at url http://www.cs.kuleuven.ac.be/
dtai/projects/ALP/newsletter/. [ bib | .pdf ] Peer-to-Peer (P2P) systems can be seen as highly dynamic distributed systems designed for very specific purposes, such as resources sharing in collaborative settings. Because of their ubiquity, it is fundamental to provide techniques for formally proving properties of the communication protocols underlying those systems. In this paper we present a formal model of MUTE, a protocol for P2P systems, in the SPL; a specification language with a striking resemblance to Concurrent Constraint Programming. Furthermore, we use the SPL reasoning techniques to show the protocol enjoys a secrecy property againts outsider attacks. By formally modeling and analyzing a popular (albeit never specified) protocol, we bear witness to the applicability of SPL as a formalism to model and reason about security protocols as well as flexibility of the its reasoning techniques. Keywords: Process Calculi, SPL (Security Protocol Language), Verification of Security Protocols, Peer-to-Peer (P2P) Systems, |

[RV05] |
C. Rueda and F. V. Valencia.
A Temporal Concurrent Constraint Calculus as an Audio
Processing Framework.
In Proc. of the Second Sound and Music Computing
Conference (SMC'05)., 2005.[ bib | .pdf ] Audio processing systems involve complex interactions of concurrent processes. These are usually implemented using domain specific visual languages and tools more concerned with providing practical solutions than with giving formal meaning to the supplied audio unit combinators. Concurrent constraint process calculi have proved to be effective in modeling with precision a wide variety of concurrent systems. We propose using ntcc , a non deterministic temporal concurrent constraint calculus, to model audio processing systems. We show how the concurrent constraint nature of the calculus greatly simplify specifying complex synchronization patterns. We illustrate ntcc as audio processing framework by modeling unit combinators and using them ina an audio processing example. Keywords: Process Calculi, Formal Languages for Computer Music, Audio Processing |

[Val05] |
F. D. Valencia.
Decidability of infinite-state timed ccp processes and first-order
ltl.
Theor. Comput. Sci., 330(3):577-607, 2005.[ bib | .pdf ] The ntcc process calculus is a timed concurrent constraint programming (ccp) model equipped with a first-order linear-temporal logic (LTL) for expressing process specifications. A typical behavioral observation in ccp is the strongest postcondition (sp). The ntcc sp denotes the set of all infinite output sequences that a given process can exhibit. The verification problem is then whether the sequences in the sp of a given process satisfy a given ntcc LTL formula. This paper presents new positive decidability results for timed ccp as well as for LTL. In particular, we shall prove that the following problems are decidable: (1) the sp equivalence for the so-called locally-independent ntcc fragment; unlike other fragments for which similar results have been published, this fragment can specify infinite-state systems, (2) verification for locally-independent processes and negation-free first-order formulae of the ntcc LTL, (3) implication for such formulae, (4) Satisfiability for a first-order fragment of Manna and Pnueli's LTL. The purpose of the last result is to illustrate the applicability of ccp to well-established formalisms for concurrency. Keywords: Process calculi; Timed concurrent constraint programming; Infinite-state systems; Temporal logic; First-order LTL; Decidability |

[DPR05] |
A. Delgado, J. A. Perez, and C. Rueda.
Implementing an Abstraction Framework for Soft Constraints.
In J. D. Zucker and L. Saitta, editors, Abstraction,
Reformulation and Approximation, Proc. of the 6th International
Symposium, SARA 2005., volume 3607 of Lecture Notes in Computer
Science, pages 60-75. Springer, 2005.[ bib | .pdf ] Soft constraints are flexible schemes for modeling a wide spectrum of problems. A model based on a hierarchy of abstractions of soft constraint problems has been proposed before. We describe an efficient implementation of this scheme aimed at solving real life problems. Our system is integrated into the Mozart language in such a way that user control of the abstraction mechanism is straightforward.We explain how we adapted the theoretical results for our purposes and describe the experiences in this adaptation. We give comparative analysis of our system with respect to an implementation using soft constraints without the abstraction mechanism. Our tests show good performance results for over-constrained problems in real settings. Keywords: (Concurrent) Constraint Programming, Soft Constraints, Semiring-Based Constraints, Mozart |

[DP05] |
A. Delgado and J. A. Perez.
Analisis e Implementacion de Mecanismos de Restricciones
Debiles para Programacion Concurrente por Restricciones.
BSc Thesis - Engineering Degree in Computer Science, Pontificia
Universidad Javeriana - Cali (Colombia)., November 2005. [ bib | .pdf ] ENGLISH: Several real-life problems can be modelled and solved using Constraint Programming (CP). In CP problems are intuitively described as a set of mandatory conditions. This feature does not allow to represent criteria such as preferences in a natural way as well as affects the fidelity of models. This thesis studies a model for Soft Constraints (SCs), or constraints that may be violated and allow to represent preferences in problems. We adapt a theoretical framework for SCs to the context of concurrent constraint programming, thus increasing its applicability in real-life problems. Our approach is implemented in the Mozart programming language; analyses, comparisons as well as case studies are also presented. Several peer-reviewed international publications support our results. SPANISH: Diversos problemas de la vida real pueden modelarse y solucionarse utilizando programación por restricciones. En este contexto, los problemas se describen en terminos de condiciones obligatorias, lo que no permite representar naturalmente criterios como preferencias, y limita la fidelidad de los modelos. Esta tesis estudia un modelo de Restricciones Débiles (RDs): restricciones que pueden violarse y permiten representar preferencias. Un modelo teórico de RDs es adaptado al contexto de la pro-gramación concurrente por restricciones, ampliando asi su aplicabilidad en problemas reales. Se presentan dos implementaciones en el lenguaje Mozart, así como análisis, comparaciones y pruebas. Estos resultados son respaldados por varias publicaciones internacionales arbitradas. Keywords: Satisfacción de Restricciones, Problemas de Satisfacción de Restricciones (CSPs), Programación Concurrente por Restricciones, Restricciones Débiles, Mozart |

[OR05] |
C. Olarte and C. Rueda.
A Stochastic Non-deterministic Temporal Concurrent
Constraint Calculus.
In Proc. of International Conference of the Chilean
Computer Science Society (SCCC 2005). IEEE-CS, 2005.[ bib | .pdf ] We propose sntcc , a stochastic extension of the ntcc calculus, a model of temporal concurrent constraint programming with the capability of modeling asynchronous and non-deterministic timed behavior. We argue that such an extension is needed to faithfully model concurrent systems in real-life situations. We provide a suitable temporal logic and proof system for sntcc and illustrate how to use them for proving properties of stochastic systems. We argue that this modeling strategy of using explicit stochastic constructs within the calculus provides a runnable specication for a wide variety of stochastic systems that eases the task of formally reasoning about them. We give examples of specications in sntcc and use the extended linear temporal logic for proving properties about them. Keywords: Process calculi, sntcc (stochastic, non-deterministic, timed concurrent constraint programming), constraint programming |

[OR05b] |
C. Olarte and C. Rueda.
Using Stochastic NTCC to Model Biological Systems.
In Proc. of CLEI 2005 (31st Latinamerican Conference on
Informatics), 2005.[ bib | .pdf ] Concurrent process calculi are powerful formalisms for modeling concurrent systems. The mathematical style underlying process calculi allow to both model and verify properties of a system, thus providing a concrete design methodology for complex systems. ntcc , a constraints-based calculus for modeling temporal nondeterministic and asynchronous behavior of processes has been proposed recently. Process interactions in ntcc can be determined by partial information (i.e. constraints) accumulated in a global store. ntcc has also an associated temporal logic with a proof system that can be conveniently used to formally verify temporal properties of processes. We are interested in using ntcc to model the activity of genes in biological systems. In order to account for issues such as the basal rate of reactions or binding anities of molecular components, we believe that stochastic features must be added to the calculus. In this paper we propose an extension of ntcc with various stochastic constructs. We describe the syntax and semantics of this extension together with the new temporal logic and proof system associated with it. We show the relevance of the added features by modeling a non trivial biological system: the gene expression mechanisms of the virus. We argue that this model is both more elaborate and compact than the stochastic calculus model proposed recently for the same system. Keywords: NTCC, Lambda-Switch, biological systems, concurrent process calculus, concurrent constraint programming |

[DOP+05] |
A. Delgado, C. Olarte, J. A. Perez, and C. Rueda.
Semiring-based Fuzzy Constraints in Concurrent Constraint
Programming.
In A. Buss, J. F. Diaz, and C. Rueda, editors, Proc. of CLEI
2005 (31st Latinamerican Conference on Informatics), October 2005.[ bib | .pdf ] Several real-life problems have been successfully modeled and solved by using constraint programming (CP). Nevertheless, existing classical (hard) constraints can not express preferences, priorities or other soft criteria in a natural way. Since these criteria often occur in many scenarios, nding techniques and tools for appropriately including them in constraint programs is crucial. This paper describes an implementation of a soft constraints module for Mozart, a concurrent constraint programming language. The module, based on the semiring formalism for soft constraints, provides an intuitive set of constraints for solving fuzzy constraint satisfaction problems and is fully orthogonal to Mozart's implementation. We modify the concept of constraint proposed in the semiring formalism in order to dene a more intuitive notion. The new concept provides straightforward user control and is suitable for ecient implementation. We present a set of intuitive examples showing the advantages of our module in dierent contexts. Some issues regarding the integration of soft constraints in existing applications are also discussed. Keywords: Programming Languages, Constraint Solving, Soft Constraints, Mozart |

[DOP+04] |
A. Delgado, C. A. Olarte, J. A. Perez, and C. Rueda.
Implementing Semiring-Based Constraints Using Mozart.
In P. Van Roy, editor, Multiparadigm Programming in
Mozart/Oz, Second International Conference, MOZ 2004, Revised
Selected and Invited Papers, number 3389 in Lecture Notes in Computer
Science, pages 224-236. Springer, 2004.[ bib | .pdf ] Although Constraint Programming (CP) is considered a useful tool for tackling combinatorial problems, its lack of flexibility when dealing with uncertainties and preferences is still a matter for research. Several formal frameworks for soft constraints have been proposed within the CP community: all of them seem to be theoretically solid, but few practical implementations exist. In this paper we present an implementation for Mozart of one of these frameworks, which is based on a semiring structure. We explain how the soft constraints constructs were adapted to the propagation process that Mozart performs, and show how they can be transparently integrated with current Mozart hard propagators. Additionally, we show how over-constrained problems can be successfully relaxed and solved, and how preferences can be added to a problem, while keeping the formal model as a direct reference. Keywords: (Concurrent) Constraint Programming, Soft Constraints, Semiring-Based Constraints, Mozart |

[DGO+04b] |
J. F. Diaz, G. Gutierrez, C. A. Olarte, and C. Rueda.
Using Constraint Programming for Reconfiguration of
Electrical Power Distribution Networks.
In P. Van Roy, editor, Multiparadigm Programming in
Mozart/Oz, Second International Conference, MOZ 2004, Revised
Selected and Invited Papers, number 3389 in Lecture Notes in Computer
Science, pages 263-276. Springer, 2004.[ bib | .pdf ] The problem of reconfiguring power distribution system to reduce power losses has been extensively studied because of its significant economic impact. A variety of approximation computational models have recently been proposed. We describe a constraint programming model for this problem, using the MOzArt system. To handle real world reconfiguration systems we implemented and integrated into MOzArt an efficient constraint propagation system for the real numbers. We show how the CP approach leads to a simpler model and allows more flexible control of reconfiguration parameters. We analyze the performance of our system in canonical distribution networks of up to 60 nodes. We describe how the adaptability of the MOzArt search engine allows defining effective strategies for tackling a real distribution system reconfiguration of around 600 nodes. Keywords: (Concurrent) Constraint Programming, Constraint Satisfaction Problem (CSP), Network reconfiguration, Power losses reduction. |

[RV04b] |
C. Rueda and F. D. Valencia.
Non-viability deductions in arc-consistency computation.
In Proc. of the International Conference on Logic Programming
(ICLP 2004), volume 3132 of Lecture Notes in Computer Science, pages
343-355. Springer, 2004.[ bib | .pdf ] Arc-Consistency (AC) techniques have been used extensively in the study of Constraint Satisfaction Problems (CSP). These techniques are used to simplify the CSP before or during the search for its solutions. Some of the most efficient algorithms for AC computation are AC6++ and AC-7. The novelty of these algorithms is that they satisfy the so-called four desirable properties for AC computation. The main purpose of these interesting properties is to reduce as far as possible the number of constraint checks during AC computation while keeping a reasonable space complexity. In this paper we prove that, despite providing a remarkable reduction in the number of constraint checks, the four desirable properties do not guarantee a minimal number of constraint checks. We therefore refute the minimality claim in the paper introducing these properties. Furthermore, we propose a new desirable property for AC computation and extend AC6++ and AC-7 to consider such a property. We show theoretically and experimentally that the new property provides a further substantial reduction in the number of constraint checks. Keywords: Constraint Programming, Constraint Satisfaction Problems (CSPs), Arc Consistency, |

[DCL+04] |
J. F. Diaz, G. Caicedo, C. Lozano, G. Gutierrez, C. Olarte, and C. Rueda.
Loss Reduction in Distribution Networks using Concurrent
Constraint Programming.
In Proc. of 8th International Conference on Probability
Methods Applied to Power Systems (PMAPS'04), pages 295- 300.
IEEE, 2004.[ bib | .pdf ] This paper presents a new technical losses reduction model in an electrical energy distribution system by using network reconfiguration technique. First-order logic is used as the model specification language. This specification is easily translated into programmable sentences in the CCP (Concurrent Constraint Programming) paradigm. Unlike other existing methods in the literature, this model includes both the system operating constraints and the electric laws related to load flow. The CCP paradigm takes advantage of the interaction between these two types of constraints to reduce significantly the search tree, in contrast with the iterative methods used traditionally. In turn, itdoes not require the constraints verification once the solution is found. The tool developed has been tested forsimulating small cases up to 50 nodes, obtaining good accuracy and running times. The power flow results were validated against NEPLAN results and the reconfiguration results were compared to those obtained with three different tools developed by other authors. Keywords: Concurrent Constraint Programming, Constraint Satisfaction Problem (CSP), Network reconfiguration, Power losses reduction |

[ADO04] |
J. Aranda, J. F. Diaz, and J. Ortiz.
The Problem of Assigning Evaluators to the Articles
Submitted in an Academic Event: A Practical Solution
Incorporating Constraint Programming and Heuristics.
In P. Van Roy, editor, Multiparadigm Programming in
Mozart/Oz, Second International Conference, MOZ 2004, Revised
Selected and Invited Papers, number 3389 in Lecture Notes in Computer
Science, pages 305-316. Springer, 2004.[ bib | .pdf ] This article shows a practical solution to The Problem of Assigning Evaluators to the Articles Submitted in an Academic Event, a problem of combinatorial optimization. Apart from stating the problem formally and proposing a constraint model, the article describes the heuristics designed to find solutions. The application was developed using Mozart; different distribution strategies were implemented based on the already mentioned heuristics. The experimental partial results turned out to be competitive for real problems (180 articles, 25 evaluators). Keywords: (Concurrent) Constraint Programming, Constraint Satisfaction Problem (CSP) |

[MH04] |
M. P. Muñoz and A. R. Hurtado.
Programming Robotic Devices with a Timed Concurrent
Constraint Language (Short Abstract).
In M. Wallace, editor, Proc. of Tenth International
Conference on Principles and Practice of Constraint Programming
(CP 2004), volume 3258 of Lecture Notes in Computer Science, page
803, 2004.[ bib | .pdf ] This work shows the implementation of ntcc-lman, a framework for ntcc, a non deterministic timed concurrent constraint process calculus. This calculus provides a formal model in which concepts proper to robotic control can be conveniently represented. The ntcc-lman framework includes a ntcc based kernel language, a compiler, a constraint system, a formal abstract machine based on ntcc reduction rules and a virtual machine. We show how the framework can be used to program typical robotic tasks to control LEGO robots in real time using timed ccp technology. To our knowledge, this is the rst timed ccp framework for programming robotic devices. Keywords: Process Calculi, Abstract and Virtual Machines, ntcc, LEGO Robots, Constraint Programming |

[DGO+04] |
J. F. Diaz, G. Gutierrez, C. A. Olarte, and C. Rueda.
CRE2: a CP application for reconfiguring a power distribution
network for power losses reduction (Short Abstract).
In M. Wallace, editor, Proc. of Tenth International
Conference on Principles and Practice of Constraint Programming
(CP 2004), volume 3258 of Lecture Notes in Computer Science, pages
813-814. Springer, 2004.[ bib | .pdf ] Keywords: Concurrent Constraint Programming, Constraint Satisfaction Problem (CSP), Network reconfiguration, Power losses reduction |

[RV04] |
C. Rueda and F. D. Valencia.
On validity in modelization of musical problems by ccp.
Soft Comput., 8(9):641-648, 2004.[ bib | .pdf ] We show how the ntcc calculus, a model of temporal concurrent constraint programming with the capability of modeling asynchronous and non-deterministic timed behavior, can be used for modeling real musical processes. In particular, we show how the expressiveness of ntcc allows to implement complex interactions among musical processes handling different kinds of partial information. The ntcc calculus integrates two dimensions of soft computing: a horizontal dimension dealing with partial information and a vertical one in which non determinism comes into play. This integration is an improvement over constraint satisfaction and concurrent constraint programming models, allowing a more natural representation of a variety of musical processes. We use the nondeterminism facility of ntcc to build weaker representations of musical processes that greatly simplifies the formal expression and analysis of its properties. We argue that this modeling strategy provides a runnable specification for music problems that eases the task of formally reasoning about them. We show how the linear temporal logic associated with ntcc gives a very expressive setting for formally proving the existence of interesting musical properties of a process. We give examples of musical specifications in ntcc and use the linear temporal logic for proving properties of a realistic musical problem. Keywords: Concurrent Constraint Programming, Formal Languages for Computer Music |

[DOP+04b] |
A. Delgado, C. A. Olarte, J. A. Perez, and C. Rueda.
Implementing Semiring-Based Constraints using a Concurrent
Constraint Programming Language.
In S. Bistarelli and F. Rossi, editors, Proc. of the Sixth
International Workshop on Preferences and Soft Constraints. Part
of CP 2004., September 2004.[ bib | .pdf ] Several real life problems have been successfully modeled and solved by using concurrent constraint programming (CCP). Nevertheless, CCP can not express preferences, costs, priorities or other soft features in a straight way. The semiring based formalism proposed by Bistarelli et al. intends to generalize the softness concepts in constraint programming by means of a framework that can be cast in several others. However, few practical implementations have been published. This paper describes two implementations of a c-semiring based constraint system in the CCP-based language Mozart, following two strategies: a tuple evaluation approach and a propagator oriented implementation. We found that the latter enables us to smoothly integrate both hard and soft constraints while obtaining better performance. Keywords: (Concurrent) Constraint Programming, Soft Constraints, Semiring-Based Constraints, Mozart |

[HM04] |
A. R. Hurtado and M. P. Muñoz.
LMAN: Máquina Abstracta del Cálculo NTCC para
Programación Concurrente de Robots LEGO.
BSc Thesis - Engineering Degree in Computer Science, Pontificia
Universidad Javeriana - Cali (Colombia)., 2004. [ bib | .pdf ] Este proyecto de grado describe LMAN, máquina abstracta del cálculo NTCC para programación concurrente de robots LEGO. LMAN incluye tanto la especificación de la máquina abstracta, como la implementación de la máquina virtual, que actúa como el ejecutor notacional del cálculo NTCC. El modelo formal presentado en forma de máquina abstracta, provee la especificación de la máquina virtual. La máquina virtual está compuesta de un conjunto de instrucciones, registros y de un modelo de memoria; que actuando junto con un protocolo de comunicaciones, permiten controlar y ejecutar de manera eficiente y en tiempo real programas escritos en NTCC sobre los robots LEGO MindStorm. Keywords: Cálculo de Procesos, Máquina Abstracta, Máquina Virtual, Robots LEGO, Concurrencia, Restricciones, LMAN. |

[DPP+04] |
A. Delgado, J. A. Perez, G. Pabon, R. Jordan, J. F. Diaz, and C. Rueda.
An Interactive Tool for the Controlled Execution of an
Automated Timetabling Constraint Engine.
In P. Van Roy, editor, Lecture Notes in
Computer Science, pages 317-327. Springer, 2004.[ bib | .pdf ] Here we introduce DePathos, a graphical tool for a timetabling constraint engine (Pathos). Since the core of Pathos is textbased and provides little user-interaction, finding an appropriate solution for large problems (1000-2000 variables) can be a very time consuming process requiring the constant supervision of a constraint programming expert. DePathos uses an incremental solution strategy. Such strategy subdivides the problem and checks the consistency of the resulting subdivisions before incrementally unifying them. This has shown to be useful in finding inconsistencies and discovering over-constrained situations. Our incremental solution is based on hierarchical groupings defined at the problem domain level. This allows users to direct the timetabling engine in finding partial solutions that are meaningful in practice. We discuss the lessons learned from using Pathos in real settings, as well as the experiences of coupling DePathos to the timetabling engine. Keywords: Constraint Programming, Timetabling Problems, Incremental Execution, Mozart |

[Val03] |
F. D. Valencia.
Temporal Concurrent Constraint Programming.
PhD thesis, BRICS, 2003.
PhD thesis. xvii+174.[ bib | .pdf ]
Keywords: Concurrent Constraint Programming, ntcc, Applications, Expressiveness of Process Calculi |

[NV03] |
M. Nielsen and F. D. Valencia.
Notes on Timed CCP.
In Lectures on Concurrency and Petri Nets, volume 3098 of
Lecture Notes in Computer Science, pages 702-741. Springer, 2003.[ bib | .pdf ] A constraint is a piece of (partial) information on the values of the variables of a system. Concurrent constraint programming (ccp) is a model of concurrency in which agents (also called processes) interact by telling and asking information (constraints) to and from a shared store (a constraint). Timed (or temporal) ccp (tccp) extends ccp by agents evolving over time. A distinguishing feature of tccp, is that it combines in one framework an operational and algebraic view from process algebra with a declarative view based upon temporal logic. Tccp has been widely used to specify, analyze and program reactive systems. This note provides a comprehensive introduction to the background for and central notions from the theory of tccp. Furthermore, it surveys recent results on a particular tccp calculus, ntcc , and it provides a classification of the expressive power of various tccp languages. Keywords: Timed Concurrent Constraint Programming, ntcc |

[SD03] |
G. Sarria, and J. Diago.
OpenMusic for Linux and MacOS X.
Technical report, AVISPA Research Group, IRCAM and Pontificia Universidad
Javeriana, September 2003. [ bib | .pdf ] This document describes the development of the OpenMusic (OM) port to Linux and MacOS X. We begin explaining the main characteristics of OM, then we show the changes made for each platform (for Linux was chosen the compiler CMUCL and Gtk+ as graphical interface, and for MacOS X the new version 5.0 of MCL was enough for OM to be ported) and we finished with some conclusions and considerations for future work. Keywords: OpenMusic, Linux, MacOS X, Computer-Aided Composition |

[NPV02] |
M. Nielsen, C. Palamidessi, and F. D. Valencia.
Temporal concurrent constraint programming: Denotation, logic and
applications.
Nord. J. Comput., 9(1):145-188, 2002.[ bib | .pdf ] The tcc model is a formalism for reactive concurrent constraint programming. We present a model of temporal concurrent constraint programming which adds to tcc the capability of modeling asynchronous and nondeterministic timed behavior. We call this tcc extension the ntcc calculus. We also give a denotational semantics for the strongestpostcondition of ntcc processes and, based on this semantics, we develop a proof system for linear-temporal properties of these processes. The expressiveness of ntcc is illustrated by modeling cells, timed systems such as RCX controllers, multi-agent systems such as the Predator/Prey game, and musical applications such as generation of rhythms patterns and controlled improvisation. Keywords: Temporal concurrent constraint programming, calculi for concurrency, program specication, timed systems, reactive systems, multi-agent systems, musical applications |

[RAQ+01] |
C. Rueda, G. Alvarez, L. O. Quesada, G. Tamura, F. D. Valencia, J. F. Diaz, and
G. Assayag.
Integrating constraints and concurrent objects in musical
applications: A calculus and its visual language.
Constraints, 6(1):21-52, 2001.[ bib | .pdf ] We propose PiCO, a calculus integrating concurrent objects and constraints, as a base for music composition tools. In contrast with calculi such as [5], [9] or TyCO [16], both constraints and objects are primitive notions in PiCO. In PiCO a base object model is extended with constraints by orthogonally adding the notion of constraint system found in the rho-calculus [12]. Concurrent processes make use of a constraint store to synchronize communications either via the ask and tell operations of the constraint model or the standard message-passing mechanism of the object model. A message delegation mechanism built into the calculus allows encoding of general forms of inheritance. This paper includes encodings in PiCO of the concepts of class and sub-class. These allow us to represent complex partially defined objects such as musical structures in a compact way. We illustrate the transparent interaction of constraints and objects by a musical example involving harmonic and temporal relations. The relationship between Cordial, a visual language for music composition applications, and its underlying model PiCO is described. Keywords: Concurrent programming, constraint programming, concurrent constraint objects, TyCO, PiCO, formal calculi, mobile processes, visual language, computer aided music composition |

[SD01] |
G. Sarria and J. Diago.
Implantacion del Kernel de OpenMusic bajo Linux.
BSc Thesis - Engineering Degree in Computer Science, Pontificia
Universidad Javeriana - Cali (Colombia)., 2001. [ bib | .pdf ] En este documento se pretende mostrar los detalles de la Implantacion del Kernel de OpenMusic bajo Linux, siguiendo una metodologıa propuesta por los autores; la implantacion en este caso hace referencia al porte de una aplicacion originalmente desarrollada en MacOS. Se da inicio al porte familiarizandose con la aplicacion en MacOS, como lo harıa cualquier otro usuario pero prestando particular atencion en los detalles que mas adelante seran decisivos en la implementacion. A continuacion se explora el codigo y se procede a escoger las herramientas de desarrollo. Las herramientas de desarrollo escogidas son CMUCL, un compilador de Lisp para Unix que ha sido desarrollado durante mas de una decada en el Departamento de Ciencias de la Computacion de la Universidad Carnegie Mellon, y GTK+ para la interfaz grafica de la aplicacion. Contando con las herramientas de desarrollo adecuadas se disenaron e implementaron los modulos de la aplicacion (tanto en su parte grafica como en su parte operativa) en Linux y se llevaron a cabo las pruebas pertinentes para constatar que el porte de la aplicacion presenta las mismas caracterısticas y funcionalidad que la aplicacion original. Keywords: OpenMusic, Lisp, Linux, MacOS |

[DR00] |
J. F. Diaz and C. Rueda.
Modelos para la computacion movil (invited paper).
Revista Colombiana de Computacion, 1(1):29-45, 2000.[ bib | .pdf ] En este articulo presentamos un analisis comparativo de algunos calculos de computacion movil propuestos recientemente. Al tiempo que se describen el pi-calculo propuesto por Milner, un calculo de ambientes propuesto por Cardelli y Gordon y PiCO; un calculo de objetos y restricciones propuesto por el grupo AVISPA, se comparan entre ellos y se comentan sus principales caracteristicas asociadas a la computacion movil. Otros calculos como MCC y DyTyCO tambien son analizados. Keywords: Process calculi for mobile processes, pi-calculus, ambient calculus, PiCo |

[DRV98] |
J. F. Diaz, C. Rueda, and F. D. Valencia.
Pi+- calculus: A calculus for concurrent processes with constraints.
CLEI Electronic Journal, 1(2), 1998.[ bib | .pdf ] The pi-calculus is a formal model of concurrent computation based on the notion of naming. It has an important role to play in the search for more abstract theories of concurrent and communicating systems. In this paper we augment the pi-calculus with a constraint store and add the notion of constraint agent to the standard -calculus concept of agent. We call this extension the pi+-calculus. We also extend the notion of barbed bisimulation to define behavioral equivalence for the pi+-calculus and use it to characterize some equivalent behaviors derived from constraint agents. The paper discusses examples of the extended calculus showing the transparent interaction of constraints and communicating processes. Keywords: Concurrent Programming, Constraint Programming, pi-calculus, pi+-calculus, Formal Calculi, Mobile Processes. |

*This file has been generated by
bibtex2html 1.75*