Split off LTL model checking stuff, cleaned up module structure a bit.