%0 Journal Article %A Rafat Alshorman and Walter Hussak %D 2009 %J International Journal of Computer and Information Engineering %B World Academy of Science, Engineering and Technology %I Open Science Index 27, 2009 %T A CTL Specification of Serializability for Transactions Accessing Uniform Data %U https://publications.waset.org/pdf/5156 %V 27 %X Existing work in temporal logic on representing the execution of infinitely many transactions, uses linear-time temporal logic (LTL) and only models two-step transactions. In this paper, we use the comparatively efficient branching-time computational tree logic CTL and extend the transaction model to a class of multistep transactions, by introducing distinguished propositional variables to represent the read and write steps of n multi-step transactions accessing m data items infinitely many times. We prove that the well known correspondence between acyclicity of conflict graphs and serializability for finite schedules, extends to infinite schedules. Furthermore, in the case of transactions accessing the same set of data items in (possibly) different orders, serializability corresponds to the absence of cycles of length two. This result is used to give an efficient encoding of the serializability condition into CTL. %P 780 - 786