Determine if/where collaterals are needed

For this ticket we need to:

• Write a CTL formula for whether collateral is required at the end of a transaction: collateral is required if the current active participant has a move in one of the possible futures where everyone cooperates.
• Build a sub-graph of all future moves when everyone is cooperating
• Translate the CTL formula into a graph algorithm on the above.