- Apr 2024
-
arxiv.org arxiv.org
-
Composing Implementations
Any
correctimplementationcan be composed with any other (compatible)correctimplementation, and it is guaranteed to becorrect. -
This implies that any correct run of the imple-mentation that stutters indefinitely has infinitely many opportunities to activatethe specification. Under the standard assumption that an opportunity that ispresented infinitely often is eventually seized, a live implementation does notdeadlock as it eventually activates the specification.
-
Live
I.e., there is a possible further computation from
ytoy', as well as fromsigma(y)tosigma(y').I.e., from any TS' computable mapped state
ythere is a computable mapped statey'. -
Complete
Any compute in a TS can be performed in an implementing TS TS'.
I.e., any compute in TS maps to compute in TS'.
I.e., any TS compute is translatable to TS'
-
Safe
I.e., any compute in an implementing TS TS' can be performed in TS.
I.e., any compute in TS' maps to compute in TS.
I.e., any TS' compute is translatable to TS.
-
implementedtransition system (henceforth – specification),
specificationis an implementation of a TS by a TS'. -
An implementation is correct if it is safe, complete and live.
-
Given two transition systems T S = (S, s0, T ) and T S′ = (S′, s′0, T ′) an im-plementation of T S by T S′ is a function σ : S′ → S where σ(s′0) = s0.
-
empty if s = s′
emptymeaning,noop\self?I guess any
shas suchemptytransition for it. -
Also note that T and T f are not necessarydisjoint, for the same reason that even a broken clock shows the correct houronce in a while
Huuh?
-
We denote by s ∗−→ s′ ∈ T the existence of a correctcomputation (empty if s = s′) from s to s′
-
A transition in T f \ T is faulty, and a computation is faulty if it
-
A transition s → s′ ∈ T is correct, and a computation of correct transitionsis correct.
-
a run of T S is a computation that starts froms0.
-
A computation of T S is a sequenceof transitions s −→ s′ −→ · · · ,
-
Atransition system T S = (S, s0, T, T f ) consists of a set of states S, an initialstate s0 ∈ S, a set of (correct) transitions T ⊆ S2 and a set of faulty transitionsT f ⊆ S2. If T f = ∅ then it may be omitted
-
the transitions over S are all pairs (s, s′) ∈ S2, also written s → s′.
-
Given a set S, referred to asstates,
-
→
What does * mean?
-