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

grupos:avispa:forces [2008/02/12 11:05] michaelm |
grupos:avispa:forces [2011/01/24 15:30] (actual) |
||
---|---|---|---|

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

+ | ====== FORCES ====== | ||

+ | ** __Formalisms from Concurrency for Emergent Systems:__ ** | ||

+ | |||

+ | ===== Motivation ===== | ||

+ | Concurrent Constraint Programming (CCP) is a mature formalism from Concurrency Theory which combines the traditional operational view of process calculi with a declarative one of processes based upon logic. Some of the members of the teams in this proposal developed and have been using NTCC [NPV02], a timed CCP calculus, to predict the behavior of several systems from emergent areas in computer science such as Security Protocols [LPP+06], Systems Biology [GPRV07] and Multimedia Semantic Interaction [RV05]. Although these areas differ significantly from one another, there is a fundamental commonality in the nature of the analysis one wants to achieve in them: Reachability, i.e., whether a system reaches a state satisfying a particular property. We chose NTCC for these systems because it provides several reasoning tools such as a temporal linear-time logic, a proof system, verification techniques and a denotational semantics which are particularly useful for reachability analysis. | ||

+ | |||

+ | Despite the success of our applications of NTCC to the above-mentioned areas, we have learned from our modeling experience and theoretical studies that NTCC is not sufficiently robust for them. For example, some security protocols use a mechanism to allow generation and communication of secrets. The NTCC calculus can at best express this mechanism indirectly [Val05]. Also, NTCC lacks probabilistic techniques. The modeling of the biological systems often requires to cope with uncertain and approximate information which can then be naturally represented using a probabilistic formalism. Furthermore, we have identified complex non-regular audio processing temporal behavior which cannot be expressed in NTCC. | ||

+ | |||

+ | In this collaboration we aim at providing more robust formalisms for analyzing the emergent systems our teams have been modeling during recent years: I.e., Security Protocols, Biological Systems and Multimedia Semantic Interaction. Our research strategy is, with the benefit of hindsight, to develop them as suitable extensions or specializations of NTCC. We believe that our expertise in process calculi and CCP as well as our experience in modeling the above-mentioned systems are fundamental for achieving this task. | ||

+ | |||

+ | ===== Approach ===== | ||

+ | |||

+ | **Concurrent Constraint Programming (CCP)** is a mature formalism which | ||

+ | combines the traditional operational view of process 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 teams have developed and implemented a | ||

+ | particular CCP timed process calculus which we called **NTCC**. | ||

+ | The calculus offers reasoning techniques such as a linear-temporal | ||

+ | specification logic and its corresponding proof system in which | ||

+ | reachability analysis can be elegantly carried out. | ||

+ | |||

+ | Our teams have been using NTCC for analyzing security protocols, | ||

+ | biological phenomena and applications from multimedia semantic | ||

+ | interaction. **Reachability analysis** is central to all of them. In | ||

+ | security protocols if there is a way to reach a state where some | ||

+ | intruder knows your secret, then there is a secrecy breach. In | ||

+ | bacterial transcription, one ones to know if there is a gene | ||

+ | expression possible in a given gene regulatory network: this is a | ||

+ | reachability analysis problem. Multimedia Semantic Interaction | ||

+ | involve complex interactions in which we may wish to know that a | ||

+ | certain undesirable property will eventually arise; again a | ||

+ | reachability question. | ||

+ | |||

+ | Despite the success of our applications of NTCC to the | ||

+ | above-mentioned areas, we have learned from our modeling experience | ||

+ | and theoretical studies that the NTCC calculus is not sufficiently | ||

+ | robust for them. For example, some security protocols use a mechanism | ||

+ | to allow generation and communication of secrets. The NTCC calculus | ||

+ | can at best express this mechanism indirectly. Also, the NTCC calculus | ||

+ | also lacks probabilistic techniques. The modeling of the biological | ||

+ | systems often requires to cope with uncertain and approximate | ||

+ | information, which one can refine by statistical measurements, and | ||

+ | which can then be naturally represented using a probabilistic | ||

+ | formalism. Furthermore, we have identified complex non-regular audio | ||

+ | processing temporal behaviour which cannot be expressed in NTCC. | ||

+ | |||

+ | ===== Goals and Expected Results ===== | ||

+ | |||

+ | Therefore, the main objectives of REACT focus on developing | ||

+ | more robust CCP theories for dealing with applications in the areas of | ||

+ | Security Protocols, Biology and Multimedia Semantic Interaction. | ||

+ | |||

+ | We propose to obtain our objectives by tailoring the CCP process | ||

+ | calculus NTCC for each of these areas. We believe that our expertise | ||

+ | in process calculi and our experience in modeling these sort of | ||

+ | applications are fundamental for achieving this task. | ||

+ | |||

+ | We expect both theoretical and practical results from our efforts on | ||

+ | this proposal. Namely: (i) CCP Process Calculi to model and reason | ||

+ | about phenomena in these areas. (ii) Tools to automatically simulate | ||

+ | and verify the encoded applications. | ||

+ | Page in development ... | ||

+ | |||

+ | |||

+ | |||

+ | ===== References ===== | ||

+ | |||

+ | * [AADR98] C. Agon, G. Assayag, O. Delerue, and C. Rueda. Objects, time, and constraints in openmusic. In ICMC 98, 1998. | ||

+ | * [AAFR94] C. Agon, G. Assayag, J. Fineberg, and C. Rueda. Kant: a critique of pure quantification. In ICMC 94, 1994. | ||

+ | * [AD02] G. Assayag and S. Dubnov. Universal prediction applied to stylistic music generation. In Mathematic and Music, EMS Diderot Forum, 2002. | ||

+ | * [AD04] G. Assayag and S. Dubnov. Using factor oracles for machine improvisation. Soft Comput., 8(9), 2004. | ||

+ | * [ADLB03] G. Assayag, S. Dubnov, O. Lartillot, and G. Bejerano. Using machine-learning methods for musical style modeling. IEEE Computers, 36(10), 2003. | ||

+ | * [ADR06] G. Assayag, S. Dubnov, and C. Rueda. A concurrent constraints factor oracle model for music improvisation. In CLEI 06, 2008. | ||

+ | * [ALV03] R. Amadio, D. Lugiez, and V. Vanackère. On the symbolic reduction of processes with cryptographic functions. Theor. Comput. Sci., 290(1), 2003. | ||

+ | * [ARL+99] G. Assayag, C. Rueda, M. Laurson, C. Agon, and O. Delerue. Computer-assisted composition at IRCAM: From Patchwork to OpenMusic. Comput. Music J., 23(3), 1999. | ||

+ | * [ASO99] C. Agon, S.Dubnov, and O.Delerue. Guessing the composer's mind : Applying universal prediction to musical style. In ICMC 99, 1999. | ||

+ | * [BB01a] G. Bella and S. Bistarelli. Soft constraints for security protocol analysis: Confidentiality. In PADL 01, 2001. | ||

+ | * [BB01b] M. Boreale and M. Buscemi. A framework for the analysis ofsecurity protocols. In WSDAAL, 2001. | ||

+ | * [BC02] A. Bockmayr and A. Courtois. Using hybrid concurrent constraint programming to model dynamic biological systems. In ICLP 02, 2002. | ||

+ | * [BR98] A. Bonnet and C. Rueda. Situation: Un langage visuel basé sur les contraintes pour la composition musical. Recherches et applications en informatique musicale, 1998. | ||

+ | * [CD99] K. Compton and S. Dexter. Proof techniques for cryptographic protocols. In ICAL 99, 1999. | ||

+ | * [CRFS04] Nathalie Chabrier-Rivier, François Fages, and Sylvain Soliman. The biochemical abstract machine biocham. In CMSB, pages 172-191, 2004. | ||

+ | * [CW01] F. Crazzolara and G. Winskel. Events in security protocols. In CCS 01, 2001. | ||

+ | * [DL03] V. Danos and C. Laneve. Graphs for core molecular biology. In CMSB 03, 2003. | ||

+ | * [dPMH04] María del Pilar Muñoz and Andrés René Hurtado. Programming robotic devices with a timed concurrent constraint language. In CP, page 803, 2004. | ||

+ | * [DRV98] J. Diaz, C. Rueda, and F. Valencia. The pi+ calculus: A calculus for concurrent processes with constraints. CLEI Electronic Journal, 1(2), 1998. | ||

+ | * [ERJ+04] D. Eveillard, D. Ropers, H. Jong, C. Branlant, and A. Bockmayr. A multi-scale constraint programming model of alternative splicing regulation. Theor. Comput. Sci., 325(1), 2004. | ||

+ | * [FA01] M. Fiore and M. Abadi. Computing symbolic models for verifying cryptographic protocols. In CSFW 01, 2001. | ||

+ | * [GPRV07] J. Gutiérrez, J. Pérez, C. Rueda, and F. Valencia. Timed concurrent constraint programming for analysing biological systems. Electron. Notes Theor. Comput. Sci., 171(2), 2007. | ||

+ | * [LPP+06] H. López, C. Palamidessi, J. Pérez, C. Rueda, and F. Valencia. A declarative framework for security: Secure concurrent constraint programming. In ICLP 2006. 2006. | ||

+ | * [Mil95] J. K. Millen. The interrogator model. In SP 95, 1995. | ||

+ | * [NPV02] M. Nielsen, C. Palamidessi, and F. Valencia. Temporal concurrent constraint programming: Denotation, logic and applications. Nordic Journal of Computing, 9(1), 2002. | ||

+ | * [NV02] Mogens Nielsen and Frank D. Valencia. Temporal concurrent constraint programming: Applications and behavior. In Formal and Natural Computing, pages 298-324, 2002. | ||

+ | * [RAQ+01] C. Rueda, G. Alvarez, L. Quesada, G. Tamura, F. Valencia, J. Diaz, and G. Assayag. Integrating constraints and concurrent objects in musical applications: A calculus and its visual language. Constraints, 6(1), 2001. | ||

+ | * [RV02] C. Rueda and F. Valencia. Proving musical properties using a temporal concurrent constraint calculus. In ICMC 02, 2002. | ||

+ | * [RV04a] C. Rueda and F. Valencia. Non-viability deductions in arc-consistency computation. In ICLP 2004. 2004. | ||

+ | * [RV04b] C. Rueda and F. Valencia. On validity in modelization of musical problems by CCP. Soft Comput., 8(9), 2004. | ||

+ | * [Sar04] V. Saraswat. Euler: an applied lcc language for graph rewriting. Technical report, Technical report, IBM TJ Watson Research Center, 2004. | ||

+ | * [Val05] F. Valencia. Decidability of infinite-state timed CCP process and first-order LTL. Theoretical Computer Science, 330(3), 2005. |