Abstract
Traditionally, developers of concurrent systems have adopted two distinct approaches: those with truly concurrent semantics and those with interleaving semantics. In the coarser interleaving interpretation parallelism can be captured in terms of non-determinism whereas in the finer, truly concurrent interpretation it cannot. Thus processes a ∥ b and a.b + b.a are identified within the interleaving approach but distinguished within the truly concurrent approach.
In [5] we explored the truly concurrent notions of conflict, whereby transitions can occur individually but not together from a given state, and confusion, whereby the conflict set of a given transition is altered by the occurrence of another transition with which it does not interfere. We presented a translation from the truly concurrent formalism of Petri nets to the interleaving process algebra CSP and demonstrated how the CSP model-checker FDR can be used to detect the presence of both conflict and confusion in Petri nets. This work is of interest firstly because, to the author’s knowledge, no existing tool for Petri nets can perform these checks, and secondly (and perhaps more significantly) because we bridged the gap between truly concurrent and interleaving formalisms, demonstrating that true concurrency can be captured in what is typically considered to be an interleaving language.
In this paper we build on the work presented in [5] further embedding the truly concurrent notions of conflict and confusion in the interleaving formalism CSP by extending the domain of our translation from the simplistic subset of safe Petri nets, in which each place can hold at most one token, to standard Petri nets, in which the number of tokens in each place is unbounded.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Petri nets tool database. Available via, URL http://www.daimi.au.dk/PetriNets/tools/
Bergstra, J.A., Klop, J.W.: Algebra of communicating processes with abstraction. Theoretical Computer Science, vol. 37(1) (1985)
Best, E., de Boer, F.S., Palamidessi, C.: Partial order and sos semantics for linear constraint programs. In: Garlan, D., Le Métayer, D. (eds.) COORDINATION 1997. LNCS, vol. 1282, Springer, Heidelberg (1997)
Bolton, C.: On the Refinement of State-Based and Event-Based Models. D.Phil., University of Oxford (2002)
Bolton, C.: Adding conflict and confusion to CSP. In: Fitzgerald, J.A., Hayes, I.J., Tarlecki, A. (eds.) FM 2005. LNCS, vol. 3582, Springer, Heidelberg (2005)
Bolton, C., Lowe, G.: A hierarchy of failures-based models. In: Proceedings of the 10th International Workshop on Expressiveness in Concurrency: EXPRESS 2003 (2003)
Clarke, E., Grumberg, O., Peled, D.: Model-Checking. The MIT Press, Cambridge (1999)
Formal Systems (Europe) Ltd. Failures-Divergence Refinement FDR 2 User Manual, (1999) Available via URL: http://www.fsel.com/fdr2_manual.html
Goltz, U., Reisig, W.: CSP-programs as nets with individual tokens. In: Rozenberg, G. (ed.) Advances in Petri Nets 1984. LNCS, vol. 188, Springer, Heidelberg (1985)
Hoare, C.A.R.: Communicating Sequential Processes. Prentice-Hall, Englewood Cliffs (1985)
Kavi, K., Sheldon, F., Shirazzi, B., Hurson, A.: Reliability analysis of CSP specifications using petri nets and markov processes. In: Proceedings of 28th Annual Hawaii International Conference on System Sciences, IEEE, Los Alamitos (1995)
Lazic, R.: A Semantic Study of Data Independence with Applications to Model Checking. PhD thesis, University of Oxford (1999)
Mazurkiewicz, A.: Introduction to trace theory. In: Diekert, V., Rozenberg, G. (eds.) The book of traces, World Scientific, Singapore (1995)
Milner, R. (ed.): A Calculus of Communication Systems. LNCS, vol. 92. Springer, Heidelberg (1980)
Milner, R.: Communications and concurrency. Prentice-Hall, Englewood Cliffs (1989)
Olderog, E.-R.: Nets, Terms and Formulas: Three Views of Concurrent Processes and Their Relationship. Cambridge University Press, Cambridge (1991)
Petri, C.A.: Fundamentals of a theory of asynchronous information flow. In: Proceedings of IFIP, Congress 1962, pp. 386–390 (1962)
Pratt, V.: On the composition of processes. In: Proceedings of 1982 ACM Symposium on Principles of Programming Languages (POPL) (1982)
Reisig, W.: Petri Nets. Springer, Heidelberg (1982)
Reisig, W., Rozenberg, G.: Informal introduction to petri nets. LNCS, vol. 1491. Springer, Berlin Heidelberg (1998)
Roscoe, A.W.: The Theory and Practice of Concurrency. Prentice-Hall, Englewood Cliffs (1997)
Schreiber, G.: Functional equivalences of petri nets. In: DeMichelis, G., Díaz, M. (eds.) Application and Theory of Petri Nets 1995. LNCS, vol. 935, Springer, Heidelberg (1995)
Steiner, W., Rushby, J., Sorea, M., Pfeifer, H.: Model checking a faulttolerant startup algorithm: From design exploration to exhaustive fault simulation. In: Proceedings of Dependable Systems and Networks (DSN 2004) (2004)
Störrle, H.: An evaluation of high-end tools for petri-nets. Technical Report 9802, Ludwig-Maximilians-Universität München (1997)
Winskel, G.: Events in Computation. D.Phil, University of Edinburgh (1980)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Marr (née Bolton), C. (2007). Capturing Conflict and Confusion in CSP. In: Davies, J., Gibbons, J. (eds) Integrated Formal Methods. IFM 2007. Lecture Notes in Computer Science, vol 4591. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-73210-5_22
Download citation
DOI: https://doi.org/10.1007/978-3-540-73210-5_22
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-73209-9
Online ISBN: 978-3-540-73210-5
eBook Packages: Computer ScienceComputer Science (R0)