Checking workflow schemas with time constraints using timed automata (extended abstract)

Nowadays, the ability of providing an automated support to the management of business processes is widely recognized as a main competitive factor for companies. One of the most critical resources to deal with is time, but, unfortunately, the time management support offered by available workflow management systems is rather rudimentary. We focus our attention on the modeling and verification of workflows extended with time constraints. We propose (finite) timed automata as an effective tool to specify timed workflow schemas and to check their consistency. More precisely, we reduce the consistency problem for workflow schemas to the emptiness problem for timed automata, making it possible to exploit the machinery developed to solve the latter to address the former.