Modal logic axiom S4, transitive and reflexive frame, tableaux solver

Question

I have a difficult problem to solve which as mentioned in the title is related to modal logic axiom S4. So, here is some background knowledge that can be useful:

• S4 axiom is a class of transitive and reflexive frames
• S4 satisfiability problem is PSpace-Complete
• lastly solver for S4 does not terminate without a trick which will allow it to return a finite model.

Knowing all this, I have implemented a solver for propositional modal logic S4 and it also terminates with a finite model. In general solver uses Tableaux approach and generates graph in which the input formula is true. So, to outline what the algorithm does we have the following:

1. algorithm start by creating a graph with a single node with the input formula.
2. then we solve alpha, beta, gamma and delta formulas until each sub-formula is marked as being visited.
3. for termination part of the algorithm, every time a new node is about to be created (which is caused by delta formulas) we check whether the same node already exists in the graph. If yes, then we do not create a new node but we add an edge to the node that has that value.

This is enough to see what the algorithm does. What I am trying to do next is to prove that the algorithm is correct and will always work. For this purpose I will need to structure a formal proof.

So is anyone familiar enough with the topic to suggest what technique can be used to with the proof? What should be used bisimulation or filtration? Furthermore, it would be great if you could sketch out the proof if possible.

Any help would be very very appreciated.