Forward analysis and model checking for trace bounded WSTS
From MaRDI portal
Publication:290914
DOI10.1016/j.tcs.2016.04.020zbMath1343.68162OpenAlexW2337536205MaRDI QIDQ290914
Sylvain Schmitz, Pierre Chambart, Alain Finkel
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
Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)
Related Items (4)
Unboundedness Problems for Languages of Vector Addition Systems. ⋮ Forward Analysis and Model Checking for Trace Bounded WSTS ⋮ Unnamed Item ⋮ Unnamed Item
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Bounded underapproximations
- Undecidable verification problems for programs with unreliable channels
- 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
- Undecidable problems in unreliable computations.
- 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
- Parallel program schemata
- Expand, enlarge and check: new algorithms for the coverability problem of WSTS
- Well-structured languages
- Complexity Hierarchies beyond Elementary
- Model-checking 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
- On Communicating Finite-State Machines
- About the decision of reachability for register machines
- Reachability in Two-Dimensional Vector Addition Systems with States Is PSPACE-Complete
- CONCUR 2004 - Concurrency Theory
- Automated Technology for Verification and Analysis
- Automated Technology for Verification and Analysis
- Bounded Algol-Like Languages
- A Characterization of Semilinear Sets
- Hierarchies of number-theoretic functions. I
- Well-structured transition systems everywhere!
This page was built for publication: Forward analysis and model checking for trace bounded WSTS
