Forward Analysis and Model Checking for Trace Bounded WSTS

DOI10.1007/978-3-642-21834-7_4zbMath1330.68197arXiv1004.2802OpenAlexW3104578959MaRDI QIDQ3011881

Pierre Chambart, Sylvain Schmitz, Alain Finkel

Publication date: 29 June 2011

Published in: Applications and Theory of Petri Nets (Search for Journal in Brave)

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

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)

Related Items (3)

Unnamed Item ⋮ Non axiomatisability of positive relation algebras with constants, via graph homomorphisms ⋮ Unnamed Item

Uses Software

• TREX
• FAST
• LASH
• ALGOL 60

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Forward analysis and model checking for trace bounded WSTS
• Undecidable verification problems for programs with unreliable channels
• Petri nets and regular languages
• Reduction and covering of infinite reachability trees
• The covering and boundedness problems for vector addition systems
• Undecidable problems in unreliable computations.
• Algorithmic analysis of programs with well quasi-ordered domains.
• 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
• Parallel program schemata
• Well-structured languages
• Model-checking CTL* over flat Presburger counter systems
• Model Checking Coverability Graphs of Vector Addition Systems
• FINDING THE GROWTH RATE OF A REGULAR OR CONTEXT-FREE LANGUAGE IN POLYNOMIAL TIME
• Forward Analysis for WSTS, Part II: Complete WSTS
• About the decision of reachability for register machines
• Verifying liveness for asynchronous programs
• Automated Technology for Verification and Analysis
• Automated Technology for Verification and Analysis
• Bounded Algol-Like Languages
• A Characterization of Semilinear Sets
• Flat Parametric Counter Automata
• Well-structured transition systems everywhere!

This page was built for publication: Forward Analysis and Model Checking for Trace Bounded WSTS