Linear Temporal Logic of Constraint Automata

Constraint automata are formalisms to describe the behavior and possible data flow in coordination models. In this paper we introduce a linear time temporal logic, called temporal logic of steps (TLS), for specifying the executions of constraint automata. TLS is the first attempt in presenting a linear temporal logic for constraint automata. Having TLS in hand, we are able to design model checking algorithms for verification of concurrent systems modeled by constraint automata.