×

zbMATH — the first resource for mathematics

Ensuring liveness properties of distributed systems: open problems. (English) Zbl 1435.68216
Summary: Often fairness assumptions need to be made in order to establish liveness properties of distributed systems, but in many situations they lead to false conclusions. This document presents a research agenda aiming at laying the foundations of a theory of concurrency that is equipped to ensure liveness properties of distributed systems without making fairness assumptions. This theory will encompass process algebra, temporal logic and semantic models. The agenda also includes the development of a methodology and tools that allow successful application of this theory to the specification, analysis and verification of realistic distributed systems.
Contemporary process algebras and temporal logics fail to make distinctions between systems of which one has a crucial liveness property and the other does not, at least when assuming justness, a strong progress property, but not assuming fairness. Setting up an alternative framework involves giving up on identifying strongly bisimilar systems, inventing new induction principles, developing new axiomatic bases for process algebras and new congruence formats for operational semantics, and creating matching treatments of time and probability.
Even simple systems like fair schedulers or mutual exclusion protocols cannot be accurately specified in standard process algebras (or Petri nets) in the absence of fairness assumptions. Hence the work involves the study of adequate language or model extensions, and their expressive power.

MSC:
68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
68M14 Distributed systems
68Q60 Specification and verification (program logics, model checking, etc.)
Software:
CADP; FDR3; LTSmin; SPIN; Uppaal
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Austry, D.; Boudol, G., Algèbre de processus et synchronisations, Theor. Comput. Sci., 30, 1, 91-131 (1984) · Zbl 0533.68026
[2] Apt, K. R.; Francez, N.; Katz, S., Appraising fairness in languages for distributed programming, Distrib. Comput., 2, 4, 226-241 (1988) · Zbl 0659.68023
[3] (Baeten, J. C.M., Applications of Process Algebra. Applications of Process Algebra, Cambridge Tracts in Theoretical Computer Science, vol. 17 (1990), Cambridge University Press) · Zbl 0716.68001
[4] Baeten, J. C.M.; Bergstra, J. A.; Klop, J. W., On the consistency of Koomen’s fair abstraction rule, Theor. Comput. Sci., 51, 1/2, 129-176 (1987) · Zbl 0621.68010
[5] Baeten, J. C.M.; Basten, T.; Reniers, M. A., Process Algebra: Equational Theories of Communicating Processes (2010), Cambridge University Press · Zbl 1234.68001
[6] Buti, F.; Callisto De Donato, M.; Corradini, F.; Di Berardini, M. R.; Vogler, W., Automated analysis of MUTEX algorithms with FASE, (D’Agostino, G.; La Torre, S., Proc. GandALF ’11. Proc. GandALF ’11, EPTCS, vol. 54 (2011), Open Publishing Association), 45-59
[7] Boudol, G.; Castellani, I.; Hennessy, M.; Kiehn, A., A theory of processes with localities, Form. Asp. Comput., 6, 2, 165-200 (1994) · Zbl 0806.68070
[8] Behrmann, G.; David, A.; Larsen, K. G., A tutorial on Uppaal, (Bernardo, M.; Corradini, F., Revised Lectures on Formal Methods for the Design of Real-Time Systems. Revised Lectures on Formal Methods for the Design of Real-Time Systems, LNCS, vol. 3185 (2004), Springer), 200-236 · Zbl 1105.68350
[9] Bloom, B.; Fokkink, W. J.; van Glabbeek, R. J., Precongruence formats for decorated trace semantics, ACM Trans. Comput. Log., 5, 1, 26-78 (2004) · Zbl 1367.68209
[10] Bol, R. N.; Groote, J. F., The meaning of negative premises in transition system specifications, J. ACM, 43, 5, 863-914 (1996) · Zbl 0889.68113
[11] Borgström, J.; Gutkovas, R.; Rodhe, I.; Victor, B., The psi-calculi workbench: a generic tool for applied process calculi, ACM Trans. Embed. Comput. Syst., 14, 1, 9:1-9:25 (2015)
[12] Brookes, S. D.; Hoare, C. A.R.; Roscoe, A. W., A theory of communicating sequential processes, J. ACM, 31, 3, 560-599 (1984) · Zbl 0628.68025
[13] Bloom, B.; Istrail, S.; Meyer, A. R., Bisimulation can’t be traced, J. ACM, 42, 1, 232-268 (1995) · Zbl 0886.68027
[14] Bengtson, J.; Johansson, M.; Parrow, J.; Victor, B., Psi-calculi: a framework for mobile processes with nominal data and logic, Log. Methods Comput. Sci., 7, 1 (2011) · Zbl 1213.68399
[15] Bergstra, J. A.; Klop, J. W., Algebra of communicating processes, (de Bakker, J. W.; Hazewinkel, M.; Lenstra, J. K., Mathematics and Computer Science. Mathematics and Computer Science, CWI Monograph, vol. 1 (1986), North-Holland: North-Holland Amsterdam), 89-138 · Zbl 0605.68013
[16] Bergstra, J. A.; Klop, J. W., Verification of an alternating bit protocol by means of process algebra, (Bibel, W.; Jantke, K. P., Mathematical Methods of Specification and Synthesis of Software Systems ’85. Mathematical Methods of Specification and Synthesis of Software Systems ’85, LNCS, vol. 215 (1986), Springer), 9-23 · Zbl 0595.68024
[17] Baier, C.; Katoen, J., Principles of Model Checking (2008), MIT Press
[18] Bloom, B., Structural operational semantics for weak bisimulations, Theor. Comput. Sci., 146, 25-68 (1995) · Zbl 0873.68130
[19] Boudol, G., Notes on algebraic calculi of processes, (Apt, K., Logics and Models of Concurrent Systems. Logics and Models of Concurrent Systems, NATO ASI Series, vol. F13 (1985), Springer), 261-303 · Zbl 0578.68025
[20] Brinksma, E.; Rensink, A.; Vogler, W., Fair testing, (Lee, I.; Smolka, S., Proceedings 6th International Conference on Concurrency Theory. Proceedings 6th International Conference on Concurrency Theory, CONCUR’95. Proceedings 6th International Conference on Concurrency Theory. Proceedings 6th International Conference on Concurrency Theory, CONCUR’95, LNCS, vol. 962 (1995), Springer), 313-327
[21] Brinksma, E.; Rensink, A.; Vogler, W., Applications of fair testing, (Gotzhein, R.; Bredereke, J., Proceedings IFIP TC6 WG6.1 International Conference on Formal Description Techniques IX: Theory, Application and Tools/Protocol Specification, Testing and Verification XVI, IFIP Conference Proceedings 69 (1996), Chapman & Hall), 145-160
[22] Bartlett, K. A.; Scantlebury, R. A.; Wilkinson, P. T., A note on reliable full-duplex transmission over half-duplex links, Commun. ACM, 12, 260-261 (1969)
[23] Baeten, J. C.M.; Weijland, W. P., Process Algebra, Cambridge Tracts in Theoretical Computer Science, vol. 18 (1990), Cambridge University Press · Zbl 0716.68002
[24] Corradini, F.; Di Berardini, M. R.; Vogler, W., Fairness of actions in system computations, Acta Inform., 43, 2, 73-130 (2006) · Zbl 1097.68087
[25] Corradini, F.; Di Berardini, M. R.; Vogler, W., Fairness of components in system computations, Theor. Comput. Sci., 356, 3, 291-324 (2006) · Zbl 1092.68065
[26] Corradini, F.; Di Berardini, M. R.; Vogler, W., Liveness of a mutex algorithm in a fair process algebra, Acta Inform., 46, 3, 209-235 (2009) · Zbl 1166.68030
[27] Corradini, F.; Di Berardini, M. R.; Vogler, W., Time and fairness in a process algebra with non-blocking reading, (Nielsen, M.; Kucera, A.; Miltersen, P. B.; Palamidessi, C.; Tuma, P.; Valencia, F. D., Theory and Practice of Computer Science. Theory and Practice of Computer Science, SOFSEM’09. Theory and Practice of Computer Science. Theory and Practice of Computer Science, SOFSEM’09, LNCS, vol. 5404 (2009), Springer), 193-204 · Zbl 1206.68213
[28] Cleaveland, R.; Lüttgen, G.; Natarajan, V., Priority in process algebra, (Bergstra, J. A.; Ponse, A.; Smolka, S. A., Handbook of Process Algebra (2001), Elsevier), 711-765, chapter 12 · Zbl 1062.68079
[29] Costa, G.; Stirling, C., A fair calculus of communicating systems, Acta Inform., 21, 417-441 (1984) · Zbl 0538.68014
[30] Costa, G.; Stirling, C., Weak and strong fairness in CCS, Inf. Comput., 73, 3, 207-244 (1987) · Zbl 0618.68026
[31] Cleaveland, R.; Sokolsky, O., Equivalence and preorder checking for finite-state systems, (Bergstra, J. A.; Ponse, A.; Smolka, S. A., Handbook of Process Algebra (2001), Elsevier), 391-424, chapter 6 · Zbl 1020.68062
[32] Dyseryn, V.; van Glabbeek, R. J.; Höfner, P., Analysing mutual exclusion using process algebra with signals, (Peters, K.; Tini, S., Proceedings Combined 24th International Workshop on Expressiveness in Concurrency and 14th Workshop on Structural Operational Semantics. Proceedings Combined 24th International Workshop on Expressiveness in Concurrency and 14th Workshop on Structural Operational Semantics, EPTCS, vol. 255 (2017), Open Publishing Association), 18-34
[33] Deng, Y.; van Glabbeek, R. J.; Hennessy, M.; Morgan, C. C., Characterising testing preorders for finite probabilistic processes, Log. Methods Comput. Sci., 4, 4, 4 (2008) · Zbl 1161.68035
[34] De Nicola, R.; Hennessy, M., Testing equivalences for processes, Theor. Comput. Sci., 34, 83-133 (1984) · Zbl 0985.68518
[35] Emerson, E. A.; Clarke, E. M., Using branching time temporal logic to synthesize synchronization skeletons, Sci. Comput. Program., 2, 3, 241-266 (1982) · Zbl 0514.68032
[36] Fehnker, A.; van Glabbeek, R. J.; Höfner, P.; McIver, A. K.; Portmann, M.; Tan, W., A process algebra for wireless mesh networks, (Seidl, H., Programming Languages and Systems: Proceedings 21st European Symposium on Programming. Programming Languages and Systems: Proceedings 21st European Symposium on Programming, ESOP’12. Programming Languages and Systems: Proceedings 21st European Symposium on Programming. Programming Languages and Systems: Proceedings 21st European Symposium on Programming, ESOP’12, LNCS, vol. 7211 (2012), Springer), 295-315 · Zbl 1352.68183
[37] Fehnker, A.; van Glabbeek, R. J.; Höfner, P.; McIver, A. K.; Portmann, M.; Tan, W. L., A Process Algebra for Wireless Mesh Networks used for Modelling, Verifying and Analysing AODV (2013), NICTA, Technical Report 5513
[38] Fokkink, W. J.; van Glabbeek, R. J.; de Wind, P., Divide and congruence: from decomposition of modal formulas to preservation of branching and η-bisimilarity, Inf. Comput., 214, 59-85 (2012) · Zbl 1277.68182
[39] Fokkink, W. J., Introduction to Process Algebra, Texts in Theoretical Computer Science, An EATCS Series (2000), Springer · Zbl 0941.68087
[40] Fokkink, W. J., Rooted branching bisimulation as a congruence, J. Comput. Syst. Sci., 60, 1, 11-27 (2000)
[41] Gibson-Robinson, T.; Armstrong, P. J.; Boulgakov, A.; Roscoe, A. W., FDR3 - a modern refinement checker for CSP, (Ábrahám, E.; Havelund, K., Proceedings 20th International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Proceedings 20th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS’14. Proceedings 20th International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Proceedings 20th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS’14, LNCS, vol. 8413 (2014), Springer), 187-201 · Zbl 1392.68300
[42] van Glabbeek, R. J.; Goltz, U., Refinement of actions and equivalence notions for concurrent systems, Acta Inform., 37, 229-327 (2001) · Zbl 0969.68081
[43] van Glabbeek, R. J.; Goltz, U.; Schicke-Uffmann, J.-W., On characterising distributability, Log. Methods Comput. Sci., 9, 3, 17 (2013) · Zbl 1274.68261
[44] van Glabbeek, R. J.; Höfner, P., CCS: It’s not fair! Fair schedulers cannot be implemented in CCS-like languages even under progress and certain fairness assumptions, Acta Inform., 52, 2-3, 175-205 (2015) · Zbl 1327.68171
[45] van Glabbeek, R. J.; Höfner, P., Progress, Fairness and Justness in Process Algebra (2015), NICTA: NICTA Sydney, Australia, Technical Report 8501
[46] van Glabbeek, R. J.; Höfner, P., Progress, justness and fairness (Survey paper), ACM Comput. Surv. (2019), in press
[47] van Glabbeek, R. J., Bisimulations for higher dimensional automata (1991), Email message July 7, 1991
[48] van Glabbeek, R. J., The linear time – branching time spectrum, II: the semantics of sequential systems with silent moves (extended abstract), (Best, E., Proceedings of the 4th International Conference on Concurrency Theory. Proceedings of the 4th International Conference on Concurrency Theory, CONCUR’93. Proceedings of the 4th International Conference on Concurrency Theory. Proceedings of the 4th International Conference on Concurrency Theory, CONCUR’93, LNCS, vol. 715 (1993), Springer), 66-81
[49] van Glabbeek, R. J., On the expressiveness of ACP (extended abstract), (Ponse, A.; Verhoef, C.; van Vlijmen, S. F.M., Proceedings First Workshop on the Algebra of Communicating Processes. Proceedings First Workshop on the Algebra of Communicating Processes, ACP’94, Workshops in Computing (1994), Springer), 188-217
[50] van Glabbeek, R. J., The linear time – branching time spectrum, I: the semantics of concrete, sequential processes, (Bergstra, J. A.; Ponse, A.; Smolka, S. A., Handbook of Process Algebra, chapter 1 (2001), Elsevier), 3-99 · Zbl 1035.68073
[51] van Glabbeek, R. J., The coarsest precongruences respecting safety and liveness properties, (Calude, C. S.; Sassone, V., Proceedings 6th IFIP TC 1/WG 2.2 International Conference on Theoretical Computer Science (TCS 2010), held as part of the World Computer Congress 2010. Proceedings 6th IFIP TC 1/WG 2.2 International Conference on Theoretical Computer Science (TCS 2010), held as part of the World Computer Congress 2010, IFIP, vol. 323 (2010), Springer), 32-52 · Zbl 1202.68268
[52] van Glabbeek, R. J., Bisimulation, (Padua, D., Encyclopedia of Parallel Computing (2011), Springer), 136-139
[53] van Glabbeek, R. J., On cool congruence formats for weak bisimulations, Theor. Comput. Sci., 412, 28, 3283-3302 (2011) · Zbl 1216.68199
[54] van Glabbeek, R. J., Musings on encodings and expressiveness, (Luttik, B.; Reniers, M. A., Proceedings EXPRESS/SOS’19. Proceedings EXPRESS/SOS’19, EPTCS, vol. 89 (2012), Open Publishing Association), 81-98
[55] van Glabbeek, R. J., Structure preserving bisimilarity, supporting an operational petri net semantics of CCSP, (Meyer, R.; Platzer, A.; Wehrheim, H., Proceedings of Correct System Design - Symposium in Honor of Ernst-Rüdiger Olderog on the Occasion of His 60th Birthday. Proceedings of Correct System Design - Symposium in Honor of Ernst-Rüdiger Olderog on the Occasion of His 60th Birthday, LNCS, vol. 9360 (2015), Springer), 99-130 · Zbl 1444.68125
[56] van Glabbeek, R. J., Lean and full congruence formats for recursion, (Proceedings of 32nd Annual ACM/IEEE Symposium on Logic in Computer Science. Proceedings of 32nd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS, vol. 2017 (2017), IEEE Computer Society Press)
[57] van Glabbeek, R. J., Justness: a completeness criterion for capturing liveness properties (extended abstract), (Bojańczyk, M.; Simpson, A., Proc. FoSSaCS’19. Proc. FoSSaCS’19, Data61, CSIRO, Sydney, Australia. Proc. FoSSaCS’19. Proc. FoSSaCS’19, Data61, CSIRO, Sydney, Australia, LNCS, vol. 11425 (2019), Springer), 505-522, Technical Report
[58] van Glabbeek, R. J., Reward testing equivalences for processes, (Boreale, M.; Corradini, F.; Loreti, M.; Pugliese, R., Models, Languages, and Tools for Concurrent and Distributed Programming, Essays Dedicated to Rocco De Nicola on the Occasion of His 65th Birthday. Models, Languages, and Tools for Concurrent and Distributed Programming, Essays Dedicated to Rocco De Nicola on the Occasion of His 65th Birthday, LNCS, vol. 11665 (2019), Springer), 45-70
[59] Garavel, H.; Lang, F.; Mateescu, R.; Serwe, W., CADP 2010: a toolbox for the construction and analysis of distributed processes, (Abdulla, P. A.; Leino, K. R.M., Proceedings 17th International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Proceedings 17th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS’11. Proceedings 17th International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Proceedings 17th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS’11, LNCS, vol. 6605 (2011), Springer), 372-387 · Zbl 1316.68074
[60] van Glabbeek, R. J.; Luttik, B.; Trčka, N., Branching bisimilarity with explicit divergence, Fundam. Inform., 93, 4, 371-392 (2009) · Zbl 1183.68404
[61] Goltz, U.; Mycroft, A., On the relationship of CCS and Petri nets, (Paredaens, J., Proceedings 11th ICALP. Proceedings 11th ICALP, LNCS, vol. 172 (1984), Springer), 196-208
[62] Groote, J. F.; Mousavi, M. R., Modeling and Analysis of Communicating Systems (2014), MIT Press
[63] Groote, J. F.; Mousavi, M. R.; Reniers, M. A., A hierarchy of SOS rule formats, Electron. Notes Theor. Comput. Sci., 156, 1, 3-25 (2006) · Zbl 1273.68206
[64] Gorla, D., Towards a unified approach to encodability and separation results for process calculi, Inf. Comput., 208, 9, 1031-1053 (2010) · Zbl 1209.68336
[65] Groote, J. F., Transition system specifications with negative premises, Theor. Comput. Sci., 118, 2, 263-299 (1993) · Zbl 0778.68057
[66] van Glabbeek, R. J.; Vaandrager, F. W., Petri net models for algebraic theories of concurrency (extended abstract), (de Bakker, J. W.; Nijman, A. J.; Treleaven, P. C., Proceedings PARLE, Parallel Architectures and Languages Europe, Vol. II: Parallel Languages. Proceedings PARLE, Parallel Architectures and Languages Europe, Vol. II: Parallel Languages, LNCS, vol. 259 (1987), Springer), 224-242
[67] Groote, J. F.; Vaandrager, F. W., Structured operational semantics and bisimulation as a congruence, Inf. Comput., 100, 2, 202-260 (1992) · Zbl 0752.68053
[68] van Glabbeek, R. J.; Vaandrager, F. W., Modular specification of process algebras, Theor. Comput. Sci., 113, 2, 293-348 (1993) · Zbl 0770.68092
[69] van Glabbeek, R. J.; Weijland, W. P., Branching time and abstraction in bisimulation semantics, J. ACM, 43, 3, 555-600 (1996), Available in part at · Zbl 0882.68085
[70] Hoare, C. A.R., Communicating Sequential Processes (1985), Prentice-Hall: Prentice-Hall Englewood Cliffs · Zbl 0637.68007
[71] Holzmann, G. J., The SPIN Model Checker - Primer and Reference Manual (2004), Addison-Wesley
[72] Henzinger, T. A.; Rajamani, S. K., Fair bisimulation, (Graf, S.; Schwartzbach, M. I., Proceedings 6th International Conference on Tools and Algorithms for Construction and Analysis of Systems. Proceedings 6th International Conference on Tools and Algorithms for Construction and Analysis of Systems, TACAS’00. Proceedings 6th International Conference on Tools and Algorithms for Construction and Analysis of Systems. Proceedings 6th International Conference on Tools and Algorithms for Construction and Analysis of Systems, TACAS’00, LNCS, vol. 1785 (2000), Springer), 299-314 · Zbl 0960.68121
[73] Kant, G.; Laarman, A.; Meijer, J.; van de Pol, J.; Blom, S.; van Dijk, T., LTSmin: high-performance language-independent model checking, (Baier, C.; Tinelli, C., Proceedings 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Proceedings 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS’15. Proceedings 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Proceedings 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS’15, LNCS, vol. 9035 (2015), Springer), 692-707
[74] Kwiatkowska, M.; Norman, G.; Parker, D., Advances and challenges of probabilistic model checking, (Proc. 48th Annual Allerton Conference on Communication, Control and Computing (2010), IEEE Press), 1691-1698
[75] Kuiper, R.; de Roever, W.-P., Fairness assumptions for CSP in a temporal logic framework, (Bjørner, D., Formal Description of Programming Concepts II (1983), North-Holland), 159-170 · Zbl 0512.68022
[76] Kindler, E.; Walter, R., Mutex needs fairness, Inf. Process. Lett., 62, 1, 31-39 (1997) · Zbl 1336.68182
[77] Lamport, L., Proving the correctness of multiprocess programs, IEEE Trans. Softw. Eng., 3, 2, 125-143 (1977) · Zbl 0349.68006
[78] Lamport, L., Specifying Systems, The TLA+ Language and Tools for Hardware and Software Engineers (2002), Addison-Wesley
[79] Lehmann, D. J.; Pnueli, A.; Stavi, J., Impartiality, justice and fairness: the ethics of concurrent termination, (Even, S.; Kariv, O., Automata, Languages and Programming. Automata, Languages and Programming, ICALP. Automata, Languages and Programming. Automata, Languages and Programming, ICALP, LNCS, vol. 115 (1981), Springer), 264-277 · Zbl 0468.68026
[80] Lynch, W. C., Reliable full-duplex file transmission over half-duplex telephone line, Commun. ACM, 11, 6, 407-410 (1968)
[81] Lynch, N. A., Distributed Algorithms (1996), Morgan Kaufmann · Zbl 0877.68061
[82] Milner, R., Communication and Concurrency, PHI Series in computer science (1989), Prentice-Hall · Zbl 0683.68008
[83] Milner, R., Communicating and Mobile Systems - the Pi-Calculus (1999), Cambridge University Press · Zbl 0942.68002
[84] McIver, A. K.; Morgan, C., Demonic, angelic and unbounded probabilistic choices in sequential programs, Acta Inform., 37, 4/5, 329-354 (2001) · Zbl 0971.68027
[85] Mazurkiewicz, A. W.; Ochmanski, E.; Penczek, W., Concurrent systems and inevitability, Theor. Comput. Sci., 64, 3, 281-304 (1989) · Zbl 0675.68015
[86] Morgan, C., Programming From Specifications, International series in computer science (1994), Prentice-Hall · Zbl 0829.68083
[87] Natarajan, V.; Cleaveland, R., Divergence and fair testing, (Fülöp, Z.; Gécseg, F., Proceedings 22nd International Colloquium on Automata, Languages and Programming. Proceedings 22nd International Colloquium on Automata, Languages and Programming, ICALP’95. Proceedings 22nd International Colloquium on Automata, Languages and Programming. Proceedings 22nd International Colloquium on Automata, Languages and Programming, ICALP’95, LNCS, vol. 944 (1995), Springer), 648-659 · Zbl 1412.68155
[88] Olderog, E.-R., Nets, Terms and Formulas: Three Views of Concurrent Processes and their Relationship, Cambridge Tracts in Theoretical Computer Science, vol. 23 (1991), Cambridge University Press · Zbl 0741.68002
[89] Perkins, C. E.; Belding-Royer, E. M.; Das, S., Ad Hoc On-Demand Distance Vector (AODV) Routing (2003), Network Working Group, RFC 3561
[90] Pnueli, A., The temporal logic of programs, (Foundations of Computer Science. Foundations of Computer Science, FOCS’77 (1977), IEEE), 46-57
[91] Pratt, V. R., Modeling concurrency with geometry, (Proc. 18th Annual ACM Symposium on Principles of Programming Languages (1991)), 311-322
[92] Reisig, W., Understanding Petri Nets — Modeling Techniques, Analysis Methods, Case Studies (2013), Springer · Zbl 1278.68222
[93] Roscoe, A. W., The Theory and Practice of Concurrency (1997), Prentice-Hall
[94] Segala, R., Testing probabilistic automata, (Proceedings of the 7th International Conference on Concurrency Theory. Proceedings of the 7th International Conference on Concurrency Theory, CONCUR’96. Proceedings of the 7th International Conference on Concurrency Theory. Proceedings of the 7th International Conference on Concurrency Theory, CONCUR’96, LNCS, vol. 1119 (1996), Springer), 299-314
[95] de Simone, R., Higher-level synchronising devices in Meije-SCCS, Theor. Comput. Sci., 37, 245-267 (1985) · Zbl 0598.68027
[96] Sangiorgi, D.; Walker, D., The π-Calculus: A Theory of Mobile Processes (2001), Cambridge University Press · Zbl 0981.68116
[97] Ulidowski, I., Equivalences on observable processes, (Proc. Seventh Annual Symposium on Logic in Computer Science. Proc. Seventh Annual Symposium on Logic in Computer Science, LICS’92 (1992), IEEE Computer Society), 148-159
[98] Ulidowski, I., Finite axiom systems for testing preorder and De Simone process languages, Theor. Comput. Sci., 239, 1, 97-139 (2000) · Zbl 0944.68125
[99] Ulidowski, I.; Phillips, I. C.C., Ordered SOS process languages for branching and eager bisimulations, Inf. Comput., 178, 1, 180-213 (2002) · Zbl 1012.68116
[100] Ulidowski, I.; Yuen, S., Process languages for rooted eager bisimulation, (Palamidessi, C., Proceedings 11th International Conference on Concurrency Theory. Proceedings 11th International Conference on Concurrency Theory, CONCUR’00. Proceedings 11th International Conference on Concurrency Theory. Proceedings 11th International Conference on Concurrency Theory, CONCUR’00, LNCS, vol. 1877 (2000), Springer), 275-289 · Zbl 0999.68143
[101] Verhoef, C., A congruence theorem for structured operational semantics with predicates and negative premises, Nord. J. Comput., 2, 2, 274-302 (1995) · Zbl 0839.68060
[102] Vogler, W., Modular Construction and Partial Order Semantics of Petri Nets, LNCS, vol. 625 (1992), Springer · Zbl 1293.68015
[103] Vogler, W., Efficiency of asynchronous systems, read arcs, and the MUTEX-problem, Theor. Comput. Sci., 275, 1-2, 589-631 (2002) · Zbl 1026.68099
[104] Walker, D. J., Bisimulation and divergence, Inf. Comput., 85, 2, 202-241 (1990) · Zbl 0713.68036
[105] Winskel, G., A new definition of morphism on Petri nets, (Fontet, M.; Mehlhorn, K., Proceedings STACS 84. Proceedings STACS 84, LNCS, vol. 166 (1984), Springer), 140-150
[106] Winskel, G., Event structures, (Brauer, W.; Reisig, W.; Rozenberg, G., Petri Nets: Applications and Relationships to Other Models of Concurrency, Advances in Petri Nets (1987)). (Brauer, W.; Reisig, W.; Rozenberg, G., Petri Nets: Applications and Relationships to Other Models of Concurrency, Advances in Petri Nets (1987)), Part II. (Brauer, W.; Reisig, W.; Rozenberg, G., Petri Nets: Applications and Relationships to Other Models of Concurrency, Advances in Petri Nets (1987)). (Brauer, W.; Reisig, W.; Rozenberg, G., Petri Nets: Applications and Relationships to Other Models of Concurrency, Advances in Petri Nets (1987)), Part II, LNCS, vol. 255, 325-392 (1986), Springer
[107] Yi, Wang; Larsen, K. G., Testing probabilistic and nondeterministic processes, (Proceedings of the IFIP TC6/WG6.1 Twelfth International Symposium on Protocol Specification, Testing and Verification, IFIP Transactions C-8 (1992), North-Holland), 47-61
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.