Web service discovery is a key problem as the number of services is expected to increase dramatically. Service discovery at the present time is based primarily on keywords, or interfaces of web services through the use of ontology. We argue that "behavior signatures" as operational level description should play an important role in the service discovery process. In this paper, we propose a new behavior model for web services using automata and logic formalisms. Roughly, the model associates messages with activities and adopts the IOPR model in OWL-S to describe activities. A new query language is developed to express temporal and semantic properties on service behaviors. Query evaluation algorithms are developed; in particular, an optimization approach using RE-tree and heuristics is shown to improve the performance. Speci?cally, experimental results show that the use of RE-tree reduces query evaluation time by an order of magnitude and with heuristics it enhances the performance by two orders of magnitude. This is clearly an encouraging starting point.