Abstract
One of the biggest challenges in model checking complex systems is the state space explosion problem. A well known technique to reduce the impact of this problem is compositional minimisation. In this technique, first the state spaces of all components are computed and minimised modulo some behavioural equivalence (e.g., some form of bisimilarity). These minimised transition systems are subsequently combined to obtain the final state space.
In earlier work a compositional minimisation technique was presented tailored to mCRL2: it provides support for the multi-action semantics of mCRL2 and allows splitting up a monolithic linear process specification into components. Only strong bisimulation minimisation of components can be used, limiting the effectiveness of the approach. In this paper we propose an extension to support branching bisimulation reduction and prove its correctness. We present a number of benchmarks using mCRL2 models derived from industrial SysML models, showing that a significant reduction can be achieved, also compared to compositional minimisation with strong bisimulation reduction.
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
Similar content being viewed by others
Notes
- 1.
- 2.
https://fsa.win.tue.nl/formasig; for more information see also [2].
References
Bouwman, M., Luttik, B., van der Wal, D.: A formalisation of SysML state machines in mCRL2. In: Peters, K., Willemse, T.A.C. (eds.) FORTE 2021. LNCS, vol. 12719, pp. 42–59. Springer, Cham (2021). https://doi.org/10.1007/978-3-030-78089-0_3
Bouwman, M., van der Wal, D., Luttik, B., Stoelinga, M., Rensink, A.: A case in point: verification and testing of a EULYNX interface. Formal Asp. Comput. (2022). https://doi.org/10.1145/3528207
Bunte, O., et al.: The mCRL2 toolset for analysing concurrent systems. In: Vojnar, T., Zhang, L. (eds.) TACAS 2019. LNCS, vol. 11428, pp. 21–39. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-17465-1_2
Cranen, S., Luttik, B., Willemse, T.A.C.: Evidence for fixpoint logic. In: Kreutzer, S. (ed.) 24th EACSL Annual Conference on Computer Science Logic, CSL 2015, Berlin, Germany, 7–10 September 2015. LIPIcs, vol. 41, pp. 78–93. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2015). https://doi.org/10.4230/LIPIcs.CSL.2015.78
Garavel, H., Lang, F., Mateescu, R., Serwe, W.: CADP 2011: a toolbox for the construction and analysis of distributed processes. Int. J. Softw. Tools Technol. Transf. 15(2), 89–107 (2013). https://doi.org/10.1007/s10009-012-0244-z
Garavel, H., Lang, F., Mounier, L.: Compositional verification in action. In: Howar, F., Barnat, J. (eds.) FMICS 2018. LNCS, vol. 11119, pp. 189–210. Springer, Cham (2018). https://doi.org/10.1007/978-3-030-00244-2_13
Glabbeek, R.J.: The linear time — branching time spectrum II. In: Best, E. (ed.) CONCUR 1993. LNCS, vol. 715, pp. 66–81. Springer, Heidelberg (1993). https://doi.org/10.1007/3-540-57208-2_6
van Glabbeek, R.J., Weijland, W.P.: Branching time and abstraction in bisimulation semantics. J. ACM 43(3), 555–600 (1996). https://doi.org/10.1145/233551.233556
Graf, S., Steffen, B.: Compositional minimization of finite state systems. In: Clarke, E.M., Kurshan, R.P. (eds.) CAV 1990. LNCS, vol. 531, pp. 186–196. Springer, Heidelberg (1991). https://doi.org/10.1007/BFb0023732
Graf, S., Steffen, B., Lüttgen, G.: Compositional minimisation of finite state systems using interface specifications. Formal Asp. Comput. 8(5), 607–616 (1996). https://doi.org/10.1007/BF01211911
Groote, J.F., Mousavi, M.R.: Modeling and Analysis of Communicating Systems. MIT Press (2014). https://mitpress.mit.edu/books/modeling-and-analysis-communicating-systems
Keiren, J.J.A., Klabbers, M.: Modelling and verifying IEEE Std 11073-20601 session setup using mCRL2. Electron. Commun. Eur. Assoc. Softw. Sci. Technol. 53 (2012). https://doi.org/10.14279/tuj.eceasst.53.793
Lang, F.: Refined interfaces for compositional verification. In: Najm, E., Pradat-Peyre, J.-F., Donzeau-Gouge, V.V. (eds.) FORTE 2006. LNCS, vol. 4229, pp. 159–174. Springer, Heidelberg (2006). https://doi.org/10.1007/11888116_13
Laveaux, M., Wesselink, W., Willemse, T.A.C.: On-the-fly solving for symbolic parity games. In: TACAS 2022. LNCS, vol. 13244, pp. 137–155. Springer, Cham (2022). https://doi.org/10.1007/978-3-030-99527-0_8
Laveaux, M., Willemse, T.A.C.: Decompositional minimisation of monolithic processes. CoRR abs/2012.06468 (2020). https://arxiv.org/abs/2012.06468
Laveaux, M., Willemse, T.A.C.: Decomposing monolithic processes in a process algebra with multi-actions. In: Lange, J., Mavridou, A., Safina, L., Scalas, A. (eds.) Proceedings 14th Interaction and Concurrency Experience, ICE 2021, 18 June 2021. EPTCS, vol. 347, pp. 57–76 (2021). https://doi.org/10.4204/EPTCS.347.4
Object Managament Group: OMG System Modeling Language, version 1.6 (2019). https://www.omg.org/spec/SysML/1.6/
Park, D.: Concurrency and automata on infinite sequences. In: Deussen, P. (ed.) GI-TCS 1981. LNCS, vol. 104, pp. 167–183. Springer, Heidelberg (1981). https://doi.org/10.1007/BFb0017309
Remenska, D., Willemse, T.A.C., Verstoep, K., Templon, J., Bal, H.E.: Using model checking to analyze the system behavior of the LHC production grid. Future Gener. Comput. Syst. 29(8), 2239–2251 (2013). https://doi.org/10.1016/j.future.2013.06.004
Wesselink, W., Willemse, T.A.C.: Evidence extraction from parameterised boolean equation systems. In: Benzmüller, C., Otten, J. (eds.) Proceedings of the 3rd International Workshop on Automated Reasoning in Quantified Non-Classical Logics (ARQNL 2018) affiliated with the International Joint Conference on Automated Reasoning (IJCAR 2018), Oxford, UK, 18 July 2018. CEUR Workshop Proceedings, vol. 2095, pp. 86–100. CEUR-WS.org (2018). http://ceur-ws.org/Vol-2095/paper6.pdf
Acknowledgements
The first author received funding for his research from ProRail and DB Netz AG. The vision presented in this article does not necessarily reflect the strategy of DB Netz AG or ProRail, but reflects the personal views of the authors.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2022 The Author(s), under exclusive license to Springer Nature Switzerland AG
About this paper
Cite this paper
Bouwman, M., Laveaux, M., Luttik, B., Willemse, T. (2022). Decompositional Branching Bisimulation Minimisation of Monolithic Processes. In: Tapia Tarifa, S.L., Proença, J. (eds) Formal Aspects of Component Software. FACS 2022. Lecture Notes in Computer Science, vol 13712. Springer, Cham. https://doi.org/10.1007/978-3-031-20872-0_10
Download citation
DOI: https://doi.org/10.1007/978-3-031-20872-0_10
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-031-20871-3
Online ISBN: 978-3-031-20872-0
eBook Packages: Computer ScienceComputer Science (R0)