Document Open Access Logo

Progress, Justness and Fairness in Modal μ-Calculus Formulae

Authors Myrthe S. C. Spronck , Bas Luttik , Tim A. C. Willemse

PDF

File

Thumbnail PDF
PDF
LIPIcs.CONCUR.2024.38.pdf
  • Filesize: 0.75 MB
  • 22 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Modal and temporal logics
Keywords
  • Modal μ-calculus
  • Property specification
  • Completeness criteria
  • Progress
  • Justness
  • Fairness
  • Liveness properties

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Abstract

When verifying liveness properties on a transition system, it is often necessary to discard spurious violating paths by making assumptions on which paths represent realistic executions. Capturing that some property holds under such an assumption in a logical formula is challenging and error-prone, particularly in the modal μ-calculus. In this paper, we present template formulae in the modal μ-calculus that can be instantiated to a broad range of liveness properties. We consider the following assumptions: progress, justness, weak fairness, strong fairness, and hyperfairness, each with respect to actions. The correctness of these formulae has been proven.

Cite As Get BibTex

Myrthe S. C. Spronck, Bas Luttik, and Tim A. C. Willemse. Progress, Justness and Fairness in Modal μ-Calculus Formulae. In 35th International Conference on Concurrency Theory (CONCUR 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 311, pp. 38:1-38:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024) https://doi.org/10.4230/LIPIcs.CONCUR.2024.38

Author Details

Myrthe S. C. Spronck
  • Eindhoven University of Technology, The Netherlands
Bas Luttik
  • Eindhoven University of Technology, The Netherlands
Tim A. C. Willemse
  • Eindhoven University of Technology, The Netherlands

Acknowledgements

We thank an anonymous reviewer for the observation that weak and strong hyperfairness must be distinguished.

References

  1. Mack W. Alford, Leslie Lamport, and Geoff P. Mullery. Basic concepts. In Mack W. Alford, Jean-Pierre Ansart, Günter Hommel, Leslie Lamport, Barbara Liskov, Geoff P. Mullery, and Fred B. Schneider, editors, Distributed Systems: Methods and Tools for Specification, An Advanced Course, April 3-12, 1984 and April 16-25, 1985, Munich, Germany, volume 190 of Lecture Notes in Computer Science, pages 7-43. Springer, 1984. URL: https://doi.org/10.1007/3-540-15216-4_12.
  2. Krzysztof R. Apt, Nissim Francez, and Shmuel Katz. Appraising fairness in languages for distributed programming. Distributed Comput., 2(4):226-241, 1988. URL: https://doi.org/10.1007/BF01872848.
  3. Paul C. Attie, Nissim Francez, and Orna Grumberg. Fairness and hyperfairness in multi-party interactions. In Frances E. Allen, editor, Conference Record of the Seventeenth Annual ACM Symposium on Principles of Programming Languages, San Francisco, California, USA, January 1990, pages 292-305. ACM Press, 1990. URL: https://doi.org/10.1145/96709.96739.
  4. Pierfrancesco Bellini, Paolo Nesi, and Davide Rogai. Expressing and organizing real-time specification patterns via temporal logics. J. Syst. Softw., 82(2):183-196, 2009. URL: https://doi.org/10.1016/j.jss.2008.06.041.
  5. Mark S. Bouwman. Supporting Railway Standardisation with Formal Verification. Phd Thesis 1 (Research TU/e / Graduation TU/e), Mathematics and Computer Science, Eindhoven University of Technology, 2023. URL: https://pure.tue.nl/ws/portalfiles/portal/307965423/20231023_Bouwman_hf.pdf.
  6. Mark S. Bouwman, Bas Luttik, and Tim A. C. Willemse. Off-the-shelf automated analysis of liveness properties for just paths. Acta Informatica, 57(3-5):551-590, 2020. URL: https://doi.org/10.1007/s00236-020-00371-w.
  7. Julian C. Bradfield and Colin Stirling. Modal logics and mu-calculi: an introduction. In Jan A. Bergstra, Alban Ponse, and Scott A. Smolka, editors, Handbook of Process Algebra, pages 293-330. Elsevier Science, 2001. URL: https://doi.org/10.1016/b978-044482830-9/50022-9.
  8. Julian C. Bradfield and Colin Stirling. Modal mu-calculi. In Patrick Blackburn, Johan Van Benthem, and Frank Wolter, editors, Handbook of Modal Logic, volume 3 of Studies in logic and practical reasoning, pages 721-756. Elsevier, 2007. URL: https://doi.org/10.1016/s1570-2464(07)80015-2.
  9. Julian C. Bradfield and Igor Walukiewicz. The mu-calculus and model checking. In Edmund M. Clarke, Thomas A. Henzinger, Helmut Veith, and Roderick Bloem, editors, Handbook of Model Checking, pages 871-919. Springer, 2018. URL: https://doi.org/10.1007/978-3-319-10575-8_26.
  10. Olav Bunte, Jan Friso Groote, Jeroen J. A. Keiren, Maurice Laveaux, Thomas Neele, Erik P. de Vink, Wieger Wesselink, Anton Wijs, and Tim A. C. Willemse. The mCRL2 toolset for analysing concurrent systems. In Tomáš Vojnar and Lijun Zhang, editors, Tools and Algorithms for the Construction and Analysis of Systems - 25th International Conference, TACAS 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Prague, Czech Republic, April 6-11, 2019, Proceedings, Part II, volume 11428 of Lecture Notes in Computer Science, pages 21-39. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-17465-1_2.
  11. Edmund M. Clarke, Orna Grumberg, Kenneth L. McMillan, and Xudong Zhao. Efficient generation of counterexamples and witnesses in symbolic model checking. In Bryan Preas, editor, Proceedings of the 32st Conference on Design Automation, San Francisco, California, USA, Moscone Center, June 12-16, 1995, pages 427-432. ACM Press, 1995. URL: https://doi.org/10.1145/217474.217565.
  12. Rachel L. Cobleigh, George S. Avrunin, and Lori A. Clarke. User guidance for creating precise and accessible property specifications. In Michal Young and Premkumar T. Devanbu, editors, Proceedings of the 14th ACM SIGSOFT International Symposium on Foundations of Software Engineering, FSE 2006, Portland, Oregon, USA, November 5-11, 2006, pages 208-218. ACM, 2006. URL: https://doi.org/10.1145/1181775.1181801.
  13. Sjoerd Cranen, Jan Friso Groote, and Michel A. Reniers. A linear translation from CTL^⋆ to the first-order modal μ-calculus. Theor. Comput. Sci., 412(28):3129-3139, 2011. URL: https://doi.org/10.1016/j.tcs.2011.02.034.
  14. Edsger W Dijkstra. Over de sequentialiteit van procesbeschrijvingen (EWD-35). EW dijkstra archive. Center for American History, University of Texas at Austin, 1962. URL: https://www.cs.utexas.edu/~EWD/ewd00xx/EWD35.PDF.
  15. Edsger W. Dijkstra. Solution of a problem in concurrent programming control. Commun. ACM, 8(9):569, 1965. URL: https://doi.org/10.1145/365559.365617.
  16. Matthew B. Dwyer, George S. Avrunin, and James C. Corbett. Patterns in property specifications for finite-state verification. In Barry W. Boehm, David Garlan, and Jeff Kramer, editors, Proceedings of the 1999 International Conference on Software Engineering, ICSE' 99, Los Angeles, CA, USA, May 16-22, 1999, pages 411-420. ACM, 1999. URL: https://doi.org/10.1145/302405.302672.
  17. E. Allen Emerson and Edmund M. Clarke. Using branching time temporal logic to synthesize synchronization skeletons. Sci. Comput. Program., 2(3):241-266, 1982. URL: https://doi.org/10.1016/0167-6423(83)90017-5.
  18. Michael J. Fischer and Richard E. Ladner. Propositional dynamic logic of regular programs. J. Comput. Syst. Sci., 18(2):194-211, 1979. URL: https://doi.org/10.1016/0022-0000(79)90046-1.
  19. Hubert Garavel, Frédéric Lang, Radu Mateescu, and Wendelin Serwe. CADP 2011: a toolbox for the construction and analysis of distributed processes. Int. J. Softw. Tools Technol. Transf., 15(2):89-107, 2013. URL: https://doi.org/10.1007/s10009-012-0244-z.
  20. Rob J. van Glabbeek. Justness - A completeness criterion for capturing liveness properties (extended abstract). In Mikołaj ojańczyk and Alex Simpson, editors, Foundations of Software Science and Computation Structures - 22nd International Conference, FOSSACS 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Prague, Czech Republic, April 6-11, 2019, Proceedings, volume 11425 of Lecture Notes in Computer Science, pages 505-522. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-17127-8_29.
  21. Rob J. van Glabbeek. Reactive temporal logic. In Ornela Dardha and Jurriaan Rot, editors, Proceedings Combined 27th International Workshop on Expressiveness in Concurrency and 17th Workshop on Structural Operational Semantics, EXPRESS/SOS 2020, and 17th Workshop on Structural Operational SemanticsOnline, 31 August 2020, volume 322 of EPTCS, pages 51-68. Open Publishing Association, 2020. URL: https://doi.org/10.4204/EPTCS.322.6.
  22. Rob J. van Glabbeek. Modelling mutual exclusion in a process algebra with time-outs. Inf. Comput., 294:105079, 2023. URL: https://doi.org/10.1016/j.ic.2023.105079.
  23. Rob J. van Glabbeek and Peter Höfner. CCS: It’s not fair! fair schedulers cannot be implemented in CCS-like languages even under progress and certain fairness assumptions. Acta Informatica, 52(2-3):175-205, 2015. URL: https://doi.org/10.1007/s00236-015-0221-6.
  24. Rob J. van Glabbeek and Peter Höfner. Progress, Justness, and Fairness. ACM Comput. Surv., 52(4):69:1-69:38, 2019. URL: https://doi.org/10.1145/3329125.
  25. Jan Friso Groote and Jeroen J. A. Keiren. Tutorial: designing distributed software in mCRL2. In Kirstin Peters and Tim A. C. Willemse, editors, Formal Techniques for Distributed Objects, Components, and Systems - 41st IFIP WG 6.1 International Conference, FORTE 2021, Held as Part of the 16th International Federated Conference on Distributed Computing Techniques, DisCoTec 2021, Valletta, Malta, June 14-18, 2021, Proceedings, volume 12719 of Lecture Notes in Computer Science, pages 226-243. Springer, 2021. URL: https://doi.org/10.1007/978-3-030-78089-0_15.
  26. Jan Friso Groote and Mohammad Reza Mousavi. Modeling and Analysis of Communicating Systems. MIT Press, August 2014. URL: https://mitpress.mit.edu/books/modeling-and-analysis-communicating-systems.
  27. Lars Grunske. Specification patterns for probabilistic quality properties. In Wilhelm Schäfer, Matthew B. Dwyer, and Volker Gruhn, editors, 30th International Conference on Software Engineering (ICSE 2008), Leipzig, Germany, May 10-18, 2008, pages 31-40. ACM, 2008. URL: https://doi.org/10.1145/1368088.1368094.
  28. Sascha Konrad and Betty H. C. Cheng. Real-time specification patterns. In Gruia-Catalin Roman, William G. Griswold, and Bashar Nuseibeh, editors, 27th International Conference on Software Engineering (ICSE 2005), 15-21 May 2005, St. Louis, Missouri, USA, pages 372-381. ACM, 2005. URL: https://doi.org/10.1145/1062455.1062526.
  29. Dexter Kozen. Results on the propositional μ-calculus. Theor. Comput. Sci., 27(3):333-354, 1983. URL: https://doi.org/10.1016/0304-3975(82)90125-6.
  30. Leslie Lamport. Fairness and hyperfairness. Distributed Comput., 13(4):239-245, 2000. URL: https://doi.org/10.1007/PL00008921.
  31. Radu Mateescu. Property Pattern Mappings for RAFMC, 2019. Available at: https://cadp.inria.fr/resources/evaluator/rafmc.html (Accessed: 26 January 2024).
  32. Amir Pnueli. The temporal logic of programs. In 18th Annual Symposium on Foundations of Computer Science, Providence, Rhode Island, USA, 31 October - 1 November 1977, pages 46-57. IEEE Computer Society, 1977. URL: https://doi.org/10.1109/SFCS.1977.32.
  33. Jaco van de Pol and Michael Weber. A multi-core solver for parity games. Electronic Notes in Theoretical Computer Science, 220(2):19-34, 2008. Proceedings of the 7th International Workshop on Parallel and Distributed Methods in verifiCation (PDMC 2008). URL: https://doi.org/10.1016/j.entcs.2008.11.011.
  34. Daniela Remenska. Bringing Model Checking Closer To Practical Software Engineering. PhD thesis, Vrije U., Amsterdam, 2016. PhD Thesis, available at: URL: https://hdl.handle.net/1871/53958.
  35. Myrthe S. C. Spronck. Fairness assumptions in the modal μ-calculus, 2023. Master’s thesis, Eindhoven University of Technology, available at URL: https://research.tue.nl/en/studentTheses/fairness-assumptions-in-the-modal-%C2%B5-calculus.
  36. Frank A. Stomp, Willem-Paul de Roever, and Rob T. Gerth. The μ-calculus as an assertion-language for fairness arguments. Inf. Comput., 82(3):278-322, 1989. URL: https://doi.org/10.1016/0890-5401(89)90004-7.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact