Reasoning about processes in applications such as manufacturing, web services, enterprise modeling, and planning requires the representation of composite processes with complicated flows of control. Previous research in process representation has used formalisms such as Event Systems, Petri nets, and the Unified Modeling Language activity diagrams. The computational hardness of temporal projection problems in Event Systems has been extensively examined in the literature, whereas Petri nets and UML activity diagrams are applied to describe more elaborate processes. This thesis takes a systematic look into the temporal reasoning problems in Event Systems and assigns accurate semantics to both Petri nets and, for the first time, to UML activity diagrams. We give an analysis of computational complexity in temporal projection problems by exploring the boundary between their tractable and intractable subproblems. Our results provide new insights into the prominent role the properties of partial ordering play, however we also show that partial ordering is not the sole source of the intractability as has been claimed in an earlier work by Nebel and B{\"a}ckstr{\"o}m. Two influential modeling languages, Petri nets and UML activity diagrams, are axiomatized as two Basic Action Theories of Situation Calculus. They are called, respectively, SCOPE (Situation Calculus Ontology of PEtri nets) and SCAD (Situation Calculus theory of Activity Diagrams). We provide a Prolog implementation of SCOPE and prove the correctness of this program for regressable queries. We use SCAD to axiomatize the structural and dynamic properties of UML activity diagrams and also provide the first set of computational results with regard to the reachability problems in activity diagrams. The correctness of each of these two axiomatizations is also demonstrated by proving that the theory is satisfiable, and the intended interpretation corresponds to a model of the theory.

Reasoning about processes in applications such as manufacturing, web services, enterprise modeling, and planning requires the representation of composite processes with complicated flows of control. Previous research in process representation has used formalisms such as Event Systems, Petri nets, and the Unified Modeling Language activity diagrams. The computational hardness of temporal projection problems in Event Systems has been extensively examined in the literature, whereas Petri nets and UML activity diagrams are applied to describe more elaborate processes. This thesis takes a systematic look into the temporal reasoning problems in Event Systems and assigns accurate semantics to both Petri nets and, for the first time, to UML activity diagrams. We give an analysis of computational complexity in temporal projection problems by exploring the boundary between their tractable and intractable subproblems. Our results provide new insights into the prominent role the properties of partial ordering play, however we also show that partial ordering is not the sole source of the intractability as has been claimed in an earlier work by Nebel and B{\"a}ckstr{\"o}m. Two influential modeling languages, Petri nets and UML activity diagrams, are axiomatized as two Basic Action Theories of Situation Calculus. They are called, respectively, SCOPE (Situation Calculus Ontology of PEtri nets) and SCAD (Situation Calculus theory of Activity Diagrams). We provide a Prolog implementation of SCOPE and prove the correctness of this program for regressable queries. We use SCAD to axiomatize the structural and dynamic properties of UML activity diagrams and also provide the first set of computational results with regard to the reachability problems in activity diagrams. The correctness of each of these two axiomatizations is also demonstrated by proving that the theory is satisfiable, and the intended interpretation corresponds to a model of the theory.

The meet up between data, processes and structural knowledge in modeling complex enterprise systems is a challenging task that has led to the study of combining formalisms from knowledge representation, database theory, and process management. Moreover, to ensure system correctness, formal verification also comes into play as a promising approach that offers well-established techniques. In line with this, significant results have been obtained within the research on data-aware business processes, which studies the marriage between static and dynamic aspects of a system within a unified framework. However, several limitations are still present. Various formalisms for data-aware processes that have been studied typically use a simple mechanism for specifying the system dynamics. The majority of works also assume a rather simple treatment of inconsistency (i.e., reject inconsistent system states). Many researches in this area that consider structural domain knowledge typically also assume that such knowledge remains fixed along the system evolution (context-independent), and this might be too restrictive. Moreover, the information model of data-aware processes sometimes relies on relatively simple structures. This situation might cause an abstraction gap between the high-level conceptual view that business stakeholders have, and the low-level representation of information. When it comes to verification, taking into account all of the aspects above makes the problem more challenging. In this thesis, we investigate the verification of data-aware processes in the presence of ontologies while at the same time addressing all limitations above. Specifically, we provide the following contributions: (1) We propose a formal framework called Golog-KABs (GKABs), by leveraging on the state of the art formalisms for data-aware processes equipped with ontologies. GKABs enable us to specify semantically-rich data-aware business processes, where the system dynamics are specified using a high-level action language inspired by the Golog programming language. (2) We propose a parametric execution semantics for GKABs that is able to elegantly accommodate a plethora of inconsistency-aware semantics based on the well-known notion of repair, and this leads us to consider several variants of inconsistency-aware GKABs. (3) We enhance GKABs towards context-sensitive GKABs that take into account the contextual information during the system evolution. (4) We marry these two settings and introduce inconsistency-aware context-sensitive GKABs. (5) We introduce the so-called Alternating-GKABs that allow for a more fine-grained analysis over the evolution of inconsistency-aware context-sensitive systems. (6) In addition to GKABs, we introduce a novel framework called Semantically-Enhanced Data-Aware Processes (SEDAPs) that, by utilizing ontologies, enable us to have a high-level conceptual view over the evolution of the underlying system. We provide not only theoretical results, but have also implemented this concept of SEDAPs. We also provide numerous reductions for the verification of sophisticated first-order temporal properties over all of the settings above, and show that verification can be addressed using existing techniques developed for Data-Centric Dynamic Systems (which is a well-established data-aware processes framework), under suitable boundedness assumptions for the number of objects freshly introduced in the system while it evolves. Notably, all proposed GKAB extensions have no negative impact on computational complexity.

Submitted by Lukas Riehl Figueiredo null (lukas_rf@hotmail.com) on 2018-06-05T16:44:30Z No. of bitstreams: 1 Dissertacao-Lukas-Riehl-Figueiredo.pdf: 2667513 bytes, checksum: ea70d94af0366189c71508909d5f3ba7 (MD5) / Rejected by Elza Mitiko Sato null (elzasato@ibilce.unesp.br), reason: Solicitamos que realize correções na submissão seguindo as orientações abaixo: Problema 01) Na folha de aprovação deve constar a data(dia, mês e ano) da defesa, no seu arquivo está somente o ano. Lembramos que o arquivo depositado no repositório deve ser igual ao impresso, o rigor com o padrão da Universidade se deve ao fato de que o seu trabalho passará a ser visível mundialmente. Agradecemos a compreensão. on 2018-06-06T15:51:03Z (GMT) / Submitted by Lukas Riehl Figueiredo null (lukas_rf@hotmail.com) on 2018-06-06T21:57:37Z No. of bitstreams: 1 Dissertacao-Lukas-VF.pdf: 2667598 bytes, checksum: 032e5b83677ed9c2b780bd1c8401aa2e (MD5) / Approved for entry into archive by Elza Mitiko Sato null (elzasato@ibilce.unesp.br) on 2018-06-08T13:33:19Z (GMT) No. of bitstreams: 1 figueiredo_lr_me_sjrp.pdf: 2667598 bytes, checksum: 032e5b83677ed9c2b780bd1c8401aa2e (MD5) / Made available in DSpace on 2018-06-08T13:33:19Z (GMT). No. of bitstreams: 1 figueiredo_lr_me_sjrp.pdf: 2667598 bytes, checksum: 032e5b83677ed9c2b780bd1c8401aa2e (MD5) Previous issue date: 2018-02-01 / Modelos de processos de negócio têm sido utilizados em ambientes organizacionais para o entendimento da cadeia de processos, visando melhorias técnicas, gerenciais e estratégicas. Esses modelos abrangem variadas informações sobre os recursos utilizados e interações entre diferentes setores e pessoas, evidenciando interdependências entre os processos. Contudo, esses modelos podem apresentar problemas de legibilidade e dificuldades de navegação à medida em que se tornam extensos. A representação do conhecimento implícito é complexa e não está padronizada; as interdependências nem sempre são fáceis de serem compreendidas. O uso de ontologias tem aberto uma perspectiva complementar para mitigar esses problemas e prover processos com semânticas acessíveis por máquina. As ontologias contribuem para a conceituação e organização da informação embutida e desestruturada que se encontra presente nos processos de negócio e que deve ser explorada. As ontologias são utilizadas para estruturar o conhecimento implícito que está presente nos processos de negócio, possibilitando a compreensão desse conhecimento por máquina. As ontologias também contribuem para o alinhamento das visões das equipes de negócio e de Tecnologia da Informação da organização. Nesse contexto, este trabalho apresenta um processo sistemático para gerar uma ontologia a partir de um modelo de processos de negócio em BPMN v2.0, permitindo consultar informações sobre o modelo. Uma ferramenta denominada PM2ONTO foi então desenvolvida, visando gerar a ontologia em OWL automaticamente e disponibilizar uma interface para consultas predefinidas, elaboradas na linguagem SPARQL. Os modelos de processos de negócio devem ser exportados para arquivos em XPDL v2.2, os quais serão as entradas do sistema PM2ONTO. As ontologias resultantes ficam disponíveis em um banco de dados para consultas e também podem ser manipuladas por outras diferentes ferramentas. A avaliação do processo sistemático apresentado neste trabalho foi feita com base em estudos de caso, usando modelos de processos de negócio de diferentes áreas e diferentes níveis de complexidade. / Aiming technical, managerial and strategic improvements, business process models have been used in organizational environments to understand the process chain. Although these models may present readability problems and navigation difficulties as they become extensive, they can cover many information about resources and interactions between different sectors and people, showing interdependencies among the processes. Interdependencies are not always easy to understand because of its complex and not standardized knowledge. The use of ontologies has opened a complementary perspective to mitigate these problems and to provide processes with machine-accessible semantics. Also, they contribute in the conceptualization and organization of the embedded and unstructured information that is present in the business processes and that must be explored. In order to ease machine knowledge, ontologies are used to structure the implicit knowledge in business processes. They also contribute to the alignment of the organization's business and IT teams. In this context, this work presents a systematic process to generate an ontology from a business process model in BPMN v2.0, allowing to query information about the model. In this way, PM2ONTO tool was developed aiming to generate the ontology in OWL automatically and to provide an interface for predefined queries elaborated in the SPARQL language. Business process models should be exported to files in XPDL v2.2, which will be the inputs of the PM2ONTO system. The resulting ontologies stay available in a database for queries and can also be manipulated by other different tools. The systematic process evaluation presented in this work was made based on case studies, using business process models of different areas and different levels of complexity.