Abstract
Given a transition system and a cover P of the set of its states, a set of local invariants with respect to P is defined as a set of predicates in bijection with the blocks of P and in such a way that a local invariant be true every time the system is in a state belonging to the corresponding block of the cover.
This definition is proved to be sufficiently general in the sense that any proof made by using global invariants can be also made by using sets of local invariants. The same result is proved for two more restrictive definitions of the notion of local invariant by using well-known properties of connections between lattices.
Finally, it is shown how the theory of connections can provide a general frame for tackling the problem of decomposing a global assertion into a logically equivalent set of local assertions.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
E.A. ASHCROFT “Proving assertions about parallel programs” Journal of Comp. and System Sciences 10, (1975), pp. 110–135.
A. BLIKLE “An algebraic approach to mathematical theory of programs” Polish Academy of Sciences, Report nℴ 119, Warszawa, 1973.
P. COUSOT “Méthodes itératives de construction et d'approximation de points fixes d'opérateurs monotones sur un treillis, analyse sémantique des programmes” Thèse d'Etat, Grenoble, March 1978.
P. COUSOT and R. COUSOT “Constructing program invariance proof methods” International Workshop on Program Construction, Château de Bonas, INRIA (Ed.) Sept. 1980, pp. 13–21.
R.W. FLOYD “Assigning meaning to programs” Proc. Symp. on Applied Mathematics, Vol. 19, I.T. Schwartz (Ed.), A.M.S., 1967, pp. 19–32.
C.A.R. HOARE “Some properties of predicate transformers” J.A.C.M., Vol. 25, nℴ 3, July 1978, pp. 461–480.
R.M. KELLER “Vector replacement systems: a formalism for modeling asynchronous systems” Princeton University technical report nℴ 117, December 1972.
R.M. KELLER “Formal verification of parallel programs” Comm. ACM, Vol. 19, nℴ 7, July 1976, pp. 371–384.
L. LAMPORT “Sometime” is sometimes “not never”-On the temporal logic of programs” Proc. of the 7th Annual ACM Symp. on Principles of Programming Languages Las Vegas, Jan. 1980, pp. 174–185.
Z. MANNA and R. WALDINGER “Is “sometime” sometimes better than “always” ?” Comm. ACM, Vol. 21, nℴ 2, Feb. 1978, pp. 159–172.
Z. MANNA and A. PNUELLI “Verification of concurrent programs: the temporal framework” Int. Summer School Theoretical Foundations of Programming Methodology, July 28 to August 9, 1981, Munich.
A. MAZURKIEWICZ “Proving properties of processes” Algorytmy, XI, nℴ 19, 1974, pp. 5–22.
O. ORE “Galois connexions”, Trans. A.M.S., 55 (1944), pp. 493–513.
A. PNUELLI “The temporal semantics of concurrent programs” LNCS Vol. 70, Springer Verlag, July 1979, pp. 1–20.
J.P. QUEILLE and J. SIFAKIS “Specification and verification of concurrent systems in CESAR: An example” Research report RR 254. IMAG, Grenoble, June 1981.
L.E. SANCHIS “Data types as lattices: retractions, closures and projectiores” RAIRO Informatique Théorique, Vol. 11, nℴ 4, 1977, pp. 329–344.
J. SIFAKIS “A unified approach for studying the properties of transition systems” Research report RR 179, IMAG, Grenoble, December 1979 (Revised December 1980); to appear in Theoretical Computer Science 1982.
J. SIFAKIS “Global and local invariants in transition systems” Research report RR nℴ 274, IMAG, Grenoble, November 1981.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1982 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Sifakis, J. (1982). Global and local invariants in transition systems. In: Nielsen, M., Schmidt, E.M. (eds) Automata, Languages and Programming. ICALP 1982. Lecture Notes in Computer Science, vol 140. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0012796
Download citation
DOI: https://doi.org/10.1007/BFb0012796
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-11576-2
Online ISBN: 978-3-540-39308-5
eBook Packages: Springer Book Archive