Translate LTLf and scLTL to DFA

[Zinoex]

Construct product IMC of the LTLf automaton and the input IMC to certify LTLf using reachability.

[Zinoex]

Create LabelledIMC and LabelledIMDP types

[Zinoex]

With #87 we can now perform value iteration for finite time/until convergence over a product process (IntervalMarkovProcess + DFA), so if we translate LTLf and scLTL properties to a DFA, we can verify these temporal properties.