Compositional verification of concurrent systems by combining bisimulations

Andersen HR (1995) Partial model checking. In: Proceedings of the 10th annual IEEE symposium on logic in computer science LICS (San Diego, California, USA). IEEE Computer Society Press, pp 398–407

Bolze R, Cappello F, Caron E, Daydé Michel J, Desprez F, Jeannot E, Jégou Y, Lanteri S, Leduc J, Melab N, Mornet G, Namyst R, Primet P, Quétier B, Richard O, Talbi E-G, Touche I (2006) Grid’5000: a large scale and highly reconfigurable experimental grid testbed. IJHPCA 20(4):481–494

Brzozowski Janusz A (1964) Derivatives of regular expressions. J Assoc Comput Mach 11(4):481–494

Champelovier D, Clerc X, Garavel H, Guerte Y, McKinty C, Powazny V, Lang F, Serwe W, Smeding G (2017) Reference manual of the LNT to LOTOS translator (version 6.7). INRIA, Grenoble

Cheung SC, Kramer J (1993) Enhancing compositional reachability analysis with context constraints. In: Proceedings of the 1st ACM SIGSOFT international symposium on the foundations of software engineering (Los Angeles, CA, USA). ACM Press, pp 115–125

Clarke EM, Emerson EA, Sistla AP (1986) Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Trans Program Lang Syst 8(2):244–263

Cleaveland R, Klein M, Steffen B (1992) Faster model checking for the modal mu-calculus. In: Bochmann GV, Probst DK (eds) Proceedings of the 4th international workshop on computer aided verification CAV ’92 (Montréal, Canada). Lecture notes in computer science, vol 663. Springer, Berlin, pp 410–422

Crouzen P, Lang F (2011) Smart reduction. In: Giannakopoulou D, Orejas F (eds) Proceedings of fundamental approaches to software engineering (FASE’11), Saarbrücken, Germany. Lecture notes in computer science, vol 6603. Springer, Berlin, pp 111–126

De Nicola R, Vaandrager FW (1990) Three logics for branching bisimulation. J Assoc Comput Mach 42:458–487

De Nicola R, Vaandrager FW (1990) Action versus state based logics for transition systems. Lecture notes in computer science, vol 469. Springer, Berlin, pp 407–419

de Putter S, Wijs A, Lang F (2018) Compositional model checking is lively—extended version. Sci Comput Program

Emerson EA, Lei C-L (1986) Efficient model checking in fragments of the propositional mu-calculus. In: Proceedings of the 1st international symposium on logic in computer science LICS’86, pp 267–278

Fantechi A, Gnesi S, Ristori G (1992) From actl to $$\mu $$-calculus (extended abstract). In: Proceedings of the workshop on theory and practice in verification. ERCIM

Fischer Michael J, Ladner Richard E (1979) Propositional dynamic logic of regular programs. J Comput Syst Sci 18(2):194–211

Garavel H, Lang F (2001) SVL: a scripting language for compositional verification. In: Kim M, Chin B, Kang S, Lee D (eds) Proceedings of the 21st IFIP WG 6.1 international conference on formal techniques for networked and distributed systems (FORTE’01), Cheju Island, Korea. Full version available as INRIA research report RR-4223. Kluwer Academic Publishers, pp 377–392

Garavel H, Lang F, Mateescu R (2015) Compositional verification of asynchronous concurrent systems using CADP. Acta Inform 52(4):337–392

Garavel H, Lang F, Mateescu R, Serwe W (2013) CADP 2011: a toolbox for the construction and analysis of distributed processes. Int J Softw Tools Technol Transf 15(2):89–107

Garavel H, Mateescu R, Bergamini D, Curic A, Descoubes N, Joubert C, Smarandache-Sturm I, Stragier G (2006) Distributor and bcg\_merge: Tools for distributed explicit state space generation. In: Hermanns H, Palberg J (eds) Proceedings of the 12th international conference on tools and algorithms for the construction and analysis of systems (TACAS’06), Vienna, Austria. Lecture notes in computer science, vol 3920. Springer, Berlin, pp 445–449

Garavel H, Thivolle D (2009) Verification of GALS systems by combining synchronous languages and process calculi. In: Pasareanu C (ed) Proceedings of the 16th international spin workshop on model checking of software (SPIN’09), Grenoble, France. Lecture notes in computer science, vol 5578. Springer, Berlin, pp 241–260

Gerth R, Kuiper R, Penczek W, Peled D (1999) A partial order approach to branching time logic model checking. Inf Comput 150(2):132–152. A short version of this paper was previously published at the third Israel symposium on theory of computing and systems ISTCS 1995

Godefroid P (1990) Using partial orders to improve automatic verification methods. In: Kurshan RP, Clarke EM (eds) Proceedings of the 2nd workshop on computer-aided verification (Rutgers, New Jersey, USA). DIMACS series in discrete mathematics and theoretical computer science, vol 3. AMS-ACM, pp 321–340

Graf S, Steffen B (1990) Compositional minimization of finite state systems. In: Clarke EM, Kurshan RP (eds) Proceedings of the 2nd workshop on computer-aided verification (CAV’90), Rutgers, New Jersey, USA. Lecture notes in computer science, vol 531. Springer, Berlin, pp 186–196

Groote JF, Mousavi MR (2014) Modeling and analysis of communicating systems. The MIT Press, Cambridge

Groote JF, Ponse A (1990) The syntax and semantics of $$\mu $$CRL. CS-R 9076. Centrum voor Wiskunde en Informatica, Amsterdam

Groote JF, Sellink MPA (1996) Confluence for process verification. Theor Comput Sci 170(1–2):47–81

Groote JF, van de Pol J (2000) State space reduction using partial $$\tau $$-confluence. In: Nielsen M, Rovan B (eds) Proceedings of the 25th international symposium on mathematical foundations of computer science (MFCS’00), Bratislava, Slovakia. Lecture notes in computer science, vol 1893. Springer, Berlin, pp 383–393. Also available as CWI Technical Report SEN-R0008, Amsterdam

Harel D, Kozen D, Tiuryn J (2000) Dynamic logic. MIT Press, Berlin

ISO/IEC (1989) LOTOS—a formal description technique based on the temporal ordering of observational behaviour. International standard 8807, international organization for standardization—information processing systems—open systems interconnection, Geneva

ISO/IEC (2001) Enhancements to LOTOS (E-LOTOS). International Standard 15437:2001, International Organization for Standardization—Information Technology, Geneva

Kozen D (1983) Results on the propositional $$\mu $$-calculus. Theor Comput Sci 27:333–354

Krimm J-P, Mounier L (1997) Compositional state space generation from LOTOS programs. In: Brinksma E (ed) Proceedings of the 3rd international workshop on tools and algorithms for the construction and analysis of systems (TACAS’97). Lecture notes in computer science, vol 1217. University of Twente, Enschede. Springer, Berlin. Extended version with proofs available as Research Report VERIMAG RR97-01

Lang F (2005) EXP.OPEN 2.0: a flexible tool integrating partial order, compositional, and on-the-fly verification methods. In: Romijn J, Smith G, van de Pol J (eds) Proceedings of the 5th international conference on integrated formal methods (IFM’05), Eindhoven, The Netherlands. Lecture notes in computer science, vol 3771. Springer, Berlin, pp 70–88. Full version available as INRIA Research Report RR-5673

Lang F, Mateescu R (2012) Partial model checking using networks of labelled transition systems and boolean equation systems. In: Flanagan C, König B (eds) Proceedings of the 18th international conference on tools and algorithms for the construction and analysis of systems (TACAS’12), Talinn, Estonia. Lecture notes in computer science, vol 7214. Springer, Berlin, pp 141–156

Lang F, Mateescu R, Mazzanti F (2019) Compositional verification of concurrent systems by combining bisimulations. In: McIver A, ter Beek M (eds) Proceedings of the 23rd international symposium on formal methods—3rd World congress on formal methods FM 2019 (Porto, Portugal). Lecture notes in computer science, vol 11800. Springer, Berlin, pp 196–213

Lang F, Mateescu R, Mazzanti F (2020) Sharp congruences adequate with temporal logics combining weak and strong modalities. In: Biere A, Parker D (eds) Proceedings of the 26th international conference on tools and algorithms for the construction and analysis of systems TACAS 2020 (Dublin, Ireland). Lecture notes in computer science, vol 12079. Springer, Berlin, pp 57–76

Larsen KG (1988) Proof systems for Hennessy–Milner logic with recursion. In: Proceedings of the 13th colloquium on trees in algebra and programming CAAP ’88 (Nancy, France). Lecture notes in computer science, vol 299. Springer, Berlin, pp 215–230

Malhotra J, Smolka SA, Giacalone A, Shapiro R (1988) A tool for hierarchical design and simulation of concurrent systems. In: Proceedings of the BCS-FACS workshop on specification and verification of concurrent systems, stirling, Scotland, UK. British Computer Society, pp 140–152

Radu Mateescu and Jose Ignacio Requeno (2018) On-the-fly model checking for extended action-based probabilistic operators. Int J Softw Tools Technol Transf 20(5):563–587

Mateescu R, Thivolle D (2008) A model checking language for concurrent value-passing systems. In: Cuellar J, Maibaum T, Sere K (eds) Proceedings of the 15th international symposium on formal methods (FM’08), Turku, Finland. Lecture notes in computer science, vol 5014. Springer, Berlin, pp 148–164

Mateescu R, Wijs A (2012) Sequential and distributed on-the-fly computation of weak tau-confluence. Sci Comput Program 77(10–11):1075–1094

Mateescu R, Wijs A (2014) Property-dependent reductions adequate with divergence-sensitive branching bisimilarity. Sci Comput Program 96(3):354–376

Milner R (1989) Communication and concurrency. Prentice-Hall, Upper Saddle River

Park D (1981) Concurrency and automata on infinite sequences. In: Deussen P (ed) Theoretical computer science. Lecture notes in computer science, vol 104. Springer, Berlin, pp 167–183

Peled D. Partial order reduction: linear and branching temporal logics and process algebras. In: Peled et al. [45]

Peled DA, Pratt VR, Holzmann GJ (eds) (1997) Proceedings of the workshop on partial order methods in verification. Dimacs series in discrete mathematics, vol 29

Pnueli A (1984) In transition from global to modular temporal reasoning about programs. Log Models Concurr Syst 13:123–144

Ramakrishna YS, Smolka SA (1997) Partial-order reduction in the weak modal mu-calculus. In: Mazurkiewicz A, Winkowski J (eds) Proceedings of the 8th international conference on concurrency theory CONCUR’97. Lecture notes in computer science, vol 1243. Springer, Berlin, pp 5–24

Roscoe AW (1997) The theory and practice of concurrency. Prentice Hall, Upper Saddle River

Sabnani KK, Lapone AM, Ümit Uyar M (1989) An algorithmic procedure for checking safety properties of protocols. IEEE Trans Commun 37(9):940–948

Streett R (1982) Propositional dynamic logic of looping and converse is elementarily decidable. Inf Control 54(1–2):121–141

Streett RS, Emerson EA (1989) An automata theoretic decision procedure for the propositional mu-calculus. Inf Comput 81(3):249–264

Tai K-C, Koppol PV (1993) An incremental approach to reachability analysis of distributed programs. In: Proceedings of the 7th international workshop on software specification and design, Los Angeles, CA, USA. IEEE Press, Piscataway, NJ, pp 141–150

Tai K-C, Koppol PV (1993) Hierarchy-based incremental reachability analysis of communication protocols. In:Proceedings of the IEEE international conference on network protocols, San Francisco, CA, USA. IEEE Press, Piscataway, NJ, pp 318–325

Valmari A. Stubborn set methods for process algebras. In: Peled et al. [45]

Valmari A (1993) Compositional state space generation. In: Rozenberg G (eds) Advances in Petri Nets 1993—papers from the 12th international conference on applications and theory of petri nets (ICATPN’91), Gjern, Denmark. Lecture notes in computer science, vol 674. Springer, Berlin, pp 427–457

van Glabbeek RJ, Weijland WP (1989) Branching-time and abstraction in bisimulation semantics (extended abstract). CS R8911. Centrum voor Wiskunde en Informatica, Amsterdam, 1989. Also in proc. IFIP 11th World computer congress, San Francisco

van Glabbeek RJ, Weijland WP (1996) Branching time and abstraction in bisimulation semantics. J ACM 43(3):555–600

Yeh WJ, Young M (1991) Compositional reachability analysis using process algebra. In: Proceedings of the ACM SIGSOFT symposium on testing, analysis, and verification (SIGSOFT’91). Victoria, British Columbia, Canada. ACM Press, pp 49–59