Maximal serializability of iterated transactions (Q1062471)

The serializability condition is usually considered in order to maintain the consistency of a Database in the presence of conflicting accesses to the Database performed by concurrent transactions. This serializability condition is considered herein as a general synchronization problem among transactions (or processes) which can be iterated infinitely often. The behaviour of such a system of transactions is represented by an infinite word over the alphabet of the operations performed by the transactions. Then a characterization of the prefixes of such behaviours satisfying the serializability condition - so-called correct behaviours - is given and it is shown that the set of all correct behaviours can be controlled by a finite automaton. As an example, the classical 'dining philosophers' problem is shown to be entirely modelled and solved as a serializability problem.