{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,1]],"date-time":"2026-04-01T13:24:33Z","timestamp":1775049873409,"version":"3.50.1"},"reference-count":41,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2009,3,13]],"date-time":"2009-03-13T00:00:00Z","timestamp":1236902400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Acta Informatica"],"published-print":{"date-parts":[[2009,4]]},"DOI":"10.1007\/s00236-009-0091-x","type":"journal-article","created":{"date-parts":[[2009,3,12]],"date-time":"2009-03-12T06:06:04Z","timestamp":1236837964000},"page":"87-137","source":"Crossref","is-referenced-by-count":20,"title":["A theory of structural stationarity in the \u03c0-Calculus"],"prefix":"10.1007","volume":"46","author":[{"given":"Roland","family":"Meyer","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2009,3,13]]},"reference":[{"issue":"1","key":"91_CR1","first-page":"70","volume":"9","author":"R.M. Amadio","year":"2002","unstructured":"Amadio R.M., Meyssonnier C.: On decidability of the control reachability problem in the asynchronous \u03c0-calculus. Nord. J. Comput. 9(1), 70\u2013101 (2002)","journal-title":"Nord. J. Comput."},{"key":"91_CR2","doi-asserted-by":"crossref","unstructured":"Bodei, C., Degano, P., Nielson, F., Riis Nielson, H.: Control flow analysis for the \u03c0-calculus. In: Proc. of the 9th International Conference on Concurrency Theory, CONCUR. LNCS, vol. 1466, pp. 84\u201398. Springer, Heidelberg (1998)","DOI":"10.1007\/BFb0055617"},{"key":"91_CR3","doi-asserted-by":"crossref","unstructured":"Busi, N., Gorrieri, R.: A Petri net semantics for \u03c0-calculus. In: Proc. of the 6th International Conference on Concurrency Theory, CONCUR. LNCS, vol. 962, pp. 145\u2013159. Springer, Heidelberg (1995)","DOI":"10.1007\/3-540-60218-6_11"},{"key":"91_CR4","unstructured":"Busi, N., Gorrieri, R.: Distributed semantics for the \u03c0-calculus based on Petri nets with inhibitor arcs. Journal of Logic and Algebraic Programming, 46\u00a0pp. (2008, to appear)"},{"issue":"1\u20132","key":"91_CR5","doi-asserted-by":"crossref","first-page":"127","DOI":"10.1016\/S0304-3975(01)00127-X","volume":"275","author":"N. Busi","year":"2002","unstructured":"Busi N.: Analysis issues in Petri nets with inhibitor arcs. Theor. Comput. Sci. 275(1\u20132), 127\u2013177 (2002)","journal-title":"Theor. Comput. Sci."},{"key":"91_CR6","doi-asserted-by":"crossref","unstructured":"Caires, L.: Behavioural and spatial observations in a logic for the \u03c0-Calculus. In: Proc. of the 7th International Conference on Foundations of Software Science and Computation Structures, FOSSACS. LNCS, vol. 2987, pp. 72\u201389. Springer, Heidelberg (2004) Spatial Logic Model Checker: http:\/\/ctp.di.fct.unl.pt\/SLMC\/","DOI":"10.1007\/978-3-540-24727-2_7"},{"issue":"2","key":"91_CR7","doi-asserted-by":"crossref","first-page":"194","DOI":"10.1016\/S0890-5401(03)00137-8","volume":"186","author":"L. Caires","year":"2003","unstructured":"Caires L., Cardelli L.: A spatial logic for concurrency (part I). Inf. Comput. 186(2), 194\u2013235 (2003)","journal-title":"Inf. Comput."},{"key":"91_CR8","doi-asserted-by":"crossref","unstructured":"Clarke, E. M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement. In: Proc. of the 12th International Conference on Computer Aided Verification, CAV. LNCS, vol. 1855, pp. 154\u2013169. Springer, Heidelberg (2000)","DOI":"10.1007\/10722167_15"},{"key":"91_CR9","volume-title":"Model Checking","author":"E. M. Clarke","year":"1999","unstructured":"Clarke E. M., Grumberg O., Peled D.: Model Checking. MIT Press, Cambridge (1999)"},{"issue":"1","key":"91_CR10","doi-asserted-by":"crossref","first-page":"35","DOI":"10.1006\/inco.1996.0072","volume":"129","author":"M. Dam","year":"1996","unstructured":"Dam M.: Model checking mobile processes. Inf. Comput. 129(1), 35\u201351 (1996)","journal-title":"Inf. Comput."},{"issue":"3","key":"91_CR11","first-page":"203","volume":"70","author":"R. Devillers","year":"2006","unstructured":"Devillers R., Klaudel H., Koutny M.: A Petri net semantics of the finite \u03c0-Calculus terms. Fundam. Inf. 70(3), 203\u2013226 (2006)","journal-title":"Fundam. Inf."},{"key":"91_CR12","doi-asserted-by":"crossref","unstructured":"Devillers, R., Klaudel, H., Koutny, M.: A Petri net translation of \u03c0-Calculus terms. In: Proc. of the 3rd International Colloquium on Theoretical Aspects of Computing, ICTAC. LNCS, vol. 4281, pp. 138\u2013152. Springer, Heidelberg (2006)","DOI":"10.1007\/11921240_10"},{"issue":"1-2","key":"91_CR13","doi-asserted-by":"crossref","first-page":"311","DOI":"10.1016\/S0304-3975(97)00179-5","volume":"211","author":"J. Engelfriet","year":"1999","unstructured":"Engelfriet J., Gelsema T.: Multisets and structural congruence of the pi-calculus with replication. Theor. Comput. Sci. 211(1-2), 311\u2013337 (1999)","journal-title":"Theor. Comput. Sci."},{"key":"91_CR14","unstructured":"Engelfriet, J., Gelsema, T.: The decidability of structural congruence for replication restricted pi-calculus processes. Technical report, Leiden Institute of Advanced Computer Science (2004). Revised 2005"},{"issue":"6","key":"91_CR15","first-page":"385","volume":"40","author":"J. Engelfriet","year":"2004","unstructured":"Engelfriet J., Gelsema T.: A new natural structural congruence in the pi-calculus with replication. Acta Inf. 40(6), 385\u2013430 (2004)","journal-title":"Acta Inf."},{"issue":"1","key":"91_CR16","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/j.ipl.2006.08.001","volume":"101","author":"J. Engelfriet","year":"2007","unstructured":"Engelfriet J., Gelsema T.: An exercise in structural congruence. Inf. Process. Lett. 101(1), 1\u20135 (2007)","journal-title":"Inf. Process. Lett."},{"issue":"1\u20132","key":"91_CR17","doi-asserted-by":"crossref","first-page":"65","DOI":"10.1016\/0304-3975(95)00118-2","volume":"153","author":"J. Engelfriet","year":"1996","unstructured":"Engelfriet J.: A multiset semantics for the pi-calculus with replication. Theor. Comput. Sci. 153(1\u20132), 65\u201394 (1996)","journal-title":"Theor. Comput. Sci."},{"issue":"3","key":"91_CR18","doi-asserted-by":"crossref","first-page":"285","DOI":"10.1023\/A:1014746130920","volume":"20","author":"J. Esparza","year":"2002","unstructured":"Esparza J., R\u00f6mer S., Vogler W.: An improvement of McMillan\u2019s unfolding algorithm. Formal Methods Syst. Des. 20(3), 285\u2013310 (2002)","journal-title":"Formal Methods Syst. Des."},{"key":"91_CR19","doi-asserted-by":"crossref","unstructured":"Esparza, J., Schr\u00f6ter, C.: Net reductions for LTL model-checking. In: Proc. of the 11th Advanced Research Working Conference on Correct Hardware Design and Verification Methods, CHARME. LNCS, vol. 2144, pp. 310\u2013324. Springer, Heidelberg (2001)","DOI":"10.1007\/3-540-44798-9_25"},{"issue":"2","key":"91_CR20","doi-asserted-by":"crossref","first-page":"85","DOI":"10.1007\/s002360050074","volume":"34","author":"J. Esparza","year":"1997","unstructured":"Esparza J.: Decidability of model checking for infinite-state concurrent systems. Acta Inf. 34(2), 85\u2013107 (1997)","journal-title":"Acta Inf."},{"issue":"1","key":"91_CR21","doi-asserted-by":"crossref","first-page":"13","DOI":"10.3233\/FI-1997-3112","volume":"31","author":"J. Esparza","year":"1997","unstructured":"Esparza J.: Petri Nets, commutative context-free grammars, and basic parallel processes. Fundam. Inf. 31(1), 13\u201325 (1997)","journal-title":"Fundam. Inf."},{"key":"91_CR22","unstructured":"Ferrari, G.-L., Gnesi, S., Montanari, U., Pistore, M.: A model-checking verification environment for mobile processes. ACM Trans. Softw. Eng. Methodol. 12(4):440\u2013473 (2003). HAL: http:\/\/fmt.isti.cnr.it:8080\/hal\/"},{"key":"91_CR23","doi-asserted-by":"crossref","unstructured":"Hsu, A., Eskafi, F., Sachs, S., Varaiya, P.: Design of platoon maneuver protocols for ivhs. Path research report, Institute of Transportation Studies, University of California, Berkeley (1991)","DOI":"10.23919\/ACC.1991.4791861"},{"issue":"2","key":"91_CR24","doi-asserted-by":"crossref","first-page":"281","DOI":"10.1016\/0304-3975(95)00037-W","volume":"148","author":"P. Jan\u010dar","year":"1995","unstructured":"Jan\u010dar P.: Undecidability of bisimilarity for Petri nets and some related problems. Theor. Comput. Sci. 148(2), 281\u2013301 (1995)","journal-title":"Theor. Comput. Sci."},{"key":"91_CR25","doi-asserted-by":"crossref","unstructured":"Khomenko, V.: Model Checking Based on Prefixes of Petri Net Unfoldings. PhD thesis, School of Computing Science, Newcastle University (2003)","DOI":"10.1007\/3-540-45657-0_49"},{"key":"91_CR26","unstructured":"Khomenko, V., Koutny, M., Niaouris, A.: Applying Petri net unfoldings for verification of mobile systems. In: Proc. of the 4th Workshop on Modelling of Objects, Components and Agents, MOCA. Bericht FBI-HH-B-267\/06, pp. 161\u2013178. University of Hamburg (2006)"},{"key":"91_CR27","unstructured":"Khomenko, V., Meyer, R.: Checking \u03c0-Calculus structural congruence is graph isomorphism complete. Technical Report CS-TR-1100, School of Computing Science, Newcastle University (2008). URL: http:\/\/www.cs.ncl.ac.uk\/publications\/trs\/abstract\/1100 ."},{"key":"91_CR28","doi-asserted-by":"crossref","unstructured":"McMillan, K.: Using unfoldings to avoid the state explosion problem in the verification of asynchronous circuits. In: Proc. of the 4th International Workshop on Computer Aided Verification, CAV. LNCS, vol. 663, pp. 164\u2013174. Springer, Heidelberg (1992)","DOI":"10.1007\/3-540-56496-9_14"},{"key":"91_CR29","doi-asserted-by":"crossref","unstructured":"Meyer, R.: On boundedness in depth in the \u03c0-calculus. In: Proc. of the 5th IFIP International Conference on Theoretical Computer Science, IFIP TCS. IFIP, vol. 273, pp. 477\u2013489. Springer, Heidelberg (2008)","DOI":"10.1007\/978-0-387-09680-3_32"},{"key":"91_CR30","volume-title":"Communicating and Mobile Systems: the \u03c0-Calculus","author":"R. Milner","year":"1999","unstructured":"Milner R.: Communicating and Mobile Systems: the \u03c0-Calculus. Cambridge University Press, London (1999)"},{"key":"91_CR31","doi-asserted-by":"crossref","unstructured":"Meyer, R., Khomenko, V., Strazny, T.: A practical approach to verification of mobile systems using net unfoldings. In: Proc. of the 29th International Conference on Application and Theory of Petri Nets and Other Models of Concurrency, ATPN. LNCS, vol. 5062, pp. 327\u2013347. Springer, Heidelberg (2008)","DOI":"10.1007\/978-3-540-68746-7_22"},{"key":"91_CR32","doi-asserted-by":"crossref","unstructured":"Montanari, U., Pistore, M.: Checking bisimilarity for finitary \u03c0-calculus. In: Proc. of the 6th International Conference on Concurrency Theory, CONCUR. LNCS, vol. 962, pp. 42\u201356. Springer, Heidelberg (1995)","DOI":"10.1007\/3-540-60218-6_4"},{"key":"91_CR33","doi-asserted-by":"crossref","first-page":"411","DOI":"10.1016\/S1571-0661(04)00024-6","volume":"1","author":"U. Montanari","year":"1995","unstructured":"Montanari U., Pistore M.: Concurrent semantics for the \u03c0-calculus. Electr. Notes Theor. Comput. Sci. 1, 411\u2013429 (1995)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"key":"91_CR34","unstructured":"Montanari, U., Pistore, M.: History dependent automata. Technical report, Instituto Trentino di Cultura (2001)"},{"key":"91_CR35","doi-asserted-by":"crossref","unstructured":"Olderog, E.-R.: Nets, Terms and Formulas: Three Views of Concurrent Processes and Their Relationship. Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, London (1991)","DOI":"10.1017\/CBO9780511526589"},{"key":"91_CR36","unstructured":"Pistore, M.: History Dependent Automata. PhD thesis, Dipartimento di Informatica, Universit\u00e0 di Pisa (1999)"},{"key":"91_CR37","doi-asserted-by":"crossref","unstructured":"Reisig, W.: Petri nets: an introduction. Monographs in Theoretical Computer Science. An EATCS Series. Springer, Heidelberg (1985)","DOI":"10.1007\/978-3-642-69968-9"},{"key":"91_CR38","unstructured":"Strazny, T., Meyer, R.: Petruchio homepage. http:\/\/petruchio.informatik.uni-oldenburg.de (2008)"},{"key":"91_CR39","unstructured":"Strazny, T.: Entwurf und Implementierung von Algorithmen zur Berechnung von Petrinetz-Semantiken f\u00fcr Pi-Kalk\u00fcl-Prozesse. Master\u2019s thesis, Department of Computing Science, University of Oldenburg (2007)"},{"key":"91_CR40","volume-title":"The \u03c0-calculus: a Theory of Mobile Processes","author":"D. Sangiorgi","year":"2001","unstructured":"Sangiorgi D., Walker D.: The \u03c0-calculus: a Theory of Mobile Processes. Cambridge University Press, London (2001)"},{"key":"91_CR41","doi-asserted-by":"crossref","unstructured":"Victor, B., Moller, F.: The mobility workbench: a tool for the \u03c0-calculus. In: Proc. of the 6th International Conference on Computer Aided Verification. LNCS, vol. 818, pp. 428\u2013440. Springer, Heidelberg (1994), Mobility Workbench: http:\/\/www.it.uu.se\/research\/group\/mobility\/mwb","DOI":"10.1007\/3-540-58179-0_73"}],"container-title":["Acta Informatica"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00236-009-0091-x.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00236-009-0091-x\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00236-009-0091-x","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,5,16]],"date-time":"2020-05-16T18:27:18Z","timestamp":1589653638000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s00236-009-0091-x"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009,3,13]]},"references-count":41,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2009,4]]}},"alternative-id":["91"],"URL":"https:\/\/doi.org\/10.1007\/s00236-009-0091-x","relation":{},"ISSN":["0001-5903","1432-0525"],"issn-type":[{"value":"0001-5903","type":"print"},{"value":"1432-0525","type":"electronic"}],"subject":[],"published":{"date-parts":[[2009,3,13]]}}}