@article{(Open Science Index):https://publications.waset.org/pdf/3317, title = {Specifying a Timestamp-based Protocol For Multi-step Transactions Using LTL}, author = {Rafat Alshorman and Walter Hussak}, country = {}, institution = {}, abstract = {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.}, journal = {International Journal of Computer and Information Engineering}, volume = {4}, number = {11}, year = {2010}, pages = {1716 - 1723}, ee = {https://publications.waset.org/pdf/3317}, url = {https://publications.waset.org/vol/47}, bibsource = {https://publications.waset.org/}, issn = {eISSN: 1307-6892}, publisher = {World Academy of Science, Engineering and Technology}, index = {Open Science Index 47, 2010}, }