This paper presents a method for engineering and programming multirobot systems, based on a combination of statecharts and hybrid automata, which are well-known in the fields of software engineering and artificial intelligence. This formal specification method allows graphical presentation of the whole multiagent system behavior. In addition, these specifications can be directly executed on mobile robots. We describe the transformation process from the specification to executable code, after introducing the necessary definitions. A translator that automatically converts hybrid hierarchical statecharts into simple flat hybrid automata (i.e. without hierarchies) has been implemented. The respective tool allows the text-based input of hybrid hierarchical automata specifications of multiagent system with synchronization. The translation into flat automata is performed by means of different plug-ins, leading e.g. to executable code for Sony Aibo robot dogs. The plug-in just mentioned has been successfully applied in the RoboCup four-legged league.
Robotic soccer provides many research challenges and one of them is behavior control
including the subjects of team play, cooperation and flexible, quick reaction. A soccer
team can be designed as a homogeneous multiagent system. Since the behavior of
multiagent systems and agents alone can be understood as driven by external events and
internal states, an efficient way to model such systems are state transition diagrams,
which are well-established in software engineering. They are graphical representations
of finite state machines with hierarchically structured states and transitions which lead
from one state to another depending on the input or events. Outputs or actions can be
done during transitions or in states. State transition diagrams have been applied
successfully for multiagent systems in general and in the RoboCup, a simulation of (human)
soccer with real or simulated robots (see e.g. [
However, state transition diagrams do not properly cover all aspects of multiagent
systems. Therefore, hybrid hierarchical automata (HHA) with timed synchronization
have been developed to take continuous processes in the environment into account [
Therefore, as a running
example, we consider a
scenario influenced by the UEFA
champions league competition
2006/2007: the Makaay move
(see Fig. 1). Let there be one
player of type A and two
players of type B in the offensive
team. Player A performs the
kick-off, while the players of
type B are waiting in different
sectors on the pitch, which is
divided into sectors (cf. [
Player A chooses a direction for passing (right or left midfield, sectors 3 or 5), then kicks off and passes to one player of type B in the destination sector. Player A runs to sector 1 (middle offense) where B has passed the ball to. Finally, player A tries to shoot to the goal directly. If it fails, A tries it again. Meanwhile, B goes to the ball if it is nearer to it. B then passes to A in sector 1 again. Fig. 1. Statechart for Makaay move.
In the sequel, Sect. 2 covers the formal specification of hybrid statecharts. Corresponding description and target languages are defined and compared in Sect. 3. With these foundations, we can create a concept for the translation process. Sect. 4 then deals with the design of the application and shows an example of use. Finally, we discuss related works in Sect. 5 and conclude with Sect. 6. 2
2.1
In a realistic physical environment, it is inevitable to consider continuous actions in
addition to discrete changes. Hybrid automata extend regular state transition diagrams
with methods that deal with those continuous actions. To understand the
characteristics, we will introduce several definitions for hierarchical hybrid automata with timed
synchronization now [
following disjoint sets: S: a finite set of states, partitioned into three disjoint sets: Ssimple, Scomp, and Sconc — called simple, composite and concurrent states, containing one designated start state s0 ∈ Scomp ∪ Sconc; X: a finite set of variables, partitioned into two disjoint sets: Xreal and Xint — the continuous/real-numbered and the integral/integer variables, respectively; for each x ∈ X we introduce the variables x′ for the conclusions of a discrete change; T: a finite set of transitions with T ⊆ S × S.
Definition 2 (state hierarchy). Each state s is associated with zero, one or more initial states α(s): a simple state has zero, a composite state exactly one, and a concurrent state more than one initial state. In the latter case, the initial states are called regions. Moreover, each state s ∈ S \ {s0} is associated to exactly one superior state β(s). Therefore, it must hold β(s) ∈ Sconc ∪ Scomp. A concurrent state must not directly contain other concurrent ones. Furthermore, it is assumed that all transitions s1T s2 ∈ T keep to the hierarchy, i. e. β(s1) = β(s2). Furthermore, we write αn(s) or βn(s) for the n-fold application of α or β to s, in particular, α0(s) = β0(s) = s. Variables x ∈ X may be declared locally in a certain state γ(x) ∈ S. A variable x ∈ X is valid in all states s ∈ S with βn(s) = γ(x) for some n ≥ 0, unless another variable with the same name overwrites it locally.
As said earlier, Fig. 1 depicts the statechart for our running soccer example. Here, states are named after their affiliation to the players or the actions which are being done at that moment. The states soccer makaay (which is the start state s0 here), kickoff, go-to-ball, player-A and player-B are composite states; teamplay is a concurrent state while all others are simple states. The oval symbol ball is a synchronization point and will be discussed in Sect. 2.2.
condition. This is a predicate with free variables from the valid variables of X ∪ X ′. Additionally, each state s ∈ S contains a state condition which describes continuous changes in s. It is a predicate with free variables from X ∪ {t}.
Events are well-known in UML statecharts [
states with the root node as the topmost initial state of the overall state machine. Whenever a state s is an immediate predecessor of s′ in c, it must hold β(s′) = s. A configuration must be completed by applying the following procedure recursively as long as possible to leaf nodes: if there is a leaf node in c labeled with a state s, then introduce all α(s) as immediate successors of s.
The semantics of our automata can now be defined by alternating sequences of
discrete and continuous steps. Following the synchrony hypothesis, we assume that
discrete state changes (via transitions whose annotated jump condition holds in the
current situation) happen in zero time, while continuous steps (within one state) may
last some time. Due to the lack of space, for details on the semantics of HHA, the reader
is referred to [
Fig. 2(b) demonstrates the relationship between state trees and configurations. It depicts several configurations that are created from the state tree in Fig. 2(a). A configuration itself can be connected to another one. The original transition t, which was used for the completion of s2 in c2, is used in a discrete step while its origin is changed from s1 to c1 and its target from s2 to c2.
(a) State tree with synchronization point x.
(b) Configurations with synchronization problem.
Synchronization is significant for modeling multiagent systems. Usually, a system deals
with limited resources. The interaction with them can take part in several states.
Especially when reacting to events from the environment, the reaction process takes some
time τ > 0. For this, a synchronization takes care of the common resources defined at
a synchronization point. While synchronization is associated with transitions,
implemented via labels in original hybrid automata [
Synchronization may take some time, since they are connected to (continuous) states and not to discrete transitions. Thus, the synchronization process can theoretically be interfered by other actions or concurrent states which also try to share the same synchronization point. To avoid side effects that may lead to inconsistency or even system failure, the process is separated into allocation and (future) occupation of resources. For this, the allocation variables x+ and x− register the request for occupation or release for each synchronization point x. Therefore, x+ and x− must be added to X .
In this case (synchronization point x and connected state s), s1T s2 is called incoming
transition for s iff αn(s2) = s for some n ≥ 0, initializing transition iff it is an incoming
one with αn(s) = γ(x), outgoing transition iff s1 = βn(s) for some n ≥ 0 where s1 occurs
in the current configuration and x is valid in s, successful outgoing transition iff it is an
outgoing transition with s1 = s and failed outgoing transition iff it is not a successful
outgoing transition. Note that outgoing transitions cannot be characterized statically but
only dynamically by investigating the configuration trees. This is an important issue for
the revoking of the allocation (see Sect. 4.2). At a synchronization point x, additional
constraints must be defined which affect the transitions that are incident with all states
s connected to x. Due to the lack of space, for details on the synchronization concept,
the reader is referred to [
The synchronization point ball in Fig. 1 has a capacity of 1. Thus, it can be interpreted as a Boolean value as there is only one ball in a soccer match. Both states go-to-ball occupy the synchronization point ball. Hence, they belong to the relation R+. The states kick-to-goal and pass-to-sector release it and therefore belong to R−.
The example in Fig. 2(a) also makes use of a synchronization point. As seen in the tree, the state R introduces the synchronization point x while 4 is somehow using it here. The definition is marked with the dashed arrow pointing at x. However, for some multiagent systems, the synchronization must be converted into ordinary variables if a target platform does not provide synchronization interfaces. 3
After having defined basic concepts, let us now consider concrete languages for programming multiagent systems with HHA. Therefore, we will discuss two languages briefly in the sequel: HAL and XABSL.
The project goals of HAL [
Another successful approach of modeling agent behavior is XABSL (Extensible
Agent Behavior Specification Language) [
The HAL converter provides a window-based flattening mechanism for state machine specifications, a batch mode for quick processing, and re-usability. Additionally, there should be a graphical editor to easily create source code from hybrid statecharts. Already created files (or files that are created manually) are allowed to be used as an input for the application. Hence, a lexer and a parser provide the conformity with the HAL syntax. With this design, it is possible to create a hybrid automaton which can be used later as input for the flattening algorithm (see below). The translator from HAL to XABSL shall cover all features of synchronized hybrid state machines that can be transferred to XABSL. 4.1
For the translation process, there is no simple one-to-one structural mapping between
HHA and XABSL. As XABSL and also standard verification tools often are not able
to cope with hierarchies, it is required to flatten the automaton, i.e., all states except
the initial one are transformed into simple ones. As the translator shall be feasible of
creating processable output for those tools, this gives us another reason to flatten the
hierarchical structure. Though this transformation may lead to state explosion, it could
be avoided, nevertheless, if hierarchical configurations could be processed as directly
as in some logic-based implementations [
In the implementation, configurations are used to clarify which agent currently is in which state. The flattening algorithm processes an input state tree and converts it to a set of configurations. In particular, the output can be used to simplify the agent’s behavior structure and to gain performance due to less complexity. For this, the algorithm is divided into four major parts.
Expand the regions in the tree according to their cardinality c (given in the upper right corner of a region). Modify each region to a composite state, copy it c-times and replace the original with the copies.
Each state may introduce variables and constants. Each local definition must be globalized as it will be used in the configuration flows and transitions later on. The global definitions must be uniquely named to avoid namespace collisions.
If a state uses a synchronization point to interact with other states, these synchronizations must be resolved. Due to their complexity, a relatively extensive inspection is required which is explained in detail in Sect. 2.2 and 4.2. Although the resulting additions to transition guards reduce readability, the even more complex process of inter-state synchronization could be eliminated. A practical approach for the detection of the correct place to revoke an allocation is given below.
Each state tree possesses an initial configuration c0. This contains all the initial states that can be reached in the tree beginning at the root. According to the completion algorithm (Def. 4), the configurations are created recursively beginning at c0. Already existing configurations will be recognized and used if transitions lead to them. These newly created transitions form the discrete steps of the system.
The synchronization conversion in the third step is a rather complex process. At first, all synchronization points in the automaton are collected. After this, the automaton will be traversed, and the occupation, the release, as well as the allocation, and its revoke are added for each synchronization found in the state tree. The synchronization point x itself, its maximum capacity C(x), and its allocation variables x+ and x− are converted into global variables. For each transition type, different expressions must be added to the guards and the discrete expressions. However, a flag x f for each synchronization point x is introduced indicating its current status. If x is occupied then x f := −1. If x is allocated but not occupied yet then x f := 1. Otherwise, x f := 0. For all not initializing incoming transitions, x f := 1 will be added to their discrete expressions, x f := 0 will be added for all initializing incoming transitions, x f := −1 will be added for all successful outgoing transitions. For each not successful outgoing transition, it must be checked if x is already allocated but not occupied by this synchronization. Therefore, the transition must be duplicated. The comparison x f = 1 is added to the guard of the first transition, x f 6= 1 is added to the second one. The revocation of the allocation is added only to the discrete expression of the first one. Finally, all synchronization points can be erased as they are now properly converted into ordinary variables. 4.2
During the development of the theoretical model of hybrid automata with timed synchronization, a problem concerning not successfully outgoing transitions occurs. The correct situation has to be found, when the allocation shall be revoked, since it must actually be done only once per occupation. For this purpose, some definitions have to be introduced.
Let δ(s) return all variables used in the state s but not defined there. Furthermore, we introduce a mapping ζ which returns all state successors of s that use x and are part of the configuration c:
ζ(s, x, c) = {si | βn(si) = s ∧ x ∈ δ(si) ∧ si ∈ S(c), n > 0} shows – among others – a transition from state 2 to 7. Fig. 2(b) shows the appropriate configurations with c0 being the initial one. In this case, the synchronization point x is defined in the state R while only 4 is using x. In fact, R must be a concurrent state as it defines a synchronization point. Though concurrent states usually have two or more regions, this example reduces complexity and actually uses only one.
Let us now have a closer look on what is happening in c1 when the process has activated state 5. State 4 is also active as it is the immediate predecessor of state 5 in the tree. The transition from 2 to 7 is a not successful outgoing transition for 4 as 2 = βn(4) with n = 1 > 0.
Now, to collect all states that may have allocated x before the transition t induces a discrete step to c2, the mapping ζ can be applied. Here, ζ is used with the parameter 2 as this state is the origin of the transition. In the configuration c1 this is a set containing one single state: ζ(2, x, c1) = {4}. That statement confirms that (only) 4 has allocated the synchronization point x in this situation. There has no occupation been done yet. So for the transition t, the allocation has to be revoked and further actions can be done during the process. On the contrary, the configuration c3 does not have an active allocation or occupation since ζ(2, x, c3) = 0/. Therefore, the synchronization point remains unchanged for the transition t.
The XabslFish plug-in defines constraints which check the input automaton for the proper structure. For this, the flattener algorithm must have processed the automaton. The regions must be copied according to their capacities, the variables must be globalized to provide an efficient handling of the XABSL symbol file and the synchronizations must be converted into ordinary variables. The variables must not be renamed during their globalization as they will later be translated by use of the configuration file.
The conversion of the flattened automaton starts with reading the appropriate configuration file. This is used to transform HAL variables to expressions, to basic behavior 4.3
From a shell the user can start the Java application in console or window mode with several mandatory and optional parameters. As shown in Fig. 4, all configurations can be set intuitively in the window mode. The required input file can either be typed into the textfield on the top of the main content pane or it can be chosen by using a file dialog window. The temporary and the target output file are named accordingly. However, they can be defined individually, too. 4.4
Fig. 4. HAL screen-shot before starting the translation. calls or for their declaration in the output symbol file. In the second step of the translation, the symbol file is generated. A Boolean flag indicates if any symbol has to be written at all. In case that there is no symbol to write, the file will not be created. In consequence of that it can be decided if the future options will include this file or not. The third step is the major part of the translation. Here, the automaton tree is traversed and each node will be converted into an option. The subsequent automata become accessible via internal states while initial subsequent states keep their status. Each transition from a successor to another automaton is implemented into the state decision tree where discrete expressions are converted into actions in the target state. If all successor nodes are completed the own flow expressions of the current automaton will be converted into actions. This algorithm is processed recursively for each automaton. 4.5
Let us now come back to our running example (Fig. 1). For purpose of clarity, the
transition labels with the jump conditions and the discrete expressions are omitted as
well as the flow expressions and invariants in the states. However, within this example
there are several main features of synchronized hybrid automata covered. The soccer
team has at least three players: one of type A, two of type B. Furthermore, there is
exactly one ball on the field which can be interpreted as a resource with the maximum
capacity 1. Due to the lack of space, for further details on the implementation, the reader
is referred to [
There are many related works on the specification of multiagent systems and also on
software engineering of multiagent systems (see e.g. [
As proposed by [
In [
The paper [
XabslFish allows the behavior control of Aibo robots (or any other XABSL-driven robots) to be designed as a multiagent system with formal methods. Therefore, the performance of the robot is enhanced. The safety of a correct behavior control is based upon the fact that the translation from HAL to XABSL can precisely be adjusted manually for each input automaton. The application XabslFish supports the modeling of hybrid automata with timed synchronization and translates the specification to an understandable format for the target platform. The soccer domain is used as an example for multiagent systems, which have to act autonomously in a dynamic environment.
XabslFish translates multiagent system specifications from the hybrid automaton language HAL to XABSL. It is designed as a plug-in for the application, the HAL converter, that deals with hybrid automata. Even though it can translate the major part of a state machine automatically, some individual mappings must be defined in a configuration file. In summary, this paper exemplifies that multiagent systems can be specified by formal methods based on standard modeling procedures (namely state machines). It is also demonstrated, how by transformation techniques executable code can be generated, running on a mobile robot (namely the Aibo robot).
Future work will concentrate on an implementation of the formalism with constraint
logic programming (CLP), which can be used for both, engineering and analysis of
multiagent systems, following the lines of [