×

Constructing weak simulations from linear implications for processes with private names. (English) Zbl 1447.68008

The processes-as-formulae paradigm studies possibilities to regard processes – usually described as terms in some process algebra like the \(\pi\)-calculus – as formulae in some logical system with the aim of transferring principal results from one world to another.
The paper at hand studies logical implication between formulae obtained as translations of terms in the \(\pi\)-calculus (and an extension thereof). It shows that this pre-order is included in weak simulation, in fact even in a stronger form of weak simulation. Hence, logical implication can be regarded as a pre-order on processes. It thus strengthens the connection between the logical and the process-algebraic world.
The paper presupposes a fair amount of expertise in these areas. A beginner would most probably struggle with the density of information. It is advisable to first get acquainted with the fundamental tools of the \(\pi\)-calculus and linear logic at least, as the paper does not introduce these notions but instead expects the reader to be familiar not only with them but also – to some extent – with the interactions between them.

MSC:

68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
03B70 Logic in computer science
03F52 Proof-theoretic aspects of linear logic and other substructural logics
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Abramsky, S. (1994). Proofs as processes. Theoretical Computer Science135 (1) 5-9. · Zbl 0850.68297
[2] Ahn, K. Y., Horne, R. and Tiu, A. (2017). A characterisation of open bisimilarity using an intuitionistic modal logic. In: Meyer, R. and Ñestmann, U. (eds.) 28th International Conference on Concurrency Theory (CONCUR 2017), Leibniz International Proceedings in Informatics (LIPIcs), vol. 85, Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, 7:1-7:17. · Zbl 1442.68121
[3] Andreoli, J.-M. (1992). Logic programming with focusing proofs in linear logic. Journal of Logic and Computation2 (3) 297-347. · Zbl 0764.03020
[4] Bellin, G. and Scott, P. J. (1994). On the pi-calculus and linear logic. Theoretical Computer Science135 (1) 11-65. · Zbl 0817.03001
[5] Bengtson, J. and Parrow, J. (2009). Formalising the pi-calculus using nominal logic. Logical Methods in Computer Science5 (2), 1-36. · Zbl 1168.68030
[6] Bernardi, G. and Hennessy, M. (2013). Mutually testing processes. In: International Conference on Concurrency Theory, Lecture Notes in Computer Science, vol. 8052, Springer, pp. 61-75. · Zbl 1390.68459
[7] Brünnler, K. and Tiu, A. F. (2001). A local system for classical logic. In: Nieuwenhuis, R. and Voronkov, A. (eds.) Logic for Programming, Artificial Intelligence, and Reasoning, Lecture Notes in Computer Science, Springer, 347-361. · Zbl 1275.03150
[8] Bruscoli, P. (2002). A purely logical account of sequentiality in proof search. In: Logic Programming, 18th International Conference, ICLP 2002, Copenhagen, Denmark, July 29-August 1, Proceedings, Lecture Notes in Computer Science, vol. 2401, Springer, 302-316. · Zbl 1045.68033
[9] Caires, L., Pfenning, F. and Toninho, B. (2016). Linear logic propositions as session types. Mathematical Structures in Computer Science26 (3) 367-423. · Zbl 1361.68162
[10] Chaudhuri, K., Guenot, N. and Straßburger, L. (2011). The focused calculus of structures. In: Bezem, M. (ed.) Computer Science Logic (CSL 2011) - 25th International Workshop/20th Annual Conference of the EACSL, Leibniz International Proceedings in Informatics, vol. 12, Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, 159-173. · Zbl 1247.03117
[11] Ciobanu, G. and Horne, R. (2015). Behavioural analysis of sessions using the calculus of structures. In: Mazzara, M. and Voronkov, A. (eds.) Perspectives of System Informatics, Springer International Publishing, 91-106. · Zbl 1461.68129
[12] Deng, Y., Van Glabbeek, R., Hennessy, M., Morgan, C. and Zhang, C. (2007). Characterising testing preorders for finite probabilistic processes. In: 22nd Annual IEEE Symposium on Logic in Computer Science, LICS 2007, IEEE, 313-325. · Zbl 1161.68035
[13] Deniélou, P. and Yoshida, N. (2013). Multiparty compatibility in communicating automata: characterisation and synthesis of global session types. In: Automata, Languages, and Programming - 40th International Colloquium, ICALP 2013, Riga, Latvia, July 8-12, Springer, 174-186. · Zbl 1334.68149
[14] Gacek, A., Miller, D. and Nadathur, G. (2011). Nominal abstraction. Information and Computation209 (1) 48-73. · Zbl 1215.03049
[15] Girard, J.-Y. (1987). Linear logic. Theoretical Computer Science50 (1) 1-112. · Zbl 0625.03037
[16] Gischer, J. L. (1988). The equational theory of pomsets. Theoretical Computer Science61199-224. · Zbl 0669.68015
[17] Guglielmi, A. (2007). A system of interaction and structure. ACM Transactions on Computational Logic8 (1) 1-64. · Zbl 1367.03110
[18] Guglielmi, A. and Straßburger, L. (2001). Non-commutativity and MELL in the calculus of structures. In: Fribourg, L. (ed.) Computer Science Logic, Lecture Notes in Computer Science, Springer, 54-68. · Zbl 0999.03054
[19] Guglielmi, A. and Straßburger, L. (2011). A system of interaction and structure V: the exponentials and splitting. Mathematical Structures in Computer Science21 (03) 563-584. · Zbl 1232.03055
[20] Horne, R. (2015). The consistency and complexity of multiplicative additive system virtual. Scientific Annals of Computer Science25 (2) 245-316. · Zbl 1424.03057
[21] Horne, R., Mauw, S. and Tiu, A. (2017). Semantics for specialising attack trees based on linear logic. Fundamenta Informaticae15357-86. · Zbl 1382.68140
[22] Horne, R., Tiu, A., Aman, B. and Ciobanu, G. (2016). Private names in non-commutative logic. In: Desharnais, J. and agadeesan, R. (eds.) 27th International Conference on Concurrency Theory (CONCUR 2016), Leibniz International Proceedings in Informatics (LIPIcs), vol. 59, Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, 31:1-31:16. · Zbl 1392.68303
[23] Horne, R., Tiu, A., Aman, B. and Ciobanu, G. (2018). Polarised Nominal Quantifiers Model Private Names in Non-commutative Logic. Technical Report 1502. ISSN 1842-1490, extended version of above supporting submission to TOCL. http://iit.iit.tuiasi.ro/TR/reports/fml1502.pdf. · Zbl 1459.03090
[24] McDowell, R., Miller, D. and Palamidessi, C. (2003). Encoding transition systems in sequent calculus. Theoretical Computer Science294 (3) 411-437. · Zbl 1028.68095
[25] Miller, D. (1993). The pi-calculus as a theory in linear logic: preliminary results. In: Extensions of Logic Programming, Third International Workshop, ELP 1992, Bologna, Italy, February 26-28, 1992, Proceedings, Lecture Notes in Computer Science, vol. 660, Springer, 242-264.
[26] Miller, D., Nadathur, G., Pfenning, F. and Scedrov, A. (1991). Uniform proofs as a foundation for logic programming. Annals of Pure and Applied Logic51 (1) 125-157. · Zbl 0721.03037
[27] Miller, D. and Tiu, A. (2005). A proof theory for generic judgements. ACM Transactions on Computational Logic (TOCL)6 (4) 749-783. · Zbl 1367.03059
[28] Milner, R. (1989). Communication and Concurrency, Prentice-Hall International. · Zbl 0683.68008
[29] Milner, R., Parrow, J. and Walker, D. (1992). A calculus of mobile processes, I and II. Information and Computation100 (1) 1-77. · Zbl 0752.68037
[30] Pitts, A. (2003). Nominal logic, a first order theory of names and binding. Information and Computation186 (2) 165-193. · Zbl 1056.03014
[31] Retoré, C. (1997). Pomset logic: a non-commutative extension of classical linear logic. In: de Groote, P.Roger Hindley, J. (eds.) Typed Lambda Calculi and Applications, Lecture Notes in Computer Science, Springer, 300-318. · Zbl 1063.03536
[32] Roversi, L. (2016). A deep inference system with a self-dual binder which is complete for linear lambda calculus. Journal of Logic and Computation26 (2) 677. · Zbl 1403.03021
[33] Sangiorgi, D. (1996a). -calculus, internal mobility, and agent-passing calculi. Theoretical Computer Science167 (1) 235-274. · Zbl 0874.68103
[34] Sangiorgi, D. (1996b). A theory of bisimulation for the -calculus. Acta Informatica33 (1) 69-97. · Zbl 0835.68072
[35] Sassone, V., Nielsen, M. and Winskel, G. (1996). Models for concurrency: towards a classification. Theoretical Computer Science170 (1-2) 297-348. · Zbl 0874.68120
[36] Straßburger, L. and Guglielmi, A. (2011). A system of interaction and structure IV: the exponentials and decomposition. ACM Transactions on Computational Logic (TOCL)12 (4) 23. · Zbl 1370.03080
[37] Tiu, A. (2006). A system of interaction and structure II: the need for deep inference. Logical Methods in Computer Science2 (2:4) 1-24. · Zbl 1126.03051
[38] Tiu, A. and Miller, D. (2010). Proof search specifications of bisimulation and modal logics for the -calculus. ACM Transactions on Computational Logic11 (2) 13. · Zbl 1351.68186
[39] van Glabbeek, R. (1990). The linear time-branching time spectrum (extended abstract). In: CONCUR 1990, Amsterdam, The Netherlands, August 27-30, Lecture Notes in Computer Science, vol. 458, Springer, 278-297.
[40] van Glabbeek, R. and Goltz, U. (2001). Refinement of actions and equivalence notions for concurrent systems. Acta Informatica37 (4-5) 229-327. · Zbl 0969.68081
[41] van Glabbeek, R. and Vaandrager, F. (1987). Petri net models for algebraic theories of concurrency. In: de Bakker, J. W., Nijman, A. J. and Treleaven, P. C. (eds.) PARLE Parallel Architectures and Languages Europe, Lecture Notes in Computer Science, volume 259, Springer, 224-242. · Zbl 0633.68054
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.