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

grupos:avispa:repository_bib [2010/08/09 18:39] crueda |
grupos:avispa:repository_bib [2011/01/24 15:30] (actual) |
||
---|---|---|---|

Línea 1: | Línea 1: | ||

+ | ====== AVISPA BibTex File====== | ||

+ | You can also see the list of publications in two flavours: [[grupos:avispa:repository_abstracts|with abstracts]] and [[grupos:avispa:publications_repository|without abstracts]] | ||

+ | ---- | ||

+ | |||

+ | |||

+ | <html> | ||

+ | |||

+ | <p><a name="CR10"></a><pre> | ||

+ | @INPROCEEDINGS{conference:matelas:2010, | ||

+ | AUTHOR = {N. Catano and C. Rueda}, | ||

+ | TITLE = {Matelas: A Predicate Calculus Common Formal | ||

+ | Definition for Social Networking}, | ||

+ | BOOKTITLE = {ABZ 2010}, | ||

+ | PAGES = {259-272}, | ||

+ | YEAR = {2010}, | ||

+ | EDITOR = {M. Frappier et al.}, | ||

+ | VOLUME = {5977}, | ||

+ | SERIES = {LNCS, Springer}, | ||

+ | ADDRESS = {Québec, Canada} | ||

+ | } | ||

+ | |||

+ | </pre> | ||

+ | </p> | ||

+ | |||

+ | <p><a name="AP09"></a><pre> | ||

+ | @MISC{AP09, | ||

+ | AUTHOR = {Jes\'{u}s Aranda and Jorge A. Perez}, | ||

+ | TITLE = {Languages for Concurrency Featuring Quantitative Information: | ||

+ | An Overview and New Perspectives}, | ||

+ | HOWPUBLISHED = {The ALP Newsletter}, | ||

+ | ABSTRACT = {The study of quantitative information within languages for | ||

+ | concurrency has recently gained a lot of momentum. In | ||

+ | many applications, quantitative information becomes | ||

+ | crucial when refining models with empirical data, and is | ||

+ | of the essence for verification purposes. In this paper | ||

+ | we survey some of the existing languages for concurrency | ||

+ | that feature quantitative information, with a special | ||

+ | interest in those proposed for biological applications. | ||

+ | This survey is then used as a context to motivate a | ||

+ | novel approach for analyzing systems exhibiting | ||

+ | stochastic behavior, in the form of a discrete-timed | ||

+ | concurrent constraint process calculus. Some design | ||

+ | decisions involved in the definition of an operational | ||

+ | semantics for such a calculus are discussed.}, | ||

+ | VOLUME = {22}, | ||

+ | NUMBER = {1}, | ||

+ | INSTITUTION = {Association for Logic Programming (ALP)}, | ||

+ | MONTH = {March}, | ||

+ | PDF = {/wiki/lib/exe/fetch.php?media=grupos:avispa:papers:ap09.pdf}, | ||

+ | YEAR = {2009} | ||

+ | } | ||

+ | </pre> | ||

+ | </p> | ||

+ | |||

+ | <p><a name="MP09"></a><pre> | ||

+ | @MISC{mp09, | ||

+ | AUTHOR = {Jaime A. Mu\~{n}oz and Henry A. Perez}, | ||

+ | TITLE = {Aplicaci\'{o}n de la Programaci\'{o}n Concurrente por Restricciones | ||

+ | en el Modelado de Procesos en la Membrana Celular}, | ||

+ | HOWPUBLISHED = {BSc Thesis -- Engineering Degree in Computer Science, | ||

+ | Pontificia Universidad Javeriana - Cali (Colombia).}, | ||

+ | ABSTRACT = {The functional behavior of biological systems has become a | ||

+ | task of increasing interest to the scientic community of | ||

+ | biologists, who constantly search to infer this behavior | ||

+ | from biological data, in order to analyze, to forecast | ||

+ | some situations and to do detailed studies about some | ||

+ | behaviors which occur at biological level. This fact has | ||

+ | also led to the exploration of computational tools that | ||

+ | complement this study, inspiring new programming | ||

+ | paradigms to describe and model the operation of these | ||

+ | biological systems. | ||

+ | Computationally one of the alternatives in the current | ||

+ | time is the use of Process Caluli based on a concurrent | ||

+ | constraint programming model (CCP), where it is possible | ||

+ | to model abstractions between the components of the | ||

+ | systems and the basics elements of the calculus, | ||

+ | allowing to model partial information through formalisms | ||

+ | based on constraints in a store where all information | ||

+ | about the system is kept. Particularly in this | ||

+ | dissertation the Utcc Calculus (Universal Timed | ||

+ | Concurrent Constraint) will be used as a language | ||

+ | derived from TCC (extension of CCP) by adding new | ||

+ | constructions like the abstraction of processes allowing | ||

+ | the calculus to represent the notion of mobility. | ||

+ | This work is mainly focused on the "Mobile Computing | ||

+ | with membranes", one of the main problems in | ||

+ | bioinformatics, where the mechanisms which the cell | ||

+ | communicates with the outside through the cell membrane | ||

+ | are studied. | ||

+ | The document outlines two calculi focused on the | ||

+ | modeling of these kinds of biological processes based on | ||

+ | the interaction between membranes, the first one is | ||

+ | BioAmbients derived from Ambient Calculus, allowing the | ||

+ | creation of local processes within environments, thus | ||

+ | defining the basic configuration of a membrane. The | ||

+ | second one is "Brane calculi"which defines a set of | ||

+ | biologically inspired primitives in the interaction | ||

+ | between membranes, with a fidelity to the biological | ||

+ | reality modeled in the calculus. Then a detailed | ||

+ | approach to the syntax, functionality and reactions | ||

+ | modeled in Brane Calculi will be presented and then an | ||

+ | interpretation of the processes in Brane Calculi to | ||

+ | Utcc, generating an encoding which allows to translate | ||

+ | processes in Brane Calculi to equivalent processes in | ||

+ | Utcc. | ||

+ | Finally the results obtained are presented, with an | ||

+ | analysis of the most important points of this work and | ||

+ | establishing a set of conclusions that describe the main | ||

+ | advantages and disadvantages to dene an interpretation | ||

+ | of the calculi, and also to suggest some guidelines for | ||

+ | future work. The main contributions of Utcc to modeling | ||

+ | biological membrane systems will be analyzed. The last | ||

+ | part is intended to work through the findings and | ||

+ | results, motivate and encourage the study and analysis | ||

+ | of programming models based on CCP to model more complex | ||

+ | biological systems.}, | ||

+ | PDF = {/wiki/lib/exe/fetch.php?media=grupos:avispa:papers:mp09.pdf}, | ||

+ | YEAR = {2009} | ||

+ | } | ||

+ | </pre> | ||

+ | </p> | ||

+ | |||

+ | <p><a name="LPSS09"></a><pre> | ||

+ | @INPROCEEDINGS{LPSS09, | ||

+ | AUTHOR = {Ivan Lanese and Jorge A. Perez and Davide Sangiorgi and Alan | ||

+ | Schmitt}, | ||

+ | TITLE = {On the Expressiveness of Polyadicity in Higher-Order Communication}, | ||

+ | BOOKTITLE = {Proc. of 11th Italian Conference on Theoretical Computer | ||

+ | Science (ICTCS09)}, | ||

+ | ABSTRACT = {In higher-order process calculi the values exchanged in | ||

+ | communications may contain processes. We describe a | ||

+ | study of the expressive power of strictly higher-order | ||

+ | process calculi, i.e. calculi in which only process | ||

+ | passing is allowed and no name-passing is present. In | ||

+ | this setting, the polyadicity (i.e. the number of | ||

+ | parameters) allowed in communications is shown to induce | ||

+ | a hierarchy of calculi of strictly increasing | ||

+ | expressiveness: a higher-order calculus with n-adic | ||

+ | communication cannot be encoded into a calculus with | ||

+ | n - 1-adic communication. In this note we outline this | ||

+ | result, and discuss on how it relies on a notion of | ||

+ | encoding that takes a rather fine standpoint with | ||

+ | respect to internal behavior.}, | ||

+ | MONTH = {September}, | ||

+ | PDF = {/wiki/lib/exe/fetch.php?media=grupos:avispa:papers:lpss09.pdf}, | ||

+ | YEAR = {2009} | ||

+ | } | ||

+ | </pre> | ||

+ | </p> | ||

+ | |||

+ | <p><a name="GPZ09"></a><pre> | ||

+ | @INPROCEEDINGS{GPZ09, | ||

+ | AUTHOR = {Cinzia Di Giusto and Jorge A. Perez and Gianluigi Zavattaro}, | ||

+ | TITLE = {On the Expressiveness of Forwarding in Higher-Order Communication}, | ||

+ | BOOKTITLE = {Proc. of 6th International Colloquium on Theoretical Aspects | ||

+ | of Computing (ICTAC09)}, | ||

+ | PAGES = {155-169}, | ||

+ | PUBLISHER = {Springer}, | ||

+ | SERIES = {Lecture Notes in Computer Science}, | ||

+ | VOLUME = {5684}, | ||

+ | LOCATION = {Amsterdam, The Netherlands}, | ||

+ | ISBN = {978-3-540-74791-8}, | ||

+ | ABSTRACT = {In higher-order process calculi the values exchanged in | ||

+ | communications may contain processes. There are only | ||

+ | two capabilities for received processes: execution and | ||

+ | forwarding. Here we propose a limited form of | ||

+ | forwarding: output actions can only communicate the | ||

+ | parallel composition of statically known closed | ||

+ | processes and processes received through previously | ||

+ | executed input actions. We study the expressiveness of a | ||

+ | higher-order process calculus featuring this style of | ||

+ | communication. Our main result shows that in this | ||

+ | calculus termination is decidable while convergence is | ||

+ | undecidable.}, | ||

+ | MONTH = {August}, | ||

+ | PDF = {/wiki/lib/exe/fetch.php?media=grupos:avispa:papers:gpz09.pdf}, | ||

+ | YEAR = {2009} | ||

+ | } | ||

+ | </pre> | ||

+ | </p> | ||

+ | |||

+ | <p><a name="CBG+09"></a><pre> | ||

+ | @ARTICLE{cbg+09, | ||

+ | AUTHOR = {Nestor Catano and Fernando Barraza and Daniel Garcia and Pablo | ||

+ | Ortega and Camilo Rueda}, | ||

+ | TITLE = {A Case Study in JML-Assisted Software Development}, | ||

+ | JOURNAL = {Electronic Notes in Theoretical Computer Science (ENTCS)}, | ||

+ | VOLUME = {240}, | ||

+ | ISSN = {1571-0661}, | ||

+ | PAGES = {5--21}, | ||

+ | PUBLISHER = {Elsevier Science Publishers B. V.}, | ||

+ | ADDRESS = {Amsterdam, The Netherlands, The Netherlands}, | ||

+ | ABSTRACT = {This paper presents a case study in formal software | ||

+ | development of a plugin for a Java Desktop project | ||

+ | management application using JML. Our goals for the case | ||

+ | study include determining how JML-based formal methods | ||

+ | can be incorporated in traditional software engineering | ||

+ | practices used in the software industry and how the use | ||

+ | of JML for modeling software requirements can enforce | ||

+ | the programming of correct Java code. We demonstrate how | ||

+ | JML-based formal methods can be used so as to | ||

+ | effectively contribute to the making of decisions within | ||

+ | a software development team.}, | ||

+ | PDF = {/wiki/lib/exe/fetch.php?media=grupos:avispa:papers:cbg_09.pdf}, | ||

+ | YEAR = {2009} | ||

+ | } | ||

+ | </pre> | ||

+ | </p> | ||

+ | |||

+ | <p><a name="CR09"></a><pre> | ||

+ | @INPROCEEDINGS{cr09, | ||

+ | AUTHOR = {Nestor Catano and Camilo Rueda}, | ||

+ | TITLE = {Teaching Formal Methods for the Unconquered Territory}, | ||

+ | BOOKTITLE = {Proceedings of the 2nd International FME Conference on | ||

+ | Teaching Formal Methods (TFM2009)}, | ||

+ | PAGES = {2--19}, | ||

+ | LOCATION = {Eindhoven, the Netherlands}, | ||

+ | ISBN = {978-3-642-04911-8}, | ||

+ | MONTH = {November}, | ||

+ | PUBLISHER = {Springer}, | ||

+ | SERIES = {Lecture Notes in Computer Science}, | ||

+ | VOLUME = {5846/2009}, | ||

+ | ABSTRACT = {We summarise our experiences in teaching two formal methods | ||

+ | courses at Pontificia Universidad Javeriana. The first | ||

+ | course is a JML-based software engineering course. The | ||

+ | second course is a modeldriven software engineering | ||

+ | course realised in the B method for software | ||

+ | development. We explain how formal methods are promoted | ||

+ | in Pontificia Universidad Javeriana, how we motivate | ||

+ | students to embrace formal methods techniques, and how | ||

+ | they are promoted through the presentation of motivating | ||

+ | examples.}, | ||

+ | PDF = {/wiki/lib/exe/fetch.php?media=grupos:avispa:papers:cr09.pdf}, | ||

+ | YEAR = {2009} | ||

+ | } | ||

+ | </pre> | ||

+ | </p> | ||

+ | |||

+ | <p><a name="ARA09"></a><pre> | ||

+ | @PHDTHESIS{Ara09, | ||

+ | AUTHOR = {Jes\'{u}s Aranda}, | ||

+ | TITLE = {On the Expressivity of Infinite and Local Behaviour in Fragments of the Pi-calculus}, | ||

+ | SCHOOL = {l'X, Ecole Polytechnique}, | ||

+ | NOTE = {PhD thesis}, | ||

+ | ABSTRACT = {The pi-calculus is one the most influential formalisms for | ||

+ | modelling and analyzing the behaviour of concurrent | ||

+ | systems. This calculus provides a language in which the | ||

+ | structure of terms represents the structure of processes | ||

+ | together with an operational semantics to represent | ||

+ | computational steps. For example, the parallel | ||

+ | composition term P | Q, which is built from the terms P | ||

+ | and Q, represents the process that results from the | ||

+ | parallel execution of the processes P and Q. Similarly, | ||

+ | the restriction (\nu x)P represents a process P with | ||

+ | local resource x. The replication !P can be thought of | ||

+ | as abbreviating the parallel composition P | P | P .... | ||

+ | of an unbounded number of P processes. | ||

+ | As for other language-based formalisms (e.g., logic, | ||

+ | formal grammars and the lambda-calculus) a fundamental | ||

+ | part of the research in process calculi involves the | ||

+ | study of the expressiveness of fragments or variants of | ||

+ | a given process calculus. In this dissertation we shall | ||

+ | study the expressiveness of some variants of the | ||

+ | pi-calculus focusing on the role of the terms used to | ||

+ | represent local and infinite behaviour, namely | ||

+ | restriction and replication. | ||

+ | The first part of this dissertation is devoted to the | ||

+ | expressiveness of the zero-adic variant of the | ||

+ | (polyadic) pi-calculus, i.e., CCS with replication | ||

+ | (CCS!). | ||

+ | Busi et al show that CCS! is Turing powerful. The | ||

+ | result is obtained by encoding Random Access Machines | ||

+ | (RAMs) in CCS!. The encoding is said to be non-faithful | ||

+ | because it may move from a state which can lead to | ||

+ | termination into a divergent one which do not | ||

+ | correspond to any configuration of the encoded RAM. | ||

+ | I.e., the encoding is not termination preserving. | ||

+ | In this dissertation we shall study the existence of | ||

+ | faithful encodings into CCS! of models of computability | ||

+ | strictly less expressive than Turing Machines. Namely, | ||

+ | grammars of Types 1 (Context Sensitive Languages), 2 | ||

+ | (Context Free Languages) and 3 (Regular Languages) in | ||

+ | the Chomsky Hierarchy. We provide faithful encodings of | ||

+ | Type 3 grammars. We show that it is impossible to | ||

+ | provide a faithful encoding of Type 2 grammars and that | ||

+ | termination-preserving CCS! processes can generate | ||

+ | languages which are not Type 2. We finally conjecture | ||

+ | that the languages generated by termination-preserving | ||

+ | CCS! processes are Type 1 . | ||

+ | We also observe that the encoding of RAMs and several | ||

+ | encoding of Turing-powerful formalisms in pi-calculus | ||

+ | variants may generate an unbounded number of | ||

+ | restrictions during the simulation of a given machine. | ||

+ | This unboundedness arises from having restrictions under | ||

+ | the scope of replication (or recursion) as in e.g., | ||

+ | $!(nu x)P$ or $\mu X.(\nu x)(P | X)$. This suggests that | ||

+ | such an interplay between these operators is fundamental | ||

+ | for Turing completeness. | ||

+ | We shall also study the expressive power of restriction | ||

+ | and its interplay with replication. We do this by | ||

+ | considering several syntactic variants of CCS! which | ||

+ | differ from each other in the use of restriction with | ||

+ | respect to replication. We consider three syntactic | ||

+ | variations of CCS! which do not allow the generation of | ||

+ | unbounded number of restrictions: C1 is the fragment of | ||

+ | CCS! not allowing restrictions under the scope of a | ||

+ | replication, C2 is the restriction-free fragment of CCS!. | ||

+ | The third variant is C3 which extends C1 with Phillips' | ||

+ | priority guards. | ||

+ | We shall show that the use of an unboundedly many | ||

+ | restrictions in CCS! is necessary for obtaining Turing | ||

+ | expressiveness in the sense of Busi et al. We do this by | ||

+ | showing that there is no encoding of RAMs into C1 which | ||

+ | preserves and reflects convergence. We also prove that | ||

+ | up to failures equivalence, there is no encoding from | ||

+ | CCS! into C1 nor from C1 into C2 . Thus up to failures | ||

+ | equivalence, we cannot encode a process with an | ||

+ | unbounded number of restrictions into one with a bounded | ||

+ | number of restrictions, nor one with a bounded number of | ||

+ | restrictions into a restriction-free process. | ||

+ | As lemmata for the above results we prove that | ||

+ | convergence is decidable for C1 and that language | ||

+ | equivalence is decidable for C2 but undecidable for C1. | ||

+ | As corollary it follows that convergence is decidable | ||

+ | for restriction-free CCS. Finally, we show the | ||

+ | expressive power of priorities by providing a faithful | ||

+ | encoding of RAMs in C3. Thus bearing witness to the | ||

+ | expressive power of Phillips' priority guards. | ||

+ | The second part of this dissertation is devoted to | ||

+ | expressiveness of the asynchronous monadic pi-calculus, | ||

+ | Api. In [C. Palamidessi, V. Saraswat, F. Valencia and B. | ||

+ | Victor. On the Expressiveness of Linearity vs | ||

+ | Persistence in the Asynchronous Pi Calculus. LICS | ||

+ | 2006:59-68, 2006] the authors studied the expressiveness | ||

+ | of persistence in Api wrt weak barbed congruence. The | ||

+ | study is incomplete because it ignores divergence. | ||

+ | We shall present an expressiveness study of persistence | ||

+ | in Api wrt De Nicola and Hennessy's testing scenario | ||

+ | which is sensitive to divergence. Following [C. | ||

+ | Palamidessi, V. Saraswat, F. Valencia and B. Victor. On | ||

+ | the Expressiveness of Linearity vs Persistence in the | ||

+ | Asynchronous Pi Calculus. LICS 2006:59-68, 2006], we | ||

+ | consider Api and three sub-languages of it, each | ||

+ | capturing one source of persistence: the | ||

+ | persistent-input Api-calculus (PIpi), the | ||

+ | persistent-output Api-calculus (POpi) and the persistent | ||

+ | Api-calculus (Ppi). In [C. Palamidessi, V. Saraswat, F. | ||

+ | Valencia and B. Victor. On the Expressiveness of | ||

+ | Linearity vs Persistence in the Asynchronous Pi | ||

+ | Calculus. LICS 2006:59-68, 2006] the authors showed | ||

+ | encodings from Api into the semi-persistent calculi | ||

+ | (i.e., POpi and PIpi) correct wrt weak barbed | ||

+ | congruence. We show that, under some general conditions | ||

+ | related to compositionality of the encoding and | ||

+ | preservation of the infinite behaviour, there cannot be | ||

+ | an encoding from Api into a (semi)-persistent calculus | ||

+ | preserving the must testing semantics. We also prove | ||

+ | that convergence and divergence are decidable for POpi | ||

+ | (and Ppi). As a consequence there is no encoding | ||

+ | preserving and reflecting divergence or convergence from | ||

+ | Api into POpi (and Ppi). This study fills a gap on the | ||

+ | expressiveness study of persistence in Api in [C. | ||

+ | Palamidessi, V. Saraswat, F. Valencia and B. Victor. On | ||

+ | the Expressiveness of Linearity vs Persistence in the | ||

+ | Asynchronous Pi Calculus. LICS 2006:59-68, 2006].}, | ||

+ | COMMENT = {Defence: November 27, 2009}, | ||

+ | INSTITUTION = {Ecole Polytechnique, France}, | ||

+ | KEYWORDS = {Concurrent Constraint Based Calculi, Denotational Semantics, | ||

+ | Symbolic Semantics, Security Protocols, Temporal Logic}, | ||

+ | PDF = {/wiki/lib/exe/fetch.php?media=grupos:avispa:papers:ara09.pdf}, | ||

+ | YEAR = 2009 | ||

+ | } | ||

+ | </pre> | ||

+ | </p> | ||

+ | |||

+ | <p><a name="FOP09"></a><pre> | ||

+ | @INPROCEEDINGS{fop09, | ||

+ | AUTHOR = {Moreno Falaschi and Carlos Olarte and Catuscia Palamidessi}, | ||

+ | TITLE = {A framework for abstract interpretation of timed concurrent | ||

+ | constraint programs}, | ||

+ | BOOKTITLE = {Proceedings of the 11th International ACM SIGPLAN Conference | ||

+ | on Principles and Practice of Declarative Programming | ||

+ | (PPDP09)}, | ||

+ | PAGES = {207-218}, | ||

+ | LOCATION = {Coimbra, Portugal}, | ||

+ | ISBN = {978-1-60558-568-0}, | ||

+ | MONTH = {September}, | ||

+ | EDITOR = {Ant{\'o}nio Porto and Francisco Javier L{\'o}pez-Fraguas}, | ||

+ | PUBLISHER = {ACM}, | ||

+ | ABSTRACT = {Timed Concurrent Constraint Programming (tcc) is a | ||

+ | declarative model for concurrency offering a logic for | ||

+ | specifying reactive systems, i.e. systems that | ||

+ | continuously interact with the environment. The | ||

+ | universal tcc formalism (utcc) is an extension of tcc | ||

+ | with the ability to express mobility. Here mobility is | ||

+ | understood as communication of private names as | ||

+ | typically done for mobile systems and security | ||

+ | protocols. In this paper we consider the denotational | ||

+ | semantics for tcc, and we extend it to a "collecting" | ||

+ | semantics for utcc based on closure operators over | ||

+ | sequences of constraints. Relying on this semantics, we | ||

+ | formalize the first general framework for data flow | ||

+ | analyses of tcc and utcc programs by abstract | ||

+ | interpretation techniques. The concrete and abstract | ||

+ | semantics we propose are compositional, thus allowing us | ||

+ | to reduce the complexity of data flow analyses. We show | ||

+ | that our method is sound and parametric w.r.t. the | ||

+ | abstract domain. Thus, different analyses can be | ||

+ | performed by instantiating the framework. We illustrate | ||

+ | how it is possible to reuse abstract domains previously | ||

+ | defined for logic programming, e.g., to perform a | ||

+ | groundness analysis for tcc programs. We show the | ||

+ | applicability of this analysis in the context of | ||

+ | reactive systems. Furthermore, we make also use of the | ||

+ | abstract semantics to exhibit a secrecy flaw in a | ||

+ | security protocol. We have developed a prototypical | ||

+ | implementation of our methodology and we have | ||

+ | implemented the abstract domain for security to perform | ||

+ | automatically the secrecy analysis.}, | ||

+ | PDF = {http://hal.archives-ouvertes.fr/docs/00/42/66/08/PDF/ppdp21-olarte.pdf}, | ||

+ | YEAR = {2009} | ||

+ | } | ||

+ | </pre> | ||

+ | </p> | ||

+ | |||

+ | <p><a name="LOP09"></a><pre> | ||

+ | @INPROCEEDINGS{LOP09, | ||

+ | title = { {T}owards a {U}nified {F}ramework for {D}eclarative {S}tructured {C}ommunications}, | ||

+ | author = {{H}ugo, {L}opez and {O}larte, {C}arlos and {J}orge, {P}erez}, | ||

+ | abstract = {{W}e describe a uniﬁed framework for the declarative analysis of structured communications. {B}y relying on a (timed) concurrent constraint programming language, we show that in addition to the usual operational techniques from process calculi, the analysis of structured communications can elegantly exploit logic-based reasoning techniques. {I}n this work, we present a concurrent constraint interpretation of the language for structured communications proposed by {H}onda, {V}asconcelos, and {K}ubo. {D}istinguishing features of our approach are: the possibility of including partial information (constraints) in the session model; the use of explicit time for reasoning about session duration and expiration; a tight correspondence with logic, which formally relates session execution and linear-time temporal logic formulas.}, | ||

+ | keywords = {{C}oncurrent {C}onstraint {P}rogramming {S}essions {S}ervice {O}riented {C}omputing}, | ||

+ | publisher = {{E}lsevier }, | ||

+ | booktitle = {{P}roc. of {PLACES}'09 }, | ||

+ | PDF = {http://hal.inria.fr/inria-00426609/en/}, | ||

+ | YEAR = 2009 | ||

+ | } | ||

+ | </pre> | ||

+ | </p> | ||

+ | |||

+ | |||

+ | <p><a name="AAO+09"></a><pre> | ||

+ | @INPROCEEDINGS{aao+09, | ||

+ | AUTHOR = {Jes{\'u}s Aranda and G{\'e}rard Assayag and Carlos Olarte and | ||

+ | Jorge A. P{\'e}rez and Camilo Rueda and Mauricio Toro | ||

+ | and Frank D. Valencia}, | ||

+ | TITLE = {An Overview of FORCES: An INRIA Project on Declarative | ||

+ | Formalisms for Emergent Systems}, | ||

+ | BOOKTITLE = {Proc of 25th International Conference on Logic Programming | ||

+ | (ICLP 2009)}, | ||

+ | PAGES = {509-513}, | ||

+ | LOCATION = {Pasadena, CA, USA}, | ||

+ | ISBN = {978-3-642-02845-8}, | ||

+ | MONTH = {July}, | ||

+ | EDITOR = {Patricia M. Hill and David Scott Warren}, | ||

+ | PUBLISHER = {Springer}, | ||

+ | SERIES = {Lecture Notes in Computer Science}, | ||

+ | VOLUME = {5649}, | ||

+ | ABSTRACT = {The FORCES project aims at providing robust and declarative | ||

+ | formalisms for analyzing systems in the emerging areas | ||

+ | of Security Protocols, Biological Systems and Multimedia | ||

+ | Semantic Interaction. This short paper describes | ||

+ | FORCES's motivations, results and future research | ||

+ | directions.}, | ||

+ | PDF = {http://hal.archives-ouvertes.fr/docs/00/42/66/10/PDF/forces-iclp.pdf}, | ||

+ | YEAR = {2009} | ||

+ | } | ||

+ | </pre> | ||

+ | </p> | ||

+ | |||

+ | <p><a name="PS09"></a><pre> | ||

+ | @INPROCEEDINGS{ps09, | ||

+ | AUTHOR = {Salim Perchy and Gerardo Sarria}, | ||

+ | TITLE = {Dissonances: Brief Description and its Computational | ||

+ | Representation in the RTCC Calculus}, | ||

+ | BOOKTITLE = {Proc of 6th Sound and Music Computing Conference (SMC2009)}, | ||

+ | PAGES = {53-58}, | ||

+ | LOCATION = {Porto, Portugal}, | ||

+ | ISBN = {978-989-95577-6-5}, | ||

+ | MONTH = {July}, | ||

+ | EDITOR = {Fabien Gouyon and \'{A}lvaro Barbosa and Xavier Serra}, | ||

+ | ABSTRACT = {Dissonances in music have had a long evolution history dating | ||

+ | back to days of strictly prohibition to times of | ||

+ | enricheness of musical motives and forms. Nowadays, | ||

+ | dissonances account for most of the musical | ||

+ | expressiveness and contain a full application theory | ||

+ | supporting their use making them a frequently adopted | ||

+ | resource of composition. This work partially describes | ||

+ | their theoretical background as well as their evolution | ||

+ | in music and finally proposing a new model for their | ||

+ | computational use.}, | ||

+ | PDF = {/wiki/lib/exe/fetch.php?media=grupos:avispa:papers:ps09.pdf}, | ||

+ | YEAR = {2009} | ||

+ | } | ||

+ | </pre> | ||

+ | </p> | ||

+ | |||

+ | <p><a name="OLA09"></a><pre> | ||

+ | @PHDTHESIS{Ola09, | ||

+ | AUTHOR = {Olarte, C.}, | ||

+ | TITLE = {Universal Temporal Concurrent Constraint Programming}, | ||

+ | SCHOOL = {l'X, Ecole Polytechnique}, | ||

+ | NOTE = {PhD thesis}, | ||

+ | ABSTRACT = {Concurrent Constraint Programming (CCP) [Saraswat 1993] is a | ||

+ | formalism for concurrency in which agents (processes) | ||

+ | interact with one another by telling (adding) and | ||

+ | asking (reading) information represented as constraints | ||

+ | in a shared medium (the store). Temporal Concurrent | ||

+ | Constraint Programming (tcc) extends CCP by allowing | ||

+ | agents to be constrained by time conditions. This | ||

+ | dissertation studies temporal CCP as a model of | ||

+ | concurrency for mobile, timed reactive systems. The | ||

+ | study is conducted by developing a process calculus | ||

+ | called utcc, Universal Temporal CCP. The thesis is that | ||

+ | utcc is a model for concurrency where behavioral and | ||

+ | declarative reasoning techniques coexist coherently, | ||

+ | thus allowing for the specification and verification of | ||

+ | mobile reactive systems in emergent application areas. | ||

+ | The utcc calculus generalizes tcc [Saraswat 1994], a | ||

+ | temporal CCP model of reactive synchronous programming, | ||

+ | with the ability to express mobility. Here mobility is | ||

+ | understood as communication of private names as | ||

+ | typically done for mobile systems and security | ||

+ | protocols. The utcc calculus introduces parametric ask | ||

+ | operations called abstractions that behave as | ||

+ | persistent parametric asks during a time-interval but | ||

+ | may disappear afterwards. | ||

+ | The applicability of the calculus is shown in several | ||

+ | domains of Computer Science. Namely, decidability of | ||

+ | Pnueli's First-order Temporal Logic, closure-operator | ||

+ | semantic characterization of security protocols, | ||

+ | semantics of a Service-Oriented Computing language, and | ||

+ | modeling of Dynamic Multimedia-Interaction systems. | ||

+ | The utcc calculus is endowed with an operational | ||

+ | semantics and then with a symbolic semantics to deal | ||

+ | with problematic operational aspects involving | ||

+ | infinitely many substitutions and divergent internal | ||

+ | computations. The novelty of the symbolic semantics is | ||

+ | to use temporal constraints to represent finitely | ||

+ | infinitely-many substitutions. | ||

+ | In the tradition of CCP-based languages, utcc is a | ||

+ | declarative model for concurrency. It is shown that | ||

+ | utcc processes can be seen, at the same time, as | ||

+ | computing agents and as logic formulae in the Pnueli's | ||

+ | First-order Linear-time Temporal Logic (FLTL) | ||

+ | [Manna 1991]. More precisely, the outputs of a process | ||

+ | correspond to the formulae entailed by its FLTL | ||

+ | representation. | ||

+ | The above-mentioned FLTL characterization is here used | ||

+ | to prove an insightful (un)decidability result for | ||

+ | Monadic FLTL. To do this it is proven that in contrast | ||

+ | to tcc, utcc is Turing-powerful by encoding Minsky | ||

+ | machines [Minsky 1967]. The encoding uses a simple | ||

+ | decidable constraint system involving only monadic | ||

+ | predicates and no equality nor function symbols. The | ||

+ | importance of using such a constraint system is that it | ||

+ | allows for using the underlying theory of utcc to prove | ||

+ | the undecidability of the validity problem for monadic | ||

+ | FLTL without function symbols nor equality. In fact, it | ||

+ | is shown that this fragment of FLTL is strongly | ||

+ | incomplete. This result refutes a decidability | ||

+ | conjecture for FLTL from a previous work. It also | ||

+ | justifies the restriction imposed in previous | ||

+ | decidability results on the quantification of | ||

+ | flexible-variables. This dissertation then fills a gap | ||

+ | on the decidability study of monadic FLTL. | ||

+ | Similarly to tcc, utcc processes can be semantically | ||

+ | characterized as partial closure operators. Because of | ||

+ | additional technical difficulties posed by utcc, the | ||

+ | codomain of the closure operators is more involved than | ||

+ | that for tcc. Namely, processes are mapped into | ||

+ | sequences of future-free temporal formulae rather than | ||

+ | sequences of basic constraints as in tcc. This | ||

+ | representation is shown to be fully abstract with | ||

+ | respect to the input-output behavior of processes for a | ||

+ | meaningful fragment of the calculus. This shows that | ||

+ | mobility can be captured as closure operators over an | ||

+ | underlying constraint system. As a compelling | ||

+ | application of the semantic study of utcc, this | ||

+ | dissertation gives a closure operator semantics to a | ||

+ | language for security protocols. This language arises | ||

+ | as a specialization of utcc with a particular | ||

+ | cryptographic constraint systems. This brings new | ||

+ | semantic insights into the modeling and verification of | ||

+ | security protocols. | ||

+ | The utcc calculus is also used in this dissertation to | ||

+ | give an alternative interpretation of the pi-based | ||

+ | language defined by Honda, Vasconcelos and Kubo (HVK) | ||

+ | for structuring communications [Honda 1998]. The | ||

+ | encoding of HVK into utcc is straightforwardly extended | ||

+ | to explicitly model information on session duration, | ||

+ | allows for declarative preconditions within session | ||

+ | establishment constructs, and features a construct for | ||

+ | session abortion. Then, a richer language for the | ||

+ | analysis of sessions is defined where time can be | ||

+ | explicitly modeled. Additionally, relying on the | ||

+ | above-mentioned interpretation of utcc processes as | ||

+ | FLTL formulae, reachability analysis of sessions can be | ||

+ | characterized as FLTL entailment. | ||

+ | It is also illustrated that the utcc calculus allows | ||

+ | for the modeling of dynamic multimedia interaction | ||

+ | systems. The notion of constraints as partial | ||

+ | information neatly defines temporal relations between | ||

+ | interactive agents or events. Furthermore, mobility in | ||

+ | utcc allows for the specification of more flexible and | ||

+ | expressive systems in this setting, thus broadening the | ||

+ | interaction mechanisms available in previous models. | ||

+ | Finally, this dissertation proposes a general semantic | ||

+ | framework for the data flow analysis of utcc and tcc | ||

+ | programs by abstract interpretation techniques | ||

+ | [Cousot 1979]. The concrete and abstract semantics are | ||

+ | compositional reducing the complexity of data flow | ||

+ | analyses. Furthermore, the abstract semantics is | ||

+ | parametric with respect to the abstract domain and | ||

+ | allows for reusing the most popular abstract domains | ||

+ | previously defined for logic programming. Particularly, | ||

+ | a groundness analysis is developed and used in the | ||

+ | verification of a simple reactive systems. The abstract | ||

+ | semantics allows also to efficiently exhibit a secrecy | ||

+ | flaw in a security protocol modeled in utcc.}, | ||

+ | COMMENT = {Defence: September 29, 2009}, | ||

+ | INSTITUTION = {Ecole Polytechnique, France}, | ||

+ | KEYWORDS = {Concurrent Constraint Based Calculi, Denotational Semantics, | ||

+ | Symbolic Semantics, Security Protocols, Temporal Logic}, | ||

+ | PDF = {/wiki/lib/exe/fetch.php?media=grupos:avispa:papers:ola09.pdf}, | ||

+ | YEAR = 2009 | ||

+ | } | ||

+ | </pre> | ||

+ | </p> | ||

+ | |||

+ | <p><a name="TOR09c"></a><pre> | ||

+ | @TECHREPORT{Tor09c, | ||

+ | AUTHOR = {M. Toro}, | ||

+ | TITLE = {Towards a correct and efficient implementation of simulation and verification tools for Probabilistic ntcc}, | ||

+ | INSTITUTION = {AVISPA Research Group and Pontificia Universidad | ||

+ | Javeriana}, | ||

+ | ABSTRACT = {Using process calculi one can verify properties of a system and simulate the system as | ||

+ | well. One should be able to do these operations at least semi-automatically. There is a | ||

+ | tool to simulate the Non-deterministic Timed Concurrent Constraint (ntcc) calculus in the | ||

+ | Ntccrt framework, but there are not tools for veriﬁcation. We present a new simulation | ||

+ | tool for Probabilistic ntcc (pntcc) and a prototype for veriﬁcation of pntcc models. We | ||

+ | include these tools in the Ntccrt framework. We also show the formal basis for correctness | ||

+ | of the ntcc simulation tool and we show that the execution times of the simulation are still | ||

+ | acceptable for real-time interaction using pntcc.}, | ||

+ | KEYWORDS = {PNTCC, NTCC, VERIFICATION, SIMULATION, INTERPRETER}, | ||

+ | MONTH = {August}, | ||

+ | PDF = {/wiki/lib/exe/fetch.php?media=grupos:avispa:papers:tor09c.pdf}, | ||

+ | YEAR = 2009 | ||

+ | } | ||

+ | </pre> | ||

+ | </p> | ||

+ | |||

+ | <p><a name="TRAA09"></a><pre> | ||

+ | @INPROCEEDINGS{traa09, | ||

+ | AUTHOR = {Mauricio Toro-Bermudez, Camilo Rueda, Carlos Agon, and Gerard Assayag}, | ||

+ | TITLE = {NTCCRT: A Concurrent Constraint Framework for Real-Time Interaction. }, | ||

+ | BOOKTITLE = {In Proc of the International Computer Music Conference, ICMC 2009}, | ||

+ | LOCATION = {Montreal, Canada}, | ||

+ | ABSTRACT = {Writing multimedia interaction systems is not easy. | ||

+ | Their concurrent processes usually access shared resources in a non-deterministic order, | ||

+ | often leading to unpredictable be- havior. Using Pure Data (Pd) and Max/MSP is possible to program concurrency, | ||

+ | however, it is difﬁcult to synchronize processes based on multiple criteria. Process calculi such as | ||

+ | the Non-deterministic Timed Concurrent Constraint (ntcc) calculus, overcome that problem by representing | ||

+ | multiple criteria as constraints. We propose using our framework Ntccrt to manage concurrency in Pd and Max. | ||

+ | Ntccrt is a real-time capable interpreter for ntcc. Using Ntccrt exter- nals (binary plugins) in Pd we ran | ||

+ | models for machine im- provisation and signal processing.}, | ||

+ | PDF = {/wiki/lib/exe/fetch.php?media=grupos:avispa:papers:traa09.pdf}, | ||

+ | YEAR = {2009} | ||

+ | } | ||

+ | </pre> | ||

+ | </p> | ||

+ | |||

+ | <p><a name="TOR09b"></a><pre> | ||

+ | @TECHREPORT{Tor09b, | ||

+ | AUTHOR = {M. Toro, C. Rueda, C. Agon, G. Assayag}, | ||

+ | TITLE = {GELISP: A library to represent musical CSPs and search strategies}, | ||

+ | INSTITUTION = {AVISPA Research Group, IRCAM and Pontificia Universidad | ||

+ | Javeriana}, | ||

+ | ABSTRACT = {In this paper we present Gelisp, a new library to | ||

+ | represent musical Constraint Satisfaction Problems | ||

+ | and search strategies intuitively. Gelisp has two | ||

+ | interfaces, a command-line one for Common Lisp | ||

+ | and a graphical one for OpenMusic. Using Gelisp, | ||

+ | we solved a problem of automatic music genera- | ||

+ | tion proposed by composer Michael Jarrell and we | ||

+ | found solutions for the All-interval series.}, | ||

+ | KEYWORDS = {CSP, GELISP, GECODE, CONSTRAINTS, OPENMUSIC}, | ||

+ | MONTH = {May}, | ||

+ | PDF = {/wiki/lib/exe/fetch.php?media=grupos:avispa:papers:tor09b.pdf}, | ||

+ | YEAR = 2009 | ||

+ | } | ||

+ | </pre> | ||

+ | </p> | ||

+ | <p><a name="AVV09"></a><pre> | ||

+ | @INPROCEEDINGS{avv09, | ||

+ | AUTHOR = {Jes{\'u}s Aranda and Frank D. Valencia and Cristian Versari}, | ||

+ | TITLE = {On the Expressive Power of Restriction and Priorities in CCS | ||

+ | with Replication}, | ||

+ | BOOKTITLE = {Foundations of Software Science and Computational | ||

+ | Structures, 12th International Conference, FOSSACS 2009, | ||

+ | Held as Part of the Joint European Conferences on | ||

+ | Theory and Practice of Software, ETAPS 2009}, | ||

+ | PAGES = {242-256}, | ||

+ | LOCATION = {York, UK}, | ||

+ | ISBN = {978-3-642-00595-4}, | ||

+ | SERIES = {Lecture Notes in Computer Science}, | ||

+ | VOLUME = {5504}, | ||

+ | MONTH = {March}, | ||

+ | PUBLISHER = {Springer}, | ||

+ | ABSTRACT = {We study the expressive power of restriction and its | ||

+ | interplay with replication. We do this by considering | ||

+ | several syntactic variants of CCS_{!} (CCS with | ||

+ | replication instead of recursion) which differ from | ||

+ | each other in the use of restriction with respect to | ||

+ | replication. We consider three syntactic variations of | ||

+ | CCS_{!} which do not allow the use of an unbounded | ||

+ | number of restrictions: CCS_{!}^{-!v} is the fragment of | ||

+ | CCS_{!} not allowing restrictions under the scope of a | ||

+ | replication. CCS_{!}^{-v} is the restriction-free | ||

+ | fragment of CCS_{!}. The third variant is | ||

+ | CCS_{!+pr}^{-!v} which extends CCS_{!}^{-!v} with | ||

+ | Phillips' priority guards. | ||

+ | We show that the use of unboundedly many restrictions | ||

+ | in CCS_{!} is necessary for obtaining Turing | ||

+ | expressiveness in the sense of Busi et al [N. Busi, M. | ||

+ | Gabbrielli, and G. Zavattaro. Comparing recursion, | ||

+ | replication, and iteration in process calculi. In | ||

+ | ICALP'04, volume 3142 of LNCS, pages 307-319. | ||

+ | Springer-Verlag, 2004]. We do this by showing that | ||

+ | there is no encoding of RAMs into CCS_{!}^{-!v} which | ||

+ | preserves and reflects convergence. | ||

+ | We also prove that up to failures equivalence, there is | ||

+ | no encoding from CCS_{!} into CCS_{!}^{-!v} nor from | ||

+ | CCS_{!}^{-!v} into CCS_{!}^{-v}. As lemmata for the | ||

+ | above results we prove that convergence is decidable | ||

+ | for CCS_{!}^{-!v} and that language equivalence is | ||

+ | decidable for CCS_{!}^{-v}. As corollary it follows | ||

+ | that convergence is decidable for restriction-free CCS. | ||

+ | Finally, we show the expressive power of priorities by | ||

+ | providing an encoding of RAMs in CCS_{!+pr}^{-!v}.}, | ||

+ | PDF = {/wiki/lib/exe/fetch.php?media=grupos:avispa:papers:avv09.pdf}, | ||

+ | YEAR = {2009} | ||

+ | } | ||

+ | </pre> | ||

+ | </p> | ||

+ | <p><a name="LMO+09"></a><pre> | ||

+ | @INPROCEEDINGS{lmo+09, | ||

+ | AUTHOR = {David Lesaint and Deepak Mehta and Barry O'Sullivan and Luis | ||

+ | Omar Quesada and Nic Wilson}, | ||

+ | TITLE = {A Soft Global Precedence Constraint}, | ||

+ | BOOKTITLE = {IJCAI 2009: Proceedings of the Twenty-Third AAAI Conference | ||

+ | on Artificial Intelligence}, | ||

+ | PAGES = {1693-1698}, | ||

+ | LOCATION = {Chicago, Illinois, USA}, | ||

+ | ISBN = {978-1-57735-368-3}, | ||

+ | PUBLISHER = {AAAI Press}, | ||

+ | ABSTRACT = {Hard and soft precedence constraints play a key role in many | ||

+ | application domains. In telecommunications, one | ||

+ | application is the configuration of callcontrol feature | ||

+ | subscriptions where the task is to sequence a set of | ||

+ | user-selected features subject to a set of hard | ||

+ | (catalogue) precedence constraints and a set of soft | ||

+ | (user-selected) precedence constraints. When no such | ||

+ | consistent sequence exists, the task is to find an | ||

+ | optimal relaxation by discarding some features or user | ||

+ | precedences. For this purpose, we present the global | ||

+ | constraint SOFTPREC. Enforcing Generalized Arc | ||

+ | Consistency (GAC) on SOFTPREC is NP-complete. Therefore, | ||

+ | we approximate GAC based on domain pruning rules that | ||

+ | follow from the semantics of SOFTPREC; this pruning is | ||

+ | polynomial. Empirical results demonstrate that the | ||

+ | search effort required by SOFTPREC is up to one order | ||

+ | of magnitude less than the previously known best CP | ||

+ | approach for the feature subscription problem. SOFTPREC | ||

+ | is also applicable to other problem domains including | ||

+ | minimum cutset problems for which initial experiments | ||

+ | confirm the interest.}, | ||

+ | PDF = {/wiki/lib/exe/fetch.php?media=grupos:avispa:papers:lmo_09.pdf}, | ||

+ | YEAR = {2009} | ||

+ | } | ||

+ | </pre> | ||

+ | </p> | ||

+ | <p><a name="Tor09"></a><pre> | ||

+ | @MISC{tor09, | ||

+ | AUTHOR = {Mauricio Toro}, | ||

+ | TITLE = {Probabilistic Extension to the Concurrent Constraint Factor | ||

+ | Oracle model for Music Improvisation}, | ||

+ | HOWPUBLISHED = {BSc Thesis -- Engineering Degree in Computer Science, | ||

+ | Pontificia Universidad Javeriana - Cali (Colombia).}, | ||

+ | ABSTRACT = {We can program a Real-Time (RT) music improvisation system | ||

+ | in C++ without a formal semantic or we can model it | ||

+ | with process calculi such as the Non-deterministic | ||

+ | Timed Concurrent Constraint (ntcc) calculus. | ||

+ | "Concurrent Constraints Factor Oracle (FO) model for | ||

+ | Music Improvisation" (Ccfomi) is an improvisation model | ||

+ | specified on ntcc. Since Ccfomi improvises | ||

+ | non-deterministically, there is no control on choices | ||

+ | and therefore little control over the sequence | ||

+ | variation during the improvisation. To avoid this, we | ||

+ | extended Ccfomi using the Probabilistic | ||

+ | Non-deterministic Timed Concurrent Constraint calculus. | ||

+ | Our extension to Ccfomi does not change the time and | ||

+ | space complexity of building the FO, thus making our | ||

+ | extension compatible with RT. However, there was not a | ||

+ | ntcc interpreter capable of RT to execute Ccfomi. We | ||

+ | developed Ntccrt -a RT capable interpreter for ntcc- | ||

+ | and we executed Ccfomi on Ntccrt. In the future, we | ||

+ | plan to extend Ntccrt to execute our extension to | ||

+ | Ccfomi.}, | ||

+ | KEYWORDS = {Factor Oracle, Concurrent Constraint Programming, CCP, | ||

+ | Machine Learning, Machine Improvisation, CCFOMI, | ||

+ | GECODE, NTCC, PNTCC, Real-Time}, | ||

+ | PDF = {/wiki/lib/exe/fetch.php?media=grupos:avispa:papers:tor09.pdf}, | ||

+ | YEAR = 2009 | ||

+ | } | ||

+ | </pre> | ||

+ | </p> | ||

+ | |||

+ | <p><a name="PR08"></a><pre> | ||

+ | @INPROCEEDINGS{PR08, | ||

+ | AUTHOR = {Jorge A. Perez and Camilo Rueda}, | ||

+ | TITLE = {Non-determinism and Probabilities in Timed Concurrent Constraint Programming}, | ||

+ | BOOKTITLE = {Proc. of 24th International Conference on Logic Programming (ICLP 2008)}, | ||

+ | LOCATION = {Udine, Italy}, | ||

+ | VOLUME = {5366}, | ||

+ | EDITOR = {Maria Garcia de la Banda and Enrico Pontelli}, | ||

+ | SERIES = {Lecture Notes in Computer Science}, | ||

+ | PAGES = {677-681}, | ||

+ | ISBN = {978-3-540-89981-5}, | ||

+ | PUBLISHER = {Springer}, | ||

+ | ABSTRACT = {A timed concurrent constraint process calculus with | ||

+ | probabilistic and non-deterministic choices is | ||

+ | proposed. We outline the rationale of an operational | ||

+ | semantics for the calculus. The semantics ensures | ||

+ | consistent interactions between both kinds of choices | ||

+ | and is indispensable for the definition of logic-based | ||

+ | verification capabilities over system specifications.}, | ||

+ | PDF = {/wiki/lib/exe/fetch.php?media=grupos:avispa:papers:pr08.pdf}, | ||

+ | YEAR = {2008} | ||

+ | } | ||

+ | </pre> | ||

+ | </p> | ||

+ | |||

+ | <p><a name="LPSS08"></a><pre> | ||

+ | @INPROCEEDINGS{LPSS08, | ||

+ | AUTHOR = {Lanese, I. and Perez, J. and Sangiorgi, D. and Schmitt, A.}, | ||

+ | TITLE = {On the {E}xpressiveness and {D}ecidability of {H}igher-{O}rder {P}rocess {C}alculi }, | ||

+ | BOOKTITLE = {Proc. of LICS'08}, | ||

+ | PAGES = {145--155}, | ||

+ | ABSTRACT = {In higher-order process calculi the values exchanged in | ||

+ | communications may contain processes. A core calculus | ||

+ | of higher-order concurrency is studied; it has only | ||

+ | the operators necessary to express higher-order | ||

+ | communications: input prefix, process output, and | ||

+ | parallel composition. By exhibiting a nearly | ||

+ | deterministic encoding of Minsky Machines, the | ||

+ | calculus is shown to be Turing Complete andtherefore | ||

+ | its termination problem is undecidable. Strong | ||

+ | bisimilarity, however, is proved to be decidable. | ||

+ | Further, the main forms of strong bisimilarity for | ||

+ | higher-order processes (higher-order bisimilarity, | ||

+ | context bisimilarity, normal bisimilarity, barbed | ||

+ | congruence) coincide. They also coincide with their | ||

+ | asynchronous versions. A sound and complete | ||

+ | axiomatization of bisimilarity is given. Finally, | ||

+ | bisimilarity is shown to become undecidable if at | ||

+ | least four static (i.e., top-level) restrictions are | ||

+ | added to the calculus.}, | ||

+ | PDF = {/wiki/lib/exe/fetch.php?media=grupos:avispa:papers:lpss08.pdf}, | ||

+ | YEAR = 2008 | ||

+ | } | ||

+ | </pre> | ||

+ | </p> | ||

+ | |||

+ | <p><a name="BPV08"></a><pre> | ||

+ | @INPROCEEDINGS{bpv08, | ||

+ | AUTHOR = {Romain Beauxis and Catuscia Palamidessi and Frank D. Valencia}, | ||

+ | TITLE = {On the Asynchronous Nature of the Asynchronous pi-Calculus}, | ||

+ | BOOKTITLE = {Concurrency, Graphs and Models, Essays Dedicated to Ugo | ||

+ | Montanari on the Occasion of His 65th Birthday}, | ||

+ | VOLUME = {5065}, | ||

+ | PAGES = {473-492}, | ||

+ | SERIES = {Lecture Notes in Computer Science}, | ||

+ | EDITOR = {Pierpaolo Degano and Rocco De Nicola and Jos{\'e} Meseguer}, | ||

+ | ISBN = {978-3-540-68676-7}, | ||

+ | PUBLISHER = {Springer}, | ||

+ | ABSTRACT = {We address the question of what kind of asynchronous | ||

+ | communication is exactly modeled by the asynchronous | ||

+ | $\pi$-calculus ($\pi_{a}$). To this purpose we define a | ||

+ | calculus $\pi_{\mathcal{B}}$ where channels are | ||

+ | represented explicitly as special buffer processes. The | ||

+ | base language for $\pi_{\mathcal{B}}$ is the | ||

+ | (synchronous) $\pi$-calculus, except that ordinary | ||

+ | processes communicate only via buffers. Then we compare | ||

+ | this calculus with $\pi_{a}$. It turns out that there is | ||

+ | a strong correspondence between $\pi_{a}$ and | ||

+ | $\pi_{\mathcal{B}}$ in the case that buffers are bags: | ||

+ | we can indeed encode each a process into $\pi_{a}$ | ||

+ | strongly asynchronous bisimilar $\pi_{\mathcal{B}}$ | ||

+ | process, and each $\pi_{\mathcal{B}}$ process into a | ||

+ | weakly asynchronous bisimilar $\pi_{a}$ process. In case | ||

+ | the buffers are queues or stacks, on the contrary, the | ||

+ | correspondence does not hold. We show indeed that it is | ||

+ | not possible to translate a stack or a queue into a | ||

+ | weakly asynchronous bisimilar $\pi_{a}$ process. | ||

+ | Actually, for stacks we show an even stronger result, | ||

+ | namely that they cannot be encoded into weakly | ||

+ | (asynchronous) bisimilar processes in a $\pi$-calculus | ||

+ | without mixed choice.}, | ||

+ | PDF = {/wiki/lib/exe/fetch.php?media=grupos:avispa:papers:bpv08.pdf}, | ||

+ | YEAR = {2008} | ||

+ | } | ||

+ | </pre> | ||

+ | </p> | ||

+ | |||

+ | <p><a name="APRV08"></a><pre> | ||

+ | @INPROCEEDINGS{APRV08, | ||

+ | AUTHOR = {Jes\'{u}s Aranda and Jorge Perez and Camilo Rueda and Frank D. Valencia}, | ||

+ | TITLE = {Stochastic {B}ehavior and {E}xplicit {D}iscrete {T}ime in {C}oncurrent {C}onstraint {P}rogramming}, | ||

+ | BOOKTITLE = {24th International Conference on Logic Programming (ICLP 2008)}, | ||

+ | PAGES = {682--686}, | ||

+ | ISBN = {978-3-540-89981-5}, | ||

+ | SERIES = {Lecture Notes in Computer Science}, | ||

+ | VOLUME = {5366}, | ||

+ | LOCATION = {Udine, Italy}, | ||

+ | PUBLISHER = {Springer-Verlag}, | ||

+ | ABSTRACT = {We address the inclusion of stochastic information into an | ||

+ | explicitly timed concurrent constraint process | ||

+ | language. An operational semantics is proposed as a | ||

+ | preliminary result. Our approach finds applications in | ||

+ | biology, among other areas.}, | ||

+ | PDF = {/wiki/lib/exe/fetch.php?media=grupos:avispa:papers:aprv08.pdf}, | ||

+ | YEAR = 2008 | ||

+ | } | ||

+ | </pre> | ||

+ | </p> | ||

+ | <p><a name="CCAV08"></a><pre> | ||

+ | @ARTICLE{ccav08, | ||

+ | AUTHOR = {Diletta Cacciagrano and Flavio Corradini and Jes\'{u}s Aranda | ||

+ | and Frank D. Valencia}, | ||

+ | TITLE = {Linearity, Persistence and Testing Semantics in the | ||

+ | Asynchronous Pi-Calculus}, | ||

+ | JOURNAL = {Electronic Notes in Theoretical Computer Science (ENTCS)}, | ||

+ | VOLUME = {194}, | ||

+ | NUMBER = {2}, | ||

+ | ISSN = {1571-0661}, | ||

+ | PAGES = {59--84}, | ||

+ | PUBLISHER = {Elsevier Science Publishers B. V.}, | ||

+ | ADDRESS = {Amsterdam, The Netherlands, The Netherlands}, | ||

+ | ABSTRACT = {In [C. Palamidessi, V. Saraswat, F. Valencia and B. Victor. | ||

+ | On the Expressiveness of Linearity vs Persistence in | ||

+ | the Asynchronous Pi Calculus. LICS 2006:59-68, 2006] | ||

+ | the authors studied the expressiveness of persistence | ||

+ | in the asynchronous $\pi$-calculus (A$\pi$) wrt weak | ||

+ | barbed congruence. The study is incomplete because it | ||

+ | ignores the issue of divergence. In this paper, we | ||

+ | present an expressiveness study of persistence in the | ||

+ | asynchronous $\pi$-calculus (A$\pi$) wrt De Nicola and | ||

+ | Hennessy's testing scenario which is sensitive to | ||

+ | divergence. Following [C. Palamidessi, V. Saraswat, | ||

+ | F. Valencia and B. Victor. On the Expressiveness of | ||

+ | Linearity vs Persistence in the Asynchronous Pi | ||

+ | Calculus. LICS 2006:59-68, 2006], we consider A$\pi$ | ||

+ | and three sub-languages of it, each capturing one | ||

+ | source of persistence: the persistent-input calculus | ||

+ | (PIA$\pi$), the persistent-output calculus (POA$\pi$) | ||

+ | and persistent calculus (PA$\pi$). In [C. Palamidessi, | ||

+ | V. Saraswat, F. Valencia and B. Victor. On the | ||

+ | Expressiveness of Linearity vs Persistence in the | ||

+ | Asynchronous Pi Calculus. LICS 2006:59-68, 2006] the | ||

+ | authors showed encodings from A$\pi$ into the | ||

+ | semi-persistent calculi (i.e., POA$\pi$ and PIA$\pi$) | ||

+ | correct wrt weak barbed congruence. In this paper we | ||

+ | prove that, under some general conditions, there | ||

+ | cannot be an encoding from A$\pi$ into a | ||

+ | (semi)-persistent calculus preserving the must testing | ||

+ | semantics.}, | ||

+ | PDF = {/wiki/lib/exe/fetch.php?media=grupos:avispa:papers:ccav08.pdf}, | ||

+ | YEAR = {2008} | ||

+ | } | ||

+ | </pre> | ||

+ | </p> | ||

+ | <p><a name="OV08b"></a><pre> | ||

+ | @INPROCEEDINGS{OV08b, | ||

+ | AUTHOR = {Olarte, C. and Valencia, F.D.}, | ||

+ | TITLE = {The {E}xpressivity of {U}niversal {T}imed {CCP}: | ||

+ | {U}ndecidability of {M}onadic {FLTL} and {C}losure | ||

+ | {O}perators for {S}ecurity}, | ||

+ | BOOKTITLE = {PPDP '08: Proceedings of the 10th international ACM | ||

+ | SIGPLAN conference on Principles and practice of | ||

+ | declarative programming}, | ||

+ | YEAR = {2008}, | ||

+ | ISBN = {978-1-60558-117-0}, | ||

+ | PAGES = {8--19}, | ||

+ | LOCATION = {Valencia, Spain}, | ||

+ | PUBLISHER = {ACM}, | ||

+ | ADDRESS = {New York, NY, USA}, | ||

+ | ABSTRACT = {The timed concurrent constraint programing model (tcc) is a | ||

+ | declarative framework, closely related to First-Order | ||

+ | Linear Temporal Logic (FLTL), for modeling reactive | ||

+ | systems. The universal tcc formalism (utcc) is an | ||

+ | extension of tcc with the ability to express mobility. | ||

+ | Here mobility is understood as communication of | ||

+ | private names as typically done for mobile systems and | ||

+ | security protocols. | ||

+ | This paper is devoted to the study of 1) the | ||

+ | expressiveness of utcc and 2) its semantic foundations. | ||

+ | As applications of this study, we also state 3) a | ||

+ | noteworthy decidability result for the well-established | ||

+ | framework of FLTL and 4) bring new semantic insights | ||

+ | into the modeling of security protocols. | ||

+ | More precisely, we show that in contrast to tcc, utcc | ||

+ | is Turingpowerful by encoding Minsky machines. The | ||

+ | encoding uses a monadic constraint system allowing us | ||

+ | to prove a new result for a fragment of FLTL: The | ||

+ | undecidability of the validity problem for monadic | ||

+ | FLTL without equality and function symbols. This | ||

+ | result refutes a decidability conjecture for FLTL from | ||

+ | a previous paper. It also justifies the restriction | ||

+ | imposed in previous decidability results on the | ||

+ | quantification of flexible-variables. | ||

+ | We shall also show that as in tcc, utcc processes can | ||

+ | be semantically represented as partial closure | ||

+ | operators. The representation is fully abstract wrt | ||

+ | the input-output behavior of processes for a | ||

+ | meaningful fragment of the utcc. This shows that | ||

+ | mobility can be captured as closure operators over an | ||

+ | underlying constraint system. As an application we | ||

+ | identify a language for security protocols that can be | ||

+ | represented as closure operators over a cryptographic | ||

+ | constraint system.}, | ||

+ | PDF = {/wiki/lib/exe/fetch.php?media=grupos:avispa:papers:ov08b.pdf}, | ||

+ | YEAR = 2008 | ||

+ | } | ||

+ | </pre> | ||

+ | </p> | ||

+ | <p><a name="OV08a"></a><pre> | ||

+ | @INPROCEEDINGS{OV08a, | ||

+ | AUTHOR = {Olarte, C. and Valencia, F.D.}, | ||

+ | TITLE = {Universal {C}oncurrent {C}onstraint {P}rogramming: {S}ymbolic | ||

+ | {S}emantics and {A}pplications to {S}ecurity}, | ||

+ | BOOKTITLE = {SAC '08: Proceedings of the 2008 ACM symposium on Applied | ||

+ | computing}, | ||

+ | YEAR = {2008}, | ||

+ | ISBN = {978-1-59593-753-7}, | ||

+ | PAGES = {145--150}, | ||

+ | LOCATION = {Fortaleza, Ceara, Brazil}, | ||

+ | PUBLISHER = {ACM}, | ||

+ | ADDRESS = {New York, NY, USA}, | ||

+ | ABSTRACT = {We introduce the Universal Timed Concurrent Constraint | ||

+ | Programming (utcc) process calculus; a generalisation | ||

+ | of Timed Concurrent Constraint Programming. The utcc | ||

+ | calculus allows for the specication of mobile | ||

+ | behaviours in the sense of Milner's pi-calculus: | ||

+ | Generation and communication of private channels or | ||

+ | links. We first endow utcc with an operational | ||

+ | semantics and then with a symbolic semantics to deal | ||

+ | with problematic operational aspects involving | ||

+ | infinitely many substitutions and divergent internal | ||

+ | computations. The novelty of the symbolic semantics is | ||

+ | to use temporal constraints to represent finitely | ||

+ | infinitely-many substitutions. We also show that utcc | ||

+ | has a strong connection with Pnueli's Temporal Logic. | ||

+ | This connection can be used to prove reachability | ||

+ | properties of utcc processes. As a compelling example, | ||

+ | we use utcc to exhibit the secrecy flaw of the | ||

+ | Needham-Schroeder security protocol.}, | ||

+ | PDF = {/wiki/lib/exe/fetch.php?media=grupos:avispa:papers:ov08a.pdf}, | ||

+ | YEAR = 2008 | ||

+ | } | ||

+ | </pre> | ||

+ | </p> | ||

+ | <p><a name="ORV08"></a><pre> | ||

+ | @INPROCEEDINGS{ORV08, | ||

+ | AUTHOR = {Olarte, C. Rueda, C. and Valencia, F. D.}, | ||

+ | TITLE = {Universal Timed CCP: Expressivity and Application to Musical Improvisation}, | ||

+ | BOOKTITLE = {CLEI2008}, | ||

+ | ISBN = {978-950-9770-02-7}, | ||

+ | PAGES = {1465--1474}, | ||

+ | LOCATION = {Santa Fe, Argentina}, | ||

+ | ABSTRACT = {Universal timed concurrent constraint programming (utcc) is | ||

+ | an extension of temporal CCP (tcc) aimed at modeling | ||

+ | mobile reactive systems. The language counts with | ||

+ | several reasoning techniques such as a symbolic | ||

+ | semantics and a compositional semantics based on | ||

+ | closure operators. Additionally, utcc processes can be | ||

+ | regarded as formulae in first-order linear temporal | ||

+ | logic (FLTL). In this paper we first show how the | ||

+ | abstraction operator introduced in utcc can neatly | ||

+ | express arbitrary recursion which is not possible in | ||

+ | tcc. Second, we present an encoding of the | ||

+ | lambda-calculus into utcc. Although utcc has been | ||

+ | previously proved to be Turing powerful encoding | ||

+ | Minsky machines in it, the encoding we present here is | ||

+ | compositional unlike that of Minsky machines. | ||

+ | Compositionality is an important property of an | ||

+ | encoding as it may allow structural analysis in utcc | ||

+ | of the source terms; i.e., functional programs. | ||

+ | Finally, as compelling application, making use of the | ||

+ | recursive definitions in utcc, we model a music | ||

+ | improvisation system composed of interactive agents | ||

+ | learning a musical style and generating on the fly new | ||

+ | material in the same style.}, | ||

+ | PDF = {/wiki/lib/exe/fetch.php?media=grupos:avispa:papers:orv08.pdf}, | ||

+ | YEAR = 2008 | ||

+ | } | ||

+ | </pre> | ||

+ | </p> | ||

+ | <p><a name="SR08"></a><pre> | ||

+ | @INPROCEEDINGS{SR08, | ||

+ | AUTHOR = {Sarria, G. and Rueda, C.}, | ||

+ | TITLE = {Real-Time {C}oncurrent {C}onstraint {P}rogramming}, | ||

+ | BOOKTITLE = {CLEI2008}, | ||

+ | ISBN = {978-950-9770-02-7}, | ||

+ | PAGES = {1475--1484}, | ||

+ | LOCATION = {Santa Fe, Argentina}, | ||

+ | ABSTRACT = {The \texttt{ntcc} calculus is a model of temporal | ||

+ | concurrent constraint programming with the capability | ||

+ | of expressing asynchronous and non-deterministic | ||

+ | timed behaviour. We propose a model of real-time | ||

+ | concurrent constraint programming, which adds to | ||

+ | \texttt{ntcc} the means for specifying and modelling | ||

+ | real-time behaviour. We provide a new construct for | ||

+ | strong preemption, an operational semantics | ||

+ | supporting resources and limited time and a | ||

+ | denotational semantics based on CHU spaces. We argue | ||

+ | that the resultant calculus has a natural application | ||

+ | in various fields such as multimedia interaction.}, | ||

+ | PDF = {/wiki/lib/exe/fetch.php?media=grupos:avispa:papers:sr08.pdf}, | ||

+ | YEAR = 2008 | ||

+ | } | ||

+ | </pre> | ||

+ | </p> | ||

+ | <p><a name="HLM+08"></a><pre> | ||

+ | @INPROCEEDINGS{hlm+08, | ||

+ | AUTHOR = {Tarik Hadzic and David Lesaint and Deepak Mehta and Barry | ||

+ | O'Sullivan and Luis Omar Quesada Ramirez and Nic Wilson}, | ||

+ | TITLE = {A BDD Approach to the Feature Subscription Problem}, | ||

+ | BOOKTITLE = {ECAI 2008 - Proceedings of the 18th European Conference on | ||

+ | Artificial Intelligence}, | ||

+ | VOLUME = {178}, | ||

+ | PAGES = {698--702}, | ||

+ | LOCATION = {Patras, Greece}, | ||

+ | MONTH = {July}, | ||

+ | SERIES = {Frontiers in Artificial Intelligence and Applications}, | ||

+ | ISBN = {978-1-58603-891-5}, | ||

+ | PUBLISHER = {IOS Press}, | ||

+ | ABSTRACT = {Modern feature-rich telecommunications services offer | ||

+ | significant opportunities to human users. To make these | ||

+ | services more usable, facilitating personalisation is | ||

+ | very important since it enhances the users' experience | ||

+ | considerably. However, regardless how service providers | ||

+ | organise their catalogues of features, they cannot | ||

+ | achieve complete configurability due to the existence | ||

+ | of feature interactions. Distributed Feature | ||

+ | Composition (DFC) provides a comprehensive methodology, | ||

+ | underpinned by a formal architecture model to address | ||

+ | this issue. In this paper we present an approach based | ||

+ | on using Binary Decision Diagrams (BDD) to find optimal | ||

+ | reconfigurations of features when a user's preferences | ||

+ | violate the technical constraints defined by a set of | ||

+ | DFC rules. In particular, we propose hybridizing | ||

+ | constraint programming and standard BDD compilation | ||

+ | techniques in order to scale the construction of a BDD | ||

+ | for larger size catalogues. Our approach outperforms | ||

+ | the standard BDD techniques by reducing the memory | ||

+ | requirements by as much as five orders-of-magnitude and | ||

+ | compiles the catalogues for which the standard | ||

+ | techniques ran out of memory.}, | ||

+ | PDF = {/wiki/lib/exe/fetch.php?media=grupos:avispa:papers:hlm_08.pdf}, | ||

+ | YEAR = {2008} | ||

+ | } | ||

+ | </pre> | ||

+ | </p> | ||

+ | <p><a name="LMO+08c"></a><pre> | ||

+ | @INPROCEEDINGS{lmo+08c, | ||

+ | AUTHOR = {David Lesaint and Deepak Mehta and Barry O'Sullivan and Luis | ||

+ | Omar Quesada and Nic Wilson}, | ||

+ | TITLE = {Personalisation of Telecommunications Services as Combinatorial | ||

+ | Optimisation}, | ||

+ | BOOKTITLE = {AAAI 2008: Proceedings of the Twenty-Third AAAI Conference | ||

+ | on Artificial Intelligence}, | ||

+ | PAGES = {1693-1698}, | ||

+ | LOCATION = {Chicago, Illinois, USA}, | ||

+ | ISBN = {978-1-57735-368-3}, | ||

+ | PUBLISHER = {AAAI Press}, | ||

+ | ABSTRACT = {Modern feature-rich telecommunications services offer | ||

+ | significant opportunities to human users. To make these | ||

+ | services more usable, facilitating personalisation is | ||

+ | very important. Such personalisation enhances the | ||

+ | users' experience considerably. The Session Initiation | ||

+ | Protocol and Distributed Feature Composition | ||

+ | architecture allow users to select and compose | ||

+ | telecommunications network applications or features. In | ||

+ | this paper we view feature composition as a | ||

+ | configuration problem. We model feature composition | ||

+ | using a variety of combinatorial optimisation paradigms. | ||

+ | In particular, we present and evaluate an approach to | ||

+ | finding optimal reconfigurations of network features | ||

+ | when the user's preferences violate the technical | ||

+ | constraints defined by a set of DFC rules.}, | ||

+ | PDF = {/wiki/lib/exe/fetch.php?media=grupos:avispa:papers:lmo_08c.pdf}, | ||

+ | YEAR = {2008} | ||

+ | } | ||

+ | </pre> | ||

+ | </p> | ||

+ | <p><a name="LMO+08b"></a><pre> | ||

+ | @INPROCEEDINGS{lmo+08b, | ||

+ | AUTHOR = {David Lesaint and Deepak Mehta and Barry O'Sullivan and Luis | ||

+ | Omar Quesada Ramirez and Nic Wilson}, | ||

+ | TITLE = {Consistency Techniques for Finding an Optimal Relaxation of a | ||

+ | Feature Subscription}, | ||

+ | BOOKTITLE = {ICTAI '08: Proceedings of the 2008 20th IEEE International | ||

+ | Conference on Tools with Artificial Intelligence}, | ||

+ | VOLUME = {1}, | ||

+ | PAGES = {283--290}, | ||

+ | ISBN = {978-0-7695-3440-4}, | ||

+ | PUBLISHER = {IEEE Computer Society}, | ||

+ | ABSTRACT = {Telecommunication services are playing an increasing and | ||

+ | potentially disruptive role in our lives. As a result, | ||

+ | service providers seek to develop personalisation | ||

+ | solutions that put customers in charge of controlling | ||

+ | and enriching their services. In this context, the | ||

+ | personalisation approach consists of exposing a | ||

+ | catalogue of call control features (e.g., call-divert, | ||

+ | voice-mail) to end-users and letting them subscribe to | ||

+ | a subset of features subject to a set of precedence and | ||

+ | exclusion constraints. When a subscription is | ||

+ | inconsistent, the problem is to find an optimal | ||

+ | relaxation. We present a constraint programming | ||

+ | formulation to find an optimal reconfiguration of | ||

+ | features. We investigate the performance of maintaining | ||

+ | arc consistency within branch and bound search. We also | ||

+ | study the impact of maintaining mixed consistency, that | ||

+ | is maintaining different levels of consistency on | ||

+ | different sets of variables. We further present a | ||

+ | global constraint and a set of filtering rules that | ||

+ | exploit the structure of our problem. We theoretically | ||

+ | and experimentally compare all approaches. Our results | ||

+ | demonstrate that the filtering rules of the global | ||

+ | constraint outperform all other approaches when a | ||

+ | catalogue is dense, and mixed consistency pays off when | ||

+ | a catalogue is sparse.}, | ||

+ | PDF = {/wiki/lib/exe/fetch.php?media=grupos:avispa:papers:lmo_08b.pdf}, | ||

+ | YEAR = {2008} | ||

+ | } | ||

+ | </pre> | ||

+ | </p> | ||

+ | <p><a name="LMO+08a"></a><pre> | ||

+ | @INPROCEEDINGS{lmo+08a, | ||

+ | AUTHOR = {David Lesaint and Deepak Mehta and Barry O'Sullivan and Luis | ||

+ | Omar Quesada Ramirez and Nic Wilson}, | ||

+ | TITLE = {Solving a Telecommunications Feature Subscription Configuration | ||

+ | Problem}, | ||

+ | BOOKTITLE = {CP '08: Proceedings of the 14th international conference on | ||

+ | Principles and Practice of Constraint Programming}, | ||

+ | LOCATION = {Sydney, Australia}, | ||

+ | VOLUME = {5202}, | ||

+ | SERIES = {Lecture Notes in Computer Science}, | ||

+ | PAGES = {67--81}, | ||

+ | ISBN = {978-3-540-85957-4}, | ||

+ | PUBLISHER = {Springer}, | ||

+ | ABSTRACT = {Call control features (e.g., call-divert, voice-mail) are | ||

+ | primitive options to which users can subscribe off-line | ||

+ | to personalise their service. The configuration of a | ||

+ | feature subscription involves choosing and sequencing | ||

+ | features from a catalogue and is subject to constraints | ||

+ | that prevent undesirable feature interactions at | ||

+ | run-time. When the subscription requested by a user is | ||

+ | inconsistent, one problem is to find an optimal | ||

+ | relaxation. In this paper, we show that this problem is | ||

+ | NP-hard and we present a constraint programming | ||

+ | formulation using the variable weighted constraint | ||

+ | satisfaction problem framework. We also present simple | ||

+ | formulations using partial weighted maximum | ||

+ | satisfiability and integer linear programming. We | ||

+ | experimentally compare our formulations of the | ||

+ | different approaches; the results suggest that our | ||

+ | constraint programming approach is the best of the | ||

+ | three overall.}, | ||

+ | PDF = {/wiki/lib/exe/fetch.php?media=grupos:avispa:papers:lmo08a.pdf}, | ||

+ | YEAR = {2008} | ||

+ | } | ||

+ | </pre> | ||

+ | </p> | ||

+ | <p><a name="TOR08"></a><pre> | ||

+ | @TECHREPORT{Tor08, | ||

+ | AUTHOR = {M. Toro}, | ||

+ | TITLE = {Exploring the possibilities and limitations of Concurrent Programming for Multimedia Interaction and Visual Programming for Musical Constraint Satisfaction Problems}, | ||

+ | INSTITUTION = {AVISPA Research Group, IRCAM and Pontificia Universidad | ||

+ | Javeriana}, | ||

+ | ABSTRACT = {Multimedia interaction systems are inherently concurrent. Developing correct concurrent systems | ||

+ | is diﬃcult because we need to consider all the possible interactions between processes. To reason | ||

+ | formally about concurrent systems, there are several concurrent process calculi. We developed | ||

+ | multiple prototypes for real-time capable interpreters for both, Concurrent Constraint Program- | ||

+ | ming (CCP) and Non-deterministic Timed Concurrent Constraint (ntcc). We found out that using | ||

+ | lightweight threads to implement these interpreters is not appropriate for real-time (RT) interac- | ||

+ | tion. Instead, we recommend using event-driven programming. Using this model of concurrency, | ||

+ | we developed Ntccrt, an interpreter for ntcc capable of RT interaction. Ntccrt is based on encoding | ||

+ | ntcc processes as Gecode propagators. Using Ntccrt, we executed some models in Pure Data. Due | ||

+ | to our success using Gecode, we upgraded Gelisp, providing a graphical interface to solve musical | ||

+ | Constraint Satisfaction Problems (CSP) in OpenMusic based on Gecode. In Gelisp, constraints, | ||

+ | search heuristics, and optimization criteria can be represented graphically. Using Gelisp, we suc- | ||

+ | cessfully solved a CSP proposed by compositor Michael Jarrell. | ||

+ | }, | ||

+ | KEYWORDS = {concurrent constraint programming, constraint satisfaction problem, constraints, ntcc, | ||

+ | gelisp, csp, interpreter, ccp, ntccrt, openmusic, real-time, gecol, gecode.}, | ||

+ | MONTH = {December}, | ||

+ | PDF = {/wiki/lib/exe/fetch.php?media=grupos:avispa:papers:tor08.pdf}, | ||

+ | YEAR = 2008 | ||

+ | } | ||

+ | </pre> | ||

+ | </p> | ||

+ | <p><a name="SAR08"></a><pre> | ||

+ | @PHDTHESIS{Sar08, | ||

+ | AUTHOR = {Sarria, G.}, | ||

+ | TITLE = {Formal Models of Timed Musical Processes}, | ||

+ | SCHOOL = {Universidad del Valle}, | ||

+ | NOTE = {PhD thesis. xii+150}, | ||

+ | ABSTRACT = {In the last decades several formal models have been | ||

+ | proposed to formalize various musical applications, to | ||

+ | solve musical and improvisation problems and to prove | ||

+ | properties in music. In this document we briefly | ||

+ | describe some of those formal models, their | ||

+ | applications and we give some considerations about | ||

+ | them. We focus on the CCP calculi and specially on the | ||

+ | \texttt{ntcc} calculus, a model of temporal concurrent | ||

+ | constraint programming with the capability of | ||

+ | expressing asynchronous and non-deterministic timed | ||

+ | behaviour. This calculus has been used as a convenient | ||

+ | formalism for expressing temporal musical processes. | ||

+ | Additionally, in this thesis we propose a model of | ||

+ | real-time concurrent constraint programming, called | ||

+ | \texttt{rtcc}, which adds to \texttt{ntcc} the means | ||

+ | for specifying and modeling real-time behaviour. This | ||

+ | calculus is provided with a new construct for modeling | ||

+ | strong preemption and another one for defining delays | ||

+ | within the same time unit. Together with these new | ||

+ | features we provide an operational semantics | ||

+ | supporting resources, limited time and true | ||

+ | concurrency. | ||

+ | A denotational semantics based on Chu spaces is also | ||

+ | provided. The lack of monotonicity derived from the | ||

+ | new constructs and the inclusion of resources and time | ||

+ | in the operational semantics precludes defining the | ||

+ | denotations of processes in terms of quiescent points | ||

+ | as is usual in CCP calculi such as \texttt{ntcc}. | ||

+ | This dissertation also introduces a real-time logic | ||

+ | for expressing temporal specifications of | ||

+ | \texttt{rtcc} processes. An inference system is | ||

+ | defined to prove that a process in the calculus | ||

+ | satisfies a formula in the logic. | ||

+ | Finally, we show the applicability of the | ||

+ | \texttt{rtcc} calculus in music and multimedia | ||

+ | interaction. We formalize the notion of OpenMusic | ||

+ | Maquette as the main application.}, | ||

+ | COMMENT = {Defence: September 1, 2008}, | ||

+ | INSTITUTION = {Universidad del Valle}, | ||

+ | KEYWORDS = {Concurrent Constraint Programming, ntcc, rtcc, Music, | ||

+ | Semantics of Programming Languages}, | ||

+ | PDF = {/wiki/lib/exe/fetch.php?media=grupos:avispa:papers:sar08.pdf}, | ||

+ | YEAR = 2008 | ||

+ | } | ||

+ | </pre> | ||

+ | </p> | ||

+ | <p><a name="AGPV07"></a><pre> | ||

+ | @INPROCEEDINGS{AGPV07, | ||

+ | AUTHOR = {Jes{\'u}s Aranda and Cinzia Di Giusto and Catuscia Palamidessi | ||

+ | and Frank D. Valencia}, | ||

+ | TITLE = {On Recursion, Replication and Scope Mechanisms in Process | ||

+ | Calculi}, | ||

+ | BOOKTITLE = {Formal Methods for Components and Objects, 5th | ||

+ | International Symposium, FMCO 2006}, | ||

+ | PAGES = {185-206}, | ||

+ | PUBLISHER = {Springer}, | ||

+ | SERIES = {Lecture Notes in Computer Science}, | ||

+ | VOLUME = {4709}, | ||

+ | LOCATION = {Amsterdam, The Netherlands}, | ||

+ | ISBN = {978-3-540-74791-8}, | ||

+ | ABSTRACT = {This paper we shall survey and discuss in detail the work on | ||

+ | the relative expressiveness of Recursion and | ||

+ | Replication in various process calculi. Namely, CCS, | ||

+ | the $\pi$-calculus, the Ambient calculus, Concurrent | ||

+ | Constraint Programming and calculi for Cryptographic | ||

+ | Protocols. We shall see that often the ability of | ||

+ | expressing recursive behaviours via replication depends | ||

+ | on the scoping mechanisms of the given calculus which | ||

+ | compensate for the restriction of replication.}, | ||

+ | MONTH = {November}, | ||

+ | PDF = {/wiki/lib/exe/fetch.php?media=grupos:avispa:papers:agpv07.pdf}, | ||

+ | YEAR = 2007 | ||

+ | } | ||

+ | </pre> | ||

+ | </p> | ||

+ | <p><a name="AGNV07"></a><pre> | ||

+ | @INPROCEEDINGS{AGNV07, | ||

+ | AUTHOR = {Jes{\'u}s Aranda and Cinzia Di Giusto and Mogens Nielsen and | ||

+ | Frank D. Valencia}, | ||

+ | TITLE = {CCS with Replication in the Chomsky Hierarchy: The Expressive | ||

+ | Power of Divergence}, | ||

+ | BOOKTITLE = {Programming Languages and Systems, 5th Asian | ||

+ | Symposium, APLAS 2007}, | ||

+ | PUBLISHER = {Springer}, | ||

+ | SERIES = {Lecture Notes in Computer Science}, | ||

+ | VOLUME = {4807}, | ||

+ | PAGES = {383-398}, | ||

+ | ISBN = {978-3-540-76636-0}, | ||

+ | ABSTRACT = {A remarkable result in [N. Busi, M. Gabbrielli, and G. | ||

+ | Zavattaro. Comparing recursion, replication, and | ||

+ | iteration in process calculi. In ICALP'04, volume 3142 | ||

+ | of Lecture Notes in Computer Science, pages 307-319. | ||

+ | Springer-Verlag, 2004] shows that in spite of its being | ||

+ | less expressive than CCS w.r.t. weak bisimilarity, | ||

+ | CCS_{!} (a CCS variant where infinite behavior is | ||

+ | specified by using replication rather than recursion) | ||

+ | is Turing powerful. This is done by encoding Random | ||

+ | Access Machines (RAM) in CCS_{!}. The encoding is said | ||

+ | to be \emph{non-faithful} because it may move from a | ||

+ | state which can lead to termination into a divergent | ||

+ | one which do not correspond to any configuration of the | ||

+ | encoded RAM. I.e., the encoding is not termination | ||

+ | preserving. | ||

+ | In this paper we study the existence of faithful | ||

+ | encodings into CCS_{!} of models of computability | ||

+ | \emph{strictly less} expressive than Turing Machines. | ||

+ | Namely, grammars of Types 1 (Context Sensitive | ||

+ | Languages), 2 (Context Free Languages) and 3 (Regular | ||

+ | Languages) in the Chomsky Hierarchy. We provide | ||

+ | faithful encodings of Type 3 grammars. We show that it | ||

+ | is impossible to provide a faithful encoding of Type 2 | ||

+ | grammars and that termination-preserving CCS_{!} | ||

+ | processes can generate languages which are not Type 2. | ||

+ | We finally show that the languages generated by | ||

+ | termination-preserving CCS_{!} processes are Type 1.}, | ||

+ | PDF = {/wiki/lib/exe/fetch.php?media=grupos:avispa:papers:agnv07.pdf}, | ||

+ | YEAR = 2007 | ||

+ | } | ||

+ | </pre> | ||

+ | </p> | ||

+ | <p><a name="OPV07"></a><pre> | ||

+ | @INPROCEEDINGS{OPV07, | ||

+ | AUTHOR = {Olarte, C. and Palamidessi, C. and Valencia, F.D.}, | ||

+ | TITLE = {Universal {T}imed {C}oncurrent {C}onstraint {P}rogramming}, | ||

+ | BOOKTITLE = {ICLP 2007}, | ||

+ | ABSTRACT = {In this doctoral work we aim at developing a rich timed | ||

+ | concurrent constraint (tcc) based language with strong | ||

+ | ties to logic. The new calculus called Universal Timed | ||

+ | Concurrent Constraint (utcc) increases the | ||

+ | expressiveness of tcc languages allowing infinite | ||

+ | behaviour and mobility. We introduce a constructor of | ||

+ | the form (abs x; c)P (Abstraction in P) that can be | ||

+ | viewed as a dual operator of the hidden operator | ||

+ | local x in P. i.e. the later can be viewed as an | ||

+ | |||

+ | existential quantication on the variable x and the | ||

+ | former as an universal quantication of x, executing | ||

+ | P[t=x] for all t s.t. the current store entails c[t=x]. | ||

+ | As a compelling application, we applied this calculus | ||

+ | to verify security protocols.}, | ||

+ | PDF = {/wiki/lib/exe/fetch.php?media=grupos:avispa:papers:opv07.pdf}, | ||

+ | YEAR = 2007 | ||

+ | } | ||

+ | </pre> | ||

+ | </p> | ||

+ | <p><a name="FOPV07"></a><pre> | ||

+ | @INPROCEEDINGS{FOPV07, | ||

+ | AUTHOR = {Falaschi, M. and Olarte, C. and Palamidessi, C. and Valencia, F.D.}, | ||

+ | TITLE = {Declarative {D}iagnosis of {T}emporal {C}oncurrent {C}onstraint {P}rograms}, | ||

+ | BOOKTITLE = {ICLP 2007}, | ||

+ | ABSTRACT = {We present a framework for the declarative diagnosis of | ||

+ | nondeterministic timed concurrent constraint programs. | ||

+ | We present a denotational semantics based on a | ||

+ | (continuous) immediate consequence operator, TD, which | ||

+ | models the process behaviour associated with a program | ||

+ | D given in terms of sequences of constraints. Then, we | ||

+ | show that, given the intended specication of D, it is | ||

+ | possible to check the correctness of D by a single | ||

+ | step of TD. In order to develop an eective debugging | ||

+ | method, we approximate the denotational semantics of D. | ||

+ | We formalize this method by abstract interpretation | ||

+ | techniques, and we derive a finitely terminating | ||

+ | abstract diagnosis method, which can be used | ||

+ | statically. We define an abstract domain which allows | ||

+ | us to approximate the infinite sequences by a finite | ||

+ | `cut'. As a further development we show how to use a | ||

+ | specific linear temporal logic for deriving | ||

+ | automatically the debugging sequences. Our debugging | ||

+ | framework does not require the user to either provide | ||

+ | error symptoms in advance or answer questions | ||

+ | concerning program correctness. Our method is | ||

+ | compositional, that may allow to master the complexity | ||

+ | of the debugging methodology.}, | ||

+ | KEYWORDS = {Timed concurrent constraint programs, (modular) declarative | ||

+ | debugging, denotational semantics, specification logic.}, | ||

+ | PDF = {/wiki/lib/exe/fetch.php?media=grupos:avispa:papers:fopv07.pdf}, | ||

+ | YEAR = 2007 | ||

+ | } | ||

+ | </pre> | ||

+ | </p> | ||

+ | <p><a name="MOR07"></a><pre> | ||

+ | @ARTICLE{MOR07, | ||

+ | AUTHOR = {Monfroy, E. and Olarte, C. and Rueda, C.}, | ||

+ | TITLE = {Process {C}alculi for {A}daptive {E}numeration {S}trategies | ||

+ | in {C}onstraint {P}rogramming.}, | ||

+ | JOURNAL = {Research in Computing Science}, | ||

+ | ABSTRACT = {Constraint programming (CP) has been extensively used to | ||

+ | solve a wide variety of problems. Solving a constraint | ||

+ | problem mainly consists in two phases: propagation to | ||

+ | prune the search space, and enumeration to choose a | ||

+ | variable and one of its values for branching. | ||

+ | Enumeration strategies are crucial for resolution | ||

+ | performances. We propose a framework to model adaptive | ||

+ | enumeration strategies using a stochastic, | ||

+ | non-deterministic timed concurrent constraint calculus. | ||

+ | Using the reactivity of the calculus we can design | ||

+ | enumeration strategies that adapt themselves according | ||

+ | to information issued from the resolution process and | ||

+ | from external solvers such as an incomplete solver. | ||

+ | The experimental results show the eectiveness of our | ||

+ | approach.}, | ||

+ | PDF = {/wiki/lib/exe/fetch.php?media=grupos:avispa:papers:mor07.pdf}, | ||

+ | YEAR = 2007 | ||

+ | } | ||

+ | </pre> | ||

+ | </p> | ||

+ | <p><a name="GPRV07"></a><pre> | ||

+ | @ARTICLE{GPRV07, | ||

+ | AUTHOR = {Gutierrez, J. and Perez, J. and Rueda, C. and Valencia, F.D.}, | ||

+ | TITLE = {Timed {C}oncurrent {C}onstraint {P}rogramming for {A}nalysing | ||

+ | {B}iological {S}ystems}, | ||

+ | BOOKTITLE = {Electronic Notes in Theoretical Computer Science}, | ||

+ | ABSTRACT = {In this paper we present our first approach to model and | ||

+ | verify biological systems using ntcc, a concurrent | ||

+ | constraint process calculus. We argue that the partial | ||

+ | information constructs in ntcc can provide a suitable | ||

+ | language for such systems. We also illustrate how ntcc | ||

+ | may provide a unified framework for the analysis of | ||

+ | biological systems, as they can be described, | ||

+ | simulated and verified using the elements available in | ||

+ | the calculus.}, | ||

+ | KEYWORDS = {Process Calculi, Verification of Biological Systems, Partial | ||

+ | Information, Concurrent Constraint Programming (CCP)}, | ||

+ | VOLUME = {171}, | ||

+ | NUMBER = {2}, | ||

+ | PAGES = {117--137}, | ||

+ | PDF = {/wiki/lib/exe/fetch.php?media=grupos:avispa:papers:gprv07.pdf}, | ||

+ | YEAR = 2007 | ||

+ | } | ||

+ | </pre> | ||

+ | </p> | ||

+ | |||

+ | <p><a name="AAG+07"></a><pre> | ||

+ | @ARTICLE{AAG+07, | ||

+ | AUTHOR = {Arbelaez, A. and Aristizabal, A. and Gutierrez, J. and Lopez, | ||

+ | H. and Perez, J. A. and Rueda, C. and Valencia, F. D.}, | ||

+ | TITLE = {Process {C}alculi to {A}nalyze {E}merging {A}pplications in | ||

+ | {C}oncurrency}, | ||

+ | JOURNAL = {Matematicas: Ensenanza Universitaria}, | ||

+ | ABSTRACT = {The notion of computation has significantly evolved in the | ||

+ | last ten years or so. Modern computing systems (e.g., | ||

+ | Internet) now exhibit infinite behavior, usually in | ||

+ | the context of decentralized networks where | ||

+ | interactions are inherently concurrent. The | ||

+ | ubiquitous presence of this new kind of systems has | ||

+ | led to the urgent need of counting with techniques for | ||

+ | designing them in a reliable way. Process calculi are | ||

+ | formal specification languages of concurrent systems | ||

+ | in which the notions of process and interaction | ||

+ | prevail. They are endowed with reasoning techniques | ||

+ | that allow to rigorously determine whether a system | ||

+ | exhibits some desirable properties. The generic nature | ||

+ | of process calculi has made possible their successful | ||

+ | application in very diverse areas. Based on recent | ||

+ | work by the authors, this paper illustrates the use of | ||

+ | process calculi in two emerging application areas: | ||

+ | biology and security protocols. Basic notions of | ||

+ | process calculi are introduced, real systems in the | ||

+ | two areas are modeled and their properties are verified.}, | ||

+ | KEYWORDS = {Computer Science, Concurrency Theory, Verification of | ||

+ | Concurrent Systems, Process Calculi.}, | ||

+ | PDF = {/wiki/lib/exe/fetch.php?media=grupos:avispa:papers:aag_07.pdf}, | ||

+ | YEAR = 2007 | ||

+ | } | ||

+ | </pre> | ||

+ | </p> | ||

+ | <p><a name="OR06"></a><pre> | ||

+ | @ARTICLE{OR06, | ||

+ | AUTHOR = {Olarte, C. and Rueda, C.}, | ||

+ | TITLE = {A Stochastic Concurrent Constraint Based Framework to Model | ||

+ | and Verify Biological Systems.}, | ||

+ | JOURNAL = {CLEI Electronic Journal}, | ||

+ | VOLUME = {9}, | ||

+ | NUMBER = {2}, | ||

+ | ABSTRACT = {Concurrent process calculi are powerful formalisms for | ||

+ | modelling concurrent systems. The mathematical style | ||

+ | underlying process calculi allow to both model and | ||

+ | verify properties of a system, thus providing a | ||

+ | concrete design methodology for complex systems. ntcc, | ||

+ | a constraints-based calculus for modeling temporal | ||

+ | non-deterministic and asynchronous behaviour of | ||

+ | processes has been proposed recently. Process | ||

+ | interactions in ntcc can be determined by partial | ||

+ | information (i.e. constraints) accumulated in a global | ||

+ | store. ntcc has also an associated temporal logic with | ||

+ | a proof system that can be conveniently used to | ||

+ | formally verify temporal properties of processes. We | ||

+ | are interested in using ntcc to model the activity of | ||

+ | genes in biological systems. In order to account for | ||

+ | issues such as the basal rate of reactions or binding | ||

+ | affinities of molecular components, we believe that | ||

+ | stochastic features must be added to the calculus. In | ||

+ | this paper we propose an extension of ntcc with | ||

+ | various stochastic constructs. We describe the syntax | ||

+ | and semantics of this extension together with the new | ||

+ | temporal logic and proof system associated with it. We | ||

+ | show the relevance of the added features by modelling | ||

+ | a non trivial biological system: the gene expression | ||

+ | mechanisms of the lambda virus. We argue that this | ||

+ | model is both more elaborate and compact than the | ||

+ | stochastic pi calculus model proposed recently for the | ||

+ | same system.}, | ||

+ | PDF = {/wiki/lib/exe/fetch.php?media=grupos:avispa:papers:or06.pdf}, | ||

+ | YEAR = 2006 | ||

+ | } | ||

+ | </pre> | ||

+ | </p> | ||

+ | <p><a name="AAD+06"></a><pre> | ||

+ | @INPROCEEDINGS{AAD+06, | ||

+ | AUTHOR = {Allombert, A. and Assayag, G. and Desainte-Catherine, | ||

+ | M. and Rueda, C.}, | ||

+ | TITLE = {Concurrent {C}onstraint {M}odels for {S}pecifying | ||

+ | {I}nteractive {S}cores}, | ||

+ | BOOKTITLE = {{T}hird {S}ound and {M}usic {C}omputing | ||

+ | {C}onference ({SMC}'06).}, | ||

+ | ABSTRACT = {We propose a formalism for the construction and | ||

+ | performance of musical pieces composed of temporal | ||

+ | structures involving discrete interactive events. The | ||

+ | occurrence in time of these structures and events is | ||

+ | partially defined according to constraints, such as | ||

+ | Allen temporal relations. We represent the temporal | ||

+ | structures using two constraint models. A constraints | ||

+ | propagation model is used for the score composition | ||

+ | stage, while a non deterministic temporal concurrent | ||

+ | constraint calculus (NTCC) is used for the performance | ||

+ | phase. The models are tested with examples of temporal | ||

+ | structures computed with the GECODE constraint system | ||

+ | library and run with a NTCC interpreter. }, | ||

+ | KEYWORDS = {Concurrent Constraint Programming, Formal Languages | ||

+ | for Computer Music, Interactive Scores}, | ||

+ | MONTH = {May}, | ||

+ | PDF = {/wiki/lib/exe/fetch.php?media=grupos:avispa:papers:aad+06.pdf}, | ||

+ | YEAR = 2006 | ||

+ | } | ||

+ | </pre> | ||

+ | </p> | ||

+ | <p><a name="OMR06"></a><pre> | ||

+ | @INPROCEEDINGS{OMR06, | ||

+ | AUTHOR = {Olarte, C. and Monfroy, E. and Rueda, C.}, | ||

+ | TITLE = {Exploring {P}rocess {C}alculi as a {M}echanism to | ||

+ | {D}efine {D}ynamic {E}numeration {S}trategies in | ||

+ | {C}onstraint {P}rogramming.}, | ||

+ | BOOKTITLE = {{CLEI} 2006 (32nd {L}atinamerican | ||

+ | {C}onference on {I}nformatics)}, | ||

+ | ABSTRACT = {Constraint programming (CP) has been extensively used | ||

+ | to solve a wide variety of problems. Its declarative | ||

+ | flavor makes possible to state conditions over | ||

+ | variables and the solver finds solutions by applying | ||

+ | generic and complete techniques. The process of | ||

+ | computing a solution in CP consists mainly in two | ||

+ | phases: propagation in which values that are not | ||

+ | consistent w.r.t. the constraints are eliminated, and | ||

+ | enumeration that chooses a variable and a value for | ||

+ | this variable to continue the search when no further | ||

+ | propagation is possible. Constraint based languages | ||

+ | offer a set of static enumeration strategies. The | ||

+ | strategy chosen may affect drastically the time | ||

+ | required to find a solution. In this paper we propose a | ||

+ | framework to model dynamic enumeration strategies using | ||

+ | a stochastic, non-deterministic timed concurrent | ||

+ | constraint calculus. Thanks to the reactivity of the | ||

+ | calculus, we are able to express strategies that | ||

+ | dynamically change according to results observed. | ||

+ | Additionally, the compositional approach of the | ||

+ | calculus enables us to integrate external knowledge to | ||

+ | adapt the strategy. }, | ||

+ | ISBN = {956-303-028-1}, | ||

+ | KEYWORDS = {sntcc (stochastic, non-deterministic, timed concurrent | ||

+ | constraint programming), Constraint programming, | ||

+ | Dynamic enumeration strategies}, | ||

+ | MONTH = {August}, | ||

+ | PDF = {/wiki/lib/exe/fetch.php?media=grupos:avispa:papers:omr06.pdf}, | ||

+ | YEAR = 2006 | ||

+ | } | ||

+ | </pre> | ||

+ | </p> | ||

+ | <p><a name="PSV+06"></a><pre> | ||

+ | @INPROCEEDINGS{PSV+06, | ||

+ | AUTHOR = {C. Palamidessi and V. A. Saraswat and F. D. Valencia | ||

+ | and B. Victor}, | ||

+ | TITLE = {On the Expressiveness of Linearity vs Persistence in | ||

+ | the Asychronous Pi-Calculus.}, | ||

+ | BOOKTITLE = {21th IEEE Symposium on Logic in Computer | ||

+ | Science (LICS 2006)}, | ||

+ | PAGES = {59-68}, | ||

+ | PUBLISHER = {IEEE Computer Society}, | ||

+ | ABSTRACT = {We present an expressiveness study of linearity and | ||

+ | persistence of processes. We choose the pi-calculus, | ||

+ | one of the main representatives of process calculi, as | ||

+ | a framework to conduct our study. We consider four | ||

+ | fragments of the pi-calculus. Each one singles out a | ||

+ | natural source of linearity/ persistence also present | ||

+ | in other frameworks such as Concurrent Constraint | ||

+ | |||

+ | Programming (CCP), Linear CCP, and several calculi for | ||

+ | security. The study is presented by providing (or | ||

+ | proving the non-existence of) encodings among the | ||

+ | fragments, a processes-as-formulae interpretation and a | ||

+ | reduction from Minsky machines.}, | ||

+ | KEYWORDS = {Persistence/Linearity in process calculi, asynchronous | ||

+ | pi-calculus, expresiveness of process calculi}, | ||

+ | PDF = {/wiki/lib/exe/fetch.php?media=grupos:avispa:papers:psv+06.pdf}, | ||

+ | YEAR = 2006 | ||

+ | } | ||

+ | </pre> | ||

+ | </p> | ||

+ | <p><a name="GPR+06"></a><pre> | ||

+ | @ARTICLE{GPR+06, | ||

+ | AUTHOR = {Gutierrez, J. and Perez, J. A. and Rueda, C. and | ||

+ | Valencia, F. D.}, | ||

+ | TITLE = {Timed {C}oncurrent {C}onstraint {P}rogramming for | ||

+ | {A}nalysing {B}iological {S}ystems.}, | ||

+ | JOURNAL = {To appear in the ENTCS (Electronic Notes in | ||

+ | Theoretical Computer Science) series}, | ||

+ | NOTE = {Presented in the Workshop on Membrane Computing and | ||

+ | Biologically Inspired Process Calculi (MeCBIC 06), part | ||

+ | of ICALP'06.}, | ||

+ | ABSTRACT = {In this paper we present our first approach to model | ||

+ | and verify biological systems using ntcc, a concurrent | ||

+ | constraint process calculus. We argue that the partial | ||

+ | information constructs in ntcc can provide a suitable | ||

+ | language for such systems. We also illustrate how ntcc | ||

+ | may provide a unified framework for the analysis of | ||

+ | biological systems, as they can be described, simulated | ||

+ | and verified using the elements provided by the | ||

+ | calculus. }, | ||

+ | KEYWORDS = {Process Calculi, Verification of Biological Systems, | ||

+ | Partial Information, Concurrent Constraint Programming | ||

+ | (CCP)}, | ||

+ | PDF = {/wiki/lib/exe/fetch.php?media=grupos:avispa:papers:gpr+06.pdf}, | ||

+ | YEAR = 2006 | ||

+ | } | ||

+ | </pre> | ||

+ | </p> | ||

+ | <p><a name="AG06"></a><pre> | ||

+ | @MISC{AG06, | ||

+ | AUTHOR = {Arbelaez, A. and Gutierrez, J. E.}, | ||

+ | TITLE = {Estudio {E}xploratorio de la {A}plicacion de la | ||

+ | {P}rogramacion {C}oncurrente por {R}estricciones en | ||

+ | {B}ioinformatica}, | ||

+ | HOWPUBLISHED = {BSc Thesis -- Engineering Degree in Computer Science, | ||

+ | Pontificia Universidad Javeriana - Cali (Colombia).}, | ||

+ | KEYWORDS = {Programacion Concurrente por Restricciones, Calculos | ||

+ | de Procesos, Biologia Sistemica, Mozart, ntcc, Redes de | ||

+ | Regulacion Genetica}, | ||

+ | PDF = {/wiki/lib/exe/fetch.php?media=grupos:avispa:papers:ag06.pdf}, | ||

+ | YEAR = 2006 | ||

+ | } | ||

+ | </pre> | ||

+ | </p> | ||

+ | <p><a name="AL06"></a><pre> | ||

+ | @MISC{AL06, | ||

+ | AUTHOR = {Aristizabal, A. A. and Lopez, H. A.}, | ||

+ | TITLE = {Using {P}rocess {C}alculi to {M}odel and {V}erify | ||

+ | {S}ecurity {P}roperties in {R}eal {C}ommunication | ||

+ | {P}rotocols.}, | ||

+ | HOWPUBLISHED = {BSc Thesis -- Engineering Degree in Computer Science, | ||

+ | Pontificia Universidad Javeriana - Cali (Colombia).}, | ||

+ | KEYWORDS = {Process Calculi, Verification of Security Protocols, | ||

+ | SPL (Secure Protocol Language)}, | ||

+ | PDF = {/wiki/lib/exe/fetch.php?media=grupos:avispa:papers:al06.pdf}, | ||

+ | YEAR = 2006 | ||

+ | } | ||

+ | </pre> | ||

+ | </p> | ||

+ | <p><a name="Rod06"></a><pre> | ||

+ | @MISC{Rod06, | ||

+ | AUTHOR = {Jessica Rodriguez}, | ||

+ | TITLE = {Dise\~{n}o e Implementaci\'{o}n de un Sistema de Restricciones | ||

+ | de Armon\'{\i}a Musical para Mozart}, | ||

+ | HOWPUBLISHED = {BSc Thesis -- Engineering Degree in Computer Science, | ||

+ | Universidad del Valle - Cali (Colombia).}, | ||

+ | PDF = {/wiki/lib/exe/fetch.php?media=grupos:avispa:papers:rod06.pdf}, | ||

+ | YEAR = 2006 | ||

+ | } | ||

+ | </pre> | ||

+ | </p> | ||

+ | <p><a name="Vil06"></a><pre> | ||

+ | @MISC{Vil06, | ||

+ | AUTHOR = {Ángela Villota Gómez}, | ||

+ | TITLE = {Dise\~{n}o e Implementaci\'{o}n de un Sistema de Restricciones | ||

+ | para Búsqueda de Patrones en Secuencias de ADN para Mozart}, | ||

+ | HOWPUBLISHED = {BSc Thesis -- Engineering Degree in Computer Science, | ||

+ | Universidad del Valle - Cali (Colombia).}, | ||

+ | PDF = {/wiki/lib/exe/fetch.php?media=grupos:avispa:papers:vil06.pdf}, | ||

+ | YEAR = 2006 | ||

+ | } | ||

+ | </pre> | ||

+ | </p> | ||

+ | <p><a name="ALR+06"></a><pre> | ||

+ | @INPROCEEDINGS{ALR+06, | ||

+ | AUTHOR = {A. Aristizabal and H. A. Lopez and C. Rueda and F. D. | ||

+ | Valencia}, | ||

+ | TITLE = {{Formally Reasoning About Security Issues in P2P | ||

+ | Protocols: A Case Study}}, | ||

+ | BOOKTITLE = {Third Taiwanese-French Conference on | ||

+ | Information Technology (TFIT)}, | ||

+ | EDITOR = {S. Cruz-Lara and Y.K. Tsay}, | ||

+ | ABSTRACT = {Peer-to-Peer (P2P) systems can be seen as highly | ||

+ | dynamic distributed systems designed for very specific | ||

+ | purposes, such as resources sharing in collaborative | ||

+ | settings. Because of their ubiquity, it is fundamental | ||

+ | to provide techniques for formally proving properties | ||

+ | of the communication protocols underlying those | ||

+ | systems. In this paper we present a formal | ||

+ | specification of MUTE, a protocol for P2P systems, | ||

+ | modelled in the SPL process calculus. Furthermore, we | ||

+ | use the SPL reasoning techniques to show how the | ||

+ | protocol enjoys a secrecy property against outsider | ||

+ | attacks. By formally modeling and analyzing a | ||

+ | real-world, yet informally specified protocol, we bear | ||

+ | witness to the applicability of SPL as a formalism to | ||

+ | specify security protocols as well as the flexibility | ||

+ | of its reasoning techniques. This paper represents our | ||

+ | first approach towards the use of process calculi, in | ||

+ | particular SPL, for the specification and reasoning of | ||

+ | P2P protocols. }, | ||

+ | KEYWORDS = {Verification of Security Protocols, SPL (Securiy | ||

+ | Protocol Language), Peer-to-Peer (P2P) Systems, Process | ||

+ | calculi}, | ||

+ | MONTH = {March}, | ||

+ | PDF = {/wiki/lib/exe/fetch.php?media=grupos:avispa:papers:alr+06.pdf}, | ||

+ | YEAR = 2006 | ||

+ | } | ||

+ | </pre> | ||

+ | </p> | ||

+ | <p><a name="LPP+06"></a><pre> | ||

+ | @INPROCEEDINGS{LPP+06, | ||

+ | AUTHOR = {H. A. Lopez and C. Palamidessi and J. A. Perez and C. | ||

+ | Rueda and F. D. Valencia}, | ||

+ | TITLE = {A {D}eclarative {F}ramework for {S}ecurity: {S}ecure | ||

+ | {C}oncurrent {C}onstraint {P}rogramming ({S}hort | ||

+ | {A}bstract).}, | ||

+ | BOOKTITLE = {22nd International Conference in Logic | ||

+ | Programming (ICLP 2006)}, | ||

+ | EDITOR = {Etalle, S. and Truszczynski, M.}, | ||

+ | VOLUME = {4079}, | ||

+ | SERIES = {Lecture Notes in Computer Science}, | ||

+ | PAGES = {449-450}, | ||

+ | PUBLISHER = {Springer}, | ||

+ | ABSTRACT = {Due to technological advances, Security has become a | ||

+ | serious challenge involving several disciplines of | ||

+ | Computer Science. In recent years, there has been a | ||

+ | growing interest in the analysis of security protocols | ||

+ | and one promising approach is the development of | ||

+ | formalisms that model communicating processes, in | ||

+ | particular Process Calculi. The results are so far | ||

+ | |||

+ | |||

+ | encouraging although most remains to be done. | ||

+ | Concurrent Constraint Programming (CCP) is a | ||

+ | well-established formalism which generalizes Logic | ||

+ | Programming. One of the most appealing and distinct | ||

+ | features of CCP is that it combines the traditional | ||

+ | operational view of processes calculi with a | ||

+ | declarative one of processes based upon logic. This | ||

+ | combination allows CCP to benefit from the large body | ||

+ | of techniques of both process calculi and logic. Our | ||

+ | project Secure CCP (SCCP) aims at advancing both the | ||

+ | theory and tools of CCP for analyzing and programming | ||

+ | security protocols. The main goal is to develop a | ||

+ | CCP-based framework for security protocols. }, | ||

+ | ISBN = {3-540-36635-0}, | ||

+ | KEYWORDS = {Process Calculi, Concurrent Constraint Programming | ||

+ | (CCP), Verification of Security Protocols}, | ||

+ | PDF = {/wiki/lib/exe/fetch.php?media=grupos:avispa:papers:lpp+06.pdf}, | ||

+ | YEAR = 2006 | ||

+ | } | ||

+ | </pre> | ||

+ | </p> | ||

+ | <p><a name="AGO+06"></a><pre> | ||

+ | @INPROCEEDINGS{AGO+06, | ||

+ | AUTHOR = {Arbelaez, A. and Gutierrez, J. and Olarte, C. and | ||

+ | Rueda, C.}, | ||

+ | TITLE = {A {G}eneric {F}ramework to {M}odel, {S}imulate and | ||

+ | {V}erify {G}enetic {R}egulatory {N}etworks ({P}oster)}, | ||

+ | BOOKTITLE = {{CLEI} 2006 (32nd {L}atinamerican | ||

+ | {C}onference on {I}nformatics)}, | ||

+ | ABSTRACT = {Process calculi are formalisms to model concurrent | ||

+ | systems. Their mathematical basis and compositional | ||

+ | style make possible to decompose a system into simple | ||

+ | and well dened processes. Interaction among them is | ||

+ | formally dened by the semantic of the calculi. These | ||

+ | characteristics allow to study systems coming from | ||

+ | dierent areas such as arts, engineering and sciences. | ||

+ | In this paper we propose a generic framework to model, | ||

+ | simulate and verify genetic regulatory networks based | ||

+ | on a non-deterministic timed concurrent constraint | ||

+ | calculus. This framework provides a set of process | ||

+ | denitions to model generic/parametric components in a | ||

+ | biological context, a simulator to observe the system | ||

+ | evolution in time and some insights to perform formal | ||

+ | proofs to verify and make inferences over the systems. | ||

+ | An instantiation of the framework is presented by | ||

+ | modeling the lactose operon.}, | ||

+ | ISBN = {956-303-028-1}, | ||

+ | KEYWORDS = {Process calculi, Concurrent Constraint Programming, | ||

+ | ntcc, Genetic Regulatory Networks, Lac Operon}, | ||

+ | PDF = {/wiki/lib/exe/fetch.php?media=grupos:avispa:papers:ago+06.pdf}, | ||

+ | YEAR = 2006 | ||

+ | } | ||

+ | </pre> | ||

+ | </p> | ||

+ | <p><a name="AGP06"></a><pre> | ||

+ | @MISC{AGP06, | ||

+ | AUTHOR = {A. Arbelaez, J. Gutierrez and J. A. Perez}, | ||

+ | TITLE = {{Timed CCP in Systems Biology}}, | ||

+ | HOWPUBLISHED = {The ALP Newsletter}, | ||

+ | ABSTRACT = {Systems biology aims at getting a higher-level | ||

+ | understanding of living matter, building on the | ||

+ | available data at the molecular level. In this field, | ||

+ | theories and methods from computer science have | ||

+ | proven very useful, mainly for system modeling and | ||

+ | |||

+ | simulation. Here we argue that languages based on | ||

+ | timed concurrent constraint programming (timed ccp) - | ||

+ | a well-established model for concurrency based on the | ||

+ | idea of partial information - have a place in systems | ||

+ | biology. We summarize some works in which our group | ||

+ | has tried to assess the possibilities/limitations of | ||

+ | one such formalisms in this domain. Our base language | ||

+ | is ntcc, a non-deterministic, timed ccp process | ||

+ | calculus that provides a unified framework for | ||

+ | modeling, simulating and verifying several kinds of | ||

+ | biological systems. We discuss how the interplay of | ||

+ | the operational and logic perspectives that ntcc | ||

+ | integrates greatly favors biological systems analysis.}, | ||

+ | VOLUME = {19}, | ||

+ | NUMBER = {4}, | ||

+ | INSTITUTION = { Association for Logic Programming (ALP)}, | ||

+ | MONTH = {Nov-Dic}, | ||

+ | PDF = {/wiki/lib/exe/fetch.php?media=grupos:avispa:papers:agp06.pdf}, | ||

+ | YEAR = 2006 | ||

+ | } | ||

+ | </pre> | ||

+ | </p> | ||

+ | <p><a name="Que06"></a><pre> | ||

+ | @PHDTHESIS{Que06, | ||

+ | AUTHOR = {Quesada, L. O.}, | ||

+ | TITLE = {Solving Constrained Graph Problems using Reachability | ||

+ | Constraints based on Transitive Closure and Dominators}, | ||

+ | SCHOOL = {Universit\'{e} Catholique de Louvain}, | ||

+ | NOTE = {PhD thesis. xiv+136}, | ||

+ | COMMENT = {Defence: November 10, 2006}, | ||

+ | INSTITUTION = {Universit\'{e} Catholique de Louvain}, | ||

+ | PDF = {/wiki/lib/exe/fetch.php?media=grupos:avispa:papers:que06.pdf}, | ||

+ | YEAR = 2006 | ||

+ | } | ||

+ | </pre> | ||

+ | </p> | ||

+ | <p><a name="ALR05"></a><pre> | ||

+ | @TECHREPORT{ALR05, | ||

+ | AUTHOR = {A. Aristizabal and H. A. Lopez and C. Rueda}, | ||

+ | TITLE = {Tiempo, {L}istas negras y {S}eguridad en {SPL}}, | ||

+ | INSTITUTION = {AVISPA Research Group, Pontificia Universidad | ||

+ | Javeriana}, | ||

+ | ABSTRACT = {Diversos avances concernientes a la seguridad dentro | ||

+ | de las comunicaciones han utilizado nociones que | ||

+ | permiten denotar tanto caducidad en los mensajes para | ||

+ | sortear de manera efectiva una amplia gama de ataques, | ||

+ | como el manejo del concepto de listas negras utilizadas | ||

+ | para ubicar aquellos agentes de reputacion dudosa con | ||

+ | los cuales no se debe establecer ningun contacto para | ||

+ | evitar contratiempos. Debido a la relevancia intrinseca | ||

+ | de la inclusion de esta clase de elementos frente a | ||

+ | temas de seguridad, se introduciran nociones de este | ||

+ | tipo dentro de un calculo de procesos de seguridad bien | ||

+ | establecido denominado SPL, sin realizar cambios | ||

+ | intrusivos dentro del lenguaje. De esta forma se | ||

+ | permitiria modelar nuevos protocolos de comunicacion | ||

+ | seguros, posibilitando el razonamiento de propiedades | ||

+ | de seguridad a traves de las tecnicas inherentes a SPL. | ||

+ | Por ultimo, se presentaran modelos especificados en | ||

+ | este lenguaje de dos conocidos protocolos que hagan uso | ||

+ | de las citadas nociones, de forma que se pueda | ||

+ | verificar la validez de la inclusion de estos nuevos | ||

+ | componentes.}, | ||

+ | KEYWORDS = {Process Calculi, SPL (Security Protocol Language), | ||

+ | Verification of Security Protocols, Peer-to-Peer (P2P) | ||

+ | Systems,}, | ||

+ | MONTH = {February}, | ||

+ | PDF = {/wiki/lib/exe/fetch.php?media=grupos:avispa:papers:alr05.pdf}, | ||

+ | YEAR = 2005 | ||

+ | } | ||

+ | </pre> | ||

+ | </p> | ||

+ | <p><a name="ALR+05"></a><pre> | ||

+ | @TECHREPORT{ALR+05, | ||

+ | AUTHOR = {A. Aristizabal and H. A. Lopez and C. Rueda and F. D. | ||

+ | Valencia}, | ||

+ | TITLE = {{Process Calculi for the Verification of Security | ||

+ | Properties of Communication Protocols for Peer-to-Peer | ||

+ | systems}}, | ||

+ | INSTITUTION = {AVISPA Research Group, Pontificia Universidad | ||

+ | Javeriana}, | ||

+ | ABSTRACT = {Recent advances in communication have made the use of | ||

+ | dynamic and reconfigurable network topologies a | ||

+ | mandatory requirement in scenarios where the | ||

+ | participants must actively collaborate to each other to | ||

+ | achieve a common, specific goal. A particular case of | ||

+ | those scenarios are the Peer-to-Peer (P2P) systems. The | ||

+ | wide applicability of P2P-based applications and its | ||

+ | pervasive presence in corporate applications are two | ||

+ | important factors that suggest a careful study of the | ||

+ | communication protocols underlying these systems. | ||

+ | Surprisingly, little effort has been invested in giving | ||

+ | formal foundations that support both protocols and its | ||

+ | security properties. This paper is intended to be a | ||

+ | step towards such a research strand, using a process | ||

+ | calculus as main resource to build such foundations. In | ||

+ | particular, we focus on the reconfiguration problem in | ||

+ | P2P-based applications. We propose two protocols for | ||

+ | modeling this problem: while the first one is inspired | ||

+ | on an existing protocol (known as the Friends | ||

+ | Troubleshooting Network or FTN), the second constitutes | ||

+ | an original proposal based on a multi-layered | ||

+ | encryption system. We show how SPL (the process calculi | ||

+ | in which both models are given) is well-suited to model | ||

+ | and to proof certain security properties of the | ||

+ | protocols.}, | ||

+ | KEYWORDS = {Process Calculi, SPL (Security Protocol Language), | ||

+ | Verification of Security Protocols, Peer-to-Peer (P2P) | ||

+ | Systems,}, | ||

+ | MONTH = {February}, | ||

+ | PDF = {/wiki/lib/exe/fetch.php?media=grupos:avispa:papers:alr+05.pdf}, | ||

+ | YEAR = 2005 | ||

+ | } | ||

+ | </pre> | ||

+ | </p> | ||

+ | <p><a name="DV05"></a><pre> | ||

+ | @INPROCEEDINGS{DV05, | ||

+ | AUTHOR = {Dantchev, S. S. and Valencia, F. D.}, | ||

+ | TITLE = {On the computational limits of infinite satisfaction.}, | ||

+ | BOOKTITLE = {Proceedings of the 2005 {ACM} {S}ymposium on {A}pplied | ||

+ | {C}omputing ({SAC})}, | ||

+ | PAGES = {393-397}, | ||

+ | ABSTRACT = {We study the computational limits of Constraint | ||

+ | Satisfaction Problems (CSP's) allowing infinitely, or | ||

+ | unboundedly, many indexed variables as in, e.g., xi > | ||

+ | xi+2 for each i = 1, 2,.... We refer to these CSP's as | ||

+ | Infinite CSP's (ICSP's). These problems arise in | ||

+ | contexts in which the number of variables is unknown a | ||

+ | priori as well as in optimization problems wrt the | ||

+ | number of variables satisfying a given finite set of | ||

+ | constraints.In particular, we investigate the | ||

+ | decidability of the satisfiability problem for ICSP's | ||

+ | wrt (a) the first-order theory specifying the indices | ||

+ | of variables and (b) the dimension of the indices. We | ||

+ | first show that (1) if the indices are one-dimensional | ||

+ | and specified in the theory of the natural numbers with | ||

+ | linear order (the theory of (N, 0, succ, <)) then the | ||

+ | satisfiability problem is decidable. We then prove | ||

+ | that, in contrast to (1), (2) if we move to the | ||

+ | two-dimensional case then the satisfiability problem is | ||

+ | undecidable for indices specified in (N, 0, succ, <) | ||

+ | and even in (N, 0, succ). Finally, we show that, in | ||

+ | contrast to (1) and (2), already in the one-dimensional | ||

+ | case (3) if we also allow addition, we get | ||

+ | undecidability. I.e., if the one-dimensional indices | ||

+ | are specified in Presburger arithmetic (i.e., the | ||

+ | theory of (N, 0, succ, <, +)) then satisfiability is | ||

+ | undecidable}, | ||

+ | PDF = {/wiki/lib/exe/fetch.php?media=grupos:avispa:papers:dv05.pdf}, | ||

+ | YEAR = 2005 | ||

+ | } | ||

+ | </pre> | ||

+ | </p> | ||

+ | <p><a name="GPR05"></a><pre> | ||

+ | @ARTICLE{GPR05, | ||

+ | AUTHOR = {Gutierrez, J. and Perez, J. A. and Rueda, C.}, | ||

+ | TITLE = {Modelamiento de {S}istemas {B}iologicos usando | ||

+ | {C}alculos de {P}rocesos {C}oncurrentes ({M}odelling | ||

+ | {B}iological {S}ystems using {P}rocess {C}alculi)}, | ||

+ | JOURNAL = {Epiciclos}, | ||

+ | VOLUME = {4}, | ||

+ | NUMBER = {1}, | ||

+ | PAGES = {79-101}, | ||

+ | ABSTRACT = {ENGLISH: Process calculi are formalisms that have been | ||

+ | proposed to model concurrent systems in a wide variety | ||

+ | of areas. Their mathematical foundations allow to | ||

+ | define abstractions between the components of real | ||

+ | systems and the constructions of a calculus. This is | ||

+ | particularly convenient when verifying essential | ||

+ | properties of the modelled systems. These features make | ||

+ | process calculi an interesting approach to describe and | ||

+ | verify biological systems. This article offers a survey | ||

+ | of the process calculi proposed in the biological | ||

+ | context. A particular class of calculi, those based on | ||

+ | the notion of constraint, is thoroughly described. | ||

+ | Those calculi provide, among other useful features, the | ||

+ | transparent inclusion of quantitative and partial | ||

+ | information into formal models. SPANISH: Los calculos | ||

+ | de procesos son formalismos propuestos para modelar | ||

+ | sistemas concurrentes en diversos ambitos. Su | ||

+ | fundamentacion matematica permite establecer | ||

+ | abstracciones entre los elementos reales de los | ||

+ | sistemas y los componentes basicos del calculo, lo que | ||

+ | facilita la verificacion de propiedades interesantes de | ||

+ | los sistemas modelados. Estas caracteristicas perfilan | ||

+ | a los calculos de procesos como una alternativa | ||

+ | interesante para especificar y verificar propiedades | ||

+ | esenciales de sistemas biologicos. Este articulo | ||

+ | presenta un analisis de los calculos de procesos mas | ||

+ | importantes propuestos recientemente en el contexto | ||

+ | biologico. Especial atencion es dada a los calculos | ||

+ | basados en restricciones, que permiten, entre otras | ||

+ | cosas, el manejo transparente de informacion parcial y | ||

+ | cuantitativa.}, | ||

+ | KEYWORDS = {Process Calculi, Concurrent Constraint Programming | ||

+ | (CCP), Molecular Biology.}, | ||

+ | PDF = {/wiki/lib/exe/fetch.php?media=grupos:avispa:papers:gpr05.pdf}, | ||

+ | YEAR = 2005 | ||

+ | } | ||

+ | </pre> | ||

+ | </p> | ||

+ | <p><a name="ALR05b"></a><pre> | ||

+ | @MISC{ALR05b, | ||

+ | AUTHOR = {A. Aristizabal and H. A. Lopez and C. Rueda}, | ||

+ | TITLE = {{Using a Declarative Process Language for P2P | ||

+ | Protocols}}, | ||

+ | HOWPUBLISHED = {ALP Newsletter}, | ||

+ | NOTE = {More info at url http://www.cs.kuleuven.ac.be/ | ||

+ | dtai/projects/ALP/newsletter/}, | ||

+ | ABSTRACT = { Peer-to-Peer (P2P) systems can be seen as highly | ||

+ | dynamic distributed systems designed for very specific | ||

+ | purposes, such as resources sharing in collaborative | ||

+ | settings. Because of their ubiquity, it is fundamental | ||

+ | to provide techniques for formally proving properties | ||

+ | of the communication protocols underlying those | ||

+ | systems. In this paper we present a formal model of | ||

+ | MUTE, a protocol for P2P systems, in the SPL; a | ||

+ | specification language with a striking resemblance to | ||

+ | Concurrent Constraint Programming. Furthermore, we use | ||

+ | the SPL reasoning techniques to show the protocol | ||

+ | enjoys a secrecy property againts outsider attacks. By | ||

+ | formally modeling and analyzing a popular (albeit never | ||

+ | specified) protocol, we bear witness to the | ||

+ | applicability of SPL as a formalism to model and reason | ||

+ | about security protocols as well as flexibility of the | ||

+ | its reasoning techniques. }, | ||

+ | KEYWORDS = {Process Calculi, SPL (Security Protocol Language), | ||

+ | Verification of Security Protocols, Peer-to-Peer (P2P) | ||

+ | Systems,}, | ||

+ | MONTH = {November}, | ||

+ | PDF = {/wiki/lib/exe/fetch.php?media=grupos:avispa:papers:alr05b.pdf}, | ||

+ | YEAR = 2005 | ||

+ | } | ||

+ | </pre> | ||

+ | </p> | ||

+ | <p><a name="RV05"></a><pre> | ||

+ | @INPROCEEDINGS{RV05, | ||

+ | AUTHOR = {Rueda, C. and Valencia, F. V.}, | ||

+ | TITLE = {A {T}emporal {C}oncurrent {C}onstraint {C}alculus as | ||

+ | an {A}udio {P}rocessing {F}ramework}, | ||

+ | BOOKTITLE = {{S}econd {S}ound and {M}usic {C}omputing | ||

+ | {C}onference ({SMC}'05).}, | ||

+ | ABSTRACT = {Audio processing systems involve complex interactions | ||

+ | of concurrent processes. These are usually implemented | ||

+ | using domain specific visual languages and tools more | ||

+ | concerned with providing practical solutions than with | ||

+ | giving formal meaning to the supplied audio unit | ||

+ | combinators. Concurrent constraint process calculi have | ||

+ | proved to be effective in modeling with precision a | ||

+ | wide variety of concurrent systems. We propose using | ||

+ | ntcc , a non deterministic temporal concurrent | ||

+ | constraint calculus, to model audio processing systems. | ||

+ | We show how the concurrent constraint nature of the | ||

+ | calculus greatly simplify specifying complex | ||

+ | synchronization patterns. We illustrate ntcc as audio | ||

+ | processing framework by modeling unit combinators and | ||

+ | using them ina an audio processing example.}, | ||

+ | KEYWORDS = {Process Calculi, Formal Languages for Computer Music, | ||

+ | Audio Processing}, | ||

+ | PDF = {/wiki/lib/exe/fetch.php?media=grupos:avispa:papers:rv05.pdf}, | ||

+ | YEAR = 2005 | ||

+ | } | ||

+ | </pre> | ||

+ | </p> | ||

+ | <p><a name="Val05"></a><pre> | ||

+ | @ARTICLE{Val05, | ||

+ | AUTHOR = {Valencia, F. D.}, | ||

+ | TITLE = {Decidability of infinite-state timed ccp processes and | ||

+ | first-order ltl.}, | ||

+ | JOURNAL = {Theor. Comput. Sci.}, | ||

+ | VOLUME = {330}, | ||

+ | NUMBER = {3}, | ||

+ | PAGES = {577-607}, | ||

+ | ABSTRACT = {The ntcc process calculus is a timed concurrent | ||

+ | constraint programming (ccp) model equipped with a | ||

+ | first-order linear-temporal logic (LTL) for expressing | ||

+ | process specifications. A typical behavioral | ||

+ | observation in ccp is the strongest postcondition (sp). | ||

+ | The ntcc sp denotes the set of all infinite output | ||

+ | sequences that a given process can exhibit. The | ||

+ | verification problem is then whether the sequences in | ||

+ | the sp of a given process satisfy a given ntcc LTL | ||

+ | formula. This paper presents new positive decidability | ||

+ | results for timed ccp as well as for LTL. In | ||

+ | particular, we shall prove that the following problems | ||

+ | are decidable: (1) the sp equivalence for the so-called | ||

+ | locally-independent ntcc fragment; unlike other | ||

+ | fragments for which similar results have been | ||

+ | published, this fragment can specify infinite-state | ||

+ | systems, (2) verification for locally-independent | ||

+ | processes and negation-free first-order formulae of the | ||

+ | ntcc LTL, (3) implication for such formulae, (4) | ||

+ | Satisfiability for a first-order fragment of Manna and | ||

+ | Pnueli's LTL. The purpose of the last result is to | ||

+ | illustrate the applicability of ccp to well-established | ||

+ | formalisms for concurrency. }, | ||

+ | KEYWORDS = {Process calculi; Timed concurrent constraint | ||

+ | programming; Infinite-state systems; Temporal logic; | ||

+ | First-order LTL; Decidability}, | ||

+ | PDF = {/wiki/lib/exe/fetch.php?media=grupos:avispa:papers:val05.pdf}, | ||

+ | YEAR = 2005 | ||

+ | } | ||

+ | </pre> | ||

+ | </p> | ||

+ | <p><a name="DPR05"></a><pre> | ||

+ | @INPROCEEDINGS{DPR05, | ||

+ | AUTHOR = {Delgado, A. and Perez, J. A. and Rueda, C.}, | ||

+ | TITLE = {Implementing an {A}bstraction {F}ramework for {S}oft | ||

+ | {C}onstraints.}, | ||

+ | BOOKTITLE = {Abstraction, {R}eformulation and {A}pproximation, | ||

+ | {P}roc. of the 6th {I}nternational {S}ymposium, {SARA} | ||

+ | 2005.}, | ||

+ | EDITOR = {Zucker, J. D. and Saitta, L.}, | ||

+ | VOLUME = {3607}, | ||

+ | SERIES = {Lecture Notes in Computer Science}, | ||

+ | PAGES = {60-75}, | ||

+ | PUBLISHER = {Springer}, | ||

+ | ABSTRACT = {Soft constraints are flexible schemes for modeling a | ||

+ | wide spectrum of problems. A model based on a hierarchy | ||

+ | of abstractions of soft constraint problems has been | ||

+ | proposed before. We describe an efficient | ||

+ | implementation of this scheme aimed at solving real | ||

+ | life problems. Our system is integrated into the Mozart | ||

+ | language in such a way that user control of the | ||

+ | abstraction mechanism is straightforward.We explain how | ||

+ | we adapted the theoretical results for our purposes and | ||

+ | describe the experiences in this adaptation. We give | ||

+ | comparative analysis of our system with respect to an | ||

+ | implementation using soft constraints without the | ||

+ | abstraction mechanism. Our tests show good performance | ||

+ | results for over-constrained problems in real settings. | ||

+ | }, | ||

+ | ISBN = {3-540-27872-9}, | ||

+ | KEYWORDS = {(Concurrent) Constraint Programming, Soft Constraints, | ||

+ | Semiring-Based Constraints, Mozart}, | ||

+ | PDF = {/wiki/lib/exe/fetch.php?media=grupos:avispa:papers:dpr05.pdf}, | ||

+ | YEAR = 2005 | ||

+ | } | ||

+ | </pre> | ||

+ | </p> | ||

+ | <p><a name="DP05"></a><pre> | ||

+ | @MISC{DP05, | ||

+ | AUTHOR = {Delgado, A. and Perez, J. A.}, | ||

+ | TITLE = {Analisis e {I}mplementacion de {M}ecanismos de | ||

+ | {R}estricciones {D}ebiles para {P}rogramacion | ||

+ | {C}oncurrente por {R}estricciones}, | ||

+ | HOWPUBLISHED = {BSc Thesis -- Engineering Degree in Computer Science, | ||

+ | Pontificia Universidad Javeriana - Cali (Colombia).}, | ||

+ | ABSTRACT = {ENGLISH: Several real-life problems can be modelled | ||

+ | and solved using Constraint Programming (CP). In CP | ||

+ | problems are intuitively described as a set of | ||

+ | mandatory conditions. This feature does not allow to | ||

+ | represent criteria such as preferences in a natural way | ||

+ | as well as affects the fidelity of models. This thesis | ||

+ | studies a model for Soft Constraints (SCs), or | ||

+ | constraints that may be violated and allow to represent | ||

+ | preferences in problems. We adapt a theoretical | ||

+ | framework for SCs to the context of concurrent | ||

+ | constraint programming, thus increasing its | ||

+ | applicability in real-life problems. Our approach is | ||

+ | implemented in the Mozart programming language; | ||

+ | analyses, comparisons as well as case studies are also | ||

+ | presented. Several peer-reviewed international | ||

+ | publications support our results. SPANISH: Diversos | ||

+ | problemas de la vida real pueden modelarse y | ||

+ | solucionarse utilizando programaci\'on por | ||

+ | restricciones. En este contexto, los problemas se | ||

+ | describen en terminos de condiciones obligatorias, lo | ||

+ | que no permite representar naturalmente criterios como | ||

+ | preferencias, y limita la fidelidad de los modelos. | ||

+ | Esta tesis estudia un modelo de Restricciones D\'ebiles | ||

+ | (RDs): restricciones que pueden violarse y permiten | ||

+ | representar preferencias. Un modelo te\'orico de RDs es | ||

+ | adaptado al contexto de la pro-gramaci\'on concurrente | ||

+ | por restricciones, ampliando asi su aplicabilidad en | ||

+ | problemas reales. Se presentan dos implementaciones en | ||

+ | el lenguaje Mozart, as\'{\i} como an\'alisis, | ||

+ | comparaciones y pruebas. Estos resultados son | ||

+ | respaldados por varias publicaciones internacionales | ||

+ | arbitradas.}, | ||

+ | KEYWORDS = {Satisfacci\'on de Restricciones, Problemas de | ||

+ | Satisfacci\'on de Restricciones (CSPs), Programaci\'on | ||

+ | Concurrente por Restricciones, Restricciones D\'ebiles, | ||

+ | Mozart}, | ||

+ | MONTH = {November}, | ||

+ | PDF = {/wiki/lib/exe/fetch.php?media=grupos:avispa:papers:dp05.pdf}, | ||

+ | YEAR = 2005 | ||

+ | } | ||

+ | </pre> | ||

+ | </p> | ||

+ | <p><a name="OR05"></a><pre> | ||

+ | @INPROCEEDINGS{OR05, | ||

+ | AUTHOR = {Olarte, C. and Rueda, C.}, | ||

+ | TITLE = {A {S}tochastic {N}on-deterministic {T}emporal | ||

+ | {C}oncurrent {C}onstraint {C}alculus.}, | ||

+ | BOOKTITLE = {{I}nternational {C}onference of the {C}hilean | ||

+ | {C}omputer {S}cience {S}ociety ({SCCC} 2005)}, | ||

+ | PUBLISHER = {IEEE-CS}, | ||

+ | ABSTRACT = {We propose sntcc , a stochastic extension of the ntcc | ||

+ | calculus, a model of temporal concurrent constraint | ||

+ | programming with the capability of modeling | ||

+ | asynchronous and non-deterministic timed behavior. We | ||

+ | argue that such an extension is needed to faithfully | ||

+ | model concurrent systems in real-life situations. We | ||

+ | provide a suitable temporal logic and proof system for | ||

+ | sntcc and illustrate how to use them for proving | ||

+ | properties of stochastic systems. We argue that this | ||

+ | modeling strategy of using explicit stochastic | ||

+ | constructs within the calculus provides a runnable | ||

+ | specication for a wide variety of stochastic systems | ||

+ | that eases the task of formally reasoning about them. | ||

+ | We give examples of specications in sntcc and use the | ||

+ | extended linear temporal logic for proving properties | ||

+ | about them.}, | ||

+ | ISBN = {1522-4902}, | ||

+ | KEYWORDS = {Process calculi, sntcc (stochastic, non-deterministic, | ||

+ | timed concurrent constraint programming), constraint | ||

+ | programming}, | ||

+ | PDF = {/wiki/lib/exe/fetch.php?media=grupos:avispa:papers:or05.pdf}, | ||

+ | YEAR = 2005 | ||

+ | } | ||

+ | </pre> | ||

+ | </p> | ||

+ | <p><a name="OR05b"></a><pre> | ||

+ | @INPROCEEDINGS{OR05b, | ||

+ | AUTHOR = {Olarte, C. and Rueda, C.}, | ||

+ | TITLE = {Using {S}tochastic {NTCC} to {M}odel {B}iological | ||

+ | {S}ystems}, | ||

+ | BOOKTITLE = {{CLEI} 2005 (31st {L}atinamerican | ||

+ | {C}onference on {I}nformatics)}, | ||

+ | ABSTRACT = {Concurrent process calculi are powerful formalisms for | ||

+ | modeling concurrent systems. The mathematical style | ||

+ | underlying process calculi allow to both model and | ||

+ | verify properties of a system, thus providing a | ||

+ | concrete design methodology for complex systems. ntcc , | ||

+ | a constraints-based calculus for modeling temporal | ||

+ | nondeterministic and asynchronous behavior of processes | ||

+ | has been proposed recently. Process interactions in | ||

+ | ntcc can be determined by partial information (i.e. | ||

+ | constraints) accumulated in a global store. ntcc has | ||

+ | also an associated temporal logic with a proof system | ||

+ | that can be conveniently used to formally verify | ||

+ | temporal properties of processes. We are interested in | ||

+ | using ntcc to model the activity of genes in biological | ||

+ | systems. In order to account for issues such as the | ||

+ | basal rate of reactions or binding anities of | ||

+ | molecular components, we believe that stochastic | ||

+ | features must be added to the calculus. In this paper | ||

+ | we propose an extension of ntcc with various stochastic | ||

+ | constructs. We describe the syntax and semantics of | ||

+ | this extension together with the new temporal logic and | ||

+ | proof system associated with it. We show the relevance | ||

+ | of the added features by modeling a non trivial | ||

+ | biological system: the gene expression mechanisms of | ||

+ | the virus. We argue that this model is both more | ||

+ | elaborate and compact than the stochastic calculus | ||

+ | model proposed recently for the same system.}, | ||

+ | ISBN = {958-670-426-2}, | ||

+ | KEYWORDS = {NTCC, Lambda-Switch, biological systems, concurrent | ||

+ | process calculus, concurrent constraint programming}, | ||

+ | PDF = {/wiki/lib/exe/fetch.php?media=grupos:avispa:papers:or05b.pdf}, | ||

+ | YEAR = 2005 | ||

+ | } | ||

+ | </pre> | ||

+ | </p> | ||

+ | <p><a name="DOP+05"></a><pre> | ||

+ | @INPROCEEDINGS{DOP+05, | ||

+ | AUTHOR = {Delgado, A. and Olarte, C. and Perez, J. A. and Rueda, | ||

+ | C.}, | ||

+ | TITLE = {Semiring-based {F}uzzy {C}onstraints in {C}oncurrent | ||

+ | {C}onstraint {P}rogramming}, | ||

+ | BOOKTITLE = {{CLEI} 2005 (31st {L}atinamerican | ||

+ | {C}onference on {I}nformatics)}, | ||

+ | EDITOR = {Buss, A. and Diaz, J. F. and Rueda, C.}, | ||

+ | ABSTRACT = {Several real-life problems have been successfully | ||

+ | modeled and solved by using constraint programming | ||

+ | (CP). Nevertheless, existing classical (hard) | ||

+ | constraints can not express preferences, priorities or | ||

+ | other soft criteria in a natural way. Since these | ||

+ | criteria often occur in many scenarios, nding | ||

+ | techniques and tools for appropriately including them | ||

+ | in constraint programs is crucial. This paper describes | ||

+ | an implementation of a soft constraints module for | ||

+ | Mozart, a concurrent constraint programming language. | ||

+ | The module, based on the semiring formalism for soft | ||

+ | constraints, provides an intuitive set of constraints | ||

+ | for solving fuzzy constraint satisfaction problems and | ||

+ | is fully orthogonal to Mozart's implementation. We | ||

+ | modify the concept of constraint proposed in the | ||

+ | semiring formalism in order to dene a more intuitive | ||

+ | notion. The new concept provides straightforward user | ||

+ | control and is suitable for ecient implementation. We | ||

+ | present a set of intuitive examples showing the | ||

+ | advantages of our module in dierent contexts. Some | ||

+ | issues regarding the integration of soft constraints in | ||

+ | existing applications are also discussed.}, | ||

+ | ISBN = {958-670-426-2}, | ||

+ | KEYWORDS = {Programming Languages, Constraint Solving, Soft | ||

+ | Constraints, Mozart}, | ||

+ | MONTH = {October}, | ||

+ | PDF = {/wiki/lib/exe/fetch.php?media=grupos:avispa:papers:dop+05.pdf}, | ||

+ | YEAR = 2005 | ||

+ | } | ||

+ | </pre> | ||

+ | </p> | ||

+ | <p><a name="DOP+04"></a><pre> | ||

+ | @INPROCEEDINGS{DOP+04, | ||

+ | AUTHOR = {Delgado, A. and Olarte, C. A. and Perez, J. A. and | ||

+ | Rueda, C.}, | ||

+ | TITLE = {Implementing {S}emiring-{B}ased {C}onstraints {U}sing | ||

+ | {M}ozart.}, | ||

+ | BOOKTITLE = {Multiparadigm {P}rogramming in {M}ozart/{O}z, {S}econd | ||

+ | {I}nternational {C}onference, {MOZ} 2004, {R}evised | ||

+ | {S}elected and {I}nvited {P}apers}, | ||

+ | EDITOR = {Van Roy, P.}, | ||

+ | NUMBER = {3389}, | ||

+ | SERIES = {Lecture Notes in Computer Science}, | ||

+ | PAGES = {224-236}, | ||

+ | PUBLISHER = {Springer}, | ||

+ | ABSTRACT = {Although Constraint Programming (CP) is considered a | ||

+ | useful tool for tackling combinatorial problems, its | ||

+ | lack of flexibility when dealing with uncertainties and | ||

+ | preferences is still a matter for research. Several | ||

+ | formal frameworks for soft constraints have been | ||

+ | proposed within the CP community: all of them seem to | ||

+ | be theoretically solid, but few practical | ||

+ | implementations exist. In this paper we present an | ||

+ | implementation for Mozart of one of these frameworks, | ||

+ | which is based on a semiring structure. We explain how | ||

+ | the soft constraints constructs were adapted to the | ||

+ | propagation process that Mozart performs, and show how | ||

+ | they can be transparently integrated with current | ||

+ | Mozart hard propagators. Additionally, we show how | ||

+ | over-constrained problems can be successfully relaxed | ||

+ | |||

+ | and solved, and how preferences can be added to a | ||

+ | problem, while keeping the formal model as a direct | ||

+ | reference.}, | ||

+ | ISBN = {3-540-25079-4}, | ||

+ | KEYWORDS = {(Concurrent) Constraint Programming, Soft Constraints, | ||

+ | Semiring-Based Constraints, Mozart}, | ||

+ | PDF = {/wiki/lib/exe/fetch.php?media=grupos:avispa:papers:dop+04.pdf}, | ||

+ | YEAR = 2004 | ||

+ | } | ||

+ | </pre> | ||

+ | </p> | ||

+ | <p><a name="DGO+04b"></a><pre> | ||

+ | @INPROCEEDINGS{DGO+04b, | ||

+ | AUTHOR = {Diaz, J. F. and Gutierrez, G. and Olarte, C. A. and | ||

+ | Rueda, C.}, | ||

+ | TITLE = {Using {C}onstraint {P}rogramming for {R}econfiguration | ||

+ | of {E}lectrical {P}ower {D}istribution {N}etworks.}, | ||

+ | BOOKTITLE = {Multiparadigm {P}rogramming in {M}ozart/{O}z, {S}econd | ||

+ | {I}nternational {C}onference, {MOZ} 2004, {R}evised | ||

+ | {S}elected and {I}nvited {P}apers}, | ||

+ | EDITOR = {Van Roy, P.}, | ||

+ | NUMBER = {3389}, | ||

+ | SERIES = {Lecture Notes in Computer Science}, | ||

+ | PAGES = {263-276}, | ||

+ | PUBLISHER = {Springer}, | ||

+ | ABSTRACT = {The problem of reconfiguring power distribution system | ||

+ | to reduce power losses has been extensively studied | ||

+ | because of its significant economic impact. A variety | ||

+ | of approximation computational models have recently | ||

+ | been proposed. We describe a constraint programming | ||

+ | model for this problem, using the MOzArt system. To | ||

+ | handle real world reconfiguration systems we | ||

+ | implemented and integrated into MOzArt an efficient | ||

+ | constraint propagation system for the real numbers. We | ||

+ | show how the CP approach leads to a simpler model and | ||

+ | allows more flexible control of reconfiguration | ||

+ | parameters. We analyze the performance of our system in | ||

+ | canonical distribution networks of up to 60 nodes. We | ||

+ | describe how the adaptability of the MOzArt search | ||

+ | engine allows defining effective strategies for | ||

+ | tackling a real distribution system reconfiguration of | ||

+ | |||

+ | |||

+ | |||

+ | around 600 nodes.}, | ||

+ | ISBN = {3-540-25079-4}, | ||

+ | KEYWORDS = {(Concurrent) Constraint Programming, Constraint | ||

+ | Satisfaction Problem (CSP), Network reconfiguration, | ||

+ | Power losses reduction.}, | ||

+ | PDF = {/wiki/lib/exe/fetch.php?media=grupos:avispa:papers:dgo+04b.pdf}, | ||

+ | YEAR = 2004 | ||

+ | } | ||

+ | </pre> | ||

+ | </p> | ||

+ | <p><a name="RV04b"></a><pre> | ||

+ | @INPROCEEDINGS{RV04b, | ||

+ | AUTHOR = {C. Rueda and F. D. Valencia}, | ||

+ | TITLE = {Non-viability Deductions in Arc-Consistency | ||

+ | Computation.}, | ||

+ | BOOKTITLE = {International Conference on Logic | ||

+ | Programming (ICLP 2004)}, | ||

+ | VOLUME = {3132}, | ||

+ | SERIES = {Lecture Notes in Computer Science}, | ||

+ | PAGES = {343-355}, | ||

+ | PUBLISHER = {Springer}, | ||

+ | ABSTRACT = {Arc-Consistency (AC) techniques have been used | ||

+ | extensively in the study of Constraint Satisfaction | ||

+ | Problems (CSP). These techniques are used to simplify | ||

+ | the CSP before or during the search for its solutions. | ||

+ | Some of the most efficient algorithms for AC | ||

+ | computation are AC6++ and AC-7. The novelty of these | ||

+ | algorithms is that they satisfy the so-called four | ||

+ | desirable properties for AC computation. The main | ||

+ | purpose of these interesting properties is to reduce as | ||

+ | far as possible the number of constraint checks during | ||

+ | AC computation while keeping a reasonable space | ||

+ | complexity. In this paper we prove that, despite | ||

+ | providing a remarkable reduction in the number of | ||

+ | constraint checks, the four desirable properties do not | ||

+ | guarantee a minimal number of constraint checks. We | ||

+ | therefore refute the minimality claim in the paper | ||

+ | introducing these properties. Furthermore, we propose a | ||

+ | new desirable property for AC computation and extend | ||

+ | AC6++ and AC-7 to consider such a property. We show | ||

+ | theoretically and experimentally that the new property | ||

+ | provides a further substantial reduction in the number | ||

+ | of constraint checks.}, | ||

+ | KEYWORDS = {Constraint Programming, Constraint Satisfaction | ||

+ | Problems (CSPs), Arc Consistency,}, | ||

+ | PDF = {/wiki/lib/exe/fetch.php?media=grupos:avispa:papers:rv04b.pdf}, | ||

+ | YEAR = 2004 | ||

+ | } | ||

+ | </pre> | ||

+ | </p> | ||

+ | <p><a name="DCL+04"></a><pre> | ||

+ | @INPROCEEDINGS{DCL+04, | ||

+ | AUTHOR = {Diaz, J. F. and Caicedo, G. and Lozano, C. and | ||

+ | Gutierrez, G. and Olarte, C. and Rueda, C.}, | ||

+ | TITLE = {Loss {R}eduction in {D}istribution {N}etworks using | ||

+ | {C}oncurrent {C}onstraint {P}rogramming}, | ||

+ | BOOKTITLE = {8th {I}nternational {C}onference on | ||

+ | {P}robability {M}ethods {A}pplied to {P}ower {S}ystems | ||

+ | ({PMAPS}'04)}, | ||

+ | PAGES = {295- 300}, | ||

+ | PUBLISHER = {IEEE}, | ||

+ | ABSTRACT = {This paper presents a new technical losses reduction | ||

+ | model in an electrical energy distribution system by | ||

+ | using network reconfiguration technique. First-order | ||

+ | logic is used as the model specification language. This | ||

+ | specification is easily translated into programmable | ||

+ | sentences in the CCP (Concurrent Constraint | ||

+ | Programming) paradigm. Unlike other existing methods in | ||

+ | the literature, this model includes both the system | ||

+ | operating constraints and the electric laws related to | ||

+ | load flow. The CCP paradigm takes advantage of the | ||

+ | interaction between these two types of constraints to | ||

+ | reduce significantly the search tree, in contrast with | ||

+ | the iterative methods used traditionally. In turn, | ||

+ | itdoes not require the constraints verification once | ||

+ | the solution is found. The tool developed has been | ||

+ | tested forsimulating small cases up to 50 nodes, | ||

+ | obtaining good accuracy and running times. The power | ||

+ | flow results were validated against NEPLAN results and | ||

+ | the reconfiguration results were compared to those | ||

+ | obtained with three different tools developed by other | ||

+ | authors.}, | ||

+ | ISBN = {0-9761319-1-9}, | ||

+ | KEYWORDS = {Concurrent Constraint Programming, Constraint | ||

+ | Satisfaction Problem (CSP), Network reconfiguration, | ||

+ | Power losses reduction}, | ||

+ | PDF = {/wiki/lib/exe/fetch.php?media=grupos:avispa:papers:dcl+04.pdf}, | ||

+ | YEAR = 2004 | ||

+ | } | ||

+ | </pre> | ||

+ | |||

+ | |||

+ | </p> | ||

+ | <p><a name="ADO04"></a><pre> | ||

+ | @INPROCEEDINGS{ADO04, | ||

+ | AUTHOR = {Aranda, J. and Diaz, J. F. and Ortiz, J.}, | ||

+ | TITLE = {The {P}roblem of {A}ssigning {E}valuators to the | ||

+ | {A}rticles {S}ubmitted in an {A}cademic {E}vent: {A} | ||

+ | {P}ractical {S}olution {I}ncorporating {C}onstraint | ||

+ | {P}rogramming and {H}euristics}, | ||

+ | BOOKTITLE = {Multiparadigm {P}rogramming in {M}ozart/{O}z, {S}econd | ||

+ | {I}nternational {C}onference, {MOZ} 2004, {R}evised | ||

+ | {S}elected and {I}nvited {P}apers}, | ||

+ | EDITOR = {Van Roy, P.}, | ||

+ | NUMBER = {3389}, | ||

+ | SERIES = {Lecture Notes in Computer Science}, | ||

+ | PAGES = {305-316}, | ||

+ | PUBLISHER = {Springer}, | ||

+ | ABSTRACT = {This article shows a practical solution to The Problem | ||

+ | of Assigning Evaluators to the Articles Submitted in an | ||

+ | Academic Event, a problem of combinatorial | ||

+ | optimization. Apart from stating the problem formally | ||

+ | and proposing a constraint model, the article describes | ||

+ | the heuristics designed to find solutions. The | ||

+ | application was developed using Mozart; different | ||

+ | distribution strategies were implemented based on the | ||

+ | already mentioned heuristics. The experimental partial | ||

+ | results turned out to be competitive for real problems | ||

+ | (180 articles, 25 evaluators).}, | ||

+ | ISBN = {3-540-25079-4}, | ||

+ | KEYWORDS = {(Concurrent) Constraint Programming, Constraint | ||

+ | Satisfaction Problem (CSP)}, | ||

+ | PDF = {/wiki/lib/exe/fetch.php?media=grupos:avispa:papers:ado04.pdf}, | ||

+ | YEAR = 2004 | ||

+ | } | ||

+ | </pre> | ||

+ | </p> | ||

+ | <p><a name="MH04"></a><pre> | ||

+ | @INPROCEEDINGS{MH04, | ||

+ | AUTHOR = {Mu\~noz, M. P. and Hurtado, A. R.}, | ||

+ | TITLE = {Programming {R}obotic {D}evices with a {T}imed | ||

+ | {C}oncurrent {C}onstraint {L}anguage ({S}hort | ||

+ | {A}bstract)}, | ||

+ | BOOKTITLE = {{T}enth {I}nternational {C}onference on | ||

+ | {P}rinciples and {P}ractice of {C}onstraint | ||

+ | {P}rogramming ({CP} 2004)}, | ||

+ | EDITOR = {Wallace, M.}, | ||

+ | VOLUME = {3258}, | ||

+ | SERIES = {Lecture Notes in Computer Science}, | ||

+ | PAGES = {803}, | ||

+ | ABSTRACT = {This work shows the implementation of ntcc-lman, a | ||

+ | framework for ntcc, a non deterministic timed | ||

+ | concurrent constraint process calculus. This calculus | ||

+ | provides a formal model in which concepts proper to | ||

+ | robotic control can be conveniently represented. The | ||

+ | ntcc-lman framework includes a ntcc based kernel | ||

+ | language, a compiler, a constraint system, a formal | ||

+ | abstract machine based on ntcc reduction rules and a | ||

+ | virtual machine. We show how the framework can be used | ||

+ | to program typical robotic tasks to control LEGO robots | ||

+ | in real time using timed ccp technology. To our | ||

+ | knowledge, this is the rst timed ccp framework for | ||

+ | programming robotic devices.}, | ||

+ | KEYWORDS = {Process Calculi, Abstract and Virtual Machines, ntcc, | ||

+ | LEGO Robots, Constraint Programming}, | ||

+ | PAGE = {803}, | ||

+ | PDF = {/wiki/lib/exe/fetch.php?media=grupos:avispa:papers:mh04.pdf}, | ||

+ | YEAR = 2004 | ||

+ | } | ||

+ | </pre> | ||

+ | </p> | ||

+ | <p><a name="DGO+04"></a><pre> | ||

+ | @INPROCEEDINGS{DGO+04, | ||

+ | AUTHOR = {Diaz, J. F. and Gutierrez, G. and Olarte, C. A. and | ||

+ | Rueda, C.}, | ||

+ | TITLE = {C{RE}2: a {CP} application for reconfiguring a power | ||

+ | distribution network for power losses reduction | ||

+ | ({S}hort {A}bstract)}, | ||

+ | BOOKTITLE = {{T}enth {I}nternational {C}onference on | ||

+ | {P}rinciples and {P}ractice of {C}onstraint | ||

+ | {P}rogramming ({CP} 2004)}, | ||

+ | EDITOR = {Wallace, M.}, | ||

+ | VOLUME = {3258}, | ||

+ | SERIES = {Lecture Notes in Computer Science}, | ||

+ | PAGES = {813-814}, | ||

+ | PUBLISHER = {Springer}, | ||

+ | KEYWORDS = {Concurrent Constraint Programming, Constraint | ||

+ | Satisfaction Problem (CSP), Network reconfiguration, | ||

+ | Power losses reduction}, | ||

+ | PDF = {/wiki/lib/exe/fetch.php?media=grupos:avispa:papers:dgo+04.pdf}, | ||

+ | YEAR = 2004 | ||

+ | } | ||

+ | </pre> | ||

+ | </p> | ||

+ | <p><a name="RV04"></a><pre> | ||

+ | @ARTICLE{RV04, | ||

+ | AUTHOR = {Rueda, C. and Valencia, F. D.}, | ||

+ | TITLE = {On validity in modelization of musical problems by | ||

+ | CCP.}, | ||

+ | JOURNAL = {Soft Comput.}, | ||

+ | VOLUME = {8}, | ||

+ | NUMBER = {9}, | ||

+ | PAGES = {641-648}, | ||

+ | ABSTRACT = {We show how the ntcc calculus, a model of temporal | ||

+ | concurrent constraint programming with the capability | ||

+ | of modeling asynchronous and non-deterministic timed | ||

+ | behavior, can be used for modeling real musical | ||

+ | processes. In particular, we show how the | ||

+ | expressiveness of ntcc allows to implement complex | ||

+ | interactions among musical processes handling different | ||

+ | kinds of partial information. The ntcc calculus | ||

+ | integrates two dimensions of soft computing: a | ||

+ | horizontal dimension dealing with partial information | ||

+ | and a vertical one in which non determinism comes into | ||

+ | play. This integration is an improvement over | ||

+ | constraint satisfaction and concurrent constraint | ||

+ | programming models, allowing a more natural | ||

+ | representation of a variety of musical processes. We | ||

+ | use the nondeterminism facility of ntcc to build weaker | ||

+ | representations of musical processes that greatly | ||

+ | simplifies the formal expression and analysis of its | ||

+ | properties. We argue that this modeling strategy | ||

+ | provides a runnable specification for music problems | ||

+ | that eases the task of formally reasoning about them. | ||

+ | We show how the linear temporal logic associated with | ||

+ | ntcc gives a very expressive setting for formally | ||

+ | proving the existence of interesting musical properties | ||

+ | of a process. We give examples of musical | ||

+ | specifications in ntcc and use the linear temporal | ||

+ | logic for proving properties of a realistic musical | ||

+ | problem. }, | ||

+ | KEYWORDS = {Concurrent Constraint Programming, Formal Languages | ||

+ | |||

+ | for Computer Music}, | ||

+ | PDF = {/wiki/lib/exe/fetch.php?media=grupos:avispa:papers:rv04.pdf}, | ||

+ | YEAR = 2004 | ||

+ | } | ||

+ | </pre> | ||

+ | </p> | ||

+ | <p><a name="DOP+04b"></a><pre> | ||

+ | @INPROCEEDINGS{DOP+04b, | ||

+ | AUTHOR = {Delgado, A. and Olarte, C. A. and Perez, J. A. and | ||

+ | Rueda, C.}, | ||

+ | TITLE = {Implementing {S}emiring-{B}ased {C}onstraints using a | ||

+ | {C}oncurrent {C}onstraint {P}rogramming {L}anguage.}, | ||

+ | BOOKTITLE = {{S}ixth {I}nternational {W}orkshop on | ||

+ | {P}references and {S}oft {C}onstraints. {P}art of {CP} | ||

+ | 2004.}, | ||

+ | EDITOR = {Bistarelli, S. and Rossi, F.}, | ||

+ | ABSTRACT = {Several real life problems have been successfully | ||

+ | modeled and solved by using concurrent constraint | ||

+ | programming (CCP). Nevertheless, CCP can not express | ||

+ | preferences, costs, priorities or other soft features | ||

+ | in a straight way. The semiring based formalism | ||

+ | proposed by Bistarelli et al. intends to generalize the | ||

+ | softness concepts in constraint programming by means of | ||

+ | a framework that can be cast in several others. | ||

+ | However, few practical implementations have been | ||

+ | published. This paper describes two implementations of | ||

+ | a c-semiring based constraint system in the CCP-based | ||

+ | language Mozart, following two strategies: a tuple | ||

+ | evaluation approach and a propagator oriented | ||

+ | implementation. We found that the latter enables us to | ||

+ | smoothly integrate both hard and soft constraints while | ||

+ | obtaining better performance.}, | ||

+ | KEYWORDS = {(Concurrent) Constraint Programming, Soft Constraints, | ||

+ | Semiring-Based Constraints, Mozart}, | ||

+ | MONTH = {September}, | ||

+ | PDF = {/wiki/lib/exe/fetch.php?media=grupos:avispa:papers:dop+04b.pdf}, | ||

+ | YEAR = 2004 | ||

+ | } | ||

+ | </pre> | ||

+ | </p> | ||

+ | <p><a name="HM04"></a><pre> | ||

+ | @MISC{HM04, | ||

+ | AUTHOR = {Hurtado, A. R. and Mu\~noz, M. P.}, | ||

+ | TITLE = {L{MAN}: {M}\'aquina {A}bstracta del {C}\'alculo {NTCC} | ||

+ | para {P}rogramaci\'on {C}oncurrente de {R}obots {LEGO}}, | ||

+ | HOWPUBLISHED = {BSc Thesis -- Engineering Degree in Computer Science, | ||

+ | Pontificia Universidad Javeriana - Cali (Colombia).}, | ||

+ | ABSTRACT = {Este proyecto de grado describe LMAN, m\'aquina | ||

+ | abstracta del c\'alculo NTCC para programaci\'on | ||

+ | concurrente de robots LEGO. LMAN incluye tanto la | ||

+ | especificaci\'on de la m\'aquina abstracta, como la | ||

+ | implementaci\'on de la m\'aquina virtual, que act\'ua | ||

+ | como el ejecutor notacional del c\'alculo NTCC. El | ||

+ | modelo formal presentado en forma de m\'aquina | ||

+ | abstracta, provee la especificaci\'on de la m\'aquina | ||

+ | virtual. La m\'aquina virtual est\'a compuesta de un | ||

+ | conjunto de instrucciones, registros y de un modelo de | ||

+ | memoria; que actuando junto con un protocolo de | ||

+ | comunicaciones, permiten controlar y ejecutar de manera | ||

+ | eficiente y en tiempo real programas escritos en NTCC | ||

+ | sobre los robots LEGO MindStorm.}, | ||

+ | KEYWORDS = {C\'alculo de Procesos, M\'aquina Abstracta, M\'aquina | ||

+ | Virtual, Robots LEGO, Concurrencia, Restricciones, | ||

+ | LMAN.}, | ||

+ | PDF = {/wiki/lib/exe/fetch.php?media=grupos:avispa:papers:hm04.pdf}, | ||

+ | YEAR = 2004 | ||

+ | } | ||

+ | </pre> | ||

+ | </p> | ||

+ | <p><a name="DPP+04"></a><pre> | ||

+ | @INPROCEEDINGS{DPP+04, | ||

+ | AUTHOR = {Delgado, A. and Perez, J. A. and Pabon, G. and Jordan, | ||

+ | R. and Diaz, J. F. and Rueda, C.}, | ||

+ | TITLE = {An {I}nteractive {T}ool for the {C}ontrolled | ||

+ | {E}xecution of an {A}utomated {T}imetabling | ||

+ | {C}onstraint {E}ngine.}, | ||

+ | BOOKTITLE = {Multiparadigm {P}rogramming in {M}ozart/{O}z, {S}econd | ||

+ | {I}nternational {C}onference, {MOZ} 2004, {R}evised | ||

+ | {S}elected and {I}nvited {P}apers}, | ||

+ | EDITOR = {Van Roy, P.}, | ||

+ | VOLUME = {3389}, | ||

+ | SERIES = {Lecture Notes in Computer Science}, | ||

+ | PAGES = {317-327}, | ||

+ | PUBLISHER = {Springer}, | ||

+ | ABSTRACT = {Here we introduce DePathos, a graphical tool for a | ||

+ | timetabling constraint engine (Pathos). Since the core | ||

+ | of Pathos is textbased and provides little | ||

+ | user-interaction, finding an appropriate solution for | ||

+ | large problems (1000-2000 variables) can be a very time | ||

+ | consuming process requiring the constant supervision of | ||

+ | a constraint programming expert. DePathos uses an | ||

+ | incremental solution strategy. Such strategy subdivides | ||

+ | the problem and checks the consistency of the resulting | ||

+ | subdivisions before incrementally unifying them. This | ||

+ | has shown to be useful in finding inconsistencies and | ||

+ | discovering over-constrained situations. Our | ||

+ | incremental solution is based on hierarchical groupings | ||

+ | defined at the problem domain level. This allows users | ||

+ | to direct the timetabling engine in finding partial | ||

+ | solutions that are meaningful in practice. We discuss | ||

+ | the lessons learned from using Pathos in real settings, | ||

+ | as well as the experiences of coupling DePathos to the | ||

+ | timetabling engine.}, | ||

+ | ISBN = {3-540-25079-4}, | ||

+ | KEYWORDS = {Constraint Programming, Timetabling Problems, | ||

+ | Incremental Execution, Mozart}, | ||

+ | PDF = {/wiki/lib/exe/fetch.php?media=grupos:avispa:papers:dpp+04.pdf}, | ||

+ | YEAR = 2004 | ||

+ | } | ||

+ | </pre> | ||

+ | </p> | ||

+ | <p><a name="Val03"></a><pre> | ||

+ | @PHDTHESIS{Val03, | ||

+ | AUTHOR = {Valencia, F. D.}, | ||

+ | TITLE = {Temporal Concurrent Constraint Programming}, | ||

+ | SCHOOL = {BRICS}, | ||

+ | NOTE = {PhD thesis. xvii+174}, | ||

+ | ABSTRACT = {{\em Concurrent constraint programming} (ccp) is a | ||

+ | formalism for concurrency in which agents interact with | ||

+ | one another by telling (adding) and asking (reading) | ||

+ | information in a shared medium. Temporal ccp extends | ||

+ | ccp by allowing agents to be constrained by time | ||

+ | conditions. This dissertation studies temporal ccp as a | ||

+ | model of concurrency for discrete-timed systems. The | ||

+ | study is conducted by developing a process calculus | ||

+ | called {\tt ntcc}. \bibpar The {\tt ntcc} calculus | ||

+ | generalizes the tcc model, the latter being a temporal | ||

+ | ccp model for {\em deterministic} and {\em synchronous | ||

+ | timed reactive} systems. The calculus is built upon few | ||

+ | basic ideas but it captures several aspects of timed | ||

+ | systems. As tcc, {\tt ntcc} can model unit delays, | ||

+ | time-outs, pre-emption and synchrony. Additionally, it | ||

+ | can model {\em unbounded but finite delays, bounded | ||

+ | eventuality, asynchrony} and {\em nondeterminism}. The | ||

+ | applicability of the calculus is illustrated with | ||

+ | several interesting examples of discrete-time systems | ||

+ | involving mutable data structures, robotic devices, | ||

+ | multi-agent systems and music applications. \bibpar The | ||

+ | calculus is provided with a {\em denotational | ||

+ | semantics} that captures the reactive computations of | ||

+ | processes in the presence of arbitrary environments. | ||

+ | The denotation is proven to be {\em fully-abstract} for | ||

+ | a substantial fragment of the calculus. This | ||

+ | dissertation identifies the exact technical problems | ||

+ | (arising mainly from allowing nondeterminism, locality | ||

+ | and time-outs in the calculus) that makes it impossible | ||

+ | to obtain a fully abstract result for the full language | ||

+ | of {\tt ntcc}. \bibpar Also, the calculus is provided | ||

+ | with a process logic for expressing {\em temporal | ||

+ | specifications} of {\tt ntcc} processes. This | ||

+ | dissertation introduces a ({\em relatively}) {\em | ||

+ | complete inference system} to prove that a given {\tt | ||

+ | ntcc}process satisfies a given formula in this logic. | ||

+ | The denotation, process logic and inference system | ||

+ | presented in this dissertation significantly extend and | ||

+ | strengthen similar developments for tcc and (untimed) | ||

+ | ccp. \bibpar This dissertation addresses the {\em | ||

+ | decidability} of various behavioral equivalences for | ||

+ | the calculus and {\em characterizes} their | ||

+ | corresponding induced congruences. The equivalences | ||

+ | (and their associated congruences) are proven to be | ||

+ | decidable for a significant fragment of the calculus. | ||

+ | The decidability results involve a systematic | ||

+ | translation of processes into finite state B{\"u}chi | ||

+ | automata. To the author's best knowledge the study of | ||

+ | decidability for ccp equivalences is original to this | ||

+ | work. \bibpar Furthermore, this dissertation deepens | ||

+ | the understanding of previous ccp work by establishing | ||

+ | an {\em expressive power hierarchy} of several temporal | ||

+ | ccp languages which were proposed in the literature by | ||

+ | other authors. These languages, represented in this | ||

+ | dissertation as {\em variants} of {\tt ntcc} , differ | ||

+ | in their way of defining infinite behavior (i.e., {\em | ||

+ | replication} or {\em recursion}) and the scope of | ||

+ | variables (i.e., {\em static} or {\em dynamic scope}). | ||

+ | In particular, it is shown that (1) recursive | ||

+ | procedures with parameters can be encoded into | ||

+ | parameterless recursive procedures with dynamic | ||

+ | scoping, and vice-versa; (2) replication can be encoded | ||

+ | into parameterless recursive procedures with static | ||

+ | scoping, and vice-versa; (3) the languages from (1) are | ||

+ | {\em strictly more expressive} than the languages from | ||

+ | (2). (Thus, in this family of languages recursion is | ||

+ | more expressive than replication and dynamic scope is | ||

+ | more expressive than static scope.) Moreover, it is | ||

+ | shown that behavioral equivalence is {\em undecidable} | ||

+ | for the languages from (l), but {\em decidable} for the | ||

+ | languages from (2). Interestingly, the undecidability | ||

+ | result holds even if the process variables take values | ||

+ | from a {\em fixed finite domain} whilst the | ||

+ | decidability holds for {\em arbitrary domains}. \bibpar | ||

+ | Both the expressive power hierarchy and | ||

+ | decidability/undecidability results give a clear | ||

+ | distinction among the various temporal ccp languages. | ||

+ | Also, the distinction between static and dynamic | ||

+ | scoping helps to clarify the situation in the (untimed) | ||

+ | ccp family of languages. Moreover, the methods used in | ||

+ | the decidability results may provide a framework to | ||

+ | perform further systematic investigations of temporal | ||

+ | ccp languages.}, | ||

+ | COMMENT = {Defence: February~5, 2003}, | ||

+ | INSTITUTION = <a href="#BRICS">BRICS</a>, | ||

+ | KEYWORDS = {Concurrent Constraint Programming, ntcc, Applications, | ||

+ | Expressiveness of Process Calculi}, | ||

+ | NUMBER = {DS-03-2}, | ||

+ | PDF = {/wiki/lib/exe/fetch.php?media=grupos:avispa:papers:val03.pdf}, | ||

+ | YEAR = 2003 | ||

+ | } | ||

+ | </pre> | ||

+ | </p> | ||

+ | <p><a name="NV03"></a><pre> | ||

+ | @INPROCEEDINGS{NV03, | ||

+ | AUTHOR = {Nielsen, M. and Valencia, F. D.}, | ||

+ | TITLE = {Notes on {T}imed {CCP}}, | ||

+ | BOOKTITLE = {Lectures on {C}oncurrency and {P}etri {N}ets}, | ||

+ | VOLUME = {3098}, | ||

+ | SERIES = {Lecture Notes in Computer Science}, | ||

+ | PAGES = {702-741}, | ||

+ | PUBLISHER = {Springer}, | ||

+ | ABSTRACT = {A constraint is a piece of (partial) information on | ||

+ | the values of the variables of a system. Concurrent | ||

+ | constraint programming (ccp) is a model of concurrency | ||

+ | in which agents (also called processes) interact by | ||

+ | telling and asking information (constraints) to and | ||

+ | from a shared store (a constraint). Timed (or temporal) | ||

+ | ccp (tccp) extends ccp by agents evolving over time. A | ||

+ | distinguishing feature of tccp, is that it combines in | ||

+ | one framework an operational and algebraic view from | ||

+ | process algebra with a declarative view based upon | ||

+ | temporal logic. Tccp has been widely used to specify, | ||

+ | analyze and program reactive systems. This note | ||

+ | provides a comprehensive introduction to the background | ||

+ | for and central notions from the theory of tccp. | ||

+ | Furthermore, it surveys recent results on a particular | ||

+ | tccp calculus, ntcc , and it provides a classification | ||

+ | of the expressive power of various tccp languages.}, | ||

+ | KEYWORDS = {Timed Concurrent Constraint Programming, ntcc}, | ||

+ | PDF = {/wiki/lib/exe/fetch.php?media=grupos:avispa:papers:nv03.pdf}, | ||

+ | YEAR = 2003 | ||

+ | } | ||

+ | </pre> | ||

+ | </p> | ||

+ | <p><a name="SD03"></a><pre> | ||

+ | @TECHREPORT{SD03, | ||

+ | AUTHOR = {G. Sarria and J. Diago}, | ||

+ | TITLE = {OpenMusic for Linux and MacOS X}, | ||

+ | INSTITUTION = {AVISPA Research Group, IRCAM and Pontificia Universidad | ||

+ | Javeriana}, | ||

+ | ABSTRACT = {This document describes the development of the OpenMusic | ||

+ | (OM) port to Linux and MacOS X. We begin explaining | ||

+ | the main characteristics of OM, then we show the | ||

+ | changes made for each platform (for Linux was chosen | ||

+ | the compiler CMUCL and Gtk+ as graphical interface, | ||

+ | and for MacOS X the new version 5.0 of MCL was enough | ||

+ | for OM to be ported) and we finished with some | ||

+ | conclusions and considerations for future work.}, | ||

+ | KEYWORDS = {OpenMusic, Linux, MacOS X, Computer-Aided Composition}, | ||

+ | MONTH = {September}, | ||

+ | PDF = {/wiki/lib/exe/fetch.php?media=grupos:avispa:papers:sd03.pdf}, | ||

+ | YEAR = 2003 | ||

+ | } | ||

+ | </pre> | ||

+ | </p> | ||

+ | <p><a name="NPV02"></a><pre> | ||

+ | @ARTICLE{NPV02, | ||

+ | AUTHOR = {Nielsen, M. and Palamidessi, C. and Valencia, F. D.}, | ||

+ | TITLE = {Temporal Concurrent Constraint Programming: | ||

+ | Denotation, Logic and Applications.}, | ||

+ | JOURNAL = {Nord. J. Comput.}, | ||

+ | VOLUME = {9}, | ||

+ | NUMBER = {1}, | ||

+ | PAGES = {145-188}, | ||

+ | ABSTRACT = {The tcc model is a formalism for reactive concurrent | ||

+ | constraint programming. We present a model of temporal | ||

+ | concurrent constraint programming which adds to tcc the | ||

+ | capability of modeling asynchronous and | ||

+ | nondeterministic timed behavior. We call this tcc | ||

+ | extension the ntcc calculus. We also give a | ||

+ | denotational semantics for the strongestpostcondition | ||

+ | of ntcc processes and, based on this semantics, we | ||

+ | develop a proof system for linear-temporal properties | ||

+ | of these processes. The expressiveness of ntcc is | ||

+ | illustrated by modeling cells, timed systems such as | ||

+ | RCX controllers, multi-agent systems such as the | ||

+ | Predator/Prey game, and musical applications such as | ||

+ | generation of rhythms patterns and controlled | ||

+ | improvisation.}, | ||

+ | KEYWORDS = {Temporal concurrent constraint programming, calculi | ||

+ | for concurrency, program specication, timed systems, | ||

+ | reactive systems, multi-agent systems, musical | ||

+ | applications}, | ||

+ | PDF = {/wiki/lib/exe/fetch.php?media=grupos:avispa:papers:npv02.pdf}, | ||

+ | YEAR = 2002 | ||

+ | } | ||

+ | </pre> | ||

+ | </p> | ||

+ | <p><a name="RAQ+01"></a><pre> | ||

+ | @ARTICLE{RAQ+01, | ||

+ | AUTHOR = {Rueda, C. and Alvarez, G. and Quesada, L. O. and | ||

+ | Tamura, G. and Valencia, F. D. and Diaz, J. F. and | ||

+ | Assayag, G.}, | ||

+ | TITLE = {Integrating Constraints and Concurrent Objects in | ||

+ | Musical Applications: A Calculus and its Visual | ||

+ | Language.}, | ||

+ | JOURNAL = {Constraints}, | ||

+ | VOLUME = {6}, | ||

+ | NUMBER = {1}, | ||

+ | PAGES = {21-52}, | ||

+ | ABSTRACT = {We propose PiCO, a calculus integrating concurrent | ||

+ | objects and constraints, as a base for music | ||

+ | composition tools. In contrast with calculi such as | ||

+ | [5], [9] or TyCO [16], both constraints and objects are | ||

+ | primitive notions in PiCO. In PiCO a base object model | ||

+ | is extended with constraints by orthogonally adding the | ||

+ | notion of constraint system found in the rho-calculus | ||

+ | [12]. Concurrent processes make use of a constraint | ||

+ | store to synchronize communications either via the ask | ||

+ | and tell operations of the constraint model or the | ||

+ | standard message-passing mechanism of the object model. | ||

+ | A message delegation mechanism built into the calculus | ||

+ | allows encoding of general forms of inheritance. This | ||

+ | paper includes encodings in PiCO of the concepts of | ||

+ | class and sub-class. These allow us to represent | ||

+ | complex partially defined objects such as musical | ||

+ | structures in a compact way. We illustrate the | ||

+ | transparent interaction of constraints and objects by a | ||

+ | musical example involving harmonic and temporal | ||

+ | relations. The relationship between Cordial, a visual | ||

+ | language for music composition applications, and its | ||

+ | underlying model PiCO is described. }, | ||

+ | KEYWORDS = {Concurrent programming, constraint programming, | ||

+ | concurrent constraint objects, TyCO, PiCO, formal | ||

+ | calculi, mobile processes, visual language, computer | ||

+ | aided music composition}, | ||

+ | PDF = {/wiki/lib/exe/fetch.php?media=grupos:avispa:papers:raq+01.pdf}, | ||

+ | YEAR = 2001 | ||

+ | } | ||

+ | </pre> | ||

+ | </p> | ||

+ | <p><a name="SD01"></a><pre> | ||

+ | @MISC{SD01, | ||

+ | AUTHOR = {Sarria, G. and Diago, J.}, | ||

+ | TITLE = {Implantacion del {K}ernel de {O}penmusic bajo {L}inux}, | ||

+ | HOWPUBLISHED = {BSc Thesis -- Engineering Degree in Computer Science, | ||

+ | Pontificia Universidad Javeriana - Cali (Colombia).}, | ||

+ | KEYWORDS = {Openmusic, Lisp, Linux, MacOS}, | ||

+ | PDF = {/wiki/lib/exe/fetch.php?media=grupos:avispa:papers:sd01.pdf}, | ||

+ | YEAR = 2001 | ||

+ | } | ||

+ | </pre> | ||

+ | </p> | ||

+ | <p><a name="DR00"></a><pre> | ||

+ | @ARTICLE{DR00, | ||

+ | AUTHOR = {Diaz, J. F. and Rueda, C.}, | ||

+ | TITLE = {Modelos para la computacion movil (invited paper).}, | ||

+ | JOURNAL = {Revista Colombiana de Computacion}, | ||

+ | VOLUME = {1}, | ||

+ | NUMBER = {1}, | ||

+ | PAGES = {29-45}, | ||

+ | ABSTRACT = {En este articulo presentamos un analisis comparativo | ||

+ | de algunos calculos de computacion movil propuestos | ||

+ | recientemente. Al tiempo que se describen el pi-calculo | ||

+ | propuesto por Milner, un calculo de ambientes propuesto | ||

+ | por Cardelli y Gordon y PiCO; un calculo de objetos y | ||

+ | restricciones propuesto por el grupo AVISPA, se | ||

+ | comparan entre ellos y se comentan sus principales | ||

+ | caracteristicas asociadas a la computacion movil. Otros | ||

+ | calculos como MCC y DyTyCO tambien son analizados.}, | ||

+ | KEYWORDS = {Process calculi for mobile processes, pi-calculus, | ||

+ | ambient calculus, PiCo}, | ||

+ | PDF = {/wiki/lib/exe/fetch.php?media=grupos:avispa:papers:dr00.pdf}, | ||

+ | YEAR = 2000 | ||

+ | } | ||

+ | </pre> | ||

+ | </p> | ||

+ | <p><a name="DRV98"></a><pre> | ||

+ | @ARTICLE{DRV98, | ||

+ | AUTHOR = {Diaz, J. F. and Rueda, C. and Valencia, F. D.}, | ||

+ | TITLE = {Pi+- Calculus: A Calculus for Concurrent Processes | ||

+ | with Constraints.}, | ||

+ | JOURNAL = {CLEI Electronic Journal}, | ||

+ | VOLUME = {1}, | ||

+ | NUMBER = {2}, | ||

+ | ABSTRACT = {The pi-calculus is a formal model of concurrent | ||

+ | computation based on the notion of naming. It has an | ||

+ | important role to play in the search for more abstract | ||

+ | theories of concurrent and communicating systems. In | ||

+ | this paper we augment the pi-calculus with a | ||

+ | constraint store and add the notion of constraint agent | ||

+ | to the standard -calculus concept of agent. We call | ||

+ | this extension the pi+-calculus. We also extend the | ||

+ | notion of barbed bisimulation to define behavioral | ||

+ | equivalence for the pi+-calculus and use it to | ||

+ | characterize some equivalent behaviors derived from | ||

+ | constraint agents. The paper discusses examples of the | ||

+ | extended calculus showing the transparent interaction | ||

+ | of constraints and communicating processes.}, | ||

+ | KEYWORDS = {Concurrent Programming, Constraint Programming, | ||

+ | pi-calculus, pi+-calculus, Formal Calculi, Mobile | ||

+ | Processes.}, | ||

+ | |||

+ | PDF = {/wiki/lib/exe/fetch.php?media=grupos:avispa:papers:drv98.pdf}, | ||

+ | YEAR = 1998 | ||

+ | } | ||

+ | </pre> | ||

+ | </p> | ||

+ | <p><a name="CV96"></a><pre> | ||

+ | @MISC{CV96, | ||

+ | AUTHOR = {Castano, G. and Valencia, F. D.}, | ||

+ | TITLE = {CSP's: Unificacion Formal y Nuevos Algoritmos}, | ||

+ | HOWPUBLISHED = {BSc Thesis -- Engineering Degree in Computer Science, | ||

+ | Pontificia Universidad Javeriana - Cali (Colombia).}, | ||

+ | PDF = {/wiki/lib/exe/fetch.php?media=grupos:avispa:papers:cv96.pdf}, | ||

+ | YEAR = 1996 | ||

+ | } | ||

+ | </pre> | ||

+ | </p> | ||

+ | <hr><p><em>This file has been generated by | ||

+ | <a href="http://www.lri.fr/~filliatr/bibtex2html/">bibtex2html</a> 1.75</em></p> | ||

+ | |||

+ | </html> |