Show simple item record

dc.contributor.authorFelli P
dc.contributor.authorDe Leoni M
dc.contributor.authorMontali M
dc.contributor.editor
dc.date.accessioned2020-05-13T09:30:13Z
dc.date.available2020-05-13T09:30:13Z
dc.date.issued2019
dc.identifier.isbn978-172813843-5
dc.identifier.urihttp://dx.doi.org/10.1109/ACSD.2019.00013
dc.identifier.urihttps://ieeexplore.ieee.org/document/8843610
dc.identifier.urihttps://bia.unibz.it/handle/10863/14039
dc.description.abstractIn recent years, there has been an increasing interest in enriching the traditional control-flow perspective of processes with additional dimensions, the data perspective being the most prominent one. At the same time, variants of Petri nets with data have been extensively studied, giving raise to a plethora of formal models with different expressive power and computational guarantees. In this work, we focus on DPNs, a data-aware extension of P/T nets where the net is enriched with data variables of different types, and transitions are guarded by formulae that inspect and update such variables. Even though DPNs are less expressive than Petri nets where data are carried by tokens, they elegantly capture business processes operating over simple case data and taking complex decisions based on these data. Notably, various techniques have been implemented to discover DPNs from event data. However, such techniques do not guarantee that the discovered DPN is actually sound. In previous work, we have then studied how to check soundness of DPNs with simple data-based guards that can only compare variables with constants. In this paper, we generalize the study of soundness to DPNs to the fundamental case where the evolution of the process depends on the comparison between the values carried by different variables through linear inequations. Our main contribution is to show decidability of soundness for this sophisticated class of DPNs. This is done by constructing an abstract state space of the net relying on the manipulation of constraints, and by showing that such an abstract state space can be faithfully and effectively inspected for soundness. The construction lends itself to be directly implemented by combining standard state-space construction methods with constraint programming techniques.en_US
dc.languageEnglish
dc.language.isoenen_US
dc.publisherIEEEen_US
dc.relation19th International Conference on Application of Concurrency to System Design, ACSD 2019 ; Aachen : 22.6.2019 - 27.6.2019
dc.rights
dc.subjectData-aware processesen_US
dc.subjectSoundnessen_US
dc.titleSoundness verification of decision-aware process models with variable-to-variable conditionsen_US
dc.typeBook chapteren_US
dc.date.updated2020-05-13T03:00:21Z
dc.publication.title2019 19th International Conference on Application of Concurrency to System Design (ACSD)
dc.language.isiEN-GB
dc.description.fulltextopenen_US


Files in this item

Thumbnail

This item appears in the following Collection(s)

Show simple item record