Model checking lossy vector addition systems
From MaRDI portal
concurrent systems with unreliable communicationdecidability of model checkingtemporal logicsvector addition systems with states
Temporal logic (03B44) Logic in computer science (03B70) Automata and formal grammars in connection with logical questions (03D05) Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)
Recommendations
Cited in
(14)- On minimal elements of upward-closed sets
- Undecidable problems in unreliable computations.
- A general approach to comparing infinite-state systems with their finite-state specifications
- Expand, enlarge and check: new algorithms for the coverability problem of WSTS
- Monotonic extensions of Petri nets: forward and backward search revisited
- Narrowing and rewriting logic: from foundations to applications
- Model Checking Coverability Graphs of Vector Addition Systems
- Model checking lossy channels systems is probably decidable
- An assertional language for the verification of systems parametric in several dimensions (preliminary results)
- Regular separability of well-structured transition systems
- Coverability synthesis in parametric Petri nets
- Decidability of model checking with the temporal logic EF
- Well-structured transition systems everywhere!
- Symbolic reachability analysis using narrowing and its application to verification of cryptographic protocols
This page was built for publication: Model checking lossy vector addition systems
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4251060)
