Syntax independent descriptions of message and state dependent behaviors

[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. ↩︎