Syntax independent descriptions of message and state dependent behaviors

[degregat]

Behavioral commitments

To maximize optionality in implementation, we should define the behavioral commitments over messages that make up the protocol in ways that minimize syntactic assumptions.
We have defined a set of primitive data types to be used for message definitions. This post contains a proposal on how to specify the behaviors.

Defining a behavior

A behavioral definition for a stateful entity (e.g. an agent, engine or process) should consist of the following two descriptions, conceptually separated:

• Necessary preconditions a message needs to fulfill for the behavior to be applied. This needs to be defined only in terms of the message.
• What a valid state transition implementing the behavior looks like. This can take the message and entity state as an argument and send new messages.

This distinction is induced by physics: State is local to entities, but message properties can be evaluated at any time, when a message is available.

These behavioral definitions should only concern anything externally observable, i.e. which messages are sent depending on messages received, with any internal details (e.g. optimizations, language specific representation, syntax) being left up to choice of the implementor.

Any structure that is not directly relevant to a behavior can be considered opaque

When to decompose behaviors

Behaviors will be organized in sets corresponding to certain roles in, or layers of, the protocol. To separate behaviors and increase optionality in composition, messages over which behaviors are defined should be independent from messages over which other behaviors are defined.

Generally behaviors can be (de-)composed arbitrarily. Choices about the scope of inclusion into one behavior should be made according to what level of independence of the components seems desirable. Some rules of thumb:

• Generalization should be motivated by requirements of the system, or optionality desirable from an application perspective, not an end in itself.
• If a complex behavior can be decomposed into simpler components with straightforward composition, then decomposing it might be a good choice. If the composition is harder to analyze than the initial complex object, then it schould not be decomposed.
• If the decomposition requires assumptions that can not be justified by the underlying structure, it can mislead by introducing virtual structure that can easily be collapsed by defecting parties.

Composing behaviors

Composition can happen in different ways, for example:

• Messages output by one behavior are used as inputs for another.
• Messages can contain opaque bytestrings, which handed to another behavior which performs introspection. This can happen via local calls, or the bytestring can be treated as a message to be relayed.

Remarks

• Agent interaction with a node can be modelled in the form of messages.
• Introspection through all layers of a message, or taking into account local state of all colocated components is possible in practice and can be used for optimization purposes, but it should not be required. The externally observable behavior of the entity (or composed behavior) should not differ from the case where internal separation is preserved.

[graphomath]

note This post is spelling out some detail, which I would like to be sure to be clear and visible.

@degregat

Defining a behavior

A behavioral definition for a stateful entity (e.g. an agent, engine or process)

Let’s recall a previous related statement, which I find quite helpful^[1]

@degregat

[…] we can distinguish between:

1. Behaviors that can be checked for adherence from only input and output messages.
2. Behaviors where access to the internal state (or observable proxies thereof) of objects is needed to check adherence.

I assume that we here are mainly concerned with the second category, i.e., the category including access to internal state.^[2] In this second category, a good existing abstraction that we have been using as references are Mealy Machines, which can be succinctly described^[3] as follows:

I am not claiming that every behaviour is just a Mealy machine (and that would probably be “wrong”, but let us not jump ahead), but it is a great example of how we can be independent from syntax and/or implementation. Now, this remark is meant to make clear that Mealy machines are not the definition we are currently working on; with that being said, let us come back to the desiderata of a behavioural definition.

@degregat

A behavioral definition for a stateful entity (e.g. an agent, engine or process) should consist of the following two descriptions, conceptually separated:

• Necessary preconditions a message needs to fulfill for the behavior to be applied. This needs to be defined only in terms of the message.
• What a valid state transition implementing the behavior looks like. This can take the message and entity state as an argument and send new messages.

For the example of Mealy Machines as defined above, the set of input symbols A consists of the messages that satisfy the ‘necessary preconditions a message needs to fulfill for the behavior to be applied’, which I would simply call well-formed messages. Now, that covers how the first bullet looks like if applied to the example of Mealy Machines.

Now, for the valid state transition(s) that implement behaviour, in the case of Mealy Machines, behaviour is deterministic, namely, borrowing Moore’s words^[4],

the present state of a machine depends only on its previous input and previous state, and the present output depends only on the present state [and the input].

So, the set B of a Mealy machine can be chosen to be requests for sending messages.^[5] So much for the “obvious” observations that deserve to be written up.

Now for the interesting point: in the above description of desiderata for a definition, we see the indefinite article used: ‘a valid state transition …’. This looks suspiciously like non-determinism, as written elsewhere: instead of a Mealy Machine, we rather want (a specification of)

@cwgoes

a box (algorithm to be run on a non-deterministic Turing machine) inside an agent, “through which” the agent can send and receive messages, and which can automatically respond to messages “on behalf” of the agent (including complex responses, not just request-response).

So, the (pseudo-)non-determinism that we want—beware, that’s a claim—is actually due to some agent or other “decision device” that is affecting the choice of the actual state transitions (as sketched here): in short, we simply ask the local agent or poll an input device to make a choice (and require a default choice in the case of timeouts).^[6]

TL;DR

All this to say, we may want to be as deterministic as possible, which is achievable if in situations where we have several possible state transitions based on current input and state, an “explicit choice” is made by a user or hardware, e.g., TRNGs.

---

1. … to avoid ambiguities, given the name clash with the description of behaviour of a state in a Kripke model: “Bisimulation is intended to characterize states in Kripke models with ‘the same behaviour’”. ↩︎

2. If we were to speak about co-algebras, this means, behaviours with access to internal state are the co-algebras themselves, and we are just trying to find a natural language description. ↩︎

3. … in slightly generalized form … ↩︎

4. Note that this quote is about Moore machines … I just don’t have a quote for Mealy machines with such succinct wording. ↩︎

5. See also [Communicating finite-state machine - Wikipedia]. ↩︎

6. The point is, we do not want to get into the land of different flavours of non-determinism; we prefer to have determinism as much as possible. ↩︎

[graphomath]

@degregat

Agent interaction with a node can be modelled in the form of messages.

However, in the case of a local interaction, synchronous poll for inputs seem a good option, in particular if we want to have read access to a slow disk or similar device. That’s in any case what is cooking in the corner of the research lab.

[degregat]

This is not a contradiction: For this message, the router could pick a local call instead of a network transport.