TY - GEN N1 - Prace Naukowe Uniwersytetu Ekonomicznego we Wrocławiu = Research Papers of Wrocław University of Economics; 2010; Nr 147, s. 173-188 N2 - The paper presents a formal verification of the business processes expressed in BPMN. Verification is based on deductive reasoning. Automatic transformations of basic BPMN workflow patterns to temporal logic formulae are introduced. These formulae constitute a system specification and they are later processed using semantic tableaux method. In general, such reasoning technique has many advantages over the traditional approach, i.e., the resolution method. The paper provides automatic transformations for five basic BPMN workflow patterns and the example process is provided with description in BPMN diagram. The related temporal logic formula is obtained through automatic transformations, then the algorithm of reasoning using semantic tableaux methodology is applied to verify the business model. L1 - http://www.dbc.wroc.pl/Content/119833/Klimek_Skrzynski_Turek_Deducation_based_verufication.pdf M3 - artykuł L2 - http://www.dbc.wroc.pl/Content/119833 PY - 2010 KW - deductive reasoning KW - business processes KW - BPMN KW - workflow design patterns KW - formal verification KW - semantic tablea C1 - Wszystkie prawa zastrzeżone (Copyright) A1 - Klimek, Radosław A1 - Skrzyński, Paweł A1 - Turek, Michał PB - Publishing House of Wrocław University of Economics C6 - Dla wszystkich w zakresie dozwolonego użytku LA - eng CY - Wrocław T1 - Deduction Based Verification of Business Models UR - http://www.dbc.wroc.pl/dlibra/publication/edition/119833 T2 - Weryfikacja modeli biznesowych metodą dedukcyjną ER -