Decidability of Modular Logics for Concurrency

  • Radu Mardare
Part of the Lecture Notes in Computer Science book series (LNCS, volume 7162)


The modular logics we approach in this paper are logics for concurrent systems that reflect both behavioral and structural properties of systems. They combine dynamic modalities that express behavioural properties of a system with polyadic modalities that join properties of subsystems. Spatial and Separation Logics are examples of modular logics. Being the complex algebraic-coalgebraic semantics, these logics have interesting decidability properties. In this paper we provide a taxonomy of the decision problems for a class of modular logics with semantics based on CCS processes.


Model Check Modal Logic Parallel Operator Operational Semantic Guarantee Operator 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    van Benthem, J.: Language in action. Categories, Lambdas and Dynamic Logic. Elsevier Science Publisher (1991)Google Scholar
  2. 2.
    Bergstra, J.A., Ponse, A., Smolka, S.A. (eds.): Handbook of Process Algebra. Elsevier (2001)Google Scholar
  3. 3.
    Caires, L., Cardelli, L.: A Spatial Logic for Concurrency (Part I). Inf. and Comp. 186/2 (2003)Google Scholar
  4. 4.
    Caires, L., Lozes, É.: Elimination of Quantifiers and Undecidability in Spatial Logics for Concurrency. In: Gardner, P., Yoshida, N. (eds.) CONCUR 2004. LNCS, vol. 3170, pp. 240–257. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  5. 5.
    Calcagno, C., Cardelli, L., Gordon, A.D.: Deciding validity in a spatial logic for trees. Journal of Functional Programming 15 (2005)Google Scholar
  6. 6.
    Calcagno, C., Yang, H., O’Hearn, P.W.: Computability and Complexity Results for a Spatial Assertion Language for Data Structures. In: Hariharan, R., Mukund, M., Vinay, V. (eds.) FSTTCS 2001. LNCS, vol. 2245, pp. 108–119. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  7. 7.
    Cardelli, L., Gordon, A.D.: Anytime, Anywhere: Modal Logics for Mobile Ambients. In: Proc. of 27th ACM Symposium on Principles of Programming Languages (2000)Google Scholar
  8. 8.
    Cardelli, L., Larsen, K.G., Mardare, R.: Continuous Markovian Logics - From Complete Axiomatization to the Metric Space of Formulas. In: Proc. of Computer Science Logic CSL 2011 (2011)Google Scholar
  9. 9.
    Cardelli, L., Larsen, K.G., Mardare, R.: Modular Markovian Logic. In: Aceto, L., Henzinger, M., Sgall, J. (eds.) ICALP 2011, Part II. LNCS, vol. 6756, pp. 380–391. Springer, Heidelberg (2011)CrossRefGoogle Scholar
  10. 10.
    Cardelli, L., Mardare, R.: The Measurable Space of Stochastic Processes. In: QEST 2010. IEEE Press (2010)Google Scholar
  11. 11.
    Charatonik, W., Talbot, J.-M.: The Decidability of Model Checking Mobile Ambients. In: Fribourg, L. (ed.) CSL 2001 and EACSL 2001. LNCS, vol. 2142, pp. 339–354. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  12. 12.
    Dam, M.: Model checking mobile processes. Inf. and Comp. 129(1) (1996)Google Scholar
  13. 13.
    Gyuris, V.: Associativity does not imply undecidability without the axiom of Modal Distribution. In: Marx, M., et al. (eds.) Arrow Logic and Multi-Modal Logic, CSLI and FOLLI (1996)Google Scholar
  14. 14.
    Hennessy, M., Milner, R.: Algebraic laws for Nondeterminism and Concurrency. JACM 32(1) (1985)Google Scholar
  15. 15.
    Mardare, R.: Logical analysis of Complex Systems. Dynamic Epistemic Spatial Logics. PhD thesis, DIT, University of Trento (2006)Google Scholar
  16. 16.
    Mardare, R.: Observing Distributed Computation. A Dynamic-Epistemic Approach. In: Mossakowski, T., Montanari, U., Haveraaen, M. (eds.) CALCO 2007. LNCS, vol. 4624, pp. 379–393. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  17. 17.
    Mardare, R., Priami, C.: A logical approach to security in the context of Ambient Calculus. Electronic Notes in Theoretical Computer Science 99, 3–29 (2004)CrossRefGoogle Scholar
  18. 18.
    Mardare, R., Priami, C.: A Propositional Branching Temporal Logic for the Ambient Calculus. Tech.Rep. DIT-03-053, University of Trento, Italy (2003)Google Scholar
  19. 19.
    Mardare, R., Priami, C.: Decidable Extensions of Hennessy-Milner Logic. In: Najm, E., Pradat-Peyre, J.-F., Donzeau-Gouge, V.V. (eds.) FORTE 2006. LNCS, vol. 4229, pp. 196–211. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  20. 20.
    Mardare, R., Policriti, A.: A Complete Axiomatic System for a Process-Based Spatial Logic. In: Ochmański, E., Tyszkiewicz, J. (eds.) MFCS 2008. LNCS, vol. 5162, pp. 491–502. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  21. 21.
    Milner, R.: A Calculus of Communicating Systems. Springer-Verlag New York, Inc. (1982)Google Scholar
  22. 22.
    Milner, R., Parrow, J., Walker, D.: Modal logics for mobile processes. TCS 114 (1993)Google Scholar
  23. 23.
    Sangiorgi, D.: Extensionality and Intensionality of the Ambient Logics. In: Proc. of the 28th ACM Annual Symposium on Principles of Programming Languages (2001)Google Scholar
  24. 24.
    Stirling, C.: Modal and temporal properties of processes. Springer-Verlag New York, Inc. (2001)Google Scholar
  25. 25.
    Urquhart, A.: Semantics for Relevant Logics. Journal of Symbolic Logic 37(1) (1972)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2012

Authors and Affiliations

  • Radu Mardare
    • 1
  1. 1.Aalborg UniversityDenmark

Personalised recommendations