Forward analysis for WSTS. III: Karp-Miller trees

zbMATH Open1491.68117arXiv1710.07258MaRDI QIDQ5114831FDOQ5114831

Alain Finkel, Jean Goubault-Larrecq, Michael Blondin

Publication date: 26 June 2020

Full work available at URL: https://arxiv.org/abs/1710.07258

Recommendations

• Forward analysis for WSTS. III: Karp-Miller trees
• Forward Analysis for WSTS, Part II: Complete WSTS
• Forward analysis for WSTS. II: Complete WSTS
• The Theory of WSTS: The Case of Complete WSTS
• Ideal abstractions for well-structured transition systems

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)

Cites Work

• Title not available (Why is that?)
• Theory of relations. Transl. from the French by P. Clote
• On Context-Free Languages
• Reverse mathematics and initial intervals
• Title not available (Why is that?)
• Reduction and covering of infinite reachability trees
• 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
• Computable fixpoints in well-structured symbolic model checking
• Forward analysis and model checking for trace bounded WSTS
• ON YEN'S PATH LOGIC FOR PETRI NETS
• Lossy Counter Machines Decidability Cheat Sheet
• Forward Analysis for WSTS, Part II: Complete WSTS
• Title not available (Why is that?)
• Well-structured transition systems everywhere!
• Title not available (Why is that?)
• On the complexity of the linear-time μ-calculus for Petri Nets
• A unified approach for deciding the existence of certain petri net paths
• The residue of vector sets with applications to decidability problems in Petri nets
• On families of mutually exclusive sets
• Title not available (Why is that?)
• Undecidable verification problems for programs with unreliable channels
• Title not available (Why is that?)
• Title not available (Why is that?)
• Rélations non reconstructibles par leurs restrictions
• Multiset rewriting for the verification of depth-bounded processes with name binding
• Title not available (Why is that?)
• Dimension de Krull des ensembles ordonnés. (Krull dimension of ordered sets)
• Title not available (Why is that?)
• A Constructive Proof of the Topological Kruskal Theorem
• Bounds on Mobility
• Ordered sets with no infinite antichains
• Une extension d'un théorème de P. Jullien sur les âges de mots
• Handling infinitely branching well-structured transition systems
• Forward Analysis for WSTS, Part II: Complete WSTS
• On Computing Fixpoints in Well-Structured Regular Model Checking, with Applications to Lossy Channel Systems
• Recursive Petri nets
• FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science
• \(\omega\)-Petri nets: algorithms and complexity
• Title not available (Why is that?)
• Extending the Rackoff technique to Affine nets

Cited In (4)

• Forward analysis for WSTS, part I: completions
• Title not available (Why is that?)
• FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science
• Expand, enlarge and check: new algorithms for the coverability problem of WSTS

This page was built for publication: Forward analysis for WSTS. III: Karp-Miller trees

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