Handling infinitely branching well-structured transition systems

DOI10.1016/j.ic.2017.11.001zbMath1383.68054OpenAlexW2767753763MaRDI QIDQ1686118

Alain Finkel, Michael Blondin, Pierre McKenzie

Publication date: 20 December 2017

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

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

zbMATH Keywords

completiondecidabilityterminationwell-structured transition systemscoverabilityinfinite branching

Mathematics Subject Classification ID

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

Related Items (4)

Unnamed Item ⋮ The Ideal Approach to Computing Closed Subsets in Well-Quasi-orderings ⋮ Unnamed Item ⋮ Unnamed Item

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Theory of relations. Transl. from the French by P. Clote
• Reduction and covering of infinite reachability trees
• A note on well quasi-orderings for powersets
• A well-structured framework for analysing Petri net extensions
• Algorithmic analysis of programs with well quasi-ordered domains.
• Using forward reachability analysis for verification of lossy channel systems
• Unreliable channels are easier to verify than perfect channels
• On termination and invariance for faulty channel machines
• Computable fixpoints in well-structured symbolic model checking
• Expand, enlarge and check: new algorithms for the coverability problem of WSTS
• On families of mutually exclusive sets
• Coverability Trees for Petri Nets with Unordered Data
• The Power of Well-Structured Systems
• Ideal Abstractions for Well-Structured Transition Systems
• Efficient Coverability Analysis by Proof Minimization
• Well-Structured Graph Transformation Systems with Negative Application Conditions
• Multiply-Recursive Upper Bounds with Higman’s Lemma
• Forward Analysis of Depth-Bounded Processes
• On Languages Piecewise Testable in the Strict Sense
• Forward Analysis for WSTS, Part II: Complete WSTS
• On Communicating Finite-State Machines
• Deciding Piecewise Testable Separability for Regular Tree Languages
• Demystifying Reachability in Vector Addition Systems
• The Complexity of Coverability in ν-Petri Nets
• On the Decidability Status of Reachability and Coverability in Graph Transformation Systems
• ω-Petri Nets
• Partial well‐ordering of sets of vectors
• Verification, Model Checking, and Abstract Interpretation
• The ideal view on Rackoff's coverability technique
• Well-structured transition systems everywhere!

This page was built for publication: Handling infinitely branching well-structured transition systems