
## Appendix A. Glossary Of Notation

| Models satisfies                                           |                                                                 |                           |               |
|------------------------------------------------------------|-----------------------------------------------------------------|---------------------------|---------------|
| mod el  ch ecking                                          | A verification method entailing brute force search              |                           |               |
| AT                                                         | Automata theoretic model checking                               |                           |               |
| Single agent situation                                     |                                                                 |                           |               |
| la gent                                                    | Multiagent situation where each agent uses a multiagent plan    |                           |               |
| lplan                                                      | Multiagent situation where each agent uses an individual plan   |                           |               |
| multplans                                                  | Finite state automaton                                          |                           |               |
| The set of states  vertices  of FSA                        |                                                                 |                           |               |
| The set of state to state transitions  edges  of FSA       |                                                                 |                           |               |
| tran sition condition                                      | Logical description of the set of actions enabling a transition |                           |               |
| A Boolean algebra                                          |                                                                 |                           |               |
| Boolean algebra partial order                              | iff                                                             |                           |               |
| The matrix of transition conditions of FSA                 |                                                                 |                           |               |
| k                                                          | Transition condition associated with edge                       |                           |               |
| K i j                                                      | i j                                                             |                           |               |
| The set of initial states of FSA                           |                                                                 |                           |               |
| Primitive elements of a Boolean algebra  atoms are actions |                                                                 |                           |               |
| string                                                     | Sequence of actions  atoms                                      |                           |               |
| The language of  set of strings accepted by  FSA           |                                                                 |                           |               |
| automaton                                                  | An FSA that accepts infinite length strings                     |                           |               |
| run                                                        | The sequence of FSA vertices visited by a string                |                           |               |
| The run of a string in the FSA language                    |                                                                 |                           |               |
| accepting run                                              |                                                                 |                           |               |
| acceptance criterion                                       | A requirement of accepting runs of an FSA                       |                           |               |
| The tensor  synchronous  product of FSAs                   |                                                                 |                           |               |
| complete FSA                                               | Specifies a transition for every possible action                |                           |               |
| deterministic FSA                                          | The choice of action uniquely determines the next state         |                           |               |
| Sequence of vertices connected by edges                    |                                                                 |                           |               |
| path                                                       |                                                                 |                           |               |
| cycle                                                      | A path with start and end vertices identical                    |                           |               |
| Computational state  an action occurring in a computation  |                                                                 |                           |               |
| accessible from                                            | There exists a path from                                        |                           |               |
| □                                                          | Temporal logic  invariant"                                      |                           |               |
| Temporal logic  eventually"                                |                                                                 |                           |               |
| .                                                          |                                                                 |                           |               |
| Invariance property                                        | 口                                                              | i e                       | Invariant not |
| Every is eventually followed by                            |                                                                 |                           |               |
| Response property                                          | 口                                                              | �                         | i e           |
| First-Response property                                    | The first                                                       | trigger  is followed by a | response      |
| The set of  bad"  to be avoided  states of FSA             |                                                                 |                           |               |
| Can increase accessibility                                 |                                                                 |                           |               |
| Cannot increase accessibility                              |                                                                 |                           |               |
| ↑                                                          | Can decrease accessibility                                      |                           |               |
| Cannot decrease accessibility                              |                                                                 |                           |               |
| Safe machine learning operator i e preserves properties    |                                                                 |                           |               |
| One that is correct when it states that                    |                                                                 |                           |               |
| sound algorithm                                            |                                                                 |                           |               |
| complete algorithm                                         | One that is correct when it states that                         |                           |               |
| The FSA transition function                                |                                                                 |                           |               |
| 149                                                        |                                                                 |                           |               |
