Transforming Dynamic Condition Response Graphs to Safe Petri Nets

被引:0
|
作者
Cosma, Vlad Paul [1 ,2 ]
Hildebrandt, Thomas T. [2 ]
Slaats, Tijs [2 ]
机构
[1] KMD, Ballerup, Denmark
[2] Univ Copenhagen, Comp Sci Dept, Copenhagen, Denmark
关键词
Petri Nets; DCR graphs; Bisimilarity; REFINEMENT; NETWORKS;
D O I
10.1007/978-3-031-33620-1_22
中图分类号
TP18 [人工智能理论];
学科分类号
081104 ; 0812 ; 0835 ; 1405 ;
摘要
We present a transformation of the Dynamic Condition Response (DCR) graph constraint based process specification language to safe Petri Nets with inhibitor and read arcs, generalized with an acceptance criteria enabling the specification of the union of regular and omega-regular languages. We prove that the DCR graph and the resulting Petri Net are bisimilar and that the bisimulation respects the acceptance criterium. The transformation enables the capturing of regular and omega-regular process requirements from texts and event logs using existing tools for DCR requirements mapping and process mining. A representation of DCR Graphs as Petri Nets advances the understanding of the relationship between the two models and enables improved analysis and model checking capabilities for DCR graph specifications through mature Petri net tools. We provide a python script implementing the transformation from the DCR XML export format to the PNML exchange format extended with arc types. In the implementation, all read arcs are replaced by a pair of standard input and output arcs. This directly enables the simulation and analysis of the resulting Petri Nets in tools such as TAPAAL, but means that the acceptance criterium for infinite runs is not preserved.
引用
收藏
页码:417 / 439
页数:23
相关论文
共 50 条
  • [41] SAT-based verification of safe Petri nets
    Ogata, S
    Tsuchiya, T
    Kikuno, T
    AUTOMATED TECHNOLOGY FOR VERIFICATION AND ANALYSIS, PROCEEDINGS, 2004, 3299 : 79 - 92
  • [42] Control of safe ordinary petri nets using unfolding
    Giua, A
    Xie, XL
    DISCRETE EVENT DYNAMIC SYSTEMS-THEORY AND APPLICATIONS, 2005, 15 (04): : 349 - 373
  • [43] A Polynomial Translation of π-Calculus (FCP) to Safe Petri Nets
    Meyer, Roland
    Khomenko, Victor
    Huechting, Reiner
    CONCUR 2012 - CONCURRENCY THEORY, 2012, 7454 : 440 - 455
  • [44] A POLYNOMIAL TRANSLATION OF π-CALCULUS FCPS TO SAFE PETRI NETS
    Khomenko, Victor
    Meyer, Roland
    Huechting, Reiner
    LOGICAL METHODS IN COMPUTER SCIENCE, 2013, 9 (03)
  • [45] Analysis of approximate Petri nets by means of occurrence graphs
    Suraj, Zbigniew
    Fryc, Barbara
    FUNDAMENTA INFORMATICAE, 2007, 79 (3-4) : 541 - 551
  • [46] ALGORITHMS FOR COMPUTING COVERABILITY GRAPHS FOR CONTINUOUS PETRI NETS
    Novosad, Petr
    Ceska, Milan
    EUROPEAN SIMULATION AND MODELLING CONFERENCE 2008, 2008, : 489 - 491
  • [47] Business alignments based on reachable graphs of Petri nets
    Han D.
    Tian Y.
    Du Y.
    Zhang Q.
    Jisuanji Jicheng Zhizao Xitong/Computer Integrated Manufacturing Systems, CIMS, 2020, 26 (06): : 1589 - 1606
  • [48] Modelling condition monitoring and dynamic grouping of maintenance actions with extended coloured stochastic Petri nets
    Nebel, S.
    Dieter, A.
    Bertsche, B.
    RELIABILITY, RISK AND SAFETY: THEORY AND APPLICATIONS VOLS 1-3, 2010, : 599 - 605
  • [49] Formal design methodology for transforming ladder diagram to Petri nets
    J. C. Quezada
    J. Medina
    E. Flores
    J. C. Seck Tuoh
    N. Hernández
    The International Journal of Advanced Manufacturing Technology, 2014, 73 : 821 - 836
  • [50] Algorithm for Transforming Models of Business Processes into Monochrome Petri Nets
    Dorrer, M. G.
    AUTOMATIC CONTROL AND COMPUTER SCIENCES, 2011, 45 (07) : 460 - 468