×

zbMATH — the first resource for mathematics

UNITY and Büchi automata. (English) Zbl 07349689
Summary: 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 automaton for a given LTL formula that accepts precisely those runs that satisfy the formula.
MSC:
68-XX Computer science
Software:
SPIN; UNITY
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Abadi M, Lamport L (1991) The existence of refinement mappings. Theor Comput Sci 82:253-284 · Zbl 0728.68083
[2] Baier, C.; Katoen, JP, Principles of model checking (2008), Cambridge: MIT Press, Cambridge · Zbl 1179.68076
[3] Back, R-J; Kurki-Suonio, R., Distributed cooperation with action systems, ACM Trans Program Lang Syst, 10, 513-554 (1988) · Zbl 0663.68028
[4] 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] Collette, P.; Knapp, EA, foundation for modular reasoning about safety and progress properties of state-based concurrent programs, Theor Comput Sci, 183, 253-279 (1997) · Zbl 0901.68034
[6] Chandy, KM; Misra, J., Parallel program design, a foundation (1988), Reading, MA: Addison-Wesley, Reading, MA · Zbl 0717.68034
[7] Chandy, KM; Sanders, BA, Predicate transformers for reasoning about concurrent computation, Sci Comput Program, 24, 129-148 (1995) · Zbl 0939.68645
[8] Dijkstra, EW, A discipline of programming (1976), Englewood cliffs: Prentice Hall, Englewood cliffs · Zbl 0368.68005
[9] Dijkstra, RM, DUALITY: a simple formalism for the analysis of UNITY, Formal Aspects Comput, 7, 353-388 (1995) · Zbl 0835.68067
[10] Dijkstra, RM, Computation calculus bridging a formalization gap, Sci Comput Program, 37, 3-36 (2000) · Zbl 0954.68042
[11] Dijkstra, RM; Sanders, BA, A predicate transformer for the progress property “to-always”, Formal Aspects of Comput, 9, 270-282 (1997) · Zbl 0887.68036
[12] Gerth R, Pnueli A (1989) Rooting UNITY. In: Proceedings of the 5th international workshop on software specification and design, pp 11-19. ACM
[13] Gerth, R.; Peled, D.; Vardi, MY; Wolper, P., On-the-fly automatic verification of linear temporal logic, Proceedings 15th workshop on protocol specification, testing, and verification, 3-18 (1995), Warsaw, Poland: Chapman & Hall, Warsaw, Poland
[14] Gumm HP, Zhukov D (1996) On strong fairness in UNITY. Technical Report, Philipps Universität Marburg
[15] Hesselink, WH, Programs, recursion and unbounded choice, predicate transformation semantics and transformation rules (1992), Cambridge: Cambridge University Press, Cambridge · Zbl 0759.68057
[16] Hesselink, WH, Complete assertional proof rules for progress under weak and strong fairness, Sci Comput Program, 78, 1521-1537 (2013)
[17] Hesselink WH (2020) PVS proof script for: UNITY and Büchi automata. http://wimhesselink.nl/mechver/unity-and-beyond
[18] Holzmann GJ (2004) The SPIN model checker, primer and reference manual. Addison-Wesley, Reading
[19] 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] Knapp E (1992) Refinement as a basis for concurrent program design. PhD thesis, The University of Texas at Austin
[21] 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 · Zbl 1044.03522
[22] Lamport, L., What good is temporal logic?, Inf Process, 83, 657-668 (1983)
[23] Lamport, L., The temporal logic of actions, ACM Trans Program Lang Syst, 16, 872-923 (1994)
[24] Misra, J., A discipline of multiprogramming: programming theory for distributed applications (2001), New York: Spinger, New York · Zbl 0999.68121
[25] Morgan C (1987/88) Data refinement by miracles. Inf Process Lett, pp 243-246
[26] 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] 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, 424-439 (2009), New York: Springer, New York · Zbl 1252.68196
[28] Tsay, Y-K; Bagrodia, RL, Deducing fairness properties in UNITY logic: a new completeness result, ACM Trans Program Lang Syst, 17, 16-27 (1995)
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.