Liveness and Safety ensured by checking for these qualities as well.

Model checking can be augmented by any number of constraints and
is especially suitable for producing workflows.

Now consider classical AI Planning.