Give a CCS process which describes a coffee machine that may behave
like that given by (2.1) but may also steal the money it receives and
fail at any time.
This exercise is not quite well-defined. Should it sometimes take the
money and offer nothing in return, but continue functioning, or should
it actually fail sometimes and break down? The former case would be
described by
A finite process graph is a quadruple , where
• is a finite set of states,
• is a finite set of labels,
• is the start state, and
• is the transition function.
Using the operators introduced so far, give a CCS process that describes .
where is supposed to be a big iterative operator like
, if only I could get MathJax to accept \scalerel. The equation
is nested infinitely deep at most places that result in a loop that
doesn't include , and in some places end with , if .
Identity relation is an equivalence relation, as well as the universal
relation is. The standard relation is not an equivalence relation
(but it is a preorder, since it is an order). However, the parity relation
is.
To answer these questions, consider the coffee and tea machine CTM
defined in (2.2) and compare it with the following machine:
You should be able to convince yourself that CTM and CTM' afford the
same traces. (Do so!)
It suffices to show that traces of one recursive iteration of CTM and CTM'
are equivalent. The trace of CTM' is
(choose at the beginning, then insert coin & get beverage), the trace
of CTM is
(insert coin, then choose).
1. Do the processes (CA|CTM)\{coin, coffee, tea} and (CA|CTM')\{coin,
coffee, tea} defined above have the same completed traces?
Yes. Both processes start able to making the coin transition. Then
(CA|CTM') either finds itself in the coffee arm, makes the coffee
transition and returns to the starting state, or gets stuck only emitting
tea, but only accepting coffee. (CA|CTM) decides after the first coin
transition; if CTM transitions into the tea arm, we have a deadlock,
but if it transitions into the coffee arm, it can transition and returns
to the starting state.
For them to have different traces, CTM in (CA|CTM) would need to decide
which arm to transition into by knowing which transitions are available
in CA, which isn't included in the formalism.
Both processes have traces that can be described by the regular expression
coin(,coffee,coin)*
2. Is it true that if P and Q are two CCS processes affording the
same completed traces and L is a set of labels then P\L and Q\L also
have the same completed traces?
Yes. The restriction operator \ only restricts transitions outside of
the process it applies to, inside that process the same transitions can
still occur.
To show that this relation is a bisimulation, we examine all steps in
the model:
For : transitions to via , and
transitions to via , with in .
transitions to via , and transitions to
via , with the same relation as above.
For : transitions to via , and
transitions to via , with in .
transitions to via , and transitions to
via , with the same relation as above.
For : transitions to via , and
transitions to via , with in
(the same holds for the transition action instead of and
instead of ).
transitions to via , and transitions to
via , with the same relation as above (and, similarly, also with
and ).
For : transitions to via , and
transitions to via , with in
(the same holds for the transition action instead of and
instead of ).
transitions to via , and transitions to
via , with the same relation as above (and, similarly, also with
and instead of ).
show that the union of an arbitrary family of bisimulations is always a bisimulation.
Let be the union of a family
of bisimulations ().
For not to be a bisimulation, there must exist a
and an with
so that there is no such
that with .
If such an exists, then it must have been an element of
a bisimulation . But, by definition, for that
so that ,
must have contained an element such that
, since is a
bisimulation. So exactly that must also be an element of
because and elements don't just
get lost during a union.
Induction basis: If is a label, that is, if there exists an action
, then the definitions for strong bisimulation and string
bisimulation coincide (I'm not gonna write it all out, sorry).
Induction assumption: Assume that if is a sequence of actions, then
two states and are string bisimilar off they are strongly
bisimilar.
Induction step:
String bisimilarity strong bisimilarity:
If we know that are string bisimilar
by a transition , where is a single action. Then there must be
some so that
and and ,
and there must be some
, so that and
with
(and the other way around, with and exchanged), where
transitions to via . Then the induction
assumption holds, and we know that the states are also strongly bisimilar.
Strong bisimilarity string bisimilarity:
This is equivalent to the induction basis: if
strongly bisimilar via , then they are also string bisimilar via
.
I am slightly confused: doesn't strong bisimilarity apply to states,
and aren't and processes?
If there is no so that either or can transition to
another state, and are strongly bisimilar.
If , then
by first applying COM1 and then COM2, and so and
are strongly bisimilar.
Another idea: we can prove this by backward induction, e.g. assuming that
there is a final state , which can't transition further, and
then proving that every transition that lands there is a strong
bisimulation, and induced back as well?
The same holds if can transition via .
If , then
similarly
per COM3, so they're strongly bisimilar.
To be shown:
is a strong bisimulation.
Isn't this trivial? If , then surely
also , and if
, then
. -transitions are not possible here.
To be shown:
is a strong bisimulation.
Assume that makes an transition. Then:
If made the transition, then:
If made the transition, then on the right side can also make the transition
If made the transition, then on the right side can make the transition (e.g. to )
If made the transition, then on the right side can make the transition (e.g. to )
Otherwise asume that . Then
there must be a so that
and (or outputs
and inputs , but that's symmetric). Then similarly
by the same internal
transitions.
All other cases are symmetric, and I won't enumerate them here.
Since these relations are all bisimulations, it is clear that for any
, the mentioned combined processes are bisimilar.
Find three CCS processes such that .
I haven't been able to solve this completely yet. Let's take something
like ,
and . Then it could be the
case that in a bisimulation game, the attacker has chosen the
path on the left hand side, while the defender has chosen the
path on the right hand side. But this is not guaranteed.
can make only one transition, that is, . Then there exists a transition
in so that the result of the transition is to ,
namely , since by
definition. Therefore, action prefixing preserves bisimilarity.
Let there be a transition .
Then either the same transition was also possible before
the replacement (), in which
case no replacement took place, and the same transition should be
possible for () because we
assumed that , or a replacement took place. In that case,
the replacement would have replaced another variable (perhaps
because we thought that those greek variable names are boring after a
while),
so we assume (witout loss of generality) that .
Then we know that if and , then there is also a transition
so that .
Then the transition in the replacement version is
, and the
previous becomes
, so we know that
has the equivalent
for the transition.
is reflexive ()
because, if we assume can't make any transitions, the condition
is trivially fulfilled. If can make an transition
, the same on the right
hand side can also make that transition, and we know that
by induction.
Assume that there are so that
and , and
for every transition and there is
a so that
, and similarly for every
transition there is a
so that .
Now let there be a so that ,
then there must be the equivalent -transition to a , and
because that -transition exists for , the equivalent
must also exist.
Therefore it must also be the case that .
An equivalence relation is reflexive, symmetric, and transitive.
The converse is not true: can make an -transition,
but then it's stuck in .
For ,
.
Here, as well, the converse relation does not hold: When we do
the -transition, we have to decide which branch on the left to
take. But this brings us into a problematic situation: if we choose the
branch, we can't do the transition on the right anymore,
if we choose the branch, we can't do the transition on the
right anymore.
A binary relation is a simulation equivalence iff whenever
and is an action:
If then there is a transition so that
If then there is a transition so that
A binary relation is a bisimulation iff whenever
and is an action:
If then there is a transition so that
If then there is a transition so that
A relation is a strong bisimilarity iff there is a bisimulation
that relates them (the book is not clear on the exact distinction between
bisimulation and strong bisimulation, I have assumed they are the same).
This makes it fairly easy to see that the definitions of bisimulation
and simulation equivalence are the same. However, the definition of
strong bisimilarity requires the maximal bisimulation. So, for example,
for the processes , ,
is a simulation equivalence and also a bisimulation, but it is not
a strong bisimilarity equivalence (the maximal bisimulation being
).
There is a process that simulates every other CCS process, the null
process .
Show that observational equivalence is the largest symmetric relation
satisfying that whenever then, for
each action (including ), if then there is a transition
such that .
Assume there is a relation which satisfies the
conditions given for above. Then there must be two states
so that if
, then there must be
a transition so that
. Since
is supposed to be symmetric, the same must hold
for :
implies that there is a transition
so that .
We now have to determine whether, if we know that ,
we also know that . Then there are four different
cases:
If is realized by in the LTS, then this is equivalent to the definition of observational equivalence.
If is realized by in the LTS, then there must be a so that (per definition in the exercise), so we can take that relation as belonging to .
If is realized by in the LTS, then there must be a so that , only this time via a transition (i.e. ). So we can take that relation as belonging to . (This doesn't work! What if is realized by ? Then we can't just take the first part of the transition and declare it to be a transition. Hmmm.)
If is realized by , then we can again just chop off the last transition and declare the rest to be the transition, so that now and .
Since every transition is also a weak transition,
there can be no observational equivalence that isn't also in
. So is the biggest
observational equivalence .
Assume that there is some that the attacker would be able to play
, but not . Then the would decompose into
.
So the only additional possible action the attacker could additionally
play would be . But in this case, the defender can answer by doing
nothing, i.e. idling on the same state (see p. 89). So the additional
transition doesn't give the attacker any useful moves, and both
versions of the game are equivalent.
For example, you should be able to convince yourself
that the LTS associated with the CCS expression
has states.
Actually, I don't have a good idea of how to put this into LTS form?
I would have to invent a starting state , or maybe a set of
starting states, or perhaps starting states? Then those
would transition to via any subset of
.
Prove that the lub and the glb of are unique, if they exist.
must be an upper bound for , and for every
upper bound of . Per antisymmetry of ,
there can be no so that and with . And for to be an upper bound, then it
must be comparable to every other upper bound of , so there is no
uncomparable least other upper bound .
The same argument applies symmetrically to the greatest lower bound,
and is not worth elaborating.
: ✓ (all quantification with no elements automatically right)
: ✓
: ✗ ( can proceed with )
: ✓ ( ends up at again, which has no transitions, and an all quantification with no elements is automatically correct, even over unsatisfiable propositions like )
: ✗ (it is not possible to -transition from )
: ✓
: ✗ (it's impossible to transition from via )
: ✗ (since one can transition to via , and one can transition from via , which violates the )
Then we can argue: If , then every
that can be reached via from can also be reached in ,
and there might be some so that
there are some that can only reach those via ,
but no exists so that .
So
We can argue very similarly in the case : If , then
Assume there is a and
. Then either
, in which case it must be that
as well (since that
would mean that ), or there is some
so that but (since that would
violate the requirement that all -descendants of must be in
the set following the operator).
However, this would violate the assumption that .
So
Case :
Case :
How might we add negation to our logic?
We could define
.
However, this would violate monotonicity: If we define and , then
The attacker can pick the next state, which can only be
The next move is made by the referee of the game, and results in
The attacker then can decide on two moves:
If they pick , the defender is next
The defender can only pick the configuration
The defender wins
If they pick , the attacker is next
The attacker can only pick , which brings us back to $(s_2, \langle b \rangle \textit{t}!\textit{t} \land [b] X)$`, which means the game is infinite here
Since the formula is defined via , the defender wins
They don't want to pick , since then they are stuck
They can pick , and then are next
The only possible resulting state is , which the referee resolves to
They can now pick
Then the next state is , in which they win
For :
Starting with the configuration
The defender can pick:
Here they are stuck, and the attacker wins
The next configuration they can choose is
From there, the defender can choose two configurations:
The referee resolves this to
Either, the defender now cycles through indefinitely, by always choosing the transition, but then the attacker wins, since the formula is defined via , or they transition to , in which case the scenario described below happens, in which they also loose
The referee resolves this to
Now, the defender can either choose or , but is then stuck in both of these, so the attacker wins
A property that satisfies is ,
since we have a similar scenario to above, but the infinite
loop on makes it possible for the defender to win (since the
formula is defined via ).
