[cap-talk] Is "Authority" Subjective?

[David Hopwood]

David Wagner wrote:
> Toby Murray writes:
>> Suppose we have a system represented as the following CSP process:
>>
>> P = a1 -> a2 -> b -> STOP [] 
>>     b -> STOP
>
> If yes, my concern with this framework is that the non-determinism
> in the CSP process P conflates several different kinds of choices or
> several different sources of non-determinism:

In CSP as conventionally interpreted, P has no nondeterminism. It is
a process with deterministic behaviour depending on the environment it
is placed in. There is a separate operator ⊓ (U+2293 SQUARE CAP), that
introduces nondeterminism and is quite different from [] (choice).
It sounds as though Toby may be using a different interpretation,
but I don't understand precisely what the difference is.

>   1) The choices that Alice has: i.e., the different actions that
>      Alice might take, depending upon how she is instantiated.
>   2) Any non-determinism inherent in Alice's instantiation, if you
>      allow Alice's strategy to itself be non-deterministic.
>   3) The choices that Bob has: i.e., the different actions that
>      Bob might take, depending upon how he is instantiated.
>   4) Any non-determinism inherent in Bob's instantiation, if you
>      allow Bob's strategy to itself be non-deterministic.
>   5) Non-determinism due to scheduling or message interleaving.
> When I see a non-deterministic choice in the process P, it looks
> difficult to me to infer which of those 5 sources it might have
> come from.
> 
> Moreover, the framework combines all allowable instantiations of
> Alice with all allowable instantiations of Bob.  When we want to
> think about whether Alice has authority over Bob, we want to hold
> Bob's instantiation fixed, and vary how Alice is instantiated.
> In other words, we want to vary Alice's behavior (this is the
> counterfactual part of the reasoning) and see how this affects
> things, but we want to hold the code that implements Bob fixed so
> that it doesn't confound our analysis.

If we don't know the code of bob, then for a conservative analysis,
don't we want to consider the maximum authority that alice might have
for any instantiation of bob?

If we do know the code of bob, then that will be included in the
system description that we are analysing.

-- 
David Hopwood <david.hopwood at industrial-designers.co.uk>