Eternity variables to prove simulation of specifications
| dc.creator | Hesselink, Wim H. | |
| dc.date | 2002-07-29 | |
| dc.date | 2003-08-27 | |
| dc.date.accessioned | 2026-07-07T07:51:49Z | |
| dc.date.available | 2026-07-07T07:51:49Z | |
| dc.description | Simulations of specifications are introduced as a unification and generalization of refinement mappings, history variables, forward simulations, prophecy variables, and backward simulations. A specification implements another specification if and only if there is a simulation from the first one to the second one that satisfies a certain condition. By adding stutterings, the formalism allows that the concrete behaviours take more (or possibly less) steps than the abstract ones. Eternity variables are introduced as a more powerful alternative for prophecy variables and backward simulations. This formalism is semantically complete: every simulation that preserves quiescence is a composition of a forward simulation, an extension with eternity variables, and a refinement mapping. This result does not need finite invisible nondeterminism and machine closure as in the Abadi-Lamport Theorem. Internal continuity is weakened to preservation of quiescence. | |
| dc.description | 28 pages, to appear in ACM-TOCL | |
| dc.identifier | https://arxiv.org/abs/cs/0207095 | |
| dc.identifier | http://arxiv.org/abs/cs/0207095 | |
| dc.identifier | ACM Trans. on Computational Logic 6 (2005) 175-201. | |
| dc.identifier.uri | http://salesiana.dossiersoluciones.com/handle/123456789/125658 | |
| dc.subject | Distributed, Parallel, and Cluster Computing | |
| dc.subject | Logic in Computer Science | |
| dc.subject | F.1.1;F.3.1 | |
| dc.title | Eternity variables to prove simulation of specifications | |
| dc.type | text |