# Walter Hussak

## Publications

##### 6 Specifying a Timestamp-based Protocol For Multi-step Transactions Using LTL

**Authors:**
Rafat Alshorman,
Walter Hussak

**Abstract:**

**Keywords:**
Multi-step transactions,
LTL specifications,
Model
Checking

##### 5 Algebraic Specification of Serializability for Partitioned Transactions

**Authors:**
Walter Hussak,
John Keane

**Abstract:**

**Keywords:**
serializability,
Algebraic Specification,
Partitioned Transactions

##### 4 A Hamiltonian Decomposition of 5-star

**Authors:**
Walter Hussak,
Heiko SchrÃ¶der

**Abstract:**

Star graphs are Cayley graphs of symmetric groups of permutations, with transpositions as the generating sets. A star graph is a preferred interconnection network topology to a hypercube for its ability to connect a greater number of nodes with lower degree. However, an attractive property of the hypercube is that it has a Hamiltonian decomposition, i.e. its edges can be partitioned into disjoint Hamiltonian cycles, and therefore a simple routing can be found in the case of an edge failure. The existence of Hamiltonian cycles in Cayley graphs has been known for some time. So far, there are no published results on the much stronger condition of the existence of Hamiltonian decompositions. In this paper, we give a construction of a Hamiltonian decomposition of the star graph 5-star of degree 4, by defining an automorphism for 5-star and a Hamiltonian cycle which is edge-disjoint with its image under the automorphism.

**Keywords:**
Interconnection Networks,
paths and cycles,
graphs andgroups

##### 3 A Serializability Condition for Multi-step Transactions Accessing Ordered Data

**Authors:**
Rafat Alshorman,
Walter Hussak

**Abstract:**

**Keywords:**
directed graph,
Multi-step transactions,
serializability

##### 2 A CTL Specification of Serializability for Transactions Accessing Uniform Data

**Authors:**
Rafat Alshorman,
Walter Hussak

**Abstract:**

**Keywords:**
computational tree logic,
serializability,
multi-step
transactions

##### 1 Specifying Strict Serializability of Iterated Transactions in Propositional Temporal Logic

**Authors:**
Walter Hussak

**Abstract:**

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.

**Keywords:**
serializability,
Temporal logic,
iterated transactions