A finite domain semantics for executing temporal logic specifications