%0 Journal Article %A Rafat Alshorman and Walter Hussak %D 2010 %J International Journal of Computer and Information Engineering %B World Academy of Science, Engineering and Technology %I Open Science Index 47, 2010 %T Specifying a Timestamp-based Protocol For Multi-step Transactions Using LTL %U https://publications.waset.org/pdf/3317 %V 47 %X Most of the concurrent transactional protocols consider serializability as a correctness criterion of the transactions execution. Usually, the proof of the serializability relies on mathematical proofs for a fixed finite number of transactions. In this paper, we introduce a protocol to deal with an infinite number of transactions which are iterated infinitely often. We specify serializability of the transactions and the protocol using a specification language based on temporal logics. It is worthwhile using temporal logics such as LTL (Lineartime Temporal Logic) to specify transactions, to gain full automatic verification by using model checkers. %P 1716 - 1723