Diferencias

Muestra las diferencias entre dos versiones de la página.

Enlace a la vista de comparación

grupos:avispa:repository_bib [2010/08/09 18:39]
crueda
grupos:avispa:repository_bib [2011/01/24 15:30] (actual)
Línea 1: Línea 1:
 +====== AVISPA BibTex File======
 +You can also see the list of publications in two flavours: [[grupos:avispa:repository_abstracts|with abstracts]] and [[grupos:avispa:publications_repository|without abstracts]]
  
 +----
 +
 +
 +<html>
 +
 +<p><a name="CR10"></a><pre>
 +@INPROCEEDINGS{conference:matelas:2010,
 + AUTHOR = {N. Catano and C. Rueda},
 + TITLE = {Matelas: A Predicate Calculus Common Formal
 +                 Definition for Social Networking},
 + BOOKTITLE = {ABZ 2010},
 + PAGES = {259-272},
 + YEAR = {2010},
 + EDITOR = {M. Frappier et al.},
 + VOLUME = {5977},
 + SERIES = {LNCS, Springer},
 + ADDRESS = {Québec, Canada}
 +}
 +
 +</pre>
 +</p>
 +
 +<p><a name="AP09"></a><pre>
 +@MISC{AP09,
 +  AUTHOR = {Jes\'{u}s Aranda and Jorge A. Perez},
 +  TITLE = {Languages for Concurrency Featuring Quantitative Information: 
 +                   An Overview and New Perspectives},
 +  HOWPUBLISHED = {The ALP Newsletter},
 +  ABSTRACT = {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.},
 +  VOLUME = {22},
 +  NUMBER = {1},
 +  INSTITUTION = {Association for Logic Programming (ALP)},
 +  MONTH = {March},
 +  PDF = {/wiki/lib/exe/fetch.php?media=grupos:avispa:papers:ap09.pdf},
 +  YEAR = {2009}
 +}
 +</pre>
 +</p>
 +
 +<p><a name="MP09"></a><pre>
 +@MISC{mp09,
 +  AUTHOR = {Jaime A. Mu\~{n}oz and Henry A. Perez},
 +  TITLE = {Aplicaci\'{o}n de la Programaci\'{o}n Concurrente por Restricciones 
 +                   en el Modelado de Procesos en la Membrana Celular},
 +  HOWPUBLISHED = {BSc Thesis -- Engineering Degree in Computer Science,
 +                   Pontificia Universidad Javeriana - Cali (Colombia).},
 +  ABSTRACT = {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.},
 +  PDF = {/wiki/lib/exe/fetch.php?media=grupos:avispa:papers:mp09.pdf},
 +  YEAR = {2009}
 +}
 +</pre>
 +</p>
 +
 +<p><a name="LPSS09"></a><pre>
 +@INPROCEEDINGS{LPSS09,
 +  AUTHOR = {Ivan Lanese and Jorge A. Perez and Davide Sangiorgi and Alan 
 +                   Schmitt},
 +  TITLE = {On the Expressiveness of Polyadicity in Higher-Order Communication},
 +  BOOKTITLE = {Proc. of 11th Italian Conference on Theoretical Computer 
 +                   Science (ICTCS09)},
 +  ABSTRACT = {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.},
 +  MONTH = {September},
 +  PDF = {/wiki/lib/exe/fetch.php?media=grupos:avispa:papers:lpss09.pdf},
 +  YEAR = {2009}
 +}
 +</pre>
 +</p>
 +
 +<p><a name="GPZ09"></a><pre>
 +@INPROCEEDINGS{GPZ09,
 +  AUTHOR = {Cinzia Di Giusto and Jorge A. Perez and Gianluigi Zavattaro},
 +  TITLE = {On the Expressiveness of Forwarding in Higher-Order Communication},
 +  BOOKTITLE = {Proc. of 6th International Colloquium on Theoretical Aspects 
 +                   of Computing (ICTAC09)},
 +  PAGES = {155-169},
 +  PUBLISHER = {Springer},
 +  SERIES = {Lecture Notes in Computer Science},
 +  VOLUME = {5684},
 +  LOCATION = {Amsterdam, The Netherlands},
 +  ISBN = {978-3-540-74791-8},
 +  ABSTRACT = {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.},
 +  MONTH = {August},
 +  PDF = {/wiki/lib/exe/fetch.php?media=grupos:avispa:papers:gpz09.pdf},
 +  YEAR = {2009}
 +}
 +</pre>
 +</p>
 +
 +<p><a name="CBG+09"></a><pre>
 +@ARTICLE{cbg+09,
 +  AUTHOR = {Nestor Catano and Fernando Barraza and Daniel Garcia and Pablo 
 +                   Ortega and Camilo Rueda},
 +  TITLE = {A Case Study in JML-Assisted Software Development},
 +  JOURNAL = {Electronic Notes in Theoretical Computer Science (ENTCS)},
 +  VOLUME = {240},
 +  ISSN = {1571-0661},
 +  PAGES = {5--21},
 +  PUBLISHER = {Elsevier Science Publishers B. V.},
 +  ADDRESS = {Amsterdam, The Netherlands, The Netherlands},
 +  ABSTRACT = {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.},
 +  PDF = {/wiki/lib/exe/fetch.php?media=grupos:avispa:papers:cbg_09.pdf},
 +  YEAR = {2009}
 +}
 +</pre>
 +</p>
 +
 +<p><a name="CR09"></a><pre>
 +@INPROCEEDINGS{cr09,
 +  AUTHOR = {Nestor Catano and Camilo Rueda},
 +  TITLE = {Teaching Formal Methods for the Unconquered Territory},
 +  BOOKTITLE = {Proceedings of the 2nd International FME Conference on 
 +                   Teaching Formal Methods (TFM2009)},
 +  PAGES = {2--19},
 +  LOCATION = {Eindhoven, the Netherlands},
 +  ISBN = {978-3-642-04911-8},
 +  MONTH = {November},
 +  PUBLISHER = {Springer},
 +  SERIES = {Lecture Notes in Computer Science},
 +  VOLUME = {5846/2009},
 +  ABSTRACT = {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.},
 +  PDF = {/wiki/lib/exe/fetch.php?media=grupos:avispa:papers:cr09.pdf},
 +  YEAR = {2009}
 +}
 +</pre>
 +</p>
 +
 +<p><a name="ARA09"></a><pre>
 +@PHDTHESIS{Ara09,
 +  AUTHOR = {Jes\'{u}s Aranda},
 +  TITLE = {On the Expressivity of Infinite and Local Behaviour in Fragments of the Pi-calculus},
 +  SCHOOL = {l'X, Ecole Polytechnique},
 +  NOTE = {PhD thesis},
 +  ABSTRACT = {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].},
 +  COMMENT = {Defence: November 27, 2009},
 +  INSTITUTION = {Ecole Polytechnique, France},
 +  KEYWORDS = {Concurrent Constraint Based Calculi, Denotational Semantics, 
 +                   Symbolic Semantics, Security Protocols, Temporal Logic},
 +  PDF = {/wiki/lib/exe/fetch.php?media=grupos:avispa:papers:ara09.pdf},
 +  YEAR = 2009
 +}
 +</pre>
 +</p>
 +
 +<p><a name="FOP09"></a><pre>
 +@INPROCEEDINGS{fop09,
 +  AUTHOR = {Moreno Falaschi and Carlos Olarte and Catuscia Palamidessi},
 +  TITLE = {A framework for abstract interpretation of timed concurrent
 +                   constraint programs},
 +  BOOKTITLE = {Proceedings of the 11th International ACM SIGPLAN Conference
 +                   on Principles and Practice of Declarative Programming
 +                   (PPDP09)},
 +  PAGES = {207-218},
 +  LOCATION = {Coimbra, Portugal},
 +  ISBN = {978-1-60558-568-0},
 +  MONTH = {September},
 +  EDITOR = {Ant{\'o}nio Porto and Francisco Javier L{\'o}pez-Fraguas},
 +  PUBLISHER = {ACM},
 +  ABSTRACT = {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.},
 +  PDF = {http://hal.archives-ouvertes.fr/docs/00/42/66/08/PDF/ppdp21-olarte.pdf},
 +  YEAR = {2009}
 +}
 +</pre>
 +</p>
 +
 +<p><a name="LOP09"></a><pre>
 +@INPROCEEDINGS{LOP09,
 + title = { {T}owards a {U}nified {F}ramework for {D}eclarative {S}tructured {C}ommunications},
 + author = {{H}ugo, {L}opez and {O}larte, {C}arlos and {J}orge, {P}erez},
 + abstract = {{W}e describe a unified framework for the declarative analysis of structured communications. {B}y 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. {I}n this work, we present a concurrent constraint interpretation of the language for structured communications proposed by {H}onda, {V}asconcelos, and {K}ubo. {D}istinguishing 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.},
 + keywords = {{C}oncurrent {C}onstraint {P}rogramming {S}essions {S}ervice {O}riented {C}omputing},
 + publisher = {{E}lsevier },
 + booktitle = {{P}roc. of {PLACES}'09 },
 + PDF = {http://hal.inria.fr/inria-00426609/en/},
 + YEAR = 2009
 +}
 +</pre>
 +</p>
 +
 +
 +<p><a name="AAO+09"></a><pre>
 +@INPROCEEDINGS{aao+09,
 +  AUTHOR = {Jes{\'u}s Aranda and G{\'e}rard Assayag and Carlos Olarte and
 +                   Jorge A. P{\'e}rez and Camilo Rueda and Mauricio Toro 
 +                   and Frank D. Valencia},
 +  TITLE = {An Overview of FORCES: An INRIA Project on Declarative 
 +                   Formalisms for Emergent Systems},
 +  BOOKTITLE = {Proc of 25th International Conference on Logic Programming 
 +                   (ICLP 2009)},
 +  PAGES = {509-513},
 +  LOCATION = {Pasadena, CA, USA},
 +  ISBN = {978-3-642-02845-8},
 +  MONTH = {July},
 +  EDITOR = {Patricia M. Hill and David Scott Warren},
 +  PUBLISHER = {Springer},
 +  SERIES = {Lecture Notes in Computer Science},
 +  VOLUME = {5649},
 +  ABSTRACT = {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.},
 +  PDF = {http://hal.archives-ouvertes.fr/docs/00/42/66/10/PDF/forces-iclp.pdf},
 +  YEAR = {2009}
 +}
 +</pre>
 +</p>
 +
 +<p><a name="PS09"></a><pre>
 +@INPROCEEDINGS{ps09,
 +  AUTHOR = {Salim Perchy and Gerardo Sarria},
 +  TITLE = {Dissonances: Brief Description and its Computational 
 +                   Representation in the RTCC Calculus},
 +  BOOKTITLE = {Proc of 6th Sound and Music Computing Conference (SMC2009)},
 +  PAGES = {53-58},
 +  LOCATION = {Porto, Portugal},
 +  ISBN = {978-989-95577-6-5},
 +  MONTH = {July},
 +  EDITOR = {Fabien Gouyon and \'{A}lvaro Barbosa and Xavier Serra},
 +  ABSTRACT = {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.},
 +  PDF = {/wiki/lib/exe/fetch.php?media=grupos:avispa:papers:ps09.pdf},
 +  YEAR = {2009}
 +}
 +</pre>
 +</p>
 +
 +<p><a name="OLA09"></a><pre>
 +@PHDTHESIS{Ola09,
 +  AUTHOR = {Olarte, C.},
 +  TITLE = {Universal Temporal Concurrent Constraint Programming},
 +  SCHOOL = {l'X, Ecole Polytechnique},
 +  NOTE = {PhD thesis},
 +  ABSTRACT = {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.},
 +  COMMENT = {Defence: September 29, 2009},
 +  INSTITUTION = {Ecole Polytechnique, France},
 +  KEYWORDS = {Concurrent Constraint Based Calculi, Denotational Semantics, 
 +                   Symbolic Semantics, Security Protocols, Temporal Logic},
 +  PDF = {/wiki/lib/exe/fetch.php?media=grupos:avispa:papers:ola09.pdf},
 +  YEAR = 2009
 +}
 +</pre>
 +</p>
 +
 +<p><a name="TOR09c"></a><pre>
 +@TECHREPORT{Tor09c,
 +  AUTHOR = {M. Toro},
 +  TITLE = {Towards a correct and efficient implementation of simulation and verification tools for Probabilistic ntcc},
 +  INSTITUTION = {AVISPA Research Group and Pontificia Universidad
 +                   Javeriana},
 +  ABSTRACT = {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 verification. We present a new simulation 
 +tool for Probabilistic ntcc (pntcc) and a prototype for verification 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.},
 +  KEYWORDS = {PNTCC, NTCC, VERIFICATION, SIMULATION, INTERPRETER},
 +  MONTH = {August},
 +  PDF = {/wiki/lib/exe/fetch.php?media=grupos:avispa:papers:tor09c.pdf},
 +  YEAR = 2009
 +}
 +</pre>
 +</p>
 +
 +<p><a name="TRAA09"></a><pre>
 +@INPROCEEDINGS{traa09,
 +  AUTHOR = {Mauricio Toro-Bermudez, Camilo Rueda, Carlos Agon, and Gerard Assayag},
 +  TITLE = {NTCCRT: A Concurrent Constraint Framework for Real-Time Interaction. },
 +  BOOKTITLE = {In Proc of the International Computer Music Conference, ICMC 2009},
 +  LOCATION = {Montreal, Canada},
 +  ABSTRACT = {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 difficult 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.},
 +  PDF = {/wiki/lib/exe/fetch.php?media=grupos:avispa:papers:traa09.pdf},
 +  YEAR = {2009}
 +}
 +</pre>
 +</p>
 +
 +<p><a name="TOR09b"></a><pre>
 +@TECHREPORT{Tor09b,
 +  AUTHOR = {M. Toro, C. Rueda, C. Agon, G. Assayag},
 +  TITLE = {GELISP: A library to represent musical CSPs and search strategies},
 +  INSTITUTION = {AVISPA Research Group, IRCAM and Pontificia Universidad
 +                   Javeriana},
 +  ABSTRACT = {In this paper we present Gelisp, a new library to 
 +represent musical Constraint Satisfaction Problems 
 +and search strategies intuitively. Gelisp has two 
 +interfaces, a command-line one for Common Lisp 
 +and a graphical one for OpenMusic. Using Gelisp, 
 +we solved a problem of automatic music genera- 
 +tion proposed by composer Michael Jarrell and we 
 +found solutions for the All-interval series.},
 +  KEYWORDS = {CSP, GELISP, GECODE, CONSTRAINTS, OPENMUSIC},
 +  MONTH = {May},
 +  PDF = {/wiki/lib/exe/fetch.php?media=grupos:avispa:papers:tor09b.pdf},
 +  YEAR = 2009
 +}
 +</pre>
 +</p>
 +<p><a name="AVV09"></a><pre>
 +@INPROCEEDINGS{avv09,
 +  AUTHOR = {Jes{\'u}s Aranda and Frank D. Valencia and Cristian Versari},
 +  TITLE = {On the Expressive Power of Restriction and Priorities in CCS 
 +                   with Replication},
 +  BOOKTITLE = {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},
 +  PAGES = {242-256},
 +  LOCATION = {York, UK},
 +  ISBN = {978-3-642-00595-4},
 +  SERIES = {Lecture Notes in Computer Science},
 +  VOLUME = {5504},
 +  MONTH = {March},
 +  PUBLISHER = {Springer},
 +  ABSTRACT = {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}.},
 +  PDF = {/wiki/lib/exe/fetch.php?media=grupos:avispa:papers:avv09.pdf},
 +  YEAR = {2009}
 +}
 +</pre>
 +</p>
 +<p><a name="LMO+09"></a><pre>
 +@INPROCEEDINGS{lmo+09,
 +  AUTHOR = {David Lesaint and Deepak Mehta and Barry O'Sullivan and Luis 
 +                   Omar Quesada and Nic Wilson},
 +  TITLE = {A Soft Global Precedence Constraint},
 +  BOOKTITLE = {IJCAI 2009: Proceedings of the Twenty-Third AAAI Conference 
 +                   on Artificial Intelligence},
 +  PAGES = {1693-1698},
 +  LOCATION = {Chicago, Illinois, USA},
 +  ISBN = {978-1-57735-368-3},
 +  PUBLISHER = {AAAI Press},
 +  ABSTRACT = {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.},
 +  PDF = {/wiki/lib/exe/fetch.php?media=grupos:avispa:papers:lmo_09.pdf},
 +  YEAR = {2009}
 +}
 +</pre>
 +</p>
 +<p><a name="Tor09"></a><pre>
 +@MISC{tor09,
 +  AUTHOR = {Mauricio Toro},
 +  TITLE = {Probabilistic Extension to the Concurrent Constraint Factor 
 +                   Oracle model for Music Improvisation},
 +  HOWPUBLISHED = {BSc Thesis -- Engineering Degree in Computer Science,
 +                   Pontificia Universidad Javeriana - Cali (Colombia).},
 +  ABSTRACT = {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.},
 +  KEYWORDS = {Factor Oracle, Concurrent Constraint Programming, CCP,
 +                   Machine Learning, Machine Improvisation, CCFOMI, 
 +                   GECODE, NTCC, PNTCC, Real-Time},
 +  PDF = {/wiki/lib/exe/fetch.php?media=grupos:avispa:papers:tor09.pdf},
 +  YEAR = 2009
 +}
 +</pre>
 +</p>
 +
 +<p><a name="PR08"></a><pre>
 +@INPROCEEDINGS{PR08,
 +  AUTHOR = {Jorge A. Perez and Camilo Rueda},
 +  TITLE = {Non-determinism and Probabilities in Timed Concurrent Constraint Programming},
 +  BOOKTITLE = {Proc. of 24th International Conference on Logic Programming (ICLP 2008)},
 +  LOCATION = {Udine, Italy},
 +  VOLUME = {5366},
 +  EDITOR = {Maria Garcia de la Banda and Enrico Pontelli},
 +  SERIES = {Lecture Notes in Computer Science},
 +  PAGES = {677-681},
 +  ISBN = {978-3-540-89981-5},
 +  PUBLISHER = {Springer},
 +  ABSTRACT = {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.},
 +  PDF = {/wiki/lib/exe/fetch.php?media=grupos:avispa:papers:pr08.pdf},
 +  YEAR = {2008}
 +}
 +</pre>
 +</p>
 +
 +<p><a name="LPSS08"></a><pre>
 +@INPROCEEDINGS{LPSS08,
 +  AUTHOR = {Lanese, I. and Perez, J. and Sangiorgi, D. and Schmitt, A.},
 +  TITLE = {On the {E}xpressiveness and {D}ecidability of {H}igher-{O}rder {P}rocess {C}alculi },
 +  BOOKTITLE = {Proc. of LICS'08},
 +  PAGES = {145--155},
 +  ABSTRACT = {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.},
 +  PDF = {/wiki/lib/exe/fetch.php?media=grupos:avispa:papers:lpss08.pdf},
 +  YEAR = 2008
 +}
 +</pre>
 +</p>
 +
 +<p><a name="BPV08"></a><pre>
 +@INPROCEEDINGS{bpv08,
 +  AUTHOR = {Romain Beauxis and Catuscia Palamidessi and Frank D. Valencia},
 +  TITLE = {On the Asynchronous Nature of the Asynchronous pi-Calculus},
 +  BOOKTITLE = {Concurrency, Graphs and Models, Essays Dedicated to Ugo
 +                   Montanari on the Occasion of His 65th Birthday},
 +  VOLUME = {5065},
 +  PAGES = {473-492},
 +  SERIES = {Lecture Notes in Computer Science},
 +  EDITOR = {Pierpaolo Degano and Rocco De Nicola and Jos{\'e} Meseguer},
 +  ISBN = {978-3-540-68676-7},
 +  PUBLISHER = {Springer},
 +  ABSTRACT = {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.},
 +  PDF = {/wiki/lib/exe/fetch.php?media=grupos:avispa:papers:bpv08.pdf},
 +  YEAR = {2008}
 +}
 +</pre>
 +</p>
 +
 +<p><a name="APRV08"></a><pre>
 +@INPROCEEDINGS{APRV08,
 +  AUTHOR = {Jes\'{u}s Aranda and Jorge Perez and Camilo Rueda and Frank D. Valencia},
 +  TITLE = {Stochastic {B}ehavior and {E}xplicit {D}iscrete {T}ime in {C}oncurrent {C}onstraint {P}rogramming},
 +  BOOKTITLE = {24th International Conference on Logic Programming (ICLP 2008)},
 +  PAGES = {682--686},
 +  ISBN = {978-3-540-89981-5},
 +  SERIES = {Lecture Notes in Computer Science},
 +  VOLUME = {5366},
 +  LOCATION = {Udine, Italy},
 +  PUBLISHER = {Springer-Verlag},
 +  ABSTRACT = {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.},
 +  PDF = {/wiki/lib/exe/fetch.php?media=grupos:avispa:papers:aprv08.pdf},
 +  YEAR = 2008
 +}
 +</pre>
 +</p>
 +<p><a name="CCAV08"></a><pre>
 +@ARTICLE{ccav08,
 +  AUTHOR = {Diletta Cacciagrano and Flavio Corradini and Jes\'{u}s Aranda 
 +                   and Frank D. Valencia},
 +  TITLE = {Linearity, Persistence and Testing Semantics in the 
 +                   Asynchronous Pi-Calculus},
 +  JOURNAL = {Electronic Notes in Theoretical Computer Science (ENTCS)},
 +  VOLUME = {194},
 +  NUMBER = {2},  
 +  ISSN = {1571-0661},
 +  PAGES = {59--84},
 +  PUBLISHER = {Elsevier Science Publishers B. V.},
 +  ADDRESS = {Amsterdam, The Netherlands, The Netherlands},
 +  ABSTRACT = {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.},
 +  PDF = {/wiki/lib/exe/fetch.php?media=grupos:avispa:papers:ccav08.pdf},
 +  YEAR = {2008}
 +}
 +</pre>
 +</p>
 +<p><a name="OV08b"></a><pre>
 +@INPROCEEDINGS{OV08b,
 +  AUTHOR = {Olarte, C. and Valencia, F.D.},
 +  TITLE = {The {E}xpressivity of {U}niversal {T}imed {CCP}: 
 +                   {U}ndecidability of {M}onadic {FLTL} and {C}losure 
 +                   {O}perators for {S}ecurity},
 +  BOOKTITLE = {PPDP '08: Proceedings of the 10th international ACM 
 +                   SIGPLAN conference on Principles and practice of 
 +                   declarative programming},
 +  YEAR = {2008},
 +  ISBN = {978-1-60558-117-0},
 +  PAGES = {8--19},
 +  LOCATION = {Valencia, Spain},
 +  PUBLISHER = {ACM},
 +  ADDRESS = {New York, NY, USA},
 +  ABSTRACT = {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.},
 +  PDF = {/wiki/lib/exe/fetch.php?media=grupos:avispa:papers:ov08b.pdf},
 +  YEAR = 2008
 +}
 +</pre>
 +</p>
 +<p><a name="OV08a"></a><pre>
 +@INPROCEEDINGS{OV08a,
 +  AUTHOR = {Olarte, C. and Valencia, F.D.},
 +  TITLE = {Universal {C}oncurrent {C}onstraint {P}rogramming: {S}ymbolic 
 +                   {S}emantics and {A}pplications to {S}ecurity},
 +  BOOKTITLE = {SAC '08: Proceedings of the 2008 ACM symposium on Applied 
 +                   computing},
 +  YEAR = {2008},
 +  ISBN = {978-1-59593-753-7},
 +  PAGES = {145--150},
 +  LOCATION = {Fortaleza, Ceara, Brazil},
 +  PUBLISHER = {ACM},
 +  ADDRESS = {New York, NY, USA},
 +  ABSTRACT = {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.},
 +  PDF = {/wiki/lib/exe/fetch.php?media=grupos:avispa:papers:ov08a.pdf},
 +  YEAR = 2008
 +}
 +</pre>
 +</p>
 +<p><a name="ORV08"></a><pre>
 +@INPROCEEDINGS{ORV08,
 +  AUTHOR = {Olarte, C. Rueda, C. and Valencia, F. D.},
 +  TITLE = {Universal Timed CCP: Expressivity and Application to Musical Improvisation},
 +  BOOKTITLE = {CLEI2008},
 +  ISBN = {978-950-9770-02-7},
 +  PAGES = {1465--1474},
 +  LOCATION = {Santa Fe, Argentina},
 +  ABSTRACT = {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.},
 +  PDF = {/wiki/lib/exe/fetch.php?media=grupos:avispa:papers:orv08.pdf},
 +  YEAR = 2008
 +}
 +</pre>
 +</p>
 +<p><a name="SR08"></a><pre>
 +@INPROCEEDINGS{SR08,
 +  AUTHOR = {Sarria, G. and Rueda, C.},
 +  TITLE = {Real-Time {C}oncurrent {C}onstraint {P}rogramming},
 +  BOOKTITLE = {CLEI2008},
 +  ISBN = {978-950-9770-02-7},
 +  PAGES = {1475--1484},
 +  LOCATION = {Santa Fe, Argentina},
 +  ABSTRACT = {The \texttt{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 
 +                   \texttt{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.},
 +  PDF = {/wiki/lib/exe/fetch.php?media=grupos:avispa:papers:sr08.pdf},
 +  YEAR = 2008
 +}
 +</pre>
 +</p>
 +<p><a name="HLM+08"></a><pre>
 +@INPROCEEDINGS{hlm+08,
 +  AUTHOR = {Tarik Hadzic and David Lesaint and Deepak Mehta and Barry 
 +                   O'Sullivan and Luis Omar Quesada Ramirez and Nic Wilson},
 +  TITLE = {A BDD Approach to the Feature Subscription Problem},
 +  BOOKTITLE = {ECAI 2008 - Proceedings of the 18th European Conference on 
 +                   Artificial Intelligence},
 +  VOLUME = {178},
 +  PAGES = {698--702},
 +  LOCATION = {Patras, Greece},
 +  MONTH = {July},
 +  SERIES = {Frontiers in Artificial Intelligence and Applications},
 +  ISBN = {978-1-58603-891-5},
 +  PUBLISHER = {IOS Press},
 +  ABSTRACT = {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.},
 +  PDF = {/wiki/lib/exe/fetch.php?media=grupos:avispa:papers:hlm_08.pdf},
 +  YEAR = {2008}
 +}
 +</pre>
 +</p>
 +<p><a name="LMO+08c"></a><pre>
 +@INPROCEEDINGS{lmo+08c,
 +  AUTHOR = {David Lesaint and Deepak Mehta and Barry O'Sullivan and Luis 
 +                   Omar Quesada and Nic Wilson},
 +  TITLE = {Personalisation of Telecommunications Services as Combinatorial
 +                   Optimisation},
 +  BOOKTITLE = {AAAI 2008: Proceedings of the Twenty-Third AAAI Conference 
 +                   on Artificial Intelligence},
 +  PAGES = {1693-1698},
 +  LOCATION = {Chicago, Illinois, USA},
 +  ISBN = {978-1-57735-368-3},
 +  PUBLISHER = {AAAI Press},
 +  ABSTRACT = {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.},
 +  PDF = {/wiki/lib/exe/fetch.php?media=grupos:avispa:papers:lmo_08c.pdf},
 +  YEAR = {2008}
 +}
 +</pre>
 +</p>
 +<p><a name="LMO+08b"></a><pre>
 +@INPROCEEDINGS{lmo+08b,
 +  AUTHOR = {David Lesaint and Deepak Mehta and Barry O'Sullivan and Luis 
 +                   Omar Quesada Ramirez and Nic Wilson},
 +  TITLE = {Consistency Techniques for Finding an Optimal Relaxation of a 
 +                   Feature Subscription},
 +  BOOKTITLE = {ICTAI '08: Proceedings of the 2008 20th IEEE International 
 +                   Conference on Tools with Artificial Intelligence},
 +  VOLUME = {1},
 +  PAGES = {283--290},
 +  ISBN = {978-0-7695-3440-4},
 +  PUBLISHER = {IEEE Computer Society},
 +  ABSTRACT = {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.},
 +  PDF = {/wiki/lib/exe/fetch.php?media=grupos:avispa:papers:lmo_08b.pdf},
 +  YEAR = {2008}
 +}
 +</pre>
 +</p>
 +<p><a name="LMO+08a"></a><pre>
 +@INPROCEEDINGS{lmo+08a,
 +  AUTHOR = {David Lesaint and Deepak Mehta and Barry O'Sullivan and Luis 
 +                   Omar Quesada Ramirez and Nic Wilson},
 +  TITLE = {Solving a Telecommunications Feature Subscription Configuration 
 +                   Problem},
 +  BOOKTITLE = {CP '08: Proceedings of the 14th international conference on 
 +                   Principles and Practice of Constraint Programming},
 +  LOCATION = {Sydney, Australia},
 +  VOLUME = {5202},
 +  SERIES = {Lecture Notes in Computer Science},
 +  PAGES = {67--81},
 +  ISBN = {978-3-540-85957-4},
 +  PUBLISHER = {Springer},
 +  ABSTRACT = {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.},
 +  PDF = {/wiki/lib/exe/fetch.php?media=grupos:avispa:papers:lmo08a.pdf},
 +  YEAR = {2008}
 +}
 +</pre>
 +</p>
 +<p><a name="TOR08"></a><pre>
 +@TECHREPORT{Tor08,
 +  AUTHOR = {M. Toro},
 +  TITLE = {Exploring the possibilities and limitations of Concurrent Programming for Multimedia Interaction and Visual Programming for Musical Constraint Satisfaction Problems},
 +  INSTITUTION = {AVISPA Research Group, IRCAM and Pontificia Universidad
 +                   Javeriana},
 +  ABSTRACT = {Multimedia interaction systems are inherently concurrent. Developing correct concurrent systems 
 +is difficult 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.},
 +  MONTH = {December},
 +  PDF = {/wiki/lib/exe/fetch.php?media=grupos:avispa:papers:tor08.pdf},
 +  YEAR = 2008
 +}
 +</pre>
 +</p>
 +<p><a name="SAR08"></a><pre>
 +@PHDTHESIS{Sar08,
 +  AUTHOR = {Sarria, G.},
 +  TITLE = {Formal Models of Timed Musical Processes},
 +  SCHOOL = {Universidad del Valle},
 +  NOTE = {PhD thesis. xii+150},
 +  ABSTRACT = {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 
 +                   \texttt{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 
 +                   \texttt{rtcc}, which adds to \texttt{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 \texttt{ntcc}.
 +                   This dissertation also introduces a real-time logic 
 +                   for expressing temporal specifications of 
 +                   \texttt{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 
 +                   \texttt{rtcc} calculus in music and multimedia 
 +                   interaction. We formalize the notion of OpenMusic 
 +                   Maquette as the main application.},
 +  COMMENT = {Defence: September 1, 2008},
 +  INSTITUTION = {Universidad del Valle},
 +  KEYWORDS = {Concurrent Constraint Programming, ntcc, rtcc, Music,
 +                   Semantics of Programming Languages},
 +  PDF = {/wiki/lib/exe/fetch.php?media=grupos:avispa:papers:sar08.pdf},
 +  YEAR = 2008
 +}
 +</pre>
 +</p>
 +<p><a name="AGPV07"></a><pre>
 +@INPROCEEDINGS{AGPV07,
 +  AUTHOR = {Jes{\'u}s Aranda and Cinzia Di Giusto and Catuscia Palamidessi 
 +                   and Frank D. Valencia},
 +  TITLE = {On Recursion, Replication and Scope Mechanisms in Process
 +                   Calculi},
 +  BOOKTITLE = {Formal Methods for Components and Objects, 5th 
 +                   International Symposium, FMCO 2006},
 +  PAGES = {185-206},
 +  PUBLISHER = {Springer},
 +  SERIES = {Lecture Notes in Computer Science},
 +  VOLUME = {4709},
 +  LOCATION = {Amsterdam, The Netherlands},
 +  ISBN = {978-3-540-74791-8},
 +  ABSTRACT = {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.},
 +  MONTH = {November},
 +  PDF = {/wiki/lib/exe/fetch.php?media=grupos:avispa:papers:agpv07.pdf},
 +  YEAR = 2007
 +}
 +</pre>
 +</p>
 +<p><a name="AGNV07"></a><pre>
 +@INPROCEEDINGS{AGNV07,
 +  AUTHOR = {Jes{\'u}s Aranda and Cinzia Di Giusto and Mogens Nielsen and
 +                   Frank D. Valencia},
 +  TITLE = {CCS with Replication in the Chomsky Hierarchy: The Expressive
 +                   Power of Divergence},
 +  BOOKTITLE = {Programming Languages and Systems, 5th Asian 
 +                   Symposium, APLAS 2007},
 +  PUBLISHER = {Springer},
 +  SERIES  = {Lecture Notes in Computer Science},
 +  VOLUME = {4807},
 +  PAGES = {383-398},
 +  ISBN = {978-3-540-76636-0},
 +  ABSTRACT = {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.},
 +  PDF = {/wiki/lib/exe/fetch.php?media=grupos:avispa:papers:agnv07.pdf},
 +  YEAR = 2007
 +}
 +</pre>
 +</p>
 +<p><a name="OPV07"></a><pre>
 +@INPROCEEDINGS{OPV07,
 +  AUTHOR = {Olarte, C. and Palamidessi, C. and Valencia, F.D.},
 +  TITLE = {Universal {T}imed {C}oncurrent {C}onstraint {P}rogramming},
 +  BOOKTITLE = {ICLP 2007},
 +  ABSTRACT = {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.},
 +  PDF = {/wiki/lib/exe/fetch.php?media=grupos:avispa:papers:opv07.pdf},
 +  YEAR = 2007
 +}
 +</pre>
 +</p>
 +<p><a name="FOPV07"></a><pre>
 +@INPROCEEDINGS{FOPV07,
 +  AUTHOR = {Falaschi, M. and Olarte, C. and Palamidessi, C. and Valencia, F.D.},
 +  TITLE = {Declarative {D}iagnosis of {T}emporal {C}oncurrent {C}onstraint {P}rograms},
 +  BOOKTITLE = {ICLP 2007},
 +  ABSTRACT = {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.},
 +  PDF = {/wiki/lib/exe/fetch.php?media=grupos:avispa:papers:fopv07.pdf},
 +  YEAR = 2007
 +}
 +</pre>
 +</p>
 +<p><a name="MOR07"></a><pre>
 +@ARTICLE{MOR07,
 +  AUTHOR = {Monfroy, E. and Olarte, C. and Rueda, C.},
 +  TITLE = {Process {C}alculi for {A}daptive {E}numeration {S}trategies 
 +                   in {C}onstraint {P}rogramming.},
 +  JOURNAL = {Research in Computing Science},
 +  ABSTRACT = {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 eectiveness of our 
 +                   approach.},
 +  PDF = {/wiki/lib/exe/fetch.php?media=grupos:avispa:papers:mor07.pdf},
 +  YEAR = 2007
 +}
 +</pre>
 +</p>
 +<p><a name="GPRV07"></a><pre>
 +@ARTICLE{GPRV07,
 +  AUTHOR = {Gutierrez, J. and Perez, J. and Rueda, C. and Valencia, F.D.},
 +  TITLE = {Timed {C}oncurrent {C}onstraint {P}rogramming for {A}nalysing 
 +                   {B}iological {S}ystems},
 +  BOOKTITLE = {Electronic Notes in Theoretical Computer Science},
 +  ABSTRACT = {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)},
 +  VOLUME = {171},
 +  NUMBER = {2},
 +  PAGES = {117--137},
 +  PDF = {/wiki/lib/exe/fetch.php?media=grupos:avispa:papers:gprv07.pdf},
 +  YEAR = 2007
 +}
 +</pre>
 +</p>
 +
 +<p><a name="AAG+07"></a><pre>
 +@ARTICLE{AAG+07,
 +  AUTHOR = {Arbelaez, A. and Aristizabal, A. and Gutierrez, J. and Lopez, 
 +                   H. and Perez, J. A. and Rueda, C. and Valencia, F. D.},
 +  TITLE = {Process {C}alculi to {A}nalyze {E}merging {A}pplications in 
 +                   {C}oncurrency},
 +  JOURNAL = {Matematicas: Ensenanza Universitaria},
 +  ABSTRACT = {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.},
 +  PDF = {/wiki/lib/exe/fetch.php?media=grupos:avispa:papers:aag_07.pdf},
 +  YEAR = 2007
 +}
 +</pre>
 +</p>
 +<p><a name="OR06"></a><pre>
 +@ARTICLE{OR06,
 +  AUTHOR = {Olarte, C. and Rueda, C.},
 +  TITLE = {A Stochastic Concurrent Constraint Based Framework to Model 
 +                   and Verify Biological Systems.},
 +  JOURNAL = {CLEI Electronic Journal},
 +  VOLUME = {9},
 +  NUMBER = {2},
 +  ABSTRACT = {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.},
 +  PDF = {/wiki/lib/exe/fetch.php?media=grupos:avispa:papers:or06.pdf},
 +  YEAR = 2006
 +}
 +</pre>
 +</p>
 +<p><a name="AAD+06"></a><pre>
 +@INPROCEEDINGS{AAD+06,
 +  AUTHOR = {Allombert, A. and Assayag, G. and Desainte-Catherine,
 +                   M. and Rueda, C.},
 +  TITLE = {Concurrent {C}onstraint {M}odels for {S}pecifying
 +                   {I}nteractive {S}cores},
 +  BOOKTITLE = {{T}hird {S}ound and {M}usic {C}omputing
 +                   {C}onference ({SMC}'06).},
 +  ABSTRACT = {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},
 +  MONTH = {May},
 +  PDF = {/wiki/lib/exe/fetch.php?media=grupos:avispa:papers:aad+06.pdf},
 +  YEAR = 2006
 +}
 +</pre>
 +</p>
 +<p><a name="OMR06"></a><pre>
 +@INPROCEEDINGS{OMR06,
 +  AUTHOR = {Olarte, C. and Monfroy, E. and Rueda, C.},
 +  TITLE = {Exploring {P}rocess {C}alculi as a {M}echanism to
 +                   {D}efine {D}ynamic {E}numeration {S}trategies in
 +                   {C}onstraint {P}rogramming.},
 +  BOOKTITLE = {{CLEI} 2006 (32nd {L}atinamerican
 +                   {C}onference on {I}nformatics)},
 +  ABSTRACT = {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. },
 +  ISBN = {956-303-028-1},
 +  KEYWORDS = {sntcc (stochastic, non-deterministic, timed concurrent
 +                   constraint programming), Constraint programming,
 +                   Dynamic enumeration strategies},
 +  MONTH = {August},
 +  PDF = {/wiki/lib/exe/fetch.php?media=grupos:avispa:papers:omr06.pdf},
 +  YEAR = 2006
 +}
 +</pre>
 +</p>
 +<p><a name="PSV+06"></a><pre>
 +@INPROCEEDINGS{PSV+06,
 +  AUTHOR = {C. Palamidessi and V. A. Saraswat and F. D. Valencia
 +                   and B. Victor},
 +  TITLE = {On the Expressiveness of Linearity vs Persistence in
 +                   the Asychronous Pi-Calculus.},
 +  BOOKTITLE = {21th IEEE Symposium on Logic in Computer
 +                   Science (LICS 2006)},
 +  PAGES = {59-68},
 +  PUBLISHER = {IEEE Computer Society},
 +  ABSTRACT = {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},
 +  PDF = {/wiki/lib/exe/fetch.php?media=grupos:avispa:papers:psv+06.pdf},
 +  YEAR = 2006
 +}
 +</pre>
 +</p>
 +<p><a name="GPR+06"></a><pre>
 +@ARTICLE{GPR+06,
 +  AUTHOR = {Gutierrez, J. and Perez, J. A. and Rueda, C. and
 +                   Valencia, F. D.},
 +  TITLE = {Timed {C}oncurrent {C}onstraint {P}rogramming for
 +                   {A}nalysing {B}iological {S}ystems.},
 +  JOURNAL = {To appear in the ENTCS (Electronic Notes in
 +                   Theoretical Computer Science) series},
 +  NOTE = {Presented in the Workshop on Membrane Computing and
 +                   Biologically Inspired Process Calculi (MeCBIC 06), part
 +                   of ICALP'06.},
 +  ABSTRACT = {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)},
 +  PDF = {/wiki/lib/exe/fetch.php?media=grupos:avispa:papers:gpr+06.pdf},
 +  YEAR = 2006
 +}
 +</pre>
 +</p>
 +<p><a name="AG06"></a><pre>
 +@MISC{AG06,
 +  AUTHOR = {Arbelaez, A. and Gutierrez, J. E.},
 +  TITLE = {Estudio {E}xploratorio de la {A}plicacion de la
 +                   {P}rogramacion {C}oncurrente por {R}estricciones en
 +                   {B}ioinformatica},
 +  HOWPUBLISHED = {BSc Thesis -- Engineering Degree in Computer Science,
 +                   Pontificia Universidad Javeriana - Cali (Colombia).},
 +  KEYWORDS = {Programacion Concurrente por Restricciones, Calculos
 +                   de Procesos, Biologia Sistemica, Mozart, ntcc, Redes de
 +                   Regulacion Genetica},
 +  PDF = {/wiki/lib/exe/fetch.php?media=grupos:avispa:papers:ag06.pdf},
 +  YEAR = 2006
 +}
 +</pre>
 +</p>
 +<p><a name="AL06"></a><pre>
 +@MISC{AL06,
 +  AUTHOR = {Aristizabal, A. A. and Lopez, H. A.},
 +  TITLE = {Using {P}rocess {C}alculi to {M}odel and {V}erify
 +                   {S}ecurity {P}roperties in {R}eal {C}ommunication
 +                   {P}rotocols.},
 +  HOWPUBLISHED = {BSc Thesis -- Engineering Degree in Computer Science,
 +                   Pontificia Universidad Javeriana - Cali (Colombia).},
 +  KEYWORDS = {Process Calculi, Verification of Security Protocols,
 +                   SPL (Secure Protocol Language)},
 +  PDF = {/wiki/lib/exe/fetch.php?media=grupos:avispa:papers:al06.pdf},
 +  YEAR = 2006
 +}
 +</pre>
 +</p>
 +<p><a name="Rod06"></a><pre>
 +@MISC{Rod06,
 +  AUTHOR = {Jessica Rodriguez},
 +  TITLE = {Dise\~{n}o e Implementaci\'{o}n de un Sistema de Restricciones
 +                   de Armon\'{\i}a Musical para Mozart},
 +  HOWPUBLISHED = {BSc Thesis -- Engineering Degree in Computer Science,
 +                   Universidad del Valle - Cali (Colombia).},
 +  PDF = {/wiki/lib/exe/fetch.php?media=grupos:avispa:papers:rod06.pdf},
 +  YEAR = 2006
 +}
 +</pre>
 +</p>
 +<p><a name="Vil06"></a><pre>
 +@MISC{Vil06,
 +  AUTHOR = {Ángela Villota Gómez},
 +  TITLE = {Dise\~{n}o e Implementaci\'{o}n de un Sistema de Restricciones
 +                   para Búsqueda de Patrones en Secuencias de ADN para Mozart},
 +  HOWPUBLISHED = {BSc Thesis -- Engineering Degree in Computer Science,
 +                   Universidad del Valle - Cali (Colombia).},
 +  PDF = {/wiki/lib/exe/fetch.php?media=grupos:avispa:papers:vil06.pdf},
 +  YEAR = 2006
 +}
 +</pre>
 +</p>
 +<p><a name="ALR+06"></a><pre>
 +@INPROCEEDINGS{ALR+06,
 +  AUTHOR = {A. Aristizabal and H. A. Lopez and C. Rueda and F. D.
 +                   Valencia},
 +  TITLE = {{Formally Reasoning About Security Issues in P2P
 +                   Protocols: A Case Study}},
 +  BOOKTITLE = {Third Taiwanese-French Conference on
 +                   Information Technology (TFIT)},
 +  EDITOR = {S. Cruz-Lara and Y.K. Tsay},
 +  ABSTRACT = {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},
 +  MONTH = {March},
 +  PDF = {/wiki/lib/exe/fetch.php?media=grupos:avispa:papers:alr+06.pdf},
 +  YEAR = 2006
 +}
 +</pre>
 +</p>
 +<p><a name="LPP+06"></a><pre>
 +@INPROCEEDINGS{LPP+06,
 +  AUTHOR = {H. A. Lopez and C. Palamidessi and J. A. Perez and C.
 +                   Rueda and F. D. Valencia},
 +  TITLE = {A {D}eclarative {F}ramework for {S}ecurity: {S}ecure
 +                   {C}oncurrent {C}onstraint {P}rogramming ({S}hort
 +                   {A}bstract).},
 +  BOOKTITLE = {22nd International Conference in Logic
 +                   Programming (ICLP 2006)},
 +  EDITOR = {Etalle, S. and Truszczynski, M.},
 +  VOLUME = {4079},
 +  SERIES = {Lecture Notes in Computer Science},
 +  PAGES = {449-450},
 +  PUBLISHER = {Springer},
 +  ABSTRACT = {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. },
 +  ISBN = {3-540-36635-0},
 +  KEYWORDS = {Process Calculi, Concurrent Constraint Programming
 +                   (CCP), Verification of Security Protocols},
 +  PDF = {/wiki/lib/exe/fetch.php?media=grupos:avispa:papers:lpp+06.pdf},
 +  YEAR = 2006
 +}
 +</pre>
 +</p>
 +<p><a name="AGO+06"></a><pre>
 +@INPROCEEDINGS{AGO+06,
 +  AUTHOR = {Arbelaez, A. and Gutierrez, J. and Olarte, C. and
 +                   Rueda, C.},
 +  TITLE = {A {G}eneric {F}ramework to {M}odel, {S}imulate and
 +                   {V}erify {G}enetic {R}egulatory {N}etworks ({P}oster)},
 +  BOOKTITLE = {{CLEI} 2006 (32nd {L}atinamerican
 +                   {C}onference on {I}nformatics)},
 +  ABSTRACT = {Process calculi are formalisms to model concurrent
 +                   systems. Their mathematical basis and compositional
 +                   style make possible to decompose a system into simple
 +                   and well de ned processes. Interaction among them is
 +                   formally de ned by the semantic of the calculi. These
 +                   characteristics allow to study systems coming from
 +                   di erent 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
 +                   de nitions 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.},
 +  ISBN = {956-303-028-1},
 +  KEYWORDS = {Process calculi, Concurrent Constraint Programming,
 +                   ntcc, Genetic Regulatory Networks, Lac Operon},
 +  PDF = {/wiki/lib/exe/fetch.php?media=grupos:avispa:papers:ago+06.pdf},
 +  YEAR = 2006
 +}
 +</pre>
 +</p>
 +<p><a name="AGP06"></a><pre>
 +@MISC{AGP06,
 +  AUTHOR = {A. Arbelaez, J. Gutierrez and J. A. Perez},
 +  TITLE = {{Timed CCP in Systems Biology}},
 +  HOWPUBLISHED = {The ALP Newsletter},
 +  ABSTRACT = {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.},
 +  VOLUME = {19},
 +  NUMBER = {4},
 +  INSTITUTION = { Association for Logic Programming (ALP)},
 +  MONTH = {Nov-Dic},
 +  PDF = {/wiki/lib/exe/fetch.php?media=grupos:avispa:papers:agp06.pdf},
 +  YEAR = 2006
 +}
 +</pre>
 +</p>
 +<p><a name="Que06"></a><pre>
 +@PHDTHESIS{Que06,
 +  AUTHOR = {Quesada, L. O.},
 +  TITLE = {Solving Constrained Graph Problems using Reachability 
 +                   Constraints based on Transitive Closure and Dominators},
 +  SCHOOL = {Universit\'{e} Catholique de Louvain},
 +  NOTE = {PhD thesis. xiv+136},
 +  COMMENT = {Defence: November 10, 2006},
 +  INSTITUTION = {Universit\'{e} Catholique de Louvain},
 +  PDF = {/wiki/lib/exe/fetch.php?media=grupos:avispa:papers:que06.pdf},
 +  YEAR = 2006
 +}
 +</pre>
 +</p>
 +<p><a name="ALR05"></a><pre>
 +@TECHREPORT{ALR05,
 +  AUTHOR = {A. Aristizabal and H. A. Lopez and C. Rueda},
 +  TITLE = {Tiempo, {L}istas negras y {S}eguridad en {SPL}},
 +  INSTITUTION = {AVISPA Research Group, Pontificia Universidad
 +                   Javeriana},
 +  ABSTRACT = {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,},
 +  MONTH = {February},
 +  PDF = {/wiki/lib/exe/fetch.php?media=grupos:avispa:papers:alr05.pdf},
 +  YEAR = 2005
 +}
 +</pre>
 +</p>
 +<p><a name="ALR+05"></a><pre>
 +@TECHREPORT{ALR+05,
 +  AUTHOR = {A. Aristizabal and H. A. Lopez and C. Rueda and F. D.
 +                   Valencia},
 +  TITLE = {{Process Calculi for the Verification of Security
 +                   Properties of Communication Protocols for Peer-to-Peer
 +                   systems}},
 +  INSTITUTION = {AVISPA Research Group, Pontificia Universidad
 +                   Javeriana},
 +  ABSTRACT = {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,},
 +  MONTH = {February},
 +  PDF = {/wiki/lib/exe/fetch.php?media=grupos:avispa:papers:alr+05.pdf},
 +  YEAR = 2005
 +}
 +</pre>
 +</p>
 +<p><a name="DV05"></a><pre>
 +@INPROCEEDINGS{DV05,
 +  AUTHOR = {Dantchev, S. S. and Valencia, F. D.},
 +  TITLE = {On the computational limits of infinite satisfaction.},
 +  BOOKTITLE = {Proceedings of the 2005 {ACM} {S}ymposium on {A}pplied
 +                   {C}omputing ({SAC})},
 +  PAGES = {393-397},
 +  ABSTRACT = {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},
 +  PDF = {/wiki/lib/exe/fetch.php?media=grupos:avispa:papers:dv05.pdf},
 +  YEAR = 2005
 +}
 +</pre>
 +</p>
 +<p><a name="GPR05"></a><pre>
 +@ARTICLE{GPR05,
 +  AUTHOR = {Gutierrez, J. and Perez, J. A. and Rueda, C.},
 +  TITLE = {Modelamiento de {S}istemas {B}iologicos usando
 +                   {C}alculos de {P}rocesos {C}oncurrentes ({M}odelling
 +                   {B}iological {S}ystems using {P}rocess {C}alculi)},
 +  JOURNAL = {Epiciclos},
 +  VOLUME = {4},
 +  NUMBER = {1},
 +  PAGES = {79-101},
 +  ABSTRACT = {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.},
 +  PDF = {/wiki/lib/exe/fetch.php?media=grupos:avispa:papers:gpr05.pdf},
 +  YEAR = 2005
 +}
 +</pre>
 +</p>
 +<p><a name="ALR05b"></a><pre>
 +@MISC{ALR05b,
 +  AUTHOR = {A. Aristizabal and H. A. Lopez and C. Rueda},
 +  TITLE = {{Using a Declarative Process Language for P2P
 +                   Protocols}},
 +  HOWPUBLISHED = {ALP Newsletter},
 +  NOTE = {More info at url http://www.cs.kuleuven.ac.be/
 +                   dtai/projects/ALP/newsletter/},
 +  ABSTRACT = { 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,},
 +  MONTH = {November},
 +  PDF = {/wiki/lib/exe/fetch.php?media=grupos:avispa:papers:alr05b.pdf},
 +  YEAR = 2005
 +}
 +</pre>
 +</p>
 +<p><a name="RV05"></a><pre>
 +@INPROCEEDINGS{RV05,
 +  AUTHOR = {Rueda, C. and Valencia, F. V.},
 +  TITLE = {A {T}emporal {C}oncurrent {C}onstraint {C}alculus as
 +                   an {A}udio {P}rocessing {F}ramework},
 +  BOOKTITLE = {{S}econd {S}ound and {M}usic {C}omputing
 +                   {C}onference ({SMC}'05).},
 +  ABSTRACT = {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},
 +  PDF = {/wiki/lib/exe/fetch.php?media=grupos:avispa:papers:rv05.pdf},
 +  YEAR = 2005
 +}
 +</pre>
 +</p>
 +<p><a name="Val05"></a><pre>
 +@ARTICLE{Val05,
 +  AUTHOR = {Valencia, F. D.},
 +  TITLE = {Decidability of infinite-state timed ccp processes and
 +                   first-order ltl.},
 +  JOURNAL = {Theor. Comput. Sci.},
 +  VOLUME = {330},
 +  NUMBER = {3},
 +  PAGES = {577-607},
 +  ABSTRACT = {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},
 +  PDF = {/wiki/lib/exe/fetch.php?media=grupos:avispa:papers:val05.pdf},
 +  YEAR = 2005
 +}
 +</pre>
 +</p>
 +<p><a name="DPR05"></a><pre>
 +@INPROCEEDINGS{DPR05,
 +  AUTHOR = {Delgado, A. and Perez, J. A. and Rueda, C.},
 +  TITLE = {Implementing an {A}bstraction {F}ramework for {S}oft
 +                   {C}onstraints.},
 +  BOOKTITLE = {Abstraction, {R}eformulation and {A}pproximation,
 +                   {P}roc. of the 6th {I}nternational {S}ymposium, {SARA}
 +                   2005.},
 +  EDITOR = {Zucker, J. D. and Saitta, L.},
 +  VOLUME = {3607},
 +  SERIES = {Lecture Notes in Computer Science},
 +  PAGES = {60-75},
 +  PUBLISHER = {Springer},
 +  ABSTRACT = {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.
 +                   },
 +  ISBN = {3-540-27872-9},
 +  KEYWORDS = {(Concurrent) Constraint Programming, Soft Constraints,
 +                   Semiring-Based Constraints, Mozart},
 +  PDF = {/wiki/lib/exe/fetch.php?media=grupos:avispa:papers:dpr05.pdf},
 +  YEAR = 2005
 +}
 +</pre>
 +</p>
 +<p><a name="DP05"></a><pre>
 +@MISC{DP05,
 +  AUTHOR = {Delgado, A. and Perez, J. A.},
 +  TITLE = {Analisis e {I}mplementacion de {M}ecanismos de
 +                   {R}estricciones {D}ebiles para {P}rogramacion
 +                   {C}oncurrente por {R}estricciones},
 +  HOWPUBLISHED = {BSc Thesis -- Engineering Degree in Computer Science,
 +                   Pontificia Universidad Javeriana - Cali (Colombia).},
 +  ABSTRACT = {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\'on 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\'ebiles
 +                   (RDs): restricciones que pueden violarse y permiten
 +                   representar preferencias. Un modelo te\'orico de RDs es
 +                   adaptado al contexto de la pro-gramaci\'on concurrente
 +                   por restricciones, ampliando asi su aplicabilidad en
 +                   problemas reales. Se presentan dos implementaciones en
 +                   el lenguaje Mozart, as\'{\i} como an\'alisis,
 +                   comparaciones y pruebas. Estos resultados son
 +                   respaldados por varias publicaciones internacionales
 +                   arbitradas.},
 +  KEYWORDS = {Satisfacci\'on de Restricciones, Problemas de
 +                   Satisfacci\'on de Restricciones (CSPs), Programaci\'on
 +                   Concurrente por Restricciones, Restricciones D\'ebiles,
 +                   Mozart},
 +  MONTH = {November},
 +  PDF = {/wiki/lib/exe/fetch.php?media=grupos:avispa:papers:dp05.pdf},
 +  YEAR = 2005
 +}
 +</pre>
 +</p>
 +<p><a name="OR05"></a><pre>
 +@INPROCEEDINGS{OR05,
 +  AUTHOR = {Olarte, C. and Rueda, C.},
 +  TITLE = {A {S}tochastic {N}on-deterministic {T}emporal
 +                   {C}oncurrent {C}onstraint {C}alculus.},
 +  BOOKTITLE = {{I}nternational {C}onference of the {C}hilean
 +                   {C}omputer {S}cience {S}ociety ({SCCC} 2005)},
 +  PUBLISHER = {IEEE-CS},
 +  ABSTRACT = {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.},
 +  ISBN = {1522-4902},
 +  KEYWORDS = {Process calculi, sntcc (stochastic, non-deterministic,
 +                   timed concurrent constraint programming), constraint
 +                   programming},
 +  PDF = {/wiki/lib/exe/fetch.php?media=grupos:avispa:papers:or05.pdf},
 +  YEAR = 2005
 +}
 +</pre>
 +</p>
 +<p><a name="OR05b"></a><pre>
 +@INPROCEEDINGS{OR05b,
 +  AUTHOR = {Olarte, C. and Rueda, C.},
 +  TITLE = {Using {S}tochastic {NTCC} to {M}odel {B}iological
 +                   {S}ystems},
 +  BOOKTITLE = {{CLEI} 2005 (31st {L}atinamerican
 +                   {C}onference on {I}nformatics)},
 +  ABSTRACT = {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.},
 +  ISBN = {958-670-426-2},
 +  KEYWORDS = {NTCC, Lambda-Switch, biological systems, concurrent
 +                   process calculus, concurrent constraint programming},
 +  PDF = {/wiki/lib/exe/fetch.php?media=grupos:avispa:papers:or05b.pdf},
 +  YEAR = 2005
 +}
 +</pre>
 +</p>
 +<p><a name="DOP+05"></a><pre>
 +@INPROCEEDINGS{DOP+05,
 +  AUTHOR = {Delgado, A. and Olarte, C. and Perez, J. A. and Rueda,
 +                   C.},
 +  TITLE = {Semiring-based {F}uzzy {C}onstraints in {C}oncurrent
 +                   {C}onstraint {P}rogramming},
 +  BOOKTITLE = {{CLEI} 2005 (31st {L}atinamerican
 +                   {C}onference on {I}nformatics)},
 +  EDITOR = {Buss, A. and Diaz, J. F. and Rueda, C.},
 +  ABSTRACT = {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 de ne 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 di erent contexts. Some
 +                   issues regarding the integration of soft constraints in
 +                   existing applications are also discussed.},
 +  ISBN = {958-670-426-2},
 +  KEYWORDS = {Programming Languages, Constraint Solving, Soft
 +                   Constraints, Mozart},
 +  MONTH = {October},
 +  PDF = {/wiki/lib/exe/fetch.php?media=grupos:avispa:papers:dop+05.pdf},
 +  YEAR = 2005
 +}
 +</pre>
 +</p>
 +<p><a name="DOP+04"></a><pre>
 +@INPROCEEDINGS{DOP+04,
 +  AUTHOR = {Delgado, A. and Olarte, C. A. and Perez, J. A. and
 +                   Rueda, C.},
 +  TITLE = {Implementing {S}emiring-{B}ased {C}onstraints {U}sing
 +                   {M}ozart.},
 +  BOOKTITLE = {Multiparadigm {P}rogramming in {M}ozart/{O}z, {S}econd
 +                   {I}nternational {C}onference, {MOZ} 2004, {R}evised
 +                   {S}elected and {I}nvited {P}apers},
 +  EDITOR = {Van Roy, P.},
 +  NUMBER = {3389},
 +  SERIES = {Lecture Notes in Computer Science},
 +  PAGES = {224-236},
 +  PUBLISHER = {Springer},
 +  ABSTRACT = {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.},
 +  ISBN = {3-540-25079-4},
 +  KEYWORDS = {(Concurrent) Constraint Programming, Soft Constraints,
 +                   Semiring-Based Constraints, Mozart},
 +  PDF = {/wiki/lib/exe/fetch.php?media=grupos:avispa:papers:dop+04.pdf},
 +  YEAR = 2004
 +}
 +</pre>
 +</p>
 +<p><a name="DGO+04b"></a><pre>
 +@INPROCEEDINGS{DGO+04b,
 +  AUTHOR = {Diaz, J. F. and Gutierrez, G. and Olarte, C. A. and
 +                   Rueda, C.},
 +  TITLE = {Using {C}onstraint {P}rogramming for {R}econfiguration
 +                   of {E}lectrical {P}ower {D}istribution {N}etworks.},
 +  BOOKTITLE = {Multiparadigm {P}rogramming in {M}ozart/{O}z, {S}econd
 +                   {I}nternational {C}onference, {MOZ} 2004, {R}evised
 +                   {S}elected and {I}nvited {P}apers},
 +  EDITOR = {Van Roy, P.},
 +  NUMBER = {3389},
 +  SERIES = {Lecture Notes in Computer Science},
 +  PAGES = {263-276},
 +  PUBLISHER = {Springer},
 +  ABSTRACT = {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.},
 +  ISBN = {3-540-25079-4},
 +  KEYWORDS = {(Concurrent) Constraint Programming, Constraint
 +                   Satisfaction Problem (CSP), Network reconfiguration,
 +                   Power losses reduction.},
 +  PDF = {/wiki/lib/exe/fetch.php?media=grupos:avispa:papers:dgo+04b.pdf},
 +  YEAR = 2004
 +}
 +</pre>
 +</p>
 +<p><a name="RV04b"></a><pre>
 +@INPROCEEDINGS{RV04b,
 +  AUTHOR = {C. Rueda and F. D. Valencia},
 +  TITLE = {Non-viability Deductions in Arc-Consistency
 +                   Computation.},
 +  BOOKTITLE = {International Conference on Logic
 +                   Programming (ICLP 2004)},
 +  VOLUME = {3132},
 +  SERIES = {Lecture Notes in Computer Science},
 +  PAGES = {343-355},
 +  PUBLISHER = {Springer},
 +  ABSTRACT = {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,},
 +  PDF = {/wiki/lib/exe/fetch.php?media=grupos:avispa:papers:rv04b.pdf},
 +  YEAR = 2004
 +}
 +</pre>
 +</p>
 +<p><a name="DCL+04"></a><pre>
 +@INPROCEEDINGS{DCL+04,
 +  AUTHOR = {Diaz, J. F. and Caicedo, G. and Lozano, C. and
 +                   Gutierrez, G. and Olarte, C. and Rueda, C.},
 +  TITLE = {Loss {R}eduction in {D}istribution {N}etworks using
 +                   {C}oncurrent {C}onstraint {P}rogramming},
 +  BOOKTITLE = {8th {I}nternational {C}onference on
 +                   {P}robability {M}ethods {A}pplied to {P}ower {S}ystems
 +                   ({PMAPS}'04)},
 +  PAGES = {295- 300},
 +  PUBLISHER = {IEEE},
 +  ABSTRACT = {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.},
 +  ISBN = {0-9761319-1-9},
 +  KEYWORDS = {Concurrent Constraint Programming, Constraint
 +                   Satisfaction Problem (CSP), Network reconfiguration,
 +                   Power losses reduction},
 +  PDF = {/wiki/lib/exe/fetch.php?media=grupos:avispa:papers:dcl+04.pdf},
 +  YEAR = 2004
 +}
 +</pre>
 +
 +
 +</p>
 +<p><a name="ADO04"></a><pre>
 +@INPROCEEDINGS{ADO04,
 +  AUTHOR = {Aranda, J. and Diaz, J. F. and Ortiz, J.},
 +  TITLE = {The {P}roblem of {A}ssigning {E}valuators to the
 +                   {A}rticles {S}ubmitted in an {A}cademic {E}vent: {A}
 +                   {P}ractical {S}olution {I}ncorporating {C}onstraint
 +                   {P}rogramming and {H}euristics},
 +  BOOKTITLE = {Multiparadigm {P}rogramming in {M}ozart/{O}z, {S}econd
 +                   {I}nternational {C}onference, {MOZ} 2004, {R}evised
 +                   {S}elected and {I}nvited {P}apers},
 +  EDITOR = {Van Roy, P.},
 +  NUMBER = {3389},
 +  SERIES = {Lecture Notes in Computer Science},
 +  PAGES = {305-316},
 +  PUBLISHER = {Springer},
 +  ABSTRACT = {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).},
 +  ISBN = {3-540-25079-4},
 +  KEYWORDS = {(Concurrent) Constraint Programming, Constraint
 +                   Satisfaction Problem (CSP)},
 +  PDF = {/wiki/lib/exe/fetch.php?media=grupos:avispa:papers:ado04.pdf},
 +  YEAR = 2004
 +}
 +</pre>
 +</p>
 +<p><a name="MH04"></a><pre>
 +@INPROCEEDINGS{MH04,
 +  AUTHOR = {Mu\~noz, M. P. and Hurtado, A. R.},
 +  TITLE = {Programming {R}obotic {D}evices with a {T}imed
 +                   {C}oncurrent {C}onstraint {L}anguage ({S}hort
 +                   {A}bstract)},
 +  BOOKTITLE = {{T}enth {I}nternational {C}onference on
 +                   {P}rinciples and {P}ractice of {C}onstraint
 +                   {P}rogramming ({CP} 2004)},
 +  EDITOR = {Wallace, M.},
 +  VOLUME = {3258},
 +  SERIES = {Lecture Notes in Computer Science},
 +  PAGES = {803},
 +  ABSTRACT = {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},
 +  PAGE = {803},
 +  PDF = {/wiki/lib/exe/fetch.php?media=grupos:avispa:papers:mh04.pdf},
 +  YEAR = 2004
 +}
 +</pre>
 +</p>
 +<p><a name="DGO+04"></a><pre>
 +@INPROCEEDINGS{DGO+04,
 +  AUTHOR = {Diaz, J. F. and Gutierrez, G. and Olarte, C. A. and
 +                   Rueda, C.},
 +  TITLE = {C{RE}2: a {CP} application for reconfiguring a power
 +                   distribution network for power losses reduction
 +                   ({S}hort {A}bstract)},
 +  BOOKTITLE = {{T}enth {I}nternational {C}onference on
 +                   {P}rinciples and {P}ractice of {C}onstraint
 +                   {P}rogramming ({CP} 2004)},
 +  EDITOR = {Wallace, M.},
 +  VOLUME = {3258},
 +  SERIES = {Lecture Notes in Computer Science},
 +  PAGES = {813-814},
 +  PUBLISHER = {Springer},
 +  KEYWORDS = {Concurrent Constraint Programming, Constraint
 +                   Satisfaction Problem (CSP), Network reconfiguration,
 +                   Power losses reduction},
 +  PDF = {/wiki/lib/exe/fetch.php?media=grupos:avispa:papers:dgo+04.pdf},
 +  YEAR = 2004
 +}
 +</pre>
 +</p>
 +<p><a name="RV04"></a><pre>
 +@ARTICLE{RV04,
 +  AUTHOR = {Rueda, C. and Valencia, F. D.},
 +  TITLE = {On validity in modelization of musical problems by
 +                   CCP.},
 +  JOURNAL = {Soft Comput.},
 +  VOLUME = {8},
 +  NUMBER = {9},
 +  PAGES = {641-648},
 +  ABSTRACT = {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},
 +  PDF = {/wiki/lib/exe/fetch.php?media=grupos:avispa:papers:rv04.pdf},
 +  YEAR = 2004
 +}
 +</pre>
 +</p>
 +<p><a name="DOP+04b"></a><pre>
 +@INPROCEEDINGS{DOP+04b,
 +  AUTHOR = {Delgado, A. and Olarte, C. A. and Perez, J. A. and
 +                   Rueda, C.},
 +  TITLE = {Implementing {S}emiring-{B}ased {C}onstraints using a
 +                   {C}oncurrent {C}onstraint {P}rogramming {L}anguage.},
 +  BOOKTITLE = {{S}ixth {I}nternational {W}orkshop on
 +                   {P}references and {S}oft {C}onstraints. {P}art of {CP}
 +                   2004.},
 +  EDITOR = {Bistarelli, S. and Rossi, F.},
 +  ABSTRACT = {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},
 +  MONTH = {September},
 +  PDF = {/wiki/lib/exe/fetch.php?media=grupos:avispa:papers:dop+04b.pdf},
 +  YEAR = 2004
 +}
 +</pre>
 +</p>
 +<p><a name="HM04"></a><pre>
 +@MISC{HM04,
 +  AUTHOR = {Hurtado, A. R. and Mu\~noz, M. P.},
 +  TITLE = {L{MAN}: {M}\'aquina {A}bstracta del {C}\'alculo {NTCC}
 +                   para {P}rogramaci\'on {C}oncurrente de {R}obots {LEGO}},
 +  HOWPUBLISHED = {BSc Thesis -- Engineering Degree in Computer Science,
 +                   Pontificia Universidad Javeriana - Cali (Colombia).},
 +  ABSTRACT = {Este proyecto de grado describe LMAN, m\'aquina
 +                   abstracta del c\'alculo NTCC para programaci\'on
 +                   concurrente de robots LEGO. LMAN incluye tanto la
 +                   especificaci\'on de la m\'aquina abstracta, como la
 +                   implementaci\'on de la m\'aquina virtual, que act\'ua
 +                   como el ejecutor notacional del c\'alculo NTCC. El
 +                   modelo formal presentado en forma de m\'aquina
 +                   abstracta, provee la especificaci\'on de la m\'aquina
 +                   virtual. La m\'aquina virtual est\'a 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\'alculo de Procesos, M\'aquina Abstracta, M\'aquina
 +                   Virtual, Robots LEGO, Concurrencia, Restricciones,
 +                   LMAN.},
 +  PDF = {/wiki/lib/exe/fetch.php?media=grupos:avispa:papers:hm04.pdf},
 +  YEAR = 2004
 +}
 +</pre>
 +</p>
 +<p><a name="DPP+04"></a><pre>
 +@INPROCEEDINGS{DPP+04,
 +  AUTHOR = {Delgado, A. and Perez, J. A. and Pabon, G. and Jordan,
 +                   R. and Diaz, J. F. and Rueda, C.},
 +  TITLE = {An {I}nteractive {T}ool for the {C}ontrolled
 +                   {E}xecution of an {A}utomated {T}imetabling
 +                   {C}onstraint {E}ngine.},
 +  BOOKTITLE = {Multiparadigm {P}rogramming in {M}ozart/{O}z, {S}econd
 +                   {I}nternational {C}onference, {MOZ} 2004, {R}evised
 +                   {S}elected and {I}nvited {P}apers},
 +  EDITOR = {Van Roy, P.},
 +  VOLUME = {3389},
 +  SERIES = {Lecture Notes in Computer Science},
 +  PAGES = {317-327},
 +  PUBLISHER = {Springer},
 +  ABSTRACT = {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.},
 +  ISBN = {3-540-25079-4},
 +  KEYWORDS = {Constraint Programming, Timetabling Problems,
 +                   Incremental Execution, Mozart},
 +  PDF = {/wiki/lib/exe/fetch.php?media=grupos:avispa:papers:dpp+04.pdf},
 +  YEAR = 2004
 +}
 +</pre>
 +</p>
 +<p><a name="Val03"></a><pre>
 +@PHDTHESIS{Val03,
 +  AUTHOR = {Valencia, F. D.},
 +  TITLE = {Temporal Concurrent Constraint Programming},
 +  SCHOOL = {BRICS},
 +  NOTE = {PhD thesis. xvii+174},
 +  ABSTRACT = {{\em Concurrent constraint programming} (ccp) is a
 +                   formalism for concurrency in which agents interact with
 +                   one another by telling (adding) and asking (reading)
 +                   information in a shared medium. Temporal ccp extends
 +                   ccp by allowing agents to be constrained by time
 +                   conditions. This dissertation studies temporal ccp as a
 +                   model of concurrency for discrete-timed systems. The
 +                   study is conducted by developing a process calculus
 +                   called {\tt ntcc}. \bibpar The {\tt ntcc} calculus
 +                   generalizes the tcc model, the latter being a temporal
 +                   ccp model for {\em deterministic} and {\em synchronous
 +                   timed reactive} systems. The calculus is built upon few
 +                   basic ideas but it captures several aspects of timed
 +                   systems. As tcc, {\tt ntcc} can model unit delays,
 +                   time-outs, pre-emption and synchrony. Additionally, it
 +                   can model {\em unbounded but finite delays, bounded
 +                   eventuality, asynchrony} and {\em nondeterminism}. The
 +                   applicability of the calculus is illustrated with
 +                   several interesting examples of discrete-time systems
 +                   involving mutable data structures, robotic devices,
 +                   multi-agent systems and music applications. \bibpar The
 +                   calculus is provided with a {\em denotational
 +                   semantics} that captures the reactive computations of
 +                   processes in the presence of arbitrary environments.
 +                   The denotation is proven to be {\em fully-abstract} for
 +                   a substantial fragment of the calculus. This
 +                   dissertation identifies the exact technical problems
 +                   (arising mainly from allowing nondeterminism, locality
 +                   and time-outs in the calculus) that makes it impossible
 +                   to obtain a fully abstract result for the full language
 +                   of {\tt ntcc}. \bibpar Also, the calculus is provided
 +                   with a process logic for expressing {\em temporal
 +                   specifications} of {\tt ntcc} processes. This
 +                   dissertation introduces a ({\em relatively}) {\em
 +                   complete inference system} to prove that a given {\tt
 +                   ntcc}process satisfies a given formula in this logic.
 +                   The denotation, process logic and inference system
 +                   presented in this dissertation significantly extend and
 +                   strengthen similar developments for tcc and (untimed)
 +                   ccp. \bibpar This dissertation addresses the {\em
 +                   decidability} of various behavioral equivalences for
 +                   the calculus and {\em characterizes} their
 +                   corresponding induced congruences. The equivalences
 +                   (and their associated congruences) are proven to be
 +                   decidable for a significant fragment of the calculus.
 +                   The decidability results involve a systematic
 +                   translation of processes into finite state B{\"u}chi
 +                   automata. To the author's best knowledge the study of
 +                   decidability for ccp equivalences is original to this
 +                   work. \bibpar Furthermore, this dissertation deepens
 +                   the understanding of previous ccp work by establishing
 +                   an {\em expressive power hierarchy} of several temporal
 +                   ccp languages which were proposed in the literature by
 +                   other authors. These languages, represented in this
 +                   dissertation as {\em variants} of {\tt ntcc} , differ
 +                   in their way of defining infinite behavior (i.e., {\em
 +                   replication} or {\em recursion}) and the scope of
 +                   variables (i.e., {\em static} or {\em dynamic scope}).
 +                   In particular, it is shown that (1) recursive
 +                   procedures with parameters can be encoded into
 +                   parameterless recursive procedures with dynamic
 +                   scoping, and vice-versa; (2) replication can be encoded
 +                   into parameterless recursive procedures with static
 +                   scoping, and vice-versa; (3) the languages from (1) are
 +                   {\em strictly more expressive} than the languages from
 +                   (2). (Thus, in this family of languages recursion is
 +                   more expressive than replication and dynamic scope is
 +                   more expressive than static scope.) Moreover, it is
 +                   shown that behavioral equivalence is {\em undecidable}
 +                   for the languages from (l), but {\em decidable} for the
 +                   languages from (2). Interestingly, the undecidability
 +                   result holds even if the process variables take values
 +                   from a {\em fixed finite domain} whilst the
 +                   decidability holds for {\em arbitrary domains}. \bibpar
 +                   Both the expressive power hierarchy and
 +                   decidability/undecidability results give a clear
 +                   distinction among the various temporal ccp languages.
 +                   Also, the distinction between static and dynamic
 +                   scoping helps to clarify the situation in the (untimed)
 +                   ccp family of languages. Moreover, the methods used in
 +                   the decidability results may provide a framework to
 +                   perform further systematic investigations of temporal
 +                   ccp languages.},
 +  COMMENT = {Defence: February~5, 2003},
 +  INSTITUTION = <a href="#BRICS">BRICS</a>,
 +  KEYWORDS = {Concurrent Constraint Programming, ntcc, Applications,
 +                   Expressiveness of Process Calculi},
 +  NUMBER = {DS-03-2},
 +  PDF = {/wiki/lib/exe/fetch.php?media=grupos:avispa:papers:val03.pdf},
 +  YEAR = 2003
 +}
 +</pre>
 +</p>
 +<p><a name="NV03"></a><pre>
 +@INPROCEEDINGS{NV03,
 +  AUTHOR = {Nielsen, M. and Valencia, F. D.},
 +  TITLE = {Notes on {T}imed {CCP}},
 +  BOOKTITLE = {Lectures on {C}oncurrency and {P}etri {N}ets},
 +  VOLUME = {3098},
 +  SERIES = {Lecture Notes in Computer Science},
 +  PAGES = {702-741},
 +  PUBLISHER = {Springer},
 +  ABSTRACT = {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},
 +  PDF = {/wiki/lib/exe/fetch.php?media=grupos:avispa:papers:nv03.pdf},
 +  YEAR = 2003
 +}
 +</pre>
 +</p>
 +<p><a name="SD03"></a><pre>
 +@TECHREPORT{SD03,
 +  AUTHOR = {G. Sarria and J. Diago},
 +  TITLE = {OpenMusic for Linux and MacOS X},
 +  INSTITUTION = {AVISPA Research Group, IRCAM and Pontificia Universidad
 +                   Javeriana},
 +  ABSTRACT = {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},
 +  MONTH = {September},
 +  PDF = {/wiki/lib/exe/fetch.php?media=grupos:avispa:papers:sd03.pdf},
 +  YEAR = 2003
 +}
 +</pre>
 +</p>
 +<p><a name="NPV02"></a><pre>
 +@ARTICLE{NPV02,
 +  AUTHOR = {Nielsen, M. and Palamidessi, C. and Valencia, F. D.},
 +  TITLE = {Temporal Concurrent Constraint Programming:
 +                   Denotation, Logic and Applications.},
 +  JOURNAL = {Nord. J. Comput.},
 +  VOLUME = {9},
 +  NUMBER = {1},
 +  PAGES = {145-188},
 +  ABSTRACT = {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},
 +  PDF = {/wiki/lib/exe/fetch.php?media=grupos:avispa:papers:npv02.pdf},
 +  YEAR = 2002
 +}
 +</pre>
 +</p>
 +<p><a name="RAQ+01"></a><pre>
 +@ARTICLE{RAQ+01,
 +  AUTHOR = {Rueda, C. and Alvarez, G. and Quesada, L. O. and
 +                   Tamura, G. and Valencia, F. D. and Diaz, J. F. and
 +                   Assayag, G.},
 +  TITLE = {Integrating Constraints and Concurrent Objects in
 +                   Musical Applications: A Calculus and its Visual
 +                   Language.},
 +  JOURNAL = {Constraints},
 +  VOLUME = {6},
 +  NUMBER = {1},
 +  PAGES = {21-52},
 +  ABSTRACT = {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},
 +  PDF = {/wiki/lib/exe/fetch.php?media=grupos:avispa:papers:raq+01.pdf},
 +  YEAR = 2001
 +}
 +</pre>
 +</p>
 +<p><a name="SD01"></a><pre>
 +@MISC{SD01,
 +  AUTHOR = {Sarria, G. and Diago, J.},
 +  TITLE = {Implantacion del {K}ernel de {O}penmusic bajo {L}inux},
 +  HOWPUBLISHED = {BSc Thesis -- Engineering Degree in Computer Science,
 +                   Pontificia Universidad Javeriana - Cali (Colombia).},
 +  KEYWORDS = {Openmusic, Lisp, Linux, MacOS},
 +  PDF = {/wiki/lib/exe/fetch.php?media=grupos:avispa:papers:sd01.pdf},
 +  YEAR = 2001
 +}
 +</pre>
 +</p>
 +<p><a name="DR00"></a><pre>
 +@ARTICLE{DR00,
 +  AUTHOR = {Diaz, J. F. and Rueda, C.},
 +  TITLE = {Modelos para la computacion movil (invited paper).},
 +  JOURNAL = {Revista Colombiana de Computacion},
 +  VOLUME = {1},
 +  NUMBER = {1},
 +  PAGES = {29-45},
 +  ABSTRACT = {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},
 +  PDF = {/wiki/lib/exe/fetch.php?media=grupos:avispa:papers:dr00.pdf},
 +  YEAR = 2000
 +}
 +</pre>
 +</p>
 +<p><a name="DRV98"></a><pre>
 +@ARTICLE{DRV98,
 +  AUTHOR = {Diaz, J. F. and Rueda, C. and Valencia, F. D.},
 +  TITLE = {Pi+- Calculus: A Calculus for Concurrent Processes
 +                   with Constraints.},
 +  JOURNAL = {CLEI Electronic Journal},
 +  VOLUME = {1},
 +  NUMBER = {2},
 +  ABSTRACT = {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 defi ne 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.},
 +
 +  PDF = {/wiki/lib/exe/fetch.php?media=grupos:avispa:papers:drv98.pdf},
 +  YEAR = 1998
 +}
 +</pre>
 +</p>
 +<p><a name="CV96"></a><pre>
 +@MISC{CV96,
 +  AUTHOR = {Castano, G. and Valencia, F. D.},
 +  TITLE = {CSP's: Unificacion Formal  y Nuevos Algoritmos},
 +  HOWPUBLISHED = {BSc Thesis -- Engineering Degree in Computer Science,
 +                   Pontificia Universidad Javeriana - Cali (Colombia).},
 +  PDF = {/wiki/lib/exe/fetch.php?media=grupos:avispa:papers:cv96.pdf},
 +  YEAR = 1996
 +}
 +</pre>
 +</p>
 +<hr><p><em>This file has been generated by
 +<a href="http://www.lri.fr/~filliatr/bibtex2html/">bibtex2html</a> 1.75</em></p>
 +
 +</html>
 
grupos/avispa/repository_bib.txt · Última modificación: 2011/01/24 15:30 (editor externo)
Recent changes RSS feed Donate Powered by PHP Valid XHTML 1.0 Valid CSS Driven by DokuWiki