Multiset rewriting for the verification of depth-bounded processes with name binding

DOI10.1016/j.ic.2012.03.004zbMath1277.68204WikidataQ57831209 ScholiaQ57831209MaRDI QIDQ714507

María Martos-Salgado, Fernando Rosa-Velardo

Publication date: 11 October 2012

Published in: Information and Computation (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.ic.2012.03.004

zbMATH Keywords

verification; process algebra; Petri nets; decidability; multiset rewriting; depth-boundedness; WSTS

Mathematics Subject Classification ID

68Q60: Specification and verification (program logics, model checking, etc.)

68Q85: Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)

68Q42: Grammars and rewriting systems

Related Items

Unnamed Item, Unnamed Item, Unnamed Item, Ordinal recursive complexity of unordered data nets, Petri nets with name creation for transient secure association

Uses Software

• Petruchio

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Decidability and complexity of Petri nets with unordered data
• Reachability analysis of fragments of mobile ambients in AC term rewriting
• All about Maude -- a high-performance logical framework. How to specify, program and verify systems in rewriting logic. With CD-ROM.
• Distributed semantics for the \(\pi \)-calculus based on Petri nets with inhibitor ARCS
• A theory of structural stationarity in the \(\pi\)-calculus
• The covering and boundedness problems for vector addition systems
• A calculus for cryptographic protocols: The spi calculus
• Mobile ambients
• A well-structured framework for analysing Petri net extensions
• When ambients cannot be opened
• Algorithmic analysis of programs with well quasi-ordered domains.
• On the Power of Cliques in the Parameterized Verification of Ad Hoc Networks
• Decidability Problems in Petri Nets with Names and Replication
• Encoding Asynchronous Interactions Using Open Petri Nets
• On the Relationship between π-Calculus and Finite Place/Transition Petri Nets
• Forward Analysis of Depth-Bounded Processes
• Parameterized Verification of Ad Hoc Networks
• Depth Boundedness in Multiset Rewriting Systems with Name Binding
• Revisiting Ackermann-Hardness for Lossy Counter Machines and Reset Petri Nets
• Comparing the Expressive Power of Well-Structured Transition Systems
• Forward Analysis for WSTS, Part II: Complete WSTS
• Deciding reachability problems in Turing-complete fragments of Mobile Ambients
• Multiset Rewriting: A Semantic Framework for Concurrency with Name Binding
• Deciding Reachability in Mobile Ambients with Name Restriction
• Programming Languages and Systems
• Ordering by Divisibility in Abstract Algebras
• Verification, Model Checking, and Abstract Interpretation
• Well-structured transition systems everywhere!
• Rewriting logic as a semantic framework for concurrency: a progress report