@inproceedings(BezemG94,
 author       = {Marc Bezem and Jan Friso Groote},
 year         = {1994},
 title        = {Invariants in Process Algebra with Data},
 editor       = {Bengt Jonsson and Joachim Parrow},
 booktitle    = {{CONCUR}},
 series       = {LNCS},
 volume       = {836},
 publisher    = {Springer},
 pages        = {401--416},
 doi          = {10.1007/978-3-540-48654-1\_30},
)
@inproceedings(BouvierGL20,
 author       = {Pierre Bouvier and Hubert Garavel and Hern{\'{a}}n Ponce de Le{\'{o}}n},
 year         = {2020},
 title        = {Automatic Decomposition of Petri Nets into Automata Networks - {A} Synthetic Account},
 editor       = {Ryszard Janicki and Natalia Sidorova and Thomas Chatain},
 booktitle    = {Application and Theory of Petri Nets and Concurrency - 41st International Conference, {PETRI} {NETS} 2020, Paris, France, June 24-25, 2020, Proceedings},
 series       = {Lecture Notes in Computer Science},
 volume       = {12152},
 publisher    = {Springer},
 pages        = {3--23},
 doi          = {10.1007/978-3-030-51831-8\_1},
)
@inproceedings(BrinksmaLB93,
 author       = {Ed Brinksma and Rom Langerak and Peter Broekroelofs},
 year         = {1993},
 title        = {Functionality Decomposition by Compositional Correctness Preserving Transformation},
 editor       = {Costas Courcoubetis},
 booktitle    = {CAV},
 series       = {LNCS},
 volume       = {697},
 publisher    = {Springer},
 pages        = {371--384},
 doi          = {10.1007/3-540-56922-7\_31},
)
@inproceedings(BunteGKLNVWWW19,
 author       = {Olav Bunte and Jan Friso Groote and Jeroen J. A. Keiren and Maurice Laveaux and Thomas Neele and Erik P. de Vink and Wieger Wesselink and Anton Wijs and Tim A. C. Willemse},
 year         = {2019},
 title        = {The mCRL2 Toolset for Analysing Concurrent Systems - Improvements in Expressivity and Usability},
 editor       = {Tom{\'{a}}s Vojnar and Lijun Zhang},
 booktitle    = {TACAS},
 series       = {LNCS},
 volume       = {11428},
 publisher    = {Springer},
 pages        = {21--39},
 doi          = {10.1007/978-3-030-17465-1\_2},
)
@article(CheungK96,
 author       = {Shing{-}Chi Cheung and Jeff Kramer},
 year         = {1996},
 title        = {Context Constraints for Compositional Reachability Analysis},
 journal      = {{ACM} Trans. Softw. Eng. Methodol.},
 volume       = {5},
 number       = {4},
 pages        = {334--377},
 doi          = {10.1145/235321.235323},
)
@inproceedings(CrouzenL11,
 author       = {Pepijn Crouzen and Fr{\'{e}}d{\'{e}}ric Lang},
 year         = {2011},
 title        = {Smart Reduction},
 booktitle    = {{FASE}},
 series       = {Lecture Notes in Computer Science},
 volume       = {6603},
 publisher    = {Springer},
 pages        = {111--126},
 doi          = {10.1007/978-3-642-19811-3\_9},
)
@inproceedings(GaravelLM18,
 author       = {Hubert Garavel and Fr{\'{e}}d{\'{e}}ric Lang and Laurent Mounier},
 year         = {2018},
 title        = {Compositional Verification in Action},
 editor       = {Falk Howar and Jiri Barnat},
 booktitle    = {FMICS},
 series       = {LNCS},
 volume       = {11119},
 publisher    = {Springer},
 pages        = {189--210},
 doi          = {10.1007/978-3-030-00244-2\_13},
)
@article(GlabbeekLT09,
 author       = {R. J. van Glabbeek and B. Luttik and Tr\u{c}ka, N.},
 year         = {2009},
 title        = {Branching Bisimilarity with Explicit Divergence},
 journal      = {Fundam. Inform.},
 volume       = {93},
 number       = {4},
 pages        = {371--392},
 doi          = {10.3233/FI-2009-109},
)
@article(GrafSL96,
 author       = {Susanne Graf and Bernhard Steffen and Gerald L{\"{u}}ttgen},
 year         = {1996},
 title        = {Compositional Minimisation of Finite State Systems Using Interface Specifications},
 journal      = {Formal Asp. Comput.},
 volume       = {8},
 number       = {5},
 pages        = {607--616},
 doi          = {10.1007/BF01211911},
)
@inproceedings(GrooteM92,
 author       = {Jan Friso Groote and Faron Moller},
 year         = {1992},
 title        = {Verification of Parallel Systems via Decomposition},
 editor       = {Rance Cleaveland},
 booktitle    = {{CONCUR}},
 series       = {LNCS},
 volume       = {630},
 publisher    = {Springer},
 pages        = {62--76},
 doi          = {10.1007/BFb0084783},
)
@book(GrooteM2014,
 author       = {Jan Friso Groote and Mohammad Reza Mousavi},
 year         = {2014},
 title        = {Modeling and Analysis of Communicating Systems},
 publisher    = {{MIT} Press},
 doi          = {10.7551/mitpress/9946.001.0001},
)
@article(Hesselink98,
 author       = {Wim H. Hesselink},
 year         = {1998},
 title        = {Invariants for the Construction of a Handshake Register},
 journal      = {Inf. Process. Lett.},
 volume       = {68},
 number       = {4},
 pages        = {173--177},
 doi          = {10.1016/S0020-0190(98)00158-6},
)
@article(JongmansCP16,
 author       = {Sung{-}Shik T. Q. Jongmans and Dave Clarke and Proen{\c{c}}a, Jos{\'{e}}},
 year         = {2016},
 title        = {A procedure for splitting data-aware processes and its application to coordination},
 journal      = {Sci. Comput. Program.},
 volume       = {115-116},
 pages        = {47--78},
 doi          = {10.1016/j.scico.2014.02.017},
)
@article(artifact,
 author       = {M. Laveaux},
 year         = {2021},
 title        = {Downloadable sources for the case study},
 doi          = {10.5281/zenodo.5091850},
)
@article(Laveaux20,
 author       = {Maurice Laveaux and Tim A. C. Willemse},
 year         = {2020},
 title        = {Decompositional Minimisation of Monolithic Processes},
 journal      = {CoRR},
 volume       = {abs/2012.06468},
 url          = {https://arxiv.org/abs/2012.06468},
)
@article(Milner83,
 author       = {Robin Milner},
 year         = {1983},
 title        = {Calculi for Synchrony and Asynchrony},
 journal      = {Theor. Comput. Sci.},
 volume       = {25},
 pages        = {267--310},
 doi          = {10.1016/0304-3975(83)90114-7},
)
@inproceedings(PolT09,
 author       = {Jaco van de Pol and Mark Timmer},
 year         = {2009},
 title        = {State Space Reduction of Linear Processes Using Control Flow Reconstruction},
 editor       = {Zhiming Liu and Anders P. Ravn},
 booktitle    = {Automated Technology for Verification and Analysis, 7th International Symposium, {ATVA} 2009, Macao, China, October 14-16, 2009. Proceedings},
 series       = {Lecture Notes in Computer Science},
 volume       = {5799},
 publisher    = {Springer},
 pages        = {54--68},
 doi          = {10.1007/978-3-642-04761-9\_5},
)
@inproceedings(RemenskaWVFTB12,
 author       = {Daniela Remenska and Tim A. C. Willemse and Kees Verstoep and Wan J. Fokkink and Jeff Templon and Henri E. Bal},
 year         = {2012},
 title        = {Using Model Checking to Analyze the System Behavior of the {LHC} Production Grid},
 booktitle    = {12th {IEEE/ACM} International Symposium on Cluster, Cloud and Grid Computing, CCGrid 2012, Ottawa, Canada, May 13-16, 2012},
 publisher    = {{IEEE} Computer Society},
 pages        = {335--343},
 doi          = {10.1109/CCGrid.2012.90},
)
@inproceedings(RomijnS98,
 author       = {Judi Romijn and Jan Springintveld},
 year         = {1998},
 title        = {Exploiting Symmetry in Protocol Testing},
 editor       = {Stanislaw Budkowski and Ana R. Cavalli and Elie Najm},
 booktitle    = {{FORTE} {XI} / {PSTV} XVIII},
 series       = {{IFIP} Conference Proceedings},
 volume       = {135},
 publisher    = {Kluwer},
 pages        = {337--352},
 doi          = {10.1007/978-0-387-35394-4\_29},
)
@inproceedings(TaiK93:hierarchy,
 author       = {Kuo{-}Chung Tai and Pramod V. Koppol},
 year         = {1993},
 title        = {Hierarchy-based incremental analysis of communication protocols},
 booktitle    = {ICNP},
 publisher    = {{IEEE} Computer Society},
 pages        = {318--325},
 doi          = {10.1109/ICNP.1993.340896},
)
@inproceedings(TaiK93:incremental,
 author       = {Kuo{-}Chung Tai and Pramod V. Koppol},
 year         = {1993},
 title        = {An Incremental Approach to Reachability Analysis of Distributed Programs},
 editor       = {Jack C. Wileden},
 booktitle    = {IWSSD},
 publisher    = {{IEEE} Computer Society},
 pages        = {141--151},
 doi          = {10.1109/IWSSD.1993.315504},
)