Untanglings: a novel approach to analyzing concurrent systems. (English) Zbl 1347.68272

Summary: Substantial research efforts have been expended to deal with the complexity of concurrent systems that is inherent to their analysis, e.g., works that tackle the well-known state space explosion problem. Approaches differ in the classes of properties that they are able to suitably check and this is largely a result of the way they balance the trade-off between analysis time and space employed to describe a concurrent system. One interesting class of properties is concerned with behavioral characteristics. These properties are conveniently expressed in terms of computations, or runs, in concurrent systems. This article introduces the theory of untanglings that exploits a particular representation of a collection of runs in a concurrent system. It is shown that a representative untangling of a bounded concurrent system can be constructed that captures all and only the behavior of the system. Representative untanglings strike a unique balance between time and space, yet provide a single model for the convenient extraction of various behavioral properties. Performance measurements in terms of construction time and size of representative untanglings with respect to the original specifications of concurrent systems, conducted on a collection of models from practice, confirm the scalability of the approach. Finally, this article demonstrates practical benefits of using representative untanglings when checking various behavioral properties of concurrent systems.


68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)


Full Text: DOI Link


[1] Best, E; Desel, J, Partial order behaviour and structure of Petri nets, Form Asp Comput, 2, 123-138, (1990) · Zbl 0697.68061
[2] Desel J, Esparza J (1995) Free choice Petri nets. Cambridge tracts in theoretical computer science, vol 40. Cambridge University Press, Cambridge · Zbl 0836.68074
[3] Desel J (2000) Validation of process models by construction of process nets. In: Business process management (BPM). LNCS, vol 1806. Springer, Berlin, pp 110-128 · Zbl 0874.68120
[4] Esparza J, Heljanko K (2008) Unfoldings: a partial-order approach to model checking. Monographs in theoretical computer science. An EATCS series. Springer, Berlin · Zbl 1153.68035
[5] Esparza, J; Römer, S; Vogler, W, An improvement of mcmillan’s unfolding algorithm, Form Methods Syst Des, 20, 285-310, (2002) · Zbl 1017.68085
[6] Fahland D (2010) From Scenarios to Components. PhD thesis, Humboldt-Universität zu Berlin, Berlin, Germany
[7] Fahland, D; Favre, C; Koehler, J; Lohmann, N; Völzer, H; Wolf, K, Analysis on demand: instantaneous soundness checking of industrial business process models, Data Knowl Eng, 70, 448-466, (2011)
[8] Goltz, U; Reisig, W, The non-sequential behavior of Petri nets, Inf Control (IANDC), 57, 125-147, (1983) · Zbl 0551.68050
[9] Godefroid, P; Wolper, P, Using partial orders for the efficient verification of deadlock freedom and safety properties, Form Methods Syst Des, 2, 149-164, (1993) · Zbl 0772.68064
[10] Hack M (1975) Decidability questions for Petri nets. Outstanding dissertations in the computer sciences. Garland Publishing, New York
[11] Khomenko V (2003) Model checking based on prefixes of Petri net unfoldings. PhD thesis, University of Newcastle upon Tyne, School of Computing Science, Newcastle upon Tyne, UK · Zbl 1072.68072
[12] Khomenko, V; Kondratyev, A; Koutny, M; Vogler, W, Merged processes: a new condensed representation of Petri net behaviour, Acta Informatica, 43, 307-330, (2006) · Zbl 1104.68072
[13] Khomenko V, Mokhov A (2011) An algorithm for direct construction of complete merged processes. In: Petri nets. LNCS, vol 6709. Springer, Berlin, pp 89-108 · Zbl 1330.68206
[14] Lee, EA; Sangiovanni-Vincentelli, AL, A framework for comparing models of computation, IEEE Trans Comput Aided Des Integr Circuits Syst, 17, 1217-1229, (1998)
[15] McMillan KL (1992) Using unfoldings to avoid the state explosion problem in the verification of asynchronous circuits. In: Computer aided verification (CAV). LNCS, vol 663. Springer, Berlin, pp 164-177 · Zbl 0452.68067
[16] McMillan, KL, A technique of state space search based on unfolding, Form Methods Syst Des, 6, 45-65, (1995) · Zbl 0829.68085
[17] Melzer S, Römer S (1997) Deadlock checking using net unfoldings. In: Computer aided verification (CAV). LNCS, vol 1254. Springer, Berlin, pp 352-363
[18] Murata, T, Petri nets: properties, analysis and applications, Proc IEEE, 77, 541-580, (1989)
[19] Nielsen, M; Plotkin, GD; Winskel, G, Petri nets, event structures and domains, Part I. Theor Comput Sci, 13, 85-108, (1981) · Zbl 0452.68067
[20] Petri CA (1977) Non-sequential processes. Translation of a Lecture given at the IMMD Jubilee Colloquium on “Parallelism in Computer Science”, Unversität Erlangen-Nürnberg. Translated by Philip Krause and John Low, Petri, CA, St. Augustin: Gesellschaft fnr Mathematik und Datenverarbeitung Bonn, Interner Bericht ISF-77-5 · Zbl 0551.68050
[21] Polyvyanyy A, La Rosa M, ter Hofstede AHM (2014) Indexing and efficient instance-based retrieval of process models using untanglings. In: Advanced information systems engineering (CAiSE). LNCS, vol 8484. Springer International Publishing, Berlin, pp 439-456
[22] Pnueli A (1977) The temporal logic of programs. In: annual symposium on foundations of computer science (FOCS). IEEE Computer Society, pp 46-57 · Zbl 0697.68061
[23] Polyvyanyy A, Weidlich M (2013) Towards a compendium of process technologies: the jBPT library for process model analysis. In: CAiSE forum. CEUR workshop proceedings, vol 998. CEUR-WS.org, pp 106-113
[24] Polyvyanyy A, Weidlich M, Conforti R, La Rosa M, ter Hofstede AHM (2014) The 4C spectrum of fundamental behavioral relations for concurrent systems. In: Petri nets. LNCS, vol 8489. Springer International Publishing, Berlin, pp 210-232 · Zbl 1393.68123
[25] Rackoff, C, The covering and boundedness problems for vector addition systems, Theor Comput Sci, 6, 223-231, (1978) · Zbl 0368.68054
[26] Reisig W(2013) Understanding Petri nets: modeling techniques, analysis methods, case studies. Springer, Berlin · Zbl 1278.68222
[27] Rodríguez C, Schwoon S, Khomenko V. (2013) Contextual merged processes. In: Petri nets. LNCS, vol 7927. Springer, Berlin, pp 29-48 · Zbl 1381.68216
[28] Sassone, V; Nielsen, M; Winskel, G, Models for concurrency: towards a classification, Theor Comput Sci, 170, 297-348, (1996) · Zbl 0874.68120
[29] Tarasyuk IV (1997) Equivalence notions for models of concurrent and distributed systems. PhD thesis, A.P. Ershov Institute of Informatics Systems, Siberian Division of the Russian Academy of Sciences, Novosibirsk, Russia
[30] van der Aalst WMP (1997) Verification of workflow nets. In: Petri nets. LNCS, vol 1248. Springer, Berlin, pp 407-426 · Zbl 0874.68120
[31] van Glabbeek RJ, Vaandrager FW (1987) Petri net models for algebraic theories of concurrency. In: Parallel architectures and languages Europe (PARLE). LNCS, vol 259. Springer, Berlin, pp 224-242 · Zbl 0697.68061
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. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.