Forward analysis and model checking for trace bounded WSTS
From MaRDI portal
Recommendations
Cites work
- scientific article; zbMATH DE number 1670482 (Why is no real title available?)
- scientific article; zbMATH DE number 4024806 (Why is no real title available?)
- scientific article; zbMATH DE number 3582425 (Why is no real title available?)
- scientific article; zbMATH DE number 1223710 (Why is no real title available?)
- scientific article; zbMATH DE number 1302047 (Why is no real title available?)
- scientific article; zbMATH DE number 1954380 (Why is no real title available?)
- scientific article; zbMATH DE number 1796145 (Why is no real title available?)
- scientific article; zbMATH DE number 1392309 (Why is no real title available?)
- scientific article; zbMATH DE number 1405652 (Why is no real title available?)
- scientific article; zbMATH DE number 3310089 (Why is no real title available?)
- A Characterization of Semilinear Sets
- A well-structured framework for analysing Petri net extensions
- About the decision of reachability for register machines
- Algorithmic analysis of programs with well quasi-ordered domains.
- An algorithmic approach for checking closure properties of temporal logic specifications and -regular languages
- Automated Technology for Verification and Analysis
- Automated Technology for Verification and Analysis
- Bounded Algol-Like Languages
- Bounded underapproximations
- CONCUR 2004 - Concurrency Theory
- Complexity hierarchies beyond elementary
- Computable fixpoints in well-structured symbolic model checking
- Decidability of model checking for infinite-state concurrent systems
- Expand, enlarge and check: new algorithms for the coverability problem of WSTS
- Finding the growth rate of a regular or context-free language in polynomial time
- Forward Analysis for WSTS, Part II: Complete WSTS
- Forward analysis for WSTS. I: Completions
- From pre-historic to post-modern symbolic model checking
- Hierarchies of number-theoretic functions. I
- Interprocedural reachability for flat integer programs
- Lossy counter machines decidability cheat sheet
- Mixing Lossy and Perfect Fifo Channels
- Model Checking Coverability Graphs of Vector Addition Systems
- Model-checking \(\mathrm{CTL}^*\) over flat Presburger counter systems
- Multiply-recursive upper bounds with Higman's lemma
- ON YEN'S PATH LOGIC FOR PETRI NETS
- On Communicating Finite-State Machines
- Parallel program schemata
- Rational and recognizable complex trace languages
- Reachability in two-dimensional vector addition systems with states is PSPACE-complete
- Reduction and covering of infinite reachability trees
- Revisiting Ackermann-Hardness for Lossy Counter Machines and Reset Petri Nets
- Symbolic reachability analysis of FIFO-channel systems with nonregular sets of configurations
- Taming past LTL and flat counter systems
- The covering and boundedness problems for vector addition systems
- Undecidable problems in unreliable computations.
- Undecidable verification problems for programs with unreliable channels
- Using forward reachability analysis for verification of lossy channel systems
- Verifying programs with unreliable channels
- Well-structured languages
- Well-structured transition systems everywhere!
Cited in
(7)- Verifying unboundedness via amalgamation
- Forward analysis and model checking for trace bounded WSTS
- Forward analysis for WSTS, part I: completions
- Forward analysis for WSTS. III: Karp-Miller trees
- Forward analysis for WSTS. III: Karp-Miller trees
- Forward analysis of depth-bounded processes
- Unboundedness problems for languages of vector addition systems
This page was built for publication: Forward analysis and model checking for trace bounded WSTS
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q290914)
