Serializable histories in quantified propositional temporal logic

Abstract

The model of concurrent uninterpreted transactions [Papadimitriou, C. H. (1979). The serializability of concurrent database updates. J. ACM, 26, 631–653.] is extended to histories with infinitely many occurrences of the transactions. Such histories are viewed as models of linear temporal logic formulae with propositions representing read and write steps of transactions. A necessary and sufficient condition for histories to be serializable is encoded into temporal logic by the use of propositional quantification. The encoding differs from work on commutativity-based serializability and partial-order temporal logics in using linear temporal logic and defining serializability in terms of uninterpreted histories without reference to the state of variables. An application is the specification of a weaker form of serializability where commutativity of steps is not determined by past history.

Keywords:

• Temporal logic
• Database concurrency
• Serializability