2020
Conference article
Open Access
Sharp Congruences Adequate with Temporal Logics Combining Weak and Strong Modalities
Lang F., Mateescu R., Mazzanti F.
model checking Bisimulation Concurrency Article Mu-calculus congruences branching equivalence temporal logics sharp equivalence [INFO.INFO-SE]Computer Science [cs]/Software Engineering [cs.SE] [INFO.INFO-FL]Computer Science [cs]/Formal Languages and Automata Theory [cs.FL]
We showed in a recent paper that, when verifying a modal?-calculus formula, the actions of the system under verification can bepartitioned into sets of so-called weak and strong actions, depending onthe combination of weak and strong modalities occurring in the formula.In a compositional verification setting, where the system consists of pro-cesses executing in parallel, this partition allows us to decide whethereach individual process can be minimized for either divergence-preservingbranching (if the process contains only weak actions) or strong (other-wise) bisimilarity, while preserving the truth value of the formula. In thispaper, we refine this idea by devising a family of bisimilarity relations,named sharp bisimilarities, parameterized by the set of strong actions.We show that these relations have all the nice properties necessary tobe used for compositional verification, in particular congruence and ad-equacy with the logic. We also illustrate their practical utility on severalexamples and case-studies, and report about our success in the RERS2019 model checking challenge.
Source: 26th International Conference, TACAS 2020, pp. 57–73, Dublin, Ireland, April 25-30, 2020
Publisher: Springer, Cham, Heidelberg, New York, Dordrecht, London, CHE
1. Andersen, H.R.: Partial model checking. In: Proceedings of the 10th Annual IEEE Symposium on Logic in Computer Science LICS (San Diego, California, USA). pp. 398{407. IEEE Computer Society Press (Jun 1995)
2. Barbuti, R., De Francesco, N., Santone, A., Vaglini, G.: Selective mu-calculus and formula-based equivalence of transition systems. Journal of Computer and System Sciences 59, 537{556 (1999)
3. Blom, S., Orzan, S.: A Distributed Algorithm for Strong Bisimulation Reduction of State Spaces. Software Tools for Technology Transfer 7(1), 74{86 (2005)
4. Blom, S., Orzan, S.: Distributed State Space Minimization. Software Tools for Technology Transfer 7(3), 280{291 (2005)
5. Blom, S., van de Pol, J.: Distributed branching bisimulation minimization by inductive signatures. In: Proceedings of the 8th International Workshop on Parallel and Distributed Methods in veri Cation PDMC 2009 (Eindhoven, The Netherlands). Electronic Proceedings in Theoretical Computer Science, vol. 14 (2009)
6. Bolze, R., Cappello, F., Caron, E., Dayde, M.J., Desprez, F., Jeannot, E., Jegou, Y., Lanteri, S., Leduc, J., Melab, N., Mornet, G., Namyst, R., Primet, P., Quetier, B., Richard, O., Talbi, E., Touche, I.: Grid'5000: A large scale and highly recon gurable experimental grid testbed. IJHPCA 20(4), 481{494 (2006). https://doi.org/10.1177/1094342006070078, https://doi.org/10.1177/1094342006070078
7. Bouajjani, A., Fernandez, J.C., Graf, S., Rodr guez, C., Sifakis, J.: Safety for branching time semantics. In: Proceedings of 18th ICALP. Springer (Jul 1991)
8. Brookes, S.D., Hoare, C.A.R., Roscoe, A.W.: A Theory of Communicating Sequential Processes. J. ACM 31(3), 560{599 (Jul 1984)
9. Champelovier, D., Clerc, X., Garavel, H., Guerte, Y., McKinty, C., Powazny, V., Lang, F., Serwe, W., Smeding, G.: Reference Manual of the LNT to LOTOS Translator (Version 6.7) (Jul 2017), INRIA, Grenoble, France
10. Cheung, S.C., Kramer, J.: 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). pp. 115{125. ACM Press (Dec 1993)
11. Clarke, E.M., Emerson, E.A., Sistla, A.P.: Automatic veri cation of nite-state concurrent systems using temporal logic speci cations. ACM Transactions on Programming Languages and Systems 8(2), 244{263 (Apr 1986)
12. Crouzen, P., Lang, F.: Smart Reduction. In: Giannakopoulou, D., Orejas, F. (eds.) Proceedings of Fundamental Approaches to Software Engineering (FASE'11), Saarbrucken, Germany. Lecture Notes in Computer Science, vol. 6603, pp. 111{126. Springer (Mar 2011)
13. De Nicola, R., Vaandrager, F.: Three logics for branching bisimulation. Journal of the Association for Computing Machinery (1990)
14. Fernandez, J.C., Mounier, L.: \On the Fly" Veri cation of Behavioural Equivalences and Preorders. In: Larsen, K.G., Skou, A. (eds.) Proceedings of the 3rd Workshop on Computer-Aided Veri cation (CAV'91), Aalborg, Denmark. Lecture Notes in Computer Science, vol. 575, pp. 181{191. Springer (Jul 1991)
15. Fischer, M.J., Ladner, R.E.: Propositional dynamic logic of regular programs. J. Comput. Syst. Sci. 18(2), 194{211 (Sep 1979)
16. Garavel, H.: Nested-Unit Petri Nets. Journal of Logical and Algebraic Methods in Programming 104, 60{85 (Apr 2019)
17. Garavel, H., Lang, F.: SVL: a Scripting Language for Compositional Veri cation. 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. pp. 377{392. Kluwer Academic Publishers (Aug 2001), full version available as INRIA Research Report RR-4223
18. Garavel, H., Lang, F., Mateescu, R.: Compositional Veri cation of Asynchronous Concurrent Systems Using CADP. Acta Informatica 52(4), 337{392 (Apr 2015)
19. Garavel, H., Lang, F., Mateescu, R., Serwe, W.: CADP 2011: A Toolbox for the Construction and Analysis of Distributed Processes. Springer International Journal on Software Tools for Technology Transfer (STTT) 15(2), 89{107 (Apr 2013)
20. van Glabbeek, R.J., Weijland, W.P.: 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, 1989
21. van Glabbeek, R.J., Luttik, B., Trcka, N.: Branching bisimilarity with explicit divergence. Fundam. Inform. 93(4), 371{392 (2009). https://doi.org/10.3233/FI2009-109, https://doi.org/10.3233/FI-2009-109
22. van Glabbeek, R.J., Luttik, B., Trcka, N.: Computation tree logic with deadlock detection. Logical Methods in Computer Science 5(4) (2009), http://arxiv.org/abs/0912.2109
23. van Glabbeek, R.J., Weijland, W.P.: Branching Time and Abstraction in Bisimulation Semantics. Journal of the ACM 43(3), 555{600 (1996)
24. Graf, S., Ste en, B.: Compositional Minimization of Finite State Systems. In: Clarke, E.M., Kurshan, R.P. (eds.) Proceedings of the 2nd Workshop on ComputerAided Veri cation (CAV'90), Rutgers, New Jersey, USA. Lecture Notes in Computer Science, vol. 531, pp. 186{196. Springer (Jun 1990)
25. Groote, J.F., Jansen, D.N., Keiren, J.J.A., Wijs, A.: An o(m log n) algorithm for computing stuttering equivalence and branching bisimulation. ACM Transactions on Computational Logic 18(2) (2017)
26. Groote, J., Ponse, A.: The Syntax and Semantics of CRL. CS-R 9076, Centrum voor Wiskunde en Informatica, Amsterdam (1990)
27. Groote, J.F., Sellink, M.P.A.: Con uence for process veri cation. Theoretical Computer Science 170(1{2), 47{81 (1996)
28. Groote, J., Pol, J.: State space reduction using partial -con uence. 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, pp. 383{393. Springer (Aug 2000), also available as CWI Technical Report SEN-R0008, Amsterdam, March 2000
29. ISO/IEC: 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 (Sep 1989)
30. ISO/IEC: Enhancements to LOTOS (E-LOTOS). International Standard 15437:2001, International Organization for Standardization { Information Technology, Geneva (Sep 2001)
31. Kozen, D.: Results on the propositional -calculus. Theoretical Computer Science 27, 333{354 (1983)
32. Krimm, J.P., Mounier, L.: 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), University of Twente, Enschede, The Netherlands. Lecture Notes in Computer Science, vol. 1217. Springer (Apr 1997), extended version with proofs available as Research Report VERIMAG RR97-01
33. Lang, F.: EXP.OPEN 2.0: A Flexible Tool Integrating Partial Order, Compositional, and On-the- y Veri cation 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, pp. 70{88. Springer (Nov 2005), full version available as INRIA Research Report RR-5673
34. Lang, F., Mateescu, R.: Partial Model Checking using Networks of Labelled Transition Systems and Boolean Equation Systems. Logical Methods in Computer Science 9(4), 1{32 (Oct 2013)
35. Lang, F., Mateescu, R., Mazzanti, F.: Compositional veri cation 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, pp. 196{213. Springer (2019)
36. Malhotra, J., Smolka, S.A., Giacalone, A., Shapiro, R.: A Tool for Hierarchical Design and Simulation of Concurrent Systems. In: Proceedings of the BCS-FACS Workshop on Speci cation and Veri cation of Concurrent Systems, Stirling, Scotland, UK. pp. 140{152. British Computer Society (Jul 1988)
37. Mateescu, R., Wijs, A.: Property-Dependent Reductions Adequate with Divergence-Sensitive Branching Bisimilarity. Sci. Comput. Program. 96(3), 354{ 376 (2014)
38. Milner, R.: Communication and Concurrency. Prentice-Hall (1989)
39. Nicola, R.D., Vaandrager, F.W.: Action versus State based Logics for Transition Systems, Lecture Notes in Computer Science, vol. 469, pp. 407{419. Springer (Apr 1990)
40. Park, D.: Concurrency and Automata on In nite Sequences. In: Deussen, P. (ed.) Theoretical Computer Science. Lecture Notes in Computer Science, vol. 104, pp. 167{183. Springer (Mar 1981)
41. Pnueli, A.: In transition from global to modular temporal reasoning about programs. Logic and Models of Concurrent Systems 13, 123{144 (1984)
42. de Putter, S., Wijs, A., Lang, F.: Compositional model checking is lively | extended version (2019), submitted to Science of Computer Programming
43. Sabnani, K.K., Lapone, A.M., Umit Uyar, M.: An Algorithmic Procedure for Checking Safety Properties of Protocols. IEEE Transactions on Communications 37(9), 940{948 (Sep 1989)
44. Streett, R.: Propositional dynamic logic of looping and converse. Information and Control (54), 121{141 (1982)
45. Tai, K.C., Koppol, P.V.: An Incremental Approach to Reachability Analysis of Distributed Programs. In: Proceedings of the 7th International Workshop on Software Speci cation and Design, Los Angeles, CA, USA. pp. 141{150. IEEE Press, Piscataway, NJ (Dec 1993)
46. Tai, K.C., Koppol, P.V.: Hierarchy-Based Incremental Reachability Analysis of Communication Protocols. In: Proceedings of the IEEE International Conference on Network Protocols, San Francisco, CA, USA. pp. 318{325. IEEE Press, Piscataway, NJ (Oct 1993)
47. Valmari, A.: Compositional State Space Generation. In: Rozenberg, G. (ed.) 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, pp. 427{457. Springer (1993)
48. Yatapanage, N., Winter, K.: Next-preserving branching bisimulation. Theoretical Computer Science 594, 120{142 (2015)
49. Yeh, W.J., Young, M.: Compositional Reachability Analysis Using Process Algebra. In: Proceedings of the ACM SIGSOFT Symposium on Testing, Analysis, and Veri cation (SIGSOFT'91), Victoria, British Columbia, Canada. pp. 49{59. ACM Press (Oct 1991)
50. Ying, M.: Weak con uence and -inertness. Theoretical Computer Science 238, 465{475 (2000)
2. Barbuti, R., De Francesco, N., Santone, A., Vaglini, G.: Selective mu-calculus and formula-based equivalence of transition systems. Journal of Computer and System Sciences 59, 537{556 (1999)
3. Blom, S., Orzan, S.: A Distributed Algorithm for Strong Bisimulation Reduction of State Spaces. Software Tools for Technology Transfer 7(1), 74{86 (2005)
4. Blom, S., Orzan, S.: Distributed State Space Minimization. Software Tools for Technology Transfer 7(3), 280{291 (2005)
5. Blom, S., van de Pol, J.: Distributed branching bisimulation minimization by inductive signatures. In: Proceedings of the 8th International Workshop on Parallel and Distributed Methods in veri Cation PDMC 2009 (Eindhoven, The Netherlands). Electronic Proceedings in Theoretical Computer Science, vol. 14 (2009)
6. Bolze, R., Cappello, F., Caron, E., Dayde, M.J., Desprez, F., Jeannot, E., Jegou, Y., Lanteri, S., Leduc, J., Melab, N., Mornet, G., Namyst, R., Primet, P., Quetier, B., Richard, O., Talbi, E., Touche, I.: Grid'5000: A large scale and highly recon gurable experimental grid testbed. IJHPCA 20(4), 481{494 (2006). https://doi.org/10.1177/1094342006070078, https://doi.org/10.1177/1094342006070078
7. Bouajjani, A., Fernandez, J.C., Graf, S., Rodr guez, C., Sifakis, J.: Safety for branching time semantics. In: Proceedings of 18th ICALP. Springer (Jul 1991)
8. Brookes, S.D., Hoare, C.A.R., Roscoe, A.W.: A Theory of Communicating Sequential Processes. J. ACM 31(3), 560{599 (Jul 1984)
9. Champelovier, D., Clerc, X., Garavel, H., Guerte, Y., McKinty, C., Powazny, V., Lang, F., Serwe, W., Smeding, G.: Reference Manual of the LNT to LOTOS Translator (Version 6.7) (Jul 2017), INRIA, Grenoble, France
10. Cheung, S.C., Kramer, J.: 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). pp. 115{125. ACM Press (Dec 1993)
11. Clarke, E.M., Emerson, E.A., Sistla, A.P.: Automatic veri cation of nite-state concurrent systems using temporal logic speci cations. ACM Transactions on Programming Languages and Systems 8(2), 244{263 (Apr 1986)
12. Crouzen, P., Lang, F.: Smart Reduction. In: Giannakopoulou, D., Orejas, F. (eds.) Proceedings of Fundamental Approaches to Software Engineering (FASE'11), Saarbrucken, Germany. Lecture Notes in Computer Science, vol. 6603, pp. 111{126. Springer (Mar 2011)
13. De Nicola, R., Vaandrager, F.: Three logics for branching bisimulation. Journal of the Association for Computing Machinery (1990)
14. Fernandez, J.C., Mounier, L.: \On the Fly" Veri cation of Behavioural Equivalences and Preorders. In: Larsen, K.G., Skou, A. (eds.) Proceedings of the 3rd Workshop on Computer-Aided Veri cation (CAV'91), Aalborg, Denmark. Lecture Notes in Computer Science, vol. 575, pp. 181{191. Springer (Jul 1991)
15. Fischer, M.J., Ladner, R.E.: Propositional dynamic logic of regular programs. J. Comput. Syst. Sci. 18(2), 194{211 (Sep 1979)
16. Garavel, H.: Nested-Unit Petri Nets. Journal of Logical and Algebraic Methods in Programming 104, 60{85 (Apr 2019)
17. Garavel, H., Lang, F.: SVL: a Scripting Language for Compositional Veri cation. 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. pp. 377{392. Kluwer Academic Publishers (Aug 2001), full version available as INRIA Research Report RR-4223
18. Garavel, H., Lang, F., Mateescu, R.: Compositional Veri cation of Asynchronous Concurrent Systems Using CADP. Acta Informatica 52(4), 337{392 (Apr 2015)
19. Garavel, H., Lang, F., Mateescu, R., Serwe, W.: CADP 2011: A Toolbox for the Construction and Analysis of Distributed Processes. Springer International Journal on Software Tools for Technology Transfer (STTT) 15(2), 89{107 (Apr 2013)
20. van Glabbeek, R.J., Weijland, W.P.: 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, 1989
21. van Glabbeek, R.J., Luttik, B., Trcka, N.: Branching bisimilarity with explicit divergence. Fundam. Inform. 93(4), 371{392 (2009). https://doi.org/10.3233/FI2009-109, https://doi.org/10.3233/FI-2009-109
22. van Glabbeek, R.J., Luttik, B., Trcka, N.: Computation tree logic with deadlock detection. Logical Methods in Computer Science 5(4) (2009), http://arxiv.org/abs/0912.2109
23. van Glabbeek, R.J., Weijland, W.P.: Branching Time and Abstraction in Bisimulation Semantics. Journal of the ACM 43(3), 555{600 (1996)
24. Graf, S., Ste en, B.: Compositional Minimization of Finite State Systems. In: Clarke, E.M., Kurshan, R.P. (eds.) Proceedings of the 2nd Workshop on ComputerAided Veri cation (CAV'90), Rutgers, New Jersey, USA. Lecture Notes in Computer Science, vol. 531, pp. 186{196. Springer (Jun 1990)
25. Groote, J.F., Jansen, D.N., Keiren, J.J.A., Wijs, A.: An o(m log n) algorithm for computing stuttering equivalence and branching bisimulation. ACM Transactions on Computational Logic 18(2) (2017)
26. Groote, J., Ponse, A.: The Syntax and Semantics of CRL. CS-R 9076, Centrum voor Wiskunde en Informatica, Amsterdam (1990)
27. Groote, J.F., Sellink, M.P.A.: Con uence for process veri cation. Theoretical Computer Science 170(1{2), 47{81 (1996)
28. Groote, J., Pol, J.: State space reduction using partial -con uence. 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, pp. 383{393. Springer (Aug 2000), also available as CWI Technical Report SEN-R0008, Amsterdam, March 2000
29. ISO/IEC: 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 (Sep 1989)
30. ISO/IEC: Enhancements to LOTOS (E-LOTOS). International Standard 15437:2001, International Organization for Standardization { Information Technology, Geneva (Sep 2001)
31. Kozen, D.: Results on the propositional -calculus. Theoretical Computer Science 27, 333{354 (1983)
32. Krimm, J.P., Mounier, L.: 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), University of Twente, Enschede, The Netherlands. Lecture Notes in Computer Science, vol. 1217. Springer (Apr 1997), extended version with proofs available as Research Report VERIMAG RR97-01
33. Lang, F.: EXP.OPEN 2.0: A Flexible Tool Integrating Partial Order, Compositional, and On-the- y Veri cation 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, pp. 70{88. Springer (Nov 2005), full version available as INRIA Research Report RR-5673
34. Lang, F., Mateescu, R.: Partial Model Checking using Networks of Labelled Transition Systems and Boolean Equation Systems. Logical Methods in Computer Science 9(4), 1{32 (Oct 2013)
35. Lang, F., Mateescu, R., Mazzanti, F.: Compositional veri cation 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, pp. 196{213. Springer (2019)
36. Malhotra, J., Smolka, S.A., Giacalone, A., Shapiro, R.: A Tool for Hierarchical Design and Simulation of Concurrent Systems. In: Proceedings of the BCS-FACS Workshop on Speci cation and Veri cation of Concurrent Systems, Stirling, Scotland, UK. pp. 140{152. British Computer Society (Jul 1988)
37. Mateescu, R., Wijs, A.: Property-Dependent Reductions Adequate with Divergence-Sensitive Branching Bisimilarity. Sci. Comput. Program. 96(3), 354{ 376 (2014)
38. Milner, R.: Communication and Concurrency. Prentice-Hall (1989)
39. Nicola, R.D., Vaandrager, F.W.: Action versus State based Logics for Transition Systems, Lecture Notes in Computer Science, vol. 469, pp. 407{419. Springer (Apr 1990)
40. Park, D.: Concurrency and Automata on In nite Sequences. In: Deussen, P. (ed.) Theoretical Computer Science. Lecture Notes in Computer Science, vol. 104, pp. 167{183. Springer (Mar 1981)
41. Pnueli, A.: In transition from global to modular temporal reasoning about programs. Logic and Models of Concurrent Systems 13, 123{144 (1984)
42. de Putter, S., Wijs, A., Lang, F.: Compositional model checking is lively | extended version (2019), submitted to Science of Computer Programming
43. Sabnani, K.K., Lapone, A.M., Umit Uyar, M.: An Algorithmic Procedure for Checking Safety Properties of Protocols. IEEE Transactions on Communications 37(9), 940{948 (Sep 1989)
44. Streett, R.: Propositional dynamic logic of looping and converse. Information and Control (54), 121{141 (1982)
45. Tai, K.C., Koppol, P.V.: An Incremental Approach to Reachability Analysis of Distributed Programs. In: Proceedings of the 7th International Workshop on Software Speci cation and Design, Los Angeles, CA, USA. pp. 141{150. IEEE Press, Piscataway, NJ (Dec 1993)
46. Tai, K.C., Koppol, P.V.: Hierarchy-Based Incremental Reachability Analysis of Communication Protocols. In: Proceedings of the IEEE International Conference on Network Protocols, San Francisco, CA, USA. pp. 318{325. IEEE Press, Piscataway, NJ (Oct 1993)
47. Valmari, A.: Compositional State Space Generation. In: Rozenberg, G. (ed.) 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, pp. 427{457. Springer (1993)
48. Yatapanage, N., Winter, K.: Next-preserving branching bisimulation. Theoretical Computer Science 594, 120{142 (2015)
49. Yeh, W.J., Young, M.: Compositional Reachability Analysis Using Process Algebra. In: Proceedings of the ACM SIGSOFT Symposium on Testing, Analysis, and Veri cation (SIGSOFT'91), Victoria, British Columbia, Canada. pp. 49{59. ACM Press (Oct 1991)
50. Ying, M.: Weak con uence and -inertness. Theoretical Computer Science 238, 465{475 (2000)
Metrics
Back to previous page
BibTeX entry
@inproceedings{oai:it.cnr:prodotti:422698,
title = {Sharp Congruences Adequate with Temporal Logics Combining Weak and Strong Modalities},
author = {Lang F. and Mateescu R. and Mazzanti F.},
publisher = {Springer, Cham, Heidelberg, New York, Dordrecht, London, CHE},
doi = {10.1007/978-3-030-45237-7_4},
booktitle = {26th International Conference, TACAS 2020, pp. 57–73, Dublin, Ireland, April 25-30, 2020},
year = {2020}
}CNR authorsLaboratories
0000-0003-4562-8777CNR ExploRA
ISTI Repository
DOIAlso available from
ISTI Repository
DOIAlso available from
Europe PubMed Central
link.springer.com
link.springer.com
INRIA a CCSD electronic archive server