Decidability of LTL for vector addition systems with one zero-test

DOI10.1007/978-3-642-24288-5_9MaRDI QIDQ3172867zbMATHOpenAlexFDO

Authors Rémi Bonnet

Publication date 7 October 2011

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-24288-5_9

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Decidability of theories and sets of sentences (03B25) Temporal logic (03B44) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Recommendations

• Model checking vector addition systems with one zero-test
• The Reachability Problem for Vector Addition System with One Zero-Test
• Place-boundedness for vector addition systems with one zero-test
• Mixing coverability and reachability to analyze VASS with one zero-test
• Model Checking Coverability Graphs of Vector Addition Systems

Cited in

(4)

• The Reachability Problem for Vector Addition System with One Zero-Test
• Place-boundedness for vector addition systems with one zero-test
• On selective unboundedness of VASS
• Model checking vector addition systems with one zero-test

Describes a project that uses

Uses Software

• LTL2BA

This page was built for publication: Decidability of LTL for vector addition systems with one zero-test

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3172867)