REACT+

Robust theories for Emerging Applications in Concurrency Theory: Processes and Logic Used in Emergent Systems

A joint research effort between the AVISPA Research Group (Universidad Javeriana and Universidad del Valle at Cali, Colombia), the Musical Representations Team at IRCAM and the INRIA Team Comète (LIX, École Polytechnique de Paris, France).

REACT+ is supported by COLCIENCIAS (The Colombian Agency for Science and Technology Development).

The project is active from Septembrer 2011 to September 2013

Motivation

This project proposal, REACT PLUS, addresses the development and application of formal methods in real-life systems. It takes the challenging task of developing the underlying theory and machine-assisted tools for verifying concurrent systems specified in a formalism we have recently developed, the NTCC calculus. Our intended applications are concurrent systems from three emergent domains namely: Security, Biology and Multimedia Semantic Interaction.

Broadly speaking, we shall provide NTCC with automatic verification and simulation techniques and user-friendly tools that can be used by practitioners in our intended applications areas: Security, Biology and Multimedia Semantic Interaction. More precisely, our purpose is to show that concurrent constraint-based techniques can offer important benefits, such as runnable specifications and system properties assurance, to systems modeling in real applications. We would like to demonstrate that practitioners in different areas could be able to take advantage of these benefits, without spending undue training time and effort, by supplying the NTCC calculus with coherent tools, such as efficient simulators and automatic verifiers. We will explore ways to seamlessly integrate these tools into existent development environments in real application areas. We also aim at contributing to the area of concurrent constraint programming by devising novel techniques and formalisms that will allow an integrated modeling, execution and verification environment, similar to those available for other concurrency formalisms.

Goals and Expected Results

We expect to produce efficient techniques and user-friendly tools for the automatic verification and simulation of NTCC processes. More precisely, our expected results are the following:

  • Novel automaton-based, constraint-based and abstract-interpretation techniques for verification in the NTCC calculus.
  • A verification and simulation tool prototype allowing to describe, simulate and automatically verify NTCC systems from our intended applications namely Security, Biology and Multimedia Semantic Interaction.

Executive Summary

More precisely, our teams have developed a concurrent constraint (CC) formalism for reasoning about reactive systems under the auspices of COLCIENCIAS and the French National Institute for Research in Computer Science and Control (INRIA) via the projects REACT and FORCES. The formalism, the NTCC process calculus [NPV02], has attained a wide range of applications in emergent areas such as Security, Biology and Multimedia Semantic Interaction.

We used NTCC to establish important properties of the encoded applications (e.g, security breaches [OV08a], biological malfunctions [GPRF07] and rhythmic coherence [RV04]). Nevertheless, NTCC does not provide for automatic or machine-assisted verification of system properties. We deal with large systems, thus this kind of verification is essential to our applications. This issue, however, has hitherto been far too little considered for constraint-based formalisms. Automatic verification of reactive systems poses a fundamental challenge due to the state explosion problem; the number of states a system has is exponential in the number of concurrent processes. We therefore propose to rise to this challenge by identifying NTCC fragments amenable to automatic verification and developing techniques and tools to machine assist the verification of system properties in NTCC. We envisage two complementary approaches: (1) Automaton-based symbolic techniques and (2) abstract interpretation and types techniques. Automaton-based representations of systems are often used for automatic verification [VW86].

We already showed the decidability of the verification problem for NTCC by using automaton representations of systems and systems' properties [V05]. These representations, however, have a non-elementary space complexity (i.e., the space complexity is worse than exponential). Our plan is to use a novel symbolic approach to ameliorate this state space problem. Our symbolic approach consists in using temporal constraints to compact the state space by using them as succinct representations of many potential transitions from a state. Abstract interpretation and types techniques [CC92] aim at the efficient extraction of representative information from system specifications. They provide the theoretical guarantees that allow deducing properties of programs by processing their associated approximation and type information. By using these techniques, we expect to provide suitable abstract semantics and domains to obtain compact representations of the behavior of NTCC processes. This may facilitate their automatic verification by reducing the state space.

The present proposal is intended as the natural continuation of the international project REACT which was co-funded by COLCIENCIAS from 2007 until 2009. REACT was a productive research collaboration with over 15 international publications, one BSc thesis, one PhD thesis, and three international workshops, and involving 4 PhD students, 3 BSc students and 3 Masters students. REACT PLUS involves the same institutions that carried out REACT: Namely, Pontificia Universidad Javeriana de Cali, Universidad del Valle, the French National Institute for Research in Computer Science and Control (INRIA), the CNRS Laboratory for Informatics LIX at Ecole Polyechnique de Paris, and the Institute for Research and Coordination Acoustic/Music (IRCAM).

Approach

The Problem

During the last couple of years our teams have developed a constraint-based process calculus for reasoning about the behaviour of concurrent systems (i.e. systems of multiple agents, called processes, that interact with one another). This work involved the CNRS Laboratory for Informatics LIX at Ecole Polyechnique de Paris, IRCAM, Pontificia Universidad Javeriana Cali and Universidad del Valle and it was carried under the auspices of COLCIENCIAS, via the project REACT, and the French National Institute for Research in Computer Science and Control (INRIA), via the project FORCES.

Our process calculus, the NTCC model [NPV02], arose as an extension of the Saraswat's concurrent constraint programming (CCP) framework [SRP91] to cope with new phenomena, in particular non-deterministic and timed behaviour. The NTCC calculus is founded upon solid mathematical principles and it has attained a wide range of applications in emergent areas such as Security, Biology and Multimedia Semantic Interaction. Indeed, NTCC provides rich verification techniques allowing the inference of important temporal properties satisfied by the encoded applications, e.g., security breaches in cryptographic protocols [OV08a], prediction of organic malfunctions [GPRF07] and rhythmic coherence in music improvisation [RV04]. In spite of its modeling success, at present NTCC does not provide for the automatic, or even machine-assisted, verification of system properties. Since we deal with complex and large systems, machine-assisted verification is essential to our intended applications. Nevertheless, this issue has hitherto been far too little considered for concurrent constraint-based formalisms.

To the best of our knowledge only Villanueva et al [AdMGPV05,FV06] have addressed automatic verification but only in the context of finite-state systems. Several interesting applications of NTCC are, however, inherently infinite-state. Automatic Verification of large systems, not to mention infinite systems, represents a fundamental challenge because of the state explosion problem it poses, i.e., the number of states a system has is exponential in the number of concurrent processes. We therefore propose to rise to this challenge by identifying NTCC fragments amenable to automatic verification and developing efficient techniques and tools to machine assist the verification of system properties in NTCC. “Never send a human to do a machine's job” The Matrix, 1999.

Justification

In 2006 our teams organized the International Colloquium on Emergent Trends in Concurrency Theory in Paris in honour of Turing-award winner Robin Milner [PV08]. At this event leading researchers reflected about strategic directions in concurrency theory but we adhere in particular to Garavel's position statement [G08] because it justifies so well the present proposal: “The times have gone, where formal methods were primarily a pen-and-pencil activity for mathematicians. Today, only languages properly equipped with software tools will have a chance to be adopted by industry. It is therefore essential for the next generation of languages based on process calculi to be supported by compilers, simulators, verification tools, etc. The research agenda for theoretical concurrency should therefore address the design of efficient algorithms for translating and verifying formal specifications of concurrent systems”.

In fact, the systems in our intended application areas are inherently complex and large. E.g., security protocols may generate a large state space which may come from the unbounded power of the spy, an unbounded number of interleaved protocol runs, or unbounded behaviours of single protocol participant. Machine-assisted analysis can help coping with their complexity. Also the practitioners of these areas, in particular bench biologists and musicians may benefit from a simulation tool that is intuitive due to the distinctive declarative nature of concurrent constraint-based frameworks.

State of the Art

Presently, there are no machine-assisted tools for the automatic verification of system properties in NTCC. Since we deal with complex and large systems, machine-assisted verification is essential to our intended applications. To the best of our knowledge, in the larger context of concurrent constraint programming only Villanueva et al have addressed automatic verification but only for finite-state systems and for a framework semantically different from NTCC, namely TCCP [AdMGPV05,FV06]. Automaton-based techniques are widely used for the automatic verification of system properties in various concurrent frameworks [VW86].

The idea is that one constructs an automaton from the negation of the property in question and then determines whether or not the product of this automaton and the automaton representing the system is empty (if so, the system is correct). The decidability of the verification problem for NTCC was shown in [V05] by using automaton representations of systems. Unfortunately, the automaton construction in [V05] has a non-elementary state space complexity (i.e., the space complexity is bigger than any fixed exponential function) and hence we cannot hope to use it for automatic verification. Symbolic representation of state spaces (e.g, using BDD's or Arithmetic Constraints [BCM92,BOO]) can be used to encode states more compactly.

Temporal-constraints are used to provide a symbolic semantics for NTCC [OV08b]; temporal constraints are finite representations of the infinitely many potential evolutions of a process. We believe that this idea can be adapted to produce a novel symbolic state space representations based on temporal constraints. To the best of our knowledge temporal constraints have not been used for symbolic techniques in verification. Static and abstract interpretation techniques aim at the efficient extraction of representative information from system specifications can also be used for more compact representations of the state space. Such information can be used to reason about essential properties of systems behavior.

To understand abstract interpretation in the context of NTCC processes, it is convenient to recall that the denotational semantics of NTCC is given by a function [ [.] ] that maps processes into a (concrete) domain of objects C. Then, the behavior of a process P can be approximated by computing a compact representation of [ [P] ]. Abstract interpretation techniques provide the theoretical guarantees that allow deducing properties of programs by processing their associated approximation [CC92]. By using these techniques, we expect to provide suitable abstract semantics and domains to obtain compact representations of the behavior of NTCC processes. This may facilitate their automatic verification by reducing the state space as done in the context of TCCP [FV06].

Objectives

General Objectives

Our goal is to provide ntcc with automatic verification and simulation techniques and user-friendly tools that can be used by practitioners in our intended applications areas: Security, Biology and Multimedia Semantic Interaction. More precisely, our purpose is to show that CCP techniques can offer important benefits, such as runnable specifications and system properties assurance, to systems modeling in real applications. We would like to demonstrate that users from different areas could take advantage of these benefits, without spending undue training time and effort, by supplying the NTCC calculus with coherent tools, such as efficient simulators and automatic verifiers.

The latter, in particular, poses a great research challenge since, on the one hand, such verifiers have not been yet proposed for CCP models and, on the other, any practical verifier must cope with the potentially enormous size of the state space induced by a model of reasonable complexity. We propose to devise and implement practical verification algorithms at least for an expressive fragment of NTCC. We will explore ways to seamlessly integrate these tools into existent development environments in real application areas.

We also aim at contributing to the area of ccp by devising novel techniques and formalisms that will allow an integrated modeling, execution and verification environment, similar to those available for other concurrency formalisms.

Specific Objectives

Our specific objectives are articulated along the following topics: Techniques, Tools, and Applications.

Techniques

We aim at developing automaton-based, constraint-based symbolic methods as well as abstract-interpretation and type techniques for the automatic verification of system properties in NTCC. These methods should help cope with the state space problem in NTCC already present in previous naive automaton constructions with a non-elementary space complexity [V05]. With the labelled symbolic semantics for NTCC and its compact representations of transition systems, we aim at defining a notion of symbolic bisimulation equivalence for NTCC.

We will collaborate with Moreno Falaschi from Sienna University (Italy) and Bjorn Victor from Uppsala University (Sweden) world experts in abstract interpretation and verification techniques.

Tools

We aim at producing a tool prototype along the lines of the Mobility Workbench (MWB) [VF94], an automated tool for manipulating and analyzing mobile concurrent systems (those with evolving connectivity structures) described in the pi-calculus. The tool should allow describing, exploring, simulating and automatically verifying systems described in the NTCC calculus.

We will integrate the above into an efficient simulator of NTCC models. This will include features to display the evolution of a system in such a way appropriate to practitioners of other fields, such as biology. Multimedia systems involve interactions with high-performance tools such as sound processing. The integration of purely declarative models such as ntcc with plugins of these tools in such a way that user-defined properties of the model can still be automatically verified is a great research challenge.

We will devise a scheme to integrate plugins written in the Faust [OFL04] sound processing language into NTCC models allowing for the verification of temporal properties of the combined system. We will implement this scheme into the above mentioned verifier.

Applications
  • Security: In Security Protocols one often has to analyze thoroughly a large or even infinite state space which may come from an spy, an unbounded number of interleaved protocol runs, or unbounded behaviours of single protocol participants. We plan to use this kind of protocols to test our techniques and tools. In fact, this analysis is typically carried out using symbolic verification techniques [H99] thus making Security Protocols an ideal application candidate.
  • Biology: Computer simulation plays a fundamental role for Biological Systems because of their inherent complexity [LT04]. We plan to use our ntcc simulation tool as a test bench for (abstractions of) these systems. We expect that the declarative and parametric nature of ntcc should provide bench biologists with a tool for computing with and analyzing these systems that is intuitive.
  • Multimedia Interaction: Complex multimedia systems are usually built out of third-party components suited to specific domains, such as sound processing. We plan to use techniques such as abstract interpretation to define rigorously the interaction of ntcc models with such components. We will use our techniques and tools to verify coherence properties of composite interactive multimedia systems with sound processing plugins written in the Faust language [OFL04]. These would ensure sound manipulations integrate smoothly into user-defined patterns of performance interaction.

Proposed Methodology

Techniques and Tools like for other process calculi, automatic NTCC verification of concurrent systems presents us with serious computational challenge. The crux is the “state explotion problem”; the number of states a system has is exponential in the number of concurrent processes. We will take up this challenge by identifying NTCC fragments amenable to automatic verification and by developing techniques and tools to machine assist the verification of system properties in NTCC. We envisage two main complementary approaches for our purposes: (1) Automaton-based and symbolic techniques, and (2) Static and abstract interpretation techniques.

Automaton-based techniques are often used for the automatic verification of current systems and their properties. A symbolic representation of state spaces (e.g, using BDD's or Arithmetic Constraints [BCM92,BOO]) can be used to encode the systems more compactly. We have already shown the decidability of the verification problem for NTCC by using automaton representations of systems and systems' properties [V05]. Nevertheless, these representations were for theoretical purposes only and thus we were not concerned about their compactness. In fact, the naive automaton construction in [V05] has a non-elementary space complexity. Our plan is therefore to build upon our constructions in [V05] and use a symbolic approach to ameliorate the state space problem.

Our symbolic approach consists in taking advantage of the unique constraint nature of constraint-based calculi such as NTCC which make them ideal candidates for constraint-based symbolic techniques (e.g., [BOO]). Furthermore, we have used temporal-constraints to provide a symbolic semantics for NTCC [OV08b]; temporal constraints are finite representations of the infinitely many potential evolutions of a process. We believe that this idea can be adapted to produce a novel symbolic state space representations based on temporal constraints.

To the best of our knowledge temporal constraints have not been used for symbolic techniques in verification. As mentioned earlier, static and abstract interpretation techniques can be used to extract representative information from system specifications. We plan to use these techniques to provide suitable abstract semantics and domains which will then allows us obtain compact representations of the behavior of NTCC processes. This may facilitate their automatic verification by reducing the state space as in [FV06]. We see theories of abstract interpretation and type systems as complementary foundations for achieving this. In fact, type information could be part of the compact representations to be extracted from the system specification as done in [CRR02].

Applications

We will use Security Protocols to test the above-mentioned techniques and tools. In fact, this analysis is typically carried out using symbolic verification techniques [H99] thus making Security Protocols an ideal application candidate. It is worth noticing that computer simulation plays a fundamental role for Biological Systems because of their inherent complexity [LT04]. We also plan to use our NTCC simulation tool as a test bench for (abstractions of) biological systems.

We expect that the declarative and parametric nature of NTCC should provide bench biologists with a tool for computing with and analyzing these systems that is intuitive. Futhermore, we propose building from our previous work on exploring NTCC models of music improvisation systems based on Factor Oracle (FO) automata ([OR09]). We will explore ways to extend the FO automata so that coherent states (i.e. those representing contexts with coherent music material) can be efficiently identified by suitable concurrent NTCC processes. The performance automaton (the one used by the machine) and the construction of the learned automaton (the one being constructed from what the musician is playing) could then be cleanly synchronized using the calculus constructs.

Two difficulties can be anticipated in this. One is that there are potentially many different states coherent with some given state. We will rely on the expertise of IRCAM to find relevant musical criteria that can be used for filtering out candidates. The second one is technical: how to maintain a minimal representation of (parts of) each FO so that coherent states can be efficiently found concurrently. We intend to explore extensions of known graph path algorithms for this.

Members

Teams

Model Checking

  • Jesús Aranda (Leader)
  • Juan F. Díaz (Leader)
  • Carlos Olarte (Leader)
  • Camilo Rueda (Leader)
  • Moreno Falaschi (Consultant)
  • Julian E. Gutierrez (Consultant)
  • Jorge A. Pérez (Consultant)
  • Frank D. Valencia (Consultant)
  • Mauricio Toro (Consultant)
  • Jaime E. Arias A.
  • Jhonatan Serna M.

Equivalence Techniques

  • Juan F. Díaz (Leader)
  • Camilo Rueda (Leader)
  • Frank D. Valencia (Leader)
  • Andrés A. Aristizábal
  • Luis F. Pino

Tools

  • Juan F. Díaz (Leader)
  • Camilo Rueda (Leader)
  • Jaime E. Arias A.
  • Andrés A. Aristizábal
  • Michell Guzman C.
  • Carlos Olarte
  • Salim Perchy
  • Luis F. Pino
  • Daniel Riaño
  • Jhonatan Serna M.

Applications

Biology
  • Carlos Olarte (Leader)
  • Jesús Aranda (Leader)
  • Diana P. Hermith (Consultant)
  • Moreno Falaschi (Consultant)
  • Michell Guzman C.
Security
  • Frank D. Valencia (Leader)
  • Andrés A. Aristizábal
  • Luis F. Pino
Multimedia
  • Camilo Rueda (Leader)
  • Mauricio Toro (Consultant)
  • Salim Perchy
  • Gerardo M. Sarria M.

Activities Schedule (in weeks)

Activity Description since until
0A1 To explore the definition of an abstract semantics and type systems for NTCC allowing us to extract representative information from systems modeled in the calculus. 1 25
0A2 To identify already defined abstract domains and types for the analysis of concurrent languages that can be tailored to the ntcc setting. 20 35
0A3 To adapt the abstract domains identified above to perform static analysis of ntcc processes. 30 45
0A4 To write and present results at an international conference. 45 50
1B1 To characterize the idea of bisimulation for NTCC. 15 30
1B2 To write and present results on process equvalences at an international conference. 49 53
2S1 To explore mechanisms for the symbolic representation of states in the execution of a NTCC process. 17 30
2S2 To provide suitable abstract domains to obtain the symbolic model of the system. 29 38
2S3 To formally prove the correctness of the abstraction induced by the symbolic representation. 37 41
2S4 To write and present results at an international conference. 41 50
3AP1 To identify a relevant class of biological problems, suitable of being modelled and verified using NTCC. 37 41
3AP2 To identify relevant security protocols, suitable of being modelled and verified using NTCC. 37 41
3AP3 To identify relevant multimedia interaction systems, suitable of being modelled and verified using NTCC. 37 41
3AP4 To model in NTCC the systems above and characterize mathematically the properties to be verified. 41 45
4IM01 To define the requirements of the simulation and verification tool. 37 46
4IM02 To implement the interpreter for the NTCC calculus. 36 63
4IM03 To develop the necessary tools to implement the above mentioned semantic framework and the static analyses proposed. 45 62
4IM04 To implement and simulate the models of Security, Biological and Multimedia Interaction systems. 57 61
4IM05 To compare the theoretical behaviour of the models wrt their executions in the simulator. 57 66
4IM06 To verify the properties defined on the systems modeled. 61 78
4IM07 To write the documentation of the implementation. 77 81
4IM08 To write and present results of each application at international conferences (3). 73 86
4IM09 To integrate the NTCC simulator with the Faust processing language. 57 68
4IM10 To integrate the NTCC verifier into NTCC-Faust simulator. 65 90
4IM11 To develop the translator of the OM ccp model into the Max simulator. 65 90
4IM12 To write and present results at an international conference. 90 98
5J1 To write the journal version of the conference papers related to abstract semantics and type systems for NTCC. 92 100
5J2 To write the journal version for the applications and tools related conference papers. 92 100
6W1 To write final reports. 100 104

Bibliography

  • [AD04] G.Assayag, S.Dubnov, Using Factor Oracles for Machine Improvisation. Soft Computing 8, pp. 1432-7643, September 2004
  • [AdMGPV05] M. Alpuente, M. Gallardo, E. Pimentel, and A. Villanueva. Abstract model checking of tccp programs. Electr. Notes Theor. Comput. Sci., 112:19-36, 2005.
  • [AG99] M. Abadi and A. D. Gordon. A calculus for cryptographic protocols: The spi calculus. Inf. Comput., 148(1):1 70, 1999.
  • [AGP07] Arbelaez, A., Gutierrez, J., Perez, J.A.: Timed Concurrent Constraint Programming in Systems Biology. Newsletter of the ALP 19(4) 2006.
  • [APPSM04]M. Antoniotti, C. Piazza, A. Policriti, M. Simeoni, and B. Mishra. Taming the complexity of biochemical models through bisimulation and collapsing: theory and practice. Theor. Comput. Sci., 325(1):45{67, 2004.
  • [ARLAD99] G. Assayag, C. Rueda, M. Laurson, C. Agon, O. Delerue. Computer-assisted Composition at Ircam: from Patchwork to OpenMusic. Computer Music Journal. 23(3): 59-72. MIT Press, 1999.
  • [B00] T. Bultan. BDD vs. Constraint-Based Model Checking: An Experimental Evaluation for Asynchronous Concurrent Systems.In Proc. TACAS 2000, LNCS 1785. ©Springer, 2000.
  • [BB01] G. Bella and S. Bistarelli. Soft constraints for security protocol analysis: Confidentiality. LNCS, 1990, 2001.
  • [BC02] A. Bockmayr and A. Courtois. Using hybrid concurrent constraint programming to model dynamic biological systems. In Peter J. Stuckey, editor, ICLP, volume 2401 of LNCS, pages 85-99. Springer, 2002
  • [BCEV03] A. Bockmayr, A. Courtois, D. Eveillard, and M. Vezain. Building and Analysing an Integrative Model of HIV-1RNA Alternative Splicing. In Danos and Schachter [DL03], pages 43-57
  • [BCM92] J. R. Burch, E. M. Clarke, K. L. McMillan, D. L. Dill, and L. J. Hwang. Symbolic model checking: 10**20 states and beyond. Information and Computation, 98(2):142-170, June 1992.
  • [Bla05] Bruno Blanchet. Security Protocols: From Linear to Classical Logic by Abstract Interpretation. Information Processing Letters, 95(5), 2005.
  • [Bor01] Michele Boreale. Symbolic trace analysis of cryptographic protocols. In Proc. of ICALP'01. LNCS, 2001.
  • [CAD06] C. Rueda, G. Assayag, S. Dubnov, “A Concurrent Constraints Factor Oracle Model for Music Improvisation. Proceedings of CLEI2006 Conference, Santiago, Chile, August 2006.
  • [Car05] L. Cardelli. Abstract Machines of Systems Biology. In Transactions on Computational Systems Biology III, volume 3737 of Lecture Notes in Computer Science, 145-168. Springer, 2005.
  • [CC92] P. Cousot and R. Cousot. Abstract Interpretation and Applications to Logic Programs. J. of Logic Programming 13(2&3):103-179, 1992.
  • [CCrFS06] L. Calzone, N. Chabrier-Rivier, F. Fages, and S. Soliman. Machine learning biochemical networks from temporal logic properties. Transactions on Computational Systems Biology, 2006.
  • CMSB'05 Special Issue [CD99] K. Compton and S. Dexter. Proof techniques for cryptographic protocols. LNCS, 1644, 1999.
  • [CG98] L. Cardelli and A.D. Gordon. Mobile ambients. In FoSSaCS, volume 1378 of Lecture Notes in Computer Science, 140-155. Springer, 1998.
  • [CRR02] S. Chaki, S. Rajamani, J. Rehof. Types as Models: Model Checking Message-Passing Programs. POPL'02. ©ACM, 2002.
  • [CW01] F. Crazzolara and G. Winskel. Events in security protocols. In Proc. of CCS '01. ACM Press, 2001.
  • [DL03] V. Danos and C. Laneve. Graphs for Core Molecular Biology. In Proc. of CMSB 2003, volume 2602 of LNCS, 2003.
  • [ERJBB04]D. Eveillard, D. Ropers, H. de Jong, C. Branlant, and A. Bockmayr. A multi-scale constraint programming model of alternative splicing regulation. Theor. Comput. Sci., 325(1):324, 2004.
  • [FA02] C. Fournet and M. Abadi. Hiding names: Private authentication in the applied pi calculus. In ISSS, pages 317-338, 2002.
  • [FV06] M. Falaschi and A. Villanueva. Automatic Verification of tccp programs. Theory and Practice of Logic Programming. Volume 6, Issue 3. pages 265-300, May 2006.
  • [G08] H. Garavel. Reflections on the Future of Concurrency Theory in General and Process Calculi in Particular. Proc. of LIX Colloquium on Emergent Trends in Concurrency Theory. Electr. Notes Theor. Comput. Sci. 209: 149-164. ©Elsevier, 2008
  • [GPRF07] J. Gutierrez, J. Perez, C. Rueda and F. Valencia. Timed Concurrent Constraint Programming for Analyzing Biological Systems. Electr. Notes Theor. Comput. Sci. 171(2): 117-137.© Elsevier. 2007
  • [H99] A. Huima. Efficient infinite-state analysis of security protocols. Proc. FLOC'99 Workshop on Formal Methods and Security Protocols. 1999.
  • [HBW+05] P. Herrera, J. Bello, G. Widmer, M. Sandler, O. Celma, F. Vignoli, E. Pampalk, P. Cano, S. Pauws, X. Serra. SIMAC: Semantic interaction with music audio contents. In Proc. of the 2nd European Workshop on the Integration of Knowledge, Semantic and Digital Media Technologies. London 2005.
  • [Hoa83] C. A. R. Hoare. Communicating Sequential Processes. Commun. ACM, 26(1):100-106, 1983.
  • [HORV11] D. Hermith, C. Olarte, C. Rueda, F. Valencia. Modeling Cellular Signaling Systems: An Abstraction-Refinement Approach. In Proc. of PACBB'11. Advances in Intelligent and Soft Computing, Springer. pg. 321-328. 2011.
  • [KNP08a]M. Kwiatkowska, G. Norman and D. Parker. Using probabilistic model checking in systems biology. ACM SIGMETRICS Performance Evaluation Review, 35(4), pages 14-21, Association for Computing Machinery. March 2008.
  • [Low96] G. Lowe. Breaking and ?xing the needham-schroeder public-key protocol using fdr. In TACAS, pages 147-166, 1996.
  • [LT04] P. Lincoln and A. Tiwari. Symbolic systems biology: Hybrid modeling and analysis of biological networks. In Proc. HSCC'04. LNCS 2993:660-672. ©Springer, 2004.
  • [MAPU05] B. Mishra, M. Antoniotti, S. Paxia, and N. Ugel. Simpathica: A Computational Systems Biology Toolwithin the Valis Bioinformatics Environment. In E. Eiles and A. Kriete, editors, Computational SystemsBiology. Elsevier, 2005.
  • [Mat97] M. Mateas. An Oz-Centric Review of Interactive Drama and Believable Agents. Technical report cmucs -97-156, School of Computer Science, Carnegie Mellon University, Pittsburgh. 1997.
  • [MLA+04] B. Magerko, J. E. Laird, M. Assanie, A. Kerfoot, and D. Stokes. AI Characters and Directors for Interactive Computer Games. In Proc. of the 2004 Innovative Applications of Artificial Intelligence Confercence, AAAI Press, 2004.
  • [Mil89] R. Milner. Communication and Concurrency. Prentice Hall, 1989.
  • [Mil95] J. Millen. The Interrogator model. In IEEE Symposium on Security and Privacy, 251-260. IEEE Computer Society, 1995.
  • [Mil99] R. Milner. Communicating and Mobile Systems: The Pi-Calculus. Cambridge University Press, 1999.
  • [MMS97] J. C. Mitchell, M. Mitchell, and U. Stern. Automated analysis of cryptographic protocols using mur-phi. In IEEE Symposium on Security and Privacy, pages 141-151, 1997.
  • [NPV02] M Nielsen, C. Palamidessi and F. Valencia. Temporal Concurrent Constraint Programming: Denotation, Logic and Applications. Nord. J. Comput. 9(1): 145-188. ©NJC. 2002.
  • [OR09] C. Olarte, C. Rueda. A Declarative Language for Dynamic Multimedia Interaction Systems. Proceedings of the Mathematics and Music Conference (MCM2009). (to appear)
  • [OV08a] C. Olarte and F. Valencia. The expressivity of universal timed CCP: Undecidability of monadic FLTL and closure operators for security. In PPDP. ©ACM, 2008.
  • [OV08b] C. Olarte and F. Valencia.Universal concurrent constraint programing: Symbolic semantics and applications to security. In SAC. ©ACM, 2008.
  • [P02] M. Pucket. Max at seventeen. Computer Music Journal 26(4): 31-43. MIT Press, 2002.
  • [Pri95] C. Priami. Stochastic pi-calculus. The Computer Journal, 38(6):578–589, 1995.
  • [PV08] C. Palamidessi, F. Valencia (eds). Proc. of LIX Colloquium on Emergent Trends in Concurrency Theory. Electr. Notes Theor. Comput. Sci. 209. ©Elsevier, 2008.
  • [RS02] A. Regev and E. Shapiro. Cells as Computation. Nature, 419:343, September 2002.
  • [RS04] A. Regev and E. Shapiro. Modelling in Molecular Biology, chapter The Pi-calculus as an abstraction for biomolecular systems, 219-266. Natural Computing Series. Springer, 2004.
  • [RV04] C. Rueda and F. Valencia. On validity in modelization of musical problems by CCP. Soft Comput. 8(9): 641-648. ©Springer. 2004.
  • [Sar93] V. Saraswat. Concurrent constraint programming. MIT Press, 1993.
  • [SBP01] D. Xiaodong Song, S. Berezin, and A. Perrig. Athena: A novel approach to effcient automatic security protocol analysis. Journal of Computer Security, 9(1/2):47-74, 2001.
  • [SRP91] V. Saraswat, M. Rinard and P. Prakash Panangaden.Semantics Foundations of Concurrent Constraint Programming. POPL'91. ©ACM, 1991.
  • [V05] F. Valencia. Decidability of Infinite-State Timed CCP Processes and First-Order LTL. Theor. Comput. Sci. 330(3): 577-607. ©Elsevier. 2005 a
  • [VW86] M. Vardi and P. Wolper. An automata-theoretic approach to automatic program verification. In Symposium on Logic in Computer Science (LICS '86), pages 332-344, Cambridge, Massachusetts, June 1986. ©IEEE Computer Society Press.
  • [VF94] B. Victor, F. Moller: The Mobility Workbench - A Tool for the pi-Calculus. CAV 1994: 428-440. ©Springer, 1994.

Progress Report 2012

Report September 2012: avance.pdf

 
grupos/avispa/react-plus.txt · Última modificación: 2013/04/19 14:12 por crueda
Recent changes RSS feed Donate Powered by PHP Valid XHTML 1.0 Valid CSS Driven by DokuWiki