Local Invariance |
| |
Authors: | David H Pitt Michael Shields |
| |
Affiliation: | (1) Department of Computing, University of Surrey, Guildford, UK, GB |
| |
Abstract: | A local invariant is a set of states of a transition system with the property that every action possible from each of its
states takes the system back into the local invariant, unless it is an ‘exit’ action, each of which is accessible from every
state in the set via a sequence of non-‘exit’ actions. This idea supports a form of abstraction construction, abstracting
away from behaviour internal to the local invariants themselves, that involving their non-‘exit’ actions. In this way, for
example, it is possible to construct from a system one which exhibits precisely the externally visible behaviour. This abstraction
is reminiscent of hiding in process algebra, and we compare the notion of abstraction with that of observational equivalence
in process calculus.
Received August 2000 / Accepted in revised form March 2002
Correspondence and offprint requests to: David H. Pitt, Department of Computing, University of Surrey, Guildford GU2 5HX, UK. E-mail: d.pitt@eim.surrey.ac.ukau |
| |
Keywords: | : Abstraction Local invariance Protocol verification |
本文献已被 SpringerLink 等数据库收录! |
|