The Expressive Power of Monotonic Parallel Composition
Pages 780 - 803
Abstract
We show a separation result between on the one hand models of concurrency that contain solutions to the consensus problem, where many identical concurrent processes must reach agreement; and on the other hand models with monotonic parallel composition, where processes always have the possibility to act independently of other processes in their environment. Our definitions and proofs are easy to instantiate in order to obtain particular separation results. We illustrate this point by strengthening several results from the literature, and proving some new ones. Highlights include a separation between unreliable and reliable broadcast $$\pi $$π, between the $$\rho $$ï ź-calculus and cc-pi, and between the full psi-calculi framework and its restriction to monotonic assertion logics.
References
[1]
Niehren, J., Smolka, G.: A confluent relational calculus for higher-order programming with constraints. In: Jouannaud, J.-P. ed. CCL 1994. LNCS, vol. 845, pp. 89---104. Springer, Heidelberg 1994
[2]
Victor, B., Parrow, J.: Concurrent constraints in the fusion calculus. In: Larsen, K.G., Skyum, S., Winskel, G. eds. ICALP 1998. LNCS, vol. 1443, pp. 455---469. Springer, Heidelberg 1998
[3]
Ene, C., Muntean, T.: Expressiveness of point-to-point versus broadcast communications. In: Ciobanu, G., Pă un, G. eds. FCT 1999. LNCS, vol. 1684, pp. 258---268. Springer, Heidelberg 1999
[4]
Cleaveland, R., Hennessy, M.: Priorities in process algebras. In: LICS, pp. 193---202. IEEE Computer Society 1988
[5]
Buscemi, M.G., Montanari, U.: CC-Pi: a constraint-based language for specifying service level agreements. In: De Nicola, R. ed. ESOP 2007. LNCS, vol. 4421, pp. 18---32. Springer, Heidelberg 2007
[6]
Hennessy, M., Regan, T.: A process algebra for timed systems. Inf. Comput. 117, 221---239 1995
[7]
Bengtson, J., Johansson, M., Parrow, J., Victor, B.: Psi-calculi: mobile processes, nominal data, and logic. In: Proceedings of LICS 2009, pp. 39---48. IEEE 2009
[8]
Phillips, I.: CCS with priority guards. In: Larsen, K.G., Nielsen, M. eds. CONCUR 2001. LNCS, vol. 2154, pp. 305---320. Springer, Heidelberg 2001
[9]
Versari, C., Busi, N., Gorrieri, R.: On the expressive power of global and local priority in process calculi. In: Caires, L., Vasconcelos, V.T. eds. CONCUR 2007. LNCS, vol. 4703, pp. 241---255. Springer, Heidelberg 2007
[10]
Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle/HOL: a Proof Assistant for Higher-Order Logic. Lecture Notes in Computer Science, vol. 2283. Springer, Heidelberg 2002
[11]
Åman Pohjola, J.: The expressive power of monotonic parallel composition. http://www.it.uu.se/research/group/mobility/theorem/monopar.tgz. Isabelle 2014/HOL formalisation of the definitions, theorems and proofs
[12]
Bougé, L.: On the existence of symmetric algorithms to find leaders in networks of communicating sequential processes. Acta Inf. 25, 179---201 1988
[13]
Palamidessi, C.: Comparing the expressive power of the synchronous and the asynchronous $$\pi $$π-calculus. In: Proceedings of the 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. POPL 1997, 256---265. ACM, New York 1997
[14]
Fischer, M.J., Lynch, N.A., Paterson, M.S.: Impossibility of distributed consensus with one faulty process. J. ACM 32, 374---382 1985
[15]
Prasad, K.V.S.: A calculus of broadcasting systems. Science of Computer Programming 25, 285---327 1995
[16]
Gorla, D.: Towards a Unified Approach to Encodability and Separation Results for Process Calculi. In: van Breugel, F., Chechik, M. eds. CONCUR 2008. LNCS, vol. 5201, pp. 492---507. Springer, Heidelberg 2008
[17]
Merro, M.: An observational theory for mobile ad hoc networks full version. J. Inf. Comput. 207, 194---208 2009
[18]
Borgström, J., Huang, S., Johansson, M., Raabjerg, P., Victor, B., Åman Pohjola, J., Parrow, J.: Broadcast Psi-calculi with an application to wireless protocols. In: Barthe, G., Pardo, A., Schneider, G. eds. SEFM 2011. LNCS, vol. 7041, pp. 74---89. Springer, Heidelberg 2011
[19]
Fehnker, A., van Glabbeek, R.J., Höfner, P., McIver, A., Portmann, M., Tan, W.L.: A process algebra for wireless mesh networks used for modelling, verifying and analysing AODV. CoRR abs/1312.7645 2013
[20]
Ene, C., Muntean, T.: A broadcast-based calculus for communicating systems. In: Proceedings of the 15th International Parallel & Distributed Processing Symposium, IPDPS 2001, Computer Society, p. 149. IEEE, Washington, DC 2001
[21]
Johansson, M., Bengtson, J., Parrow, J., Victor, B.: Weak equivalences in Psi-calculi. In: LICS, pp. 322---331. IEEE Computer Society 2010
[22]
Åman Pohjola, J., Parrow, J.: Priorities without priorities: representing preemption in Psi-calculi. In: Borgström, J., Crafa, S. eds. Proceedings Combined 21st International Workshop on Expressiveness in Concurrency, EXPRESS 2014, and 11th Workshop on Structural Operational Semantics, SOS 2014, Rome, Italy, 1st. vol. 160, EPTCS, 2---15 September 2014
[23]
Gardner, P., Wischik, L.: Explicit fusions. In: Nielsen, M., Rovan, B. eds. MFCS 2000. LNCS, vol. 1893, pp. 373---382. Springer, Heidelberg 2000
[24]
Milner, R.: Calculi for synchrony and asynchrony. Theor. Comput. Sci. 25, 267---310 1983
[25]
Holmer, U.: Interpreting broadcast communication in SCCS. In: Best, E. ed. CONCUR 1993. LNCS, vol. 715, pp. 188---201. Springer, Heidelberg 1993
[26]
Corradini, F., D'Ortenzio, D., Inverardi, P.: On the relationships among four timed process algebras. Fundam. Inf. 38, 377---395 1999
[27]
Moller, F., Tofts, C.: Relating processes with respect to speed. In: Baeten, J.C., Groote, J.F. eds. CONCUR '91. Lecture Notes in Computer Science, vol. 527, pp. 424---438. Springer, Berlin Heidelberg 1991
[28]
Lochbihler, A.: Coinductive. Archive of Formal Proofs 2010 2010
[29]
Ballarin, C.: Locales: a module system for mathematical theories. J. Autom. Reasoning 52, 123---153 2014
[30]
Palamidessi, C.: Comparing the expressive power of the synchronous and asynchronous pi-calculi. Math. Struct. Comput. Sci. 13, 685---719 2003
[31]
Peters, K., Nestmann, U.: Breaking symmetries. In: Fröschle, S.B., Valencia, F.D. eds. Proceedings 17th International Workshop on Expressiveness in Concurrency, EXPRESS 2010, Paris, France, 30 August 2010, vol. 41, pp. 136---150. EPTCS 2010
[32]
Prasad, K.V.S.: Broadcast calculus interpreted in CCS upto bisimulation. Electr. Notes Theor. Comput. Sci. 52, 83---100 2001
[33]
Peters, K., Nestmann, U., Goltz, U.: On distributability in process calculi. In: Felleisen, M., Gardner, P. eds. ESOP 2013. LNCS, vol. 7792, pp. 310---329. Springer, Heidelberg 2013
- The Expressive Power of Monotonic Parallel Composition
Recommendations
BTL2 and the expressive power of ECTL+
We show that ECTL+, the classical extension of CTL with fairness properties, is expressively equivalent to BTL2, a natural fragment of the monadic logic of order. BTL2 is the branching-time logic with arbitrary quantification over paths, and where path ...
First-Order Ground Non-Monotonic Modal Logic
We study the extension of propositional ground non-monotonic modal logic to the firstorder case. We show that first-order ground non-monotonic modal logic well complies with first-order default logic by interpreting the latter in the former by the ...
On Expressive Description Logics with Composition of Roles in Number Restrictions
LPAR '02: Proceedings of the 9th International Conference on Logic for Programming, Artificial Intelligence, and ReasoningDescription Logics are knowledge representation formalisms which have been used in a wide range of application domains. Owing to their appealing expressiveness, we consider in this paper extensions of the well-known concept language ALC allowing for ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
Publisher
Springer-Verlag
Berlin, Heidelberg
Publication History
Published: 02 April 2016
Qualifiers
- Article
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- 0Total Citations
- 0Total Downloads
- Downloads (Last 12 months)0
- Downloads (Last 6 weeks)0
Reflects downloads up to 17 Nov 2024
Other Metrics
Citations
View Options
View options
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in