Download PDF

UNITY and Büchi automata

Formal Aspects of Computing (2021)Cite this article

Abstract

UNITY is a model for concurrent specifications with a complete logic for proving progress properties of the form “P leads to Q”. UNITY is generalized to U-specifications by giving more freedom to specify the steps that are to be taken infinitely often. In particular, these steps can correspond to non-total relations. The generalization keeps the logic sound and complete. The paper exploits the generalization in two ways. Firstly, the logic remains sound when the specification is extended with hypotheses of the form “F leads to G”. As the paper shows, this can make the logic incomplete. The generalization is used to show that the logic remains complete, if the added hypotheses “F leads to G” satisfy “F unless G”. The main result extends the applicability and completeness of UNITY logic to proofs that a given concurrent program satisfies any given formula of LTL, linear temporal logic, without the next-operator which is omitted because it is sensitive to stuttering. For this purpose, the program, written as a UNITY program, is extended with a number of boolean variables. The proof method relies on implementing the LTL formula, i.e., restricting the specification in such a way that only those runs remain that satisfy the formula. This result is a variation of the classical construction of a Büchi automatonfor a given LTL formula that accepts precisely those runs that satisfy the formula.

References

  1. AL91

    Abadi M, Lamport L (1991) The existence of refinement mappings. Theor Comput Sci 82:253–284

  2. BK08

    Baier, C., Katoen, J.P.: Principles of model checking. MIT Press, Cambridge (2008)

    Google Scholar 

  3. BKS88

    Back, R.-J., Kurki-Suonio, R.: Distributed cooperation with action systems. ACM Trans Program Lang Syst 10, 513–554 (1988)

    Article  Google Scholar 

  4. Bue60

    Buechi JR (1960) On a decision method in restricted second order arithmetic. In: Proceedings of international congress on logic, methodology and philosophy of science, pp 1–11. Stanford University Press

  5. CK97

    Collette, P., Knapp, E.A.: foundation for modular reasoning about safety and progress properties of state-based concurrent programs. Theor Comput Sci 183, 253–279 (1997)

    MathSciNet  Article  Google Scholar 

  6. CM88

    Chandy, K.M., Misra, J.: Parallel program design, a foundation. Addison-Wesley, Reading, MA (1988)

    Google Scholar 

  7. CS95

    Chandy, K.M., Sanders, B.A.: Predicate transformers for reasoning about concurrent computation. Sci Comput Program 24, 129–148 (1995)

    MathSciNet  Article  Google Scholar 

  8. Dij76

    Dijkstra, E.W.: A discipline of programming. Prentice Hall, Englewood cliffs (1976)

    Google Scholar 

  9. Dij95

    Dijkstra, R.M.: DUALITY: a simple formalism for the analysis of UNITY. Formal Aspects Comput 7, 353–388 (1995)

    Article  Google Scholar 

  10. Dij00

    Dijkstra, R.M.: Computation calculus bridging a formalization gap. Sci Comput Program 37, 3–36 (2000)

    MathSciNet  Article  Google Scholar 

  11. DS97

    Dijkstra, R.M., Sanders, B.A.: A predicate transformer for the progress property `to-always'. Formal Aspects of Comput 9, 270–282 (1997)

    Article  Google Scholar 

  12. GP89

    Gerth R, Pnueli A (1989) Rooting UNITY. In: Proceedings of the 5th international workshop on software specification and design, pp 11–19. ACM

  13. GPVW95

    Gerth, R., Peled, D., Vardi, M.Y., Wolper, P.: On-the-fly automatic verification of linear temporal logic. Proceedings 15th workshop on protocol specification, testing, and verification, pp. 3–18. Chapman & Hall, Warsaw, Poland (1995)

    Google Scholar 

  14. GZ96

    Gumm HP, Zhukov D (1996) On strong fairness in UNITY. Technical Report, Philipps Universität Marburg

  15. Hes92

    Hesselink, W.H.: Programs, recursion and unbounded choice, predicate transformation semantics and transformation rules. Cambridge University Press, Cambridge (1992)

    Google Scholar 

  16. Hes13

    Hesselink, W.H.: Complete assertional proof rules for progress under weak and strong fairness. Sci Comput Program 78, 1521–1537 (2013). doi:https://doi.org/10.1016/j.scico.2012.10.013

    Article  Google Scholar 

  17. Hes20

    Hesselink WH (2020) PVS proof script for: UNITY and Büchi automata. http://wimhesselink.nl/mechver/unity-and-beyond

  18. Hol04

    Holzmann GJ (2004) The SPIN model checker, primer and reference manual. Addison-Wesley, Reading

  19. JKR89

    Jutla CS, Knapp E, Rao JR (1989) A predicate transformer approach to semantics of parallel programs. In: Proceedings of 8th annual ACM symposium on principles of distributed computing. ACM Press, pp 249–263

  20. Kna92

    Knapp E (1992) Refinement as a basis for concurrent program design. PhD thesis, The University of Texas at Austin

  21. Kna94

    Knapp E (1994) Soundness and completeness of UNITY logic. In: Thiagarajan PS, (ed) Foundations of software technology and theoretical computer science, vol 880 of LNCS. Spinger, pp 378–389

  22. Lam83

    Lamport, L.: What good is temporal logic? Inf Process 83, 657–668 (1983)

    Google Scholar 

  23. Lam94

    Lamport, L.: The temporal logic of actions. ACM Trans Program Lang Syst 16, 872–923 (1994)

    Article  Google Scholar 

  24. Mis01

    Misra, J.: A discipline of multiprogramming: programming theory for distributed applications. Spinger, New York (2001)

    Google Scholar 

  25. Mor88

    Morgan C (1987/88) Data refinement by miracles. Inf Process Lett, pp 243–246

  26. MP83

    Manna Z, Pnueli A (1983) How to cook a temporal proof system for your pet language. In: Proceedings 10th annual symposium on principles of programming languages (POPL). ACM, pp 141–154

  27. SMS09

    Schimpf, A., Merz, S., Smaus, J.-G.: Construction of Büchi automata for LTL model checking verified in Isabel/HOL. International conference on theorem proving in higher order logics, TPHOLs 2009, vol 5674 of LNCS, pp. 424–439. Springer, New York (2009)

    Google Scholar 

  28. TB95

    Tsay, Y.-K., Bagrodia, R.L.: Deducing fairness properties in UNITY logic: a new completeness result. ACM Trans Program Lang Syst 17, 16–27 (1995)

    Article  Google Scholar 

Download references

Acknowledgements

I am indepted and very grateful to Ernie Cohen who taught me the main results of this paper many years ago.We had planned tomake this a joint paper, but circumstances intervened.Henoweven abstains frombeing a coauthor.

Author information

Affiliations

  1. Bernoulli Institute, University of Groningen, Groningen, P.O. Box 407, 9700 AK, The Netherlands

    Wim H. Hesselink

Authors
  1. Wim H. Hesselink
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Wim H. Hesselink.

Additional information

Eerke Albert Boiten

Rights and permissions

Open Access This article is licensed under a Creative Commons Attribution 4.0 International License, which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons licence, and indicate if changes were made. The images or other third party material in this article are included in the article's Creative Commons licence, unless indicated otherwise in a credit line to the material. If material is not included in the article's Creative Commons licence and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder. To view a copy of this licence, visit http://creativecommons.org/licenses/by/4.0/.

Reprints and Permissions

About this article

Verify currency and authenticity via CrossMark

Cite this article

Hesselink, W.H. UNITY and Büchi automata. Form Asp Comp (2021). https://doi.org/10.1007/s00165-020-00528-x

Download citation

Keywords

  • Concurrency
  • Progress
  • UNITY
  • LTL
  • Büchi automaton