Skip to main content
SpringerLink
Log in

Real-Time Rewriting Logic Semantics for Spatial Concurrent Constraint Programming

  • Conference paper
  • First Online:
Rewriting Logic and Its Applications (WRLA 2018)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 11152))

Included in the following conference series:

Abstract

Process calculi provide a language in which the structure of terms represents the structure of processes together with an operational semantics to represent computational steps. This paper uses rewriting logic for specifying and analyzing a process calculus for concurrent constraint programming (\(\textsf {ccp}\)), combining spatial and real-time behavior. In these systems, agents can run processes in different computational spaces (e.g., containers) while subject to real-time requirements (e.g., upper bounds in the execution time of a given operation), which can be specified with both discrete and dense linear time. The real-time rewriting logic semantics is fully executable in Maude with the help of rewriting modulo SMT: partial information (i.e., constraints) in the specification is represented by quantifier-free formulas on the shared variables of the system that are under the control of SMT decision procedures. The approach is used to symbolically analyze existential real-time reachability properties of process calculi in the presence of spatial hierarchies for sharing information and knowledge.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

References

  1. Aranda, J., Pérez, J.A., Rueda, C., Valencia, F.D.: Stochastic behavior and explicit discrete time in concurrent constraint programming. In: Garcia de la Banda, M., Pontelli, E. (eds.) ICLP 2008. LNCS, vol. 5366, pp. 682–686. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-89982-2_57

    Chapter  MATH  Google Scholar 

  2. Barrett, C., et al.: CVC4. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 171–177. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-22110-1_14

    Chapter  Google Scholar 

  3. Bruni, R., Meseguer, J.: Semantic foundations for generalized rewrite theories. Theor. Comput. Sci. 360(1–3), 386–414 (2006)

    Article  MathSciNet  Google Scholar 

  4. Chiarugi, D., Falaschi, M., Hermith, D., Marangoni, R., Olarte, C.: Stochastic modelling of non markovian dynamics in biochemical reactions. In: Rojas, I., Guzman, F.M.O. (eds.) International Work-Conference on Bioinformatics and Biomedical Engineering, IWBBIO 2013, Granada, Spain, 18–20 March 2013. Proceedings, pp. 537–544. Copicentro Editorial (2013)

    Google Scholar 

  5. Clavel, M., Durán, F., Eker, S., Lincoln, P., Martí-Oliet, N., Meseguer, J., Talcott, C.: All About Maude - A High-Performance Logical Framework. LNCS, vol. 4350. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-71999-1

    Book  MATH  Google Scholar 

  6. de Boer, F., Gabbrielli, M., Meo, M.C.: A timed concurrent constraint language. Inf. Comput. 161, 45–83 (2000)

    Article  MathSciNet  Google Scholar 

  7. Degano, P., Gadducci, F., Priami, C.: A causal semantics for CCS via rewriting logic. Theor. Comput. Sci. 275(1–2), 259–282 (2002)

    Article  MathSciNet  Google Scholar 

  8. Dutertre, B.: Yices 2.2. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 737–744. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-08867-9_49

    Chapter  Google Scholar 

  9. Gilbert, D., Palamidessi, C.: Concurrent constraint programming with process mobility. In: Lloyd, J., et al. (eds.) CL 2000. LNCS (LNAI), vol. 1861, pp. 463–477. Springer, Heidelberg (2000). https://doi.org/10.1007/3-540-44957-4_31

    Chapter  Google Scholar 

  10. Gupta, V., Jagadeesan, R., Panangaden, P.: Stochastic processes as concurrent constraint programs. In: Symposium on Principles of Programming Languages, pp. 189–202 (1999)

    Google Scholar 

  11. Gupta, V., Jagadeesan, R., Saraswat, V.A.: Computing with continuous change. Sci. Comput. Program. 30(1–2), 3–49 (1998)

    Article  MathSciNet  Google Scholar 

  12. Guzmán, M., Haar, S., Perchy, S., Rueda, C., Valencia, F.D.: Belief, knowledge, lies and other utterances in an algebra for space and extrusion. J. Log. Algebr. Methods Program. 86(1), 107–133 (2017)

    Article  MathSciNet  Google Scholar 

  13. Knight, S., Palamidessi, C., Panangaden, P., Valencia, F.D.: Spatial and epistemic modalities in constraint-based process calculi. In: Koutny, M., Ulidowski, I. (eds.) CONCUR 2012. LNCS, vol. 7454, pp. 317–332. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-32940-1_23

    Chapter  Google Scholar 

  14. Meseguer, J.: Conditional rewriting logic as a unified model of concurrency. Theor. Comput. Sci. 96(1), 73–155 (1992)

    Article  MathSciNet  Google Scholar 

  15. Meseguer, J., Roşu, G.: The rewriting logic semantics project: a progress report. Inf. Comput. 231, 38–69 (2013)

    Article  MathSciNet  Google Scholar 

  16. Nielsen, M., Palamidessi, C., Valencia, F.D.: Temporal concurrent constraint programming: denotation, logic and applications. Nordic J. Comput. 9(1), 145–188 (2002)

    MathSciNet  MATH  Google Scholar 

  17. Okasaki, C.: Purely Functional Data Structures. Cambridge University Press, Cambridge (1. paperback ed., transf. to digital printing edition) (2003). OCLC: 552279078

    Google Scholar 

  18. Ölveczky, P.C., Meseguer, J.: Specification of real-time and hybrid systems in rewriting logic. Theor. Comput. Sci. 285(2), 359–405 (2002)

    Article  MathSciNet  Google Scholar 

  19. Ölveczky, P.C., Meseguer, J.: Abstraction and completeness for Real-Time Maude. Electron. Notes Theor. Comput. Sci. 176(4), 5–27 (2007)

    Article  Google Scholar 

  20. Pérez, J.A., Rueda, C.: Non-determinism and probabilities in timed concurrent constraint programming. In: Garcia de la Banda, M., Pontelli, E. (eds.) ICLP 2008. LNCS, vol. 5366, pp. 677–681. Springer, Berlin, Heidelberg (2008). https://doi.org/10.1007/978-3-540-89982-2_56

    Chapter  MATH  Google Scholar 

  21. Rocha, C., Meseguer, J., Muñoz, C.: Rewriting modulo SMT and open system analysis. J. Log. Algebr Methods Program. 86(1), 269–297 (2017)

    Article  MathSciNet  Google Scholar 

  22. Romero, M., Rocha, C.: Symbolic execution and reachability analysis using rewriting modulo SMT for spatial concurrent constraint systems with extrusion. In: Dutle, A., Muñoz, C., Narkawicz, A. (eds.) NFM 2018. LNCS, vol. 10811, pp. 435–451. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-77935-5_29

    Chapter  Google Scholar 

  23. Saraswat, V., Jagadeesan, R., Gupta, V.: Foundations of timed concurrent constraint programming. In: Proceedings of the Ninth Annual IEEE Symposium on Logic in Computer Science, pp. 71–80, 4–7 July 1994

    Google Scholar 

  24. Saraswat, V., Jagadeesan, R., Gupta, V.: Foundations of timed concurrent constraint programming, pp. 71–80. In: IEEE Computer Society Press (1994)

    Google Scholar 

  25. Saraswat, V., Jagadeesan, R., Gupta, V.: Default timed concurrent constraint programming. In: Proceedings of the 22nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 272–285, Jan 1995

    Google Scholar 

  26. Saraswat, V.A., Rinard, M., Panangaden, P.: Semantic foundations of concurrent constraint programming. In: POPL 1991, pp. 333–352. ACM (1991)

    Google Scholar 

  27. Sarria, G., Rueda, C.: Real-time concurrent constraint programming. In: 34th Latin American Conference on Informatics (CLEI 2008), pp. 379–391. CLEI (2008)

    Google Scholar 

  28. Verdejo, A., Martí-Oliet, N.: Two case studies of semantics execution in Maude: CCS and LOTOS. Form. Methods Syst. Design 27(1–2), 113–172 (2005)

    Article  Google Scholar 

Download references

Acknowledgments

The authors would like to thank the anonymous referees for their helpful comments. The first author was partially supported by Colciencias via the project CLASSIC (Proj. No. 125171250031). The second author was partially supported by Colciencias’ Convocatoria 761 Jóvenes Investigadores e Innovadores 2016 and Pontificia Universidad Javeriana Cali (Contract No. 416-2017). The third author was partially supported by Capital Semilla 2017, project “SCORES: Stochastic Concurrency in Rewrite-based Probabilistic Models” (Proj. No. 020100610). The third and fourth authors were partially supported by CAPES, Colciencias, and INRIA via the STIC AmSud project “EPIC: EPistemic Interactive Concurrency” (Proj. No. 88881.117603/2016-01).

Author information

Authors and Affiliations

  1. Department of Electronics and Computer Science, Pontificia Universidad Javeriana, Cali, Colombia

    Sergio Ramírez, Miguel Romero, Camilo Rocha & Frank Valencia

  2. CNRS, LIX École Polytechnique de Paris, Paris, France

    Frank Valencia

Authors
  1. Sergio Ramírez
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Miguel Romero
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Camilo Rocha
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Frank Valencia
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding authors

Correspondence to Sergio Ramírez , Miguel Romero , Camilo Rocha or Frank Valencia .

Editor information

Editors and Affiliations

  1. Inria, Lille, France

    Vlad Rusu

Rights and permissions

Reprints and permissions

Copyright information

© 2018 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Ramírez, S., Romero, M., Rocha, C., Valencia, F. (2018). Real-Time Rewriting Logic Semantics for Spatial Concurrent Constraint Programming. In: Rusu, V. (eds) Rewriting Logic and Its Applications. WRLA 2018. Lecture Notes in Computer Science(), vol 11152. Springer, Cham. https://doi.org/10.1007/978-3-319-99840-4_13

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-99840-4_13

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-99839-8

  • Online ISBN: 978-3-319-99840-4

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation