BDD-based Bounded Model Checking for Temporal Properties of 1-Safe Petri Nets

DOI10.3233/FI-2011-513zbMath1238.68086OpenAlexW1666176304MaRDI QIDQ3097968

Wojciech Penczek, Artur Męski, Agata Półrola

Publication date: 10 November 2011

Published in: Fundamenta Informaticae (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.3233/fi-2011-513

zbMATH Keywords

verificationcorrectnessPetri netsmodel checkingtemporal logicdistributed systemconcurrencybinary decision diagrambounded model checkingLTLCTLSAT-solver

Mathematics Subject Classification ID

Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19) Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85) Distributed systems (68M14) Temporal logic (03B44) General topics in the theory of computing (68Q01)

This page was built for publication: BDD-based Bounded Model Checking for Temporal Properties of 1-Safe Petri Nets