Model checking Petri nets with names using data-centric dynamic systems

DOI10.1007/S00165-016-0370-6MaRDI QIDQ315291zbMATH OpenOpenAlexWikidataFDO

Authors Marco Montali, Andrey Rivkin

Publication date 20 September 2016

Published in Formal Aspects of Computing (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/s00165-016-0370-6

zbMATH Keywords

formal verificationdata-aware business processesfirst-order temporal logicsinfinite-state systemsPetri nets with namesresource-aware business processes

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Recommendations

• Decidability and complexity of Petri nets with unordered data
• Petri nets with structured data
• Accelerations for the coverability set of Petri nets with names
• The complexity of coverability in \(\nu\)-Petri nets
• Decidability problems in Petri nets with names and replication

Cites work

• scientific article; zbMATH DE number 5506900 (Why is no real title available?)
• scientific article; zbMATH DE number 1059247 (Why is no real title available?)
• scientific article; zbMATH DE number 1456956 (Why is no real title available?)
• A new approach to abstract syntax with variable binding
• A note on colored Petri nets
• A theory of name boundedness
• Applications and Theory of Petri Nets 2004
• Applications and Theory of Petri Nets 2005
• Coloured Petri Nets
• Computable queries for relational data bases
• Cost soundness for priced resource-constrained workflow nets
• Database Theory - ICDT 2005
• Decidability and complexity of Petri nets with unordered data
• Description logic knowledge and action bases
• Elements of finite model theory.
• First-order -calculus over generic transition systems and applications to the situation calculus
• Modeling and Verification of a Protocol for Operational Support Using Coloured Petri Nets
• Modeling business processes. A Petri net-oriented approach
• Nets with tokens which carry data
• Reasoning about cryptographic protocols in the spi calculus
• Resource-constrained workflow nets
• Soundness of workflow nets: classification, decidability, and analysis
• Towards nominal computation
• Understanding Petri Nets
• Verification of agent-based artifact systems

Cited in

(11)

• From DB-nets to Coloured Petri Nets with Priorities
• Describing Behavior of Processes with Many-to-Many Interactions
• scientific article; zbMATH DE number 5506900 (Why is no real title available?)
• Correctness Notions for Petri Nets with Identifiers
• Aligning event logs to resource-constrained \(\nu \)-Petri nets
• Data and process resonance. Identifier soundness for models of information systems
• Petri nets with name creation for transient secure association
• First-order -calculus over generic transition systems and applications to the situation calculus
• Exact and approximated log alignments for processes with inter-case dependencies
• A Non-Deterministic Multiset Query Language
• Soundness verification of data-aware process models with variable-to-variable conditions

This page was built for publication: Model checking Petri nets with names using data-centric dynamic systems

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q315291)