AVISPA BibTex File

You can also see the list of publications in two flavours: with abstracts and without abstracts


@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}
}

@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}
}

@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}
}

@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}
}

@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}
}

@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}
}

@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}
}

@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
}

@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}
}

@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
}

@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}
}

@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}
}

@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
}

@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
}

@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}
}

@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
}

@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}
}

@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}
}

@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
}

@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}
}

@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
}

@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}
}

@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
}

@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}
}

@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
}

@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
}

@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
}

@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
}

@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}
}

@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}
}

@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}
}

@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}
}

@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
}

@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
}

@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
}

@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
}

@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
}

@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
}

@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
}

@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
}

@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
}

@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
}

@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
}

@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
}

@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
}

@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
}

@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
}

@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
}

@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
}

@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
}

@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
}

@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
}

@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
                   dierent areas such as arts, engineering and sciences.
                   In this paper we propose a generic framework to model,
                   simulate and verify genetic regulatory networks based
                   on a non-deterministic timed concurrent constraint
                   calculus. This framework provides a set of process
                   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
}

@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
}

@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
}

@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
}

@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
}

@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
}

@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
}

@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
}

@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
}

@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
}

@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
}

@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
}

@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
}

@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
}

@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 dierent 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
}

@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
}

@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
}

@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
}

@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
}

@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
}

@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
}

@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
}

@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
}

@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
}

@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
}

@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
}

@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 = BRICS,
  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
}

@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
}

@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
}

@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
}

@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
}

@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
}

@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
}

@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
}

@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
}


This file has been generated by bibtex2html 1.75

 
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