This paper explores the automation of various tasks related to Web services, including simulation, verification, composition, and testing. The authors leverage the DAML-S ontology, a formalism for describing Web services, to enable markup and automated reasoning technology. They define a semantics for a subset of DAML-S using first-order logic and encode service descriptions in a Petri Net formalism. The paper provides decision procedures for Web service simulation, verification, and composition, analyzes the complexity of these tasks under different restrictions, and presents an implementation of the analysis techniques. The tool can be used as a backend for existing manual composition tools or as a standalone tool for Web service developers. The work aims to facilitate the automation of Web services tasks, enhancing their reliability and efficiency.This paper explores the automation of various tasks related to Web services, including simulation, verification, composition, and testing. The authors leverage the DAML-S ontology, a formalism for describing Web services, to enable markup and automated reasoning technology. They define a semantics for a subset of DAML-S using first-order logic and encode service descriptions in a Petri Net formalism. The paper provides decision procedures for Web service simulation, verification, and composition, analyzes the complexity of these tasks under different restrictions, and presents an implementation of the analysis techniques. The tool can be used as a backend for existing manual composition tools or as a standalone tool for Web service developers. The work aims to facilitate the automation of Web services tasks, enhancing their reliability and efficiency.