Automated Technology for Verification and Analysis

DOI10.1007/B102065MaRDI QIDQ5394178zbMATH OpenOpenAlexFDO

Authors Shougo Ogata, Tatsuhiro Tsuchiya, Tohru Kikuno

Publication date 25 October 2006

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

Full work available at URL https://doi.org/10.1007/b102065

zbMATH Keywords

Bounded model checkingPetri netsSAT

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)

Recommendations

• BDD-based bounded model checking for temporal properties of 1-safe Petri nets
• SMT-based reachability checking for bounded time Petri nets
• SAT-based (parametric) reachability for a class of distributed time Petri nets
• scientific article; zbMATH DE number 1799521
• Accelerating bounded model checking of safety properties

Cited in

(13)

• Analysis of safeness in a Petri net-based specification of the control part of cyber-physical systems
• On the combination of polyhedral abstraction and SMT-based model checking for Petri nets
• Planning as satisfiability: parallel plans and algorithms for plan search
• SAT-Based Synthesis Methods for Safety Specs
• BDD-based bounded model checking for temporal properties of 1-safe Petri nets
• A Canonical Contraction for Safe Petri Nets
• scientific article; zbMATH DE number 5286860 (Why is no real title available?)
• Planning as satisfiability: heuristics
• On the Construction of Pullbacks for Safe Petri Nets
• Exploiting step semantics for efficient bounded model checking of asynchronous systems
• scientific article; zbMATH DE number 1863166 (Why is no real title available?)
• Properties of Plain, Pure, and Safe Petri Nets
• SMT-based reachability checking for bounded time Petri nets

Describes a project that uses

Uses Software

• NuSMV
• Chaff
• SPIN
• VINAS-P

This page was built for publication: Automated Technology for Verification and Analysis

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