000 03970nam a22005535i 4500
001 978-3-031-42746-6
003 DE-He213
005 20240423130153.0
007 cr nn 008mamaa
008 231029s2023 sz | s |||| 0|eng d
020 _a9783031427466
_9978-3-031-42746-6
024 7 _a10.1007/978-3-031-42746-6
_2doi
050 4 _aHF5548.125-.6
072 7 _aKJQ
_2bicssc
072 7 _aCOM005030
_2bisacsh
072 7 _aKJQ
_2thema
082 0 4 _a650.0285
_223
082 0 4 _a658.05
_223
100 1 _aGianola, Alessandro.
_eauthor.
_4aut
_4http://id.loc.gov/vocabulary/relators/aut
245 1 0 _aVerification of Data-Aware Processes via Satisfiability Modulo Theories
_h[electronic resource] /
_cby Alessandro Gianola.
250 _a1st ed. 2023.
264 1 _aCham :
_bSpringer Nature Switzerland :
_bImprint: Springer,
_c2023.
300 _aXXVIII, 317 p. 28 illus.
_bonline resource.
336 _atext
_btxt
_2rdacontent
337 _acomputer
_bc
_2rdamedia
338 _aonline resource
_bcr
_2rdacarrier
347 _atext file
_bPDF
_2rda
490 1 _aLecture Notes in Business Information Processing,
_x1865-1356 ;
_v470
505 0 _aIntroduction -- 1.1 Overview -- 1.1.1 Finite-State Model Checking -- 1.1.2 Verification of Data-Aware Processes -- 1.1.3 Infinite-state Model Checking: from Parameterized Systems to SMT Verification -- 1.1.4 Main Goal of the Book -- 1.2 Related Literature -- 1.2.1 Formal Models for Data-Aware (Business) Processes -- 1.2.2 Verification of Data-Aware Processes -- 1.2.3 Model Checking for Infinite-State Systems using SMT-based Techniques -- 1.3 Contributions of the Book -- 1.3.1 Contributions of the First Part -- 1.3.2 Contributions of the Second Part -- 1.3.3 Contributions of the Third Part -- Part I Foundations of SMT-based Safety Verification of Artifact Systems -- 2 Preliminaries from Model Theory and Logic -- 3 Array-Based Artifact Systems: General Framework -- 4 Safety Verification of Artifact Systems -- 5 Decidability Results via Termination of the Verification Machinery -- 6. Preliminaries For (Uniform) Interpolation -- 7 Uniform Interpolation for Database Theories -- 8 Combination of Uniform Interpolants for DAPs Verification -- 9 MCMT: a Concrete Model Checker for DAPs -- 10 Business Process Management and Petri Nets: Preliminaries -- 11 DABs: a Theoretical Framework for Data-Aware BPMN -- 12 delta-BPMN: the operational and implemented counterpart of DABs -- 13 Catalog Object-Aware Nets -- 14 Conclusions -- References.
520 _aThis book is a revised version of the PhD dissertation written by the author at the University of Bozen-Bolzano in Italy. It presents a new approach to safety verification of a particular class of infinite-state systems, called Data-Aware Processes (DAPs). To do so, the developed technical machinery requires to devise novel results for uniform interpolation and its combination in the context of automated reasoning. These results are then applied to the analysis of concrete business processes enriched with real data. In 2022, the PhD dissertation won the “BPM Dissertation Award”, granted to outstanding PhD theses in the field of Business Process Management. .
650 0 _aBusiness
_xData processing.
650 0 _aArtificial intelligence.
650 0 _aBusiness information services.
650 1 4 _aBusiness Informatics.
650 2 4 _aArtificial Intelligence.
650 2 4 _aIT in Business.
710 2 _aSpringerLink (Online service)
773 0 _tSpringer Nature eBook
776 0 8 _iPrinted edition:
_z9783031427459
776 0 8 _iPrinted edition:
_z9783031427473
830 0 _aLecture Notes in Business Information Processing,
_x1865-1356 ;
_v470
856 4 0 _uhttps://doi.org/10.1007/978-3-031-42746-6
912 _aZDB-2-SCS
912 _aZDB-2-SXCS
912 _aZDB-2-LNB
942 _cSPRINGER
999 _c185818
_d185818