<p>One standard way to model this is to have one automaton per object.  The state space of that automaton is the value of all of the fields of that object.  Calling a method on object <span class="math-container">$O$</span> corresponds to message-passing: sending a message to that object <span class="math-container">$O$</span> with the name of the method and any arguments.  A system containing multiple objects is obtained by parallel composition of the automata (one automaton per object).</p>

CC BY-SA 4.0
2023-10-28T00:58:55.810Z
Is there a textbook that explores all of these things (automata, message-passing, parallel composition)?
The Pointer
CC BY-SA 4.0
2023-10-28T03:20:02.003Z
@ThePointer, any basic textbook on formal languages should explain automata.  Parallel composition is standard in the model checking literature.  See, e.g., https://en.wikipedia.org/wiki/Transition_system, https://en.wikipedia.org/wiki/Process_calculus, https://en.wikipedia.org/wiki/Actor_model_and_process_calculi, https://en.wikipedia.org/wiki/Actor_model
D.W.
CC BY-SA 4.0
2023-10-27T20:53:17.270Z
2023-10-27T20:53:17.270Z
D.W.
<p>Automata generally communicate using message passing. The base case here are finite automata using a finite alphabet of messages.</p>
<p>In your case, the state space is either infinite or very large depending on whether you are using unbounded integers, and it makes sense to use parametrised messages. For example, you could have a message <span class="math-container">$current(n)$</span> which field2 uses to communicate its current value. The automata would then have transitions like</p>
<p><span class="math-container">$k \xrightarrow[]{current(n)} 3k+2n$</span> for all <span class="math-container">$k,n$</span> in field1</p>
<p><span class="math-container">$n \xrightarrow[]{current(n)}  n$</span> for all <span class="math-container">$n$</span> in field2</p>
<p>where we use the values <span class="math-container">$k, n\in \mathbb{Z}$</span> as the states for each automaton. The automata synchronise on these messages so e.g. field2 can only use a <span class="math-container">$current(4)$</span> transition when field1 has the value <span class="math-container">$4$</span> (so that the message is enabled).</p>

CC BY-SA 4.0
2023-10-27T12:07:38.027Z
2023-10-27T12:07:38.027Z
Klaus Draeger
<p>I am trying to represent/model fields and methods in the context of programming as automata. For instance, let's say that I have <code>field1</code> with state equal to 2, <code>field2</code> with state equal to 3, and <code>method1</code> being the calculation <code>field2</code> <span class="math-container">$=$</span> <code>field1</code> <span class="math-container">$\times$</span> 2 <span class="math-container">$+$</span> <code>field2</code> <span class="math-container">$\times$</span> 3. If I represent <code>field1</code> as one automaton and <code>field2</code> as another automaton, <code>field1</code> would first change its state to <span class="math-container">$2 \times 2 = 4$</span> and then <code>field2</code> would change its state to <span class="math-container">$3 \times 3 = 9$</span>. But it isn't clear to me how one would then represent the interaction between these two automatons to make <code>field2</code> state equal to <span class="math-container">$4 + 9 = 13$</span> (since the automaton representing <code>field2</code> would need to retrieve the state value of the automaton representing <code>field1</code>), and nor is it clear to me how one would have the &quot;transience&quot;/&quot;temporary&quot; aspect, since <code>field1</code> would then have to revert back to state equal to <span class="math-container">$2$</span> (since the computation with regards to this field/automaton is temporary and not permanent).</p>
<p>I suspect that this stuff has already been figured out, but I'm a fresh grad student, so I'm not really aware of this stuff.</p>

<automata-theory>
Representing/Modelling fields and methods in the context of programming as automata
The Pointer
# Representing/Modelling fields and methods in the context of programming as automata

(Asked by: username_0 on 2023-10-27)

I am trying to represent/model fields and methods in the context of programming as automata. For instance, let's say that I have `field1` with state equal to 2, `field2` with state equal to 3, and `method1` being the calculation `field2` $=$ `field1` $\times$ 2 $+$ `field2` $\times$ 3. If I represent `field1` as one automaton and `field2` as another automaton, `field1` would first change its state to $2 \times 2 = 4$ and then `field2` would change its state to $3 \times 3 = 9$. But it isn't clear to me how one would then represent the interaction between these two automatons to make `field2` state equal to $4 + 9 = 13$ (since the automaton representing `field2` would need to retrieve the state value of the automaton representing `field1`), and nor is it clear to me how one would have the "transience"/"temporary" aspect, since `field1` would then have to revert back to state equal to $2$ (since the computation with regards to this field/automaton is temporary and not permanent).

I suspect that this stuff has already been figured out, but I'm a fresh grad student, so I'm not really aware of this stuff.

**Tags:** automata-theory

---

## 2 answers

### Answer by username_1 on 2023-10-27. Score: -1 | Accepted answer

One standard way to model this is to have one automaton per object. The state space of that automaton is the value of all of the fields of that object. Calling a method on object $O$ corresponds to message-passing: sending a message to that object $O$ with the name of the method and any arguments. A system containing multiple objects is obtained by parallel composition of the automata (one automaton per object).

> **Comments:**
> **username_0**: Is there a textbook that explores all of these things (automata, message-passing, parallel composition)?  
> **username_1**: @ThePointer, any basic textbook on formal languages should explain automata.  Parallel composition is standard in the model checking literature.  See, e.g., https://en.wikipedia.org/wiki/Transition_system, https://en.wikipedia.org/wiki/Process_calculus, https://en.wikipedia.org/wiki/Actor_model_and_process_calculi, https://en.wikipedia.org/wiki/Actor_model  

---

### Answer by username_2 on 2023-10-27. Score: 1

Automata generally communicate using message passing. The base case here are finite automata using a finite alphabet of messages.

In your case, the state space is either infinite or very large depending on whether you are using unbounded integers, and it makes sense to use parametrised messages. For example, you could have a message $current(n)$ which field2 uses to communicate its current value. The automata would then have transitions like

$k \xrightarrow[]{current(n)} 3k+2n$ for all $k,n$ in field1

$n \xrightarrow[]{current(n)} n$ for all $n$ in field2

where we use the values $k, n\in \mathbb{Z}$ as the states for each automaton. The automata synchronise on these messages so e.g. field2 can only use a $current(4)$ transition when field1 has the value $4$ (so that the message is enabled).


---

