Hostname: page-component-78c5997874-8bhkd Total loading time: 0 Render date: 2024-11-19T07:19:04.376Z Has data issue: false hasContentIssue false
  • English
  • Français

On the expressive power of process interruption and compensation

Published online by Cambridge University Press:  01 June 2009

MARIO BRAVETTI  and
GIANLUIGI ZAVATTARO
MARIO BRAVETTI
Affiliation:
Department of Computer Science, Università di Bologna Email: [email protected], [email protected]
GIANLUIGI ZAVATTARO
Affiliation:
Department of Computer Science, Università di Bologna Email: [email protected], [email protected]
Get access Rights & Permissions [Opens in a new window]

Abstract

The investigation into the foundational aspects of linguistic mechanisms for programming long-running transactions (such as the scope operator of WS-BPEL) has recently renewed the interest in process algebraic operators that, due to the occurrence of a failure, interrupt the execution of one process, replacing it with another one called the failure handler. We investigate the decidability of termination problems for two simple fragments of CCS (one with recursion and one with replication) extended with one of two such operators, the interrupt operator of CSP and the try-catch operator for exception handling. More precisely, we consider the existential termination problem (existence of one terminated computation) and the universal termination problem (all computations terminate). We prove that, as far as the decidability of the considered problems is concerned, under replication there is no difference between interrupt and try-catch (universal termination is decidable while existential termination is not), while under recursion this is not the case (existential termination is undecidable while universal termination is decidable only for interrupt). As a consequence of our undecidability results, we show the existence of an expressiveness gap between a fragment of CCS and its extension with either the interrupt or the try-catch operator.

Type
Paper
Information
Mathematical Structures in Computer Science , Volume 19 , Issue 3 , June 2009 , pp. 565 - 599
Copyright
Copyright © Cambridge University Press 2009

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

Baeten, J. C. M., Basten, T. and Reniers, M. A. (2008) Process algebra (equational theories of communicating processes), Cambridge Tracts in Theoretical Computer Science, Cambridge University Press.Google Scholar
Baeten, J. C. M. and Bergstra, J. A. (2000) Mode transfer in process algebra. Report CSR 00-01, Technische Universiteit Eindhoven. (This paper is an expanded and revised version of: Bergstra, J. (2000) A mode transfer operator in process algebra, Report P8808, Programming Research Group, University of Amsterdam, which is available at http://alexandria.tue.nl/extra1/wskrap/publichtml/200010731.pdf.)Google Scholar
Bocchi, L., Laneve, C. and Zavattaro, G. (2003) A calculus for long running transactions. In: FMOODS'03: Proceedings of the 6th IFIP International Conference on Formal Methods for Open Object-based Distributed Systems. Springer-Verlag Lecture Notes in Computer Science 2884 124–138.Google Scholar
Boreale, M., Bruni, R., Caires, L., De Nicola, R., Lanese, I., Loreti, M., Martins, F., Montanari, U., Ravara, A., Sangiorgi, D., Vasconcelos, V. T. and Zavattaro, G. (2006) SCC: A Service Centered Calculus. In: WS-FM 2006: Proceedings of the Third International Workshop on Web Services and Formal Methods. Springer-Verlag Lecture Notes in Computer Science 4184 38–57.CrossRefGoogle Scholar
Bruni, R., Melgratti, H. C. and Montanari, U. (2004) Nested Commits for Mobile Calculi: Extending Join. In: TCS 2004: IFIP 18th World Computer Congress, TC1 3rd International Conference on Theoretical Computer Science, Kluwer 563–576.Google Scholar
Bruni, R., Melgratti, H. C. and Montanari, U. (2005) Theoretical foundations for compensations in flow composition languages. In: POPL 2005: Proceedings of the 32nd Symposium on Principles of Programming Languages, ACM Press 209–220.Google Scholar
Busi, N., Gabbrielli, M. and Zavattaro, G. (2003) Replication vs. Recursive Definitions in Channel Based Calculi. In: ICALP'03: Proceedings of 30th International Colloquium on Automata, Languages and Programming. Springer-Verlag Lecture Notes in Computer Science 2719 133–144.Google Scholar
Busi, N., Gabbrielli, M. and Zavattaro, G. (2009) On the Expressive Power of Recursion, Replication and Iteration in Process Calculi. Mathematical Structures in Computer Science (to appear). (This is an extended version of Busi et al. (2003).)Google Scholar
Butler, M. and Ferreira, C. (2004) An operational semantics for StAC, a language for modelling long-running business transactions. In: COORDINATION'04: Proceedings of the 6th International Conference on Coordination Models and Languages. Springer-Verlag Lecture Notes in Computer Science 2949 87–104.Google Scholar
Butler, M., Hoare, C. A. R. and Ferreira, C. (2003) A trace semantics for long-running transactions. Springer-Verlag Lecture Notes in Computer Science 3525 133–150.CrossRefGoogle Scholar
Esparza, J. and Nielsen, M. (1994) Decidability Issues for Petri Nets-a Survey. Bulletin of the European Association for TCS 52 245–262.Google Scholar
Finkel, A. and Schnoebelen, P. (2001) Well-Structured Transition Systems Everywhere! Theoretical Computer Science 256 63–92.CrossRefGoogle Scholar
Goltz, U. (1988) On Representing CCS Programs by Finite Petri Nets. In: MFCS'88: Proceedings of Mathematical Foundations of Computer Science. Springer-Verlag Lecture Notes in Computer Science 324 339–350.Google Scholar
Guidi, C., Lanese, I., Montesi, F. and Zavattaro, G. (2008) On the Interplay between Fault Handling and Request-Response Service Invocations. In: ACSD'08: Proceedings of 8th International Conference on Application of Concurrency to System Design, IEEE Computer Society press 190–199.Google Scholar
Higman, G. (1952) Ordering by divisibility in abstract algebras. Proc. London Math. Soc. 2 236–366.Google Scholar
Hoare, C. A. R. (1985) Communicating Sequential Processes, Prentice-Hall.Google Scholar
Kruskal, J. B. (1960) Well-Quasi-Ordering, The Tree Theorem, and Vazsonyi's Conjecture. Transactions of the American Mathematical Society 95 (2)210–225.Google Scholar
Laneve, C. and Zavattaro, G. (2005) Foundations of web transactions. In: FOSSACS 2005: Proceedings of the 8th International Conference on Foundations of Software Science and Computational Structures. Springer-Verlag Lecture Notes in Computer Science 3441 282–298.Google Scholar
Lapadula, A., Pugliese, R. and Tiezzi, F. (2007) A Calculus for Orchestration of Web Services. In: ESOP 2007: Proceedings of 16th European Symposium on Programming. Springer-Verlag Lecture Notes in Computer Science 4421 33–47.CrossRefGoogle Scholar
Milner, R. (1989) Communication and Concurrency, Prentice-Hall.Google Scholar
Milner, R., Parrow, J. and Walker, D. (1992) A Calculus of Mobile Processes, Part I + II. Information and Computation 100 (1)1–77.Google Scholar
Minsky, M. L. (1967) Computation: finite and infinite machines, Prentice-Hall.Google Scholar
Misra, J. and Cook, W. R. (2007) Computation Orchestration. Journal of Software and System Modeling 6 (1)83–110.CrossRefGoogle Scholar
OASIS (2003) WS-BPEL: Web Services Business Process Execution Language Version 2.0. Technical report, OASIS, 2003.Google Scholar
Palamidessi, C. (2003) Comparing the expressive power of the synchronous and asynchronous pi-calculus. Mathematical Structures in Computer Science 13 (5)685–719. (A short version of this paper appeared in POPL'97.)Google Scholar
Shepherdson, J. C. and Sturgis, J. E. (1963) Computability of recursive functions. Journal of the ACM 10 217–255.CrossRefGoogle Scholar
Simpson, S. G. (1985) Nonprovability of certain combinatorial properties of finite trees. In: Harvey Friedman's Research on the Foundations of Mathematics, North-Holland 87–117.CrossRefGoogle Scholar
Vieira, H. T., Caires, L. and Seco, J. C. (2008) The Conversation Calculus: A Model of Service-Oriented Computation. In: ESOP 2008: Proceedings of 17th European Symposium on Programming. Springer-Verlag Lecture Notes in Computer Science 4960 269–283.Google Scholar
W3C (2004) WS-CDL: Web Services Choreography Description Language. Technical report, W3C.Google Scholar