%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