000 04104nam a22005775i 4500
001 978-3-031-42746-6
003 DE-He213
005 20240207153738.0
007 cr nn 008mamaa
008 231029s2023 sz | s |||| 0|eng d
020 _a9783031427466
_9978-3-031-42746-6
050 4 _aHF5548.125-.6
072 7 _aKJQ
_2bicssc
072 7 _aCOM014000
_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
500 _aAcceso multiusuario
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. .
541 _fUABC ;
_cPerpetuidad
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 _zLibro electrónico
_uhttp://libcon.rec.uabc.mx:2048/login?url=https://doi.org/10.1007/978-3-031-42746-6
912 _aZDB-2-SCS
912 _aZDB-2-SXCS
912 _aZDB-2-LNB
942 _cLIBRO_ELEC
999 _c263124
_d263123