Forward Analysis for WSTS, Part II: Complete WSTS

DOI10.1007/978-3-642-02930-1_16MaRDI QIDQ3638095zbMATH OpenOpenAlexFDO

Authors Jean Goubault-Larrecq, Alain Finkel

Publication date 14 July 2009

Published in Automata, Languages and Programming (Search for Journal in Brave)

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

Mathematics Subject Classification ID

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

Abstract: We describe a simple, conceptual forward analysis procedure for infinity-complete WSTS S. This computes the so-called clover of a state. When S is the completion of a WSTS X, the clover in S is a finite description of the downward closure of the reachability set. We show that such completions are infinity-complete exactly when X is an omega-2-WSTS, a new robust class of WSTS. We show that our procedure terminates in more cases than the generalized Karp-Miller procedure on extensions of Petri nets and on lossy channel systems. We characterize the WSTS where our procedure terminates as those that are clover-flattable. Finally, we apply this to well-structured counter systems.

Recommendations

• Forward analysis for WSTS. II: Complete WSTS
• The Theory of WSTS: The Case of Complete WSTS
• Forward analysis for WSTS. III: Karp-Miller trees
• Forward analysis for WSTS. III: Karp-Miller trees
• Forward analysis for WSTS. I: Completions

Cited in

(19)

• Multiset rewriting for the verification of depth-bounded processes with name binding
• Separability and non-determinizability of WSTS
• Ideal abstractions for well-structured transition systems
• Deciding safety properties in infinite-state pi-calculus via behavioural types
• Forward analysis and model checking for trace bounded WSTS
• The Theory of WSTS: The Case of Complete WSTS
• Forward analysis and model checking for trace bounded WSTS
• Forward analysis for WSTS, part I: completions
• Forward analysis for WSTS. III: Karp-Miller trees
• Minimal coverability set for Petri nets: Karp and Miller algorithm with pruning
• Forward analysis for WSTS. III: Karp-Miller trees
• Decidability and complexity of Petri nets with unordered data
• Coverability synthesis in parametric Petri nets
• Forward analysis for WSTS. I: Completions
• Handling infinitely branching well-structured transition systems
• Directed regular and context-free languages
• The ideal theory for WSTS
• The ideal approach to computing closed subsets in well-quasi-orderings
• Forward analysis for WSTS. II: Complete WSTS

This page was built for publication: Forward Analysis for WSTS, Part II: Complete WSTS

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