Forward analysis and model checking for trace bounded WSTS
DOI10.1016/J.TCS.2016.04.020zbMATH Open1343.68162OpenAlexW2337536205MaRDI QIDQ290914FDOQ290914
Authors: Pierre Chambart, Alain Finkel, Sylvain Schmitz 
Publication date: 3 June 2016
Published in: Theoretical Computer Science (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/j.tcs.2016.04.020
Recommendations
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?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Parallel program schemata
- Bounded Algol-Like Languages
- On Communicating Finite-State Machines
- Undecidable problems in unreliable computations.
- Title not available (Why is that?)
- Reduction and covering of infinite reachability trees
- The covering and boundedness problems for vector addition systems
- An algorithmic approach for checking closure properties of temporal logic specifications and \(\omega\)-regular languages
- Rational and recognizable complex trace languages
- A well-structured framework for analysing Petri net extensions
- Algorithmic analysis of programs with well quasi-ordered domains.
- From pre-historic to post-modern symbolic model checking
- Using forward reachability analysis for verification of lossy channel systems
- Decidability of model checking for infinite-state concurrent systems
- Verifying programs with unreliable channels
- Symbolic reachability analysis of FIFO-channel systems with nonregular sets of configurations
- Computable fixpoints in well-structured symbolic model checking
- Taming past LTL and flat counter systems
- Expand, enlarge and check: new algorithms for the coverability problem of WSTS
- Well-structured languages
- Title not available (Why is that?)
- Complexity hierarchies beyond elementary
- Model-checking \(\mathrm{CTL}^*\) over flat Presburger counter systems
- Interprocedural reachability for flat integer programs
- Multiply-recursive upper bounds with Higman's lemma
- ON YEN'S PATH LOGIC FOR PETRI NETS
- Model Checking Coverability Graphs of Vector Addition Systems
- Mixing Lossy and Perfect Fifo Channels
- Lossy counter machines decidability cheat sheet
- Revisiting Ackermann-Hardness for Lossy Counter Machines and Reset Petri Nets
- Finding the growth rate of a regular or context-free language in polynomial time
- Forward Analysis for WSTS, Part II: Complete WSTS
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- About the decision of reachability for register machines
- Bounded underapproximations
- Reachability in two-dimensional vector addition systems with states is PSPACE-complete
- Title not available (Why is that?)
- CONCUR 2004 - Concurrency Theory
- Forward analysis for WSTS. I: Completions
- Automated Technology for Verification and Analysis
- Automated Technology for Verification and Analysis
- A Characterization of Semilinear Sets
- Hierarchies of number-theoretic functions. I
- Well-structured transition systems everywhere!
- Undecidable verification problems for programs with unreliable channels
Cited In (6)
- 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
Uses Software
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)
