Understanding federations

[mkep-dev]

I would like to understand how federations work.

As far as I understand they are a union of multiple zones (DBMs) to represent non-convex zones.

Is there a paper or a documentation to understand this data structure and its operations better?

I need to represent a zone where upper right corner (future) is excluded (in case of 2 clocks).

I already have a working implementation of DBMs, but I need to represent non-convex zones.
It would be great of there is something like pseudo code for the logic of the main zone operations on federations:

• up (let time pass)
• down
• reset clocks
• free clocks
• subset or equal
• canonical form of the federation (?)
• intersection
• is federation empty
• reduce the federation
• k-normalization
• subtract (this should be simply the intersection of the negated DBMs with the federation)

As far as I understand up, down, reset, free and intersection are just directly applied on every sub DBM. The rest of the code is not that as easy to understand.

Is it necessary to manually reduce the federation after every operation.

I know that's a strange and not lightweighted request, but it's important for my thesis.

Thank you in advance.

[mikucionisaau]

There are quite a few pointers to literature on the wiki tab.

I think the easiest would be to explore it through ruby bindings (it can display DBM graphically). Unfortunately this part is currently broken and awaits a new repository.