Specifying Strict Serializability of Iterated Transactions in Propositional Temporal Logic

We present an operator for a propositional linear temporal logic over infinite schedules of iterated transactions, which, when applied to a formula, asserts that any schedule satisfying the formula is serializable. The resulting logic is suitable for specifying and verifying consistency properties of concurrent transaction management systems, that can be defined in terms of serializability, as well as other general safety and liveness properties. A strict form of serializability is used requiring that, whenever the read and write steps of a transaction occurrence precede the read and write steps of another transaction occurrence in a schedule, the first transaction must precede the second transaction in an equivalent serial schedule. This work improves on previous work in providing a propositional temporal logic with a serializability operator that is of the same PSPACE complete computational complexity as standard propositional linear temporal logic without a serializability operator.

• Walter Hussak

• Temporal logic
• iterated transactions
• serializability.

[1] A. Cimatti, E. Clarke, F. Giunchiglia, and M. Roveri, "NuSMV: a new
symbolic model verifier," Lecture Notes in Computer Science, vol. 1633,
pp. 495-499, 1999.
[2] E. Clarke, O. Grumberg and D. Peled, Model Checking, MIT Press,
1999.
[3] C.J. Date, An Introduction to Database Systems, Addison Wesley, 2004.
[4] M.P. Fle and G. Roucairol, "On serializability of iterated transactions,"
Proc, 1st ACM SIGACT-SIGOPS Symp. on Principles of Distributed
Computing, pp. 194-200, 1982.
[5] M.P. Fle and G. Roucairol, "Multiserialization of iterated transactions,"
Information Processing Letters, vol. 18, pp. 243-247, 1984.
[6] G.J. Holzmann, The SPIN model checker. Addison-Wesley, 2004.
[7] W. Hussak, "Serializable Histories in Quantified Propositional Temporal
Logic," International Journal of Computer Mathematics, vol. 81(10), pp.
1203-1211, 2004.
[8] W. Hussak and J.A. Keane, "Algebraic Specification of Serializability
for Partitioned Transactions," International Journal of Computer Systems
Science and Engineering, vol. 1(1), pp. 60-67, 2007.
[9] S. Katz and D. Peled, "Defining conditional independence using collapses,"
Theoretical Computer Science, vol. 101, pp. 337-359, 1992.
[10] C. Papadimitriou, "The Serializability of Concurrent Database Updates,"
Journal of ACM, vol. 26(4), pp. 631-653, 1979.
[11] D. Peled and A. Pnueli, "Proving partial order properties," Theoretical
Computer Science, vol. 126, pp. 143-182, 1994.
[12] A. Pnueli, "Temporal logic of programs," Proc. 18th IEEE Symp. on
Foundations of Computer Science, pp. 46-57, IEEE Computer Society
Press, 1977.
[13] L. Sha, J.P. Lehoczky and E.D. Jensen, "Modular Concurrency Control
and Failure Recovery," IEEE Transactions on Computers, vol. 37(2), pp.
146-159, 1988.
[14] A.P. Sistla and E.M. Clarke, "The Complexity of Propositional Linear
Temporal Logics," Journal of the ACM, vol. 32, pp. 733-49, 1985.
[15] K. Vidyasankar, "Generalized Theory of Serializability," Acta Informatica,
vol. 24, pp. 105-119, 1987.