This paper presents a framework for simulating, verifying, and automatically composing Web services using semantic markup and automated reasoning. The authors leverage the DAML-S ontology for Web services to define a formal semantics for a subset of DAML-S in terms of first-order logic. They then encode service descriptions in Petri Nets and develop decision procedures for simulation, verification, and composition. The framework also analyzes the complexity of these tasks under different restrictions on DAML-S composite services. An implementation is provided that takes a DAML-S description of a Web service, automatically generates a Petri Net, and performs the desired analysis. This tool has broad applicability as a backend for existing manual composition tools and as a standalone tool for Web service developers. The paper discusses the semantics of DAML-S, mapping it to the situation calculus, and provides an operational semantics using Petri Nets. It also describes the complexity of Web service tasks, showing that the reachability problem for DAML-S 0.5 service descriptions is PSPACE-complete, and that without iterate constructs, it is NP-complete. The paper concludes with an implementation of the framework for automated reasoning tasks.This paper presents a framework for simulating, verifying, and automatically composing Web services using semantic markup and automated reasoning. The authors leverage the DAML-S ontology for Web services to define a formal semantics for a subset of DAML-S in terms of first-order logic. They then encode service descriptions in Petri Nets and develop decision procedures for simulation, verification, and composition. The framework also analyzes the complexity of these tasks under different restrictions on DAML-S composite services. An implementation is provided that takes a DAML-S description of a Web service, automatically generates a Petri Net, and performs the desired analysis. This tool has broad applicability as a backend for existing manual composition tools and as a standalone tool for Web service developers. The paper discusses the semantics of DAML-S, mapping it to the situation calculus, and provides an operational semantics using Petri Nets. It also describes the complexity of Web service tasks, showing that the reachability problem for DAML-S 0.5 service descriptions is PSPACE-complete, and that without iterate constructs, it is NP-complete. The paper concludes with an implementation of the framework for automated reasoning tasks.