DCModelChecker 2.0: A BMC tool for Unbounded PN

20260 citationsOthergreen Open Access

Authors

Tephilla Prince · Indian Institute of Technology Dharwad

Ramchandra Phawade · Indian Institute of Technology Dharwad

S Sheerazuddin · Fukushima National College of Technology

Abstract

DCModelChecker 2.0 is a bounded model checking tool that uses the 2D-BMC algorithm.InputLogic: Linear temporal logic with integer arithmeticModel: Petri net in PNML formatbound Features:* Uses concurrent Petri net semantics* Showcases the 2D-BMC algorithm* Provides counterexample trace when property is falsified. In case of any issues with installation or queries, please write to the developer tephilla.prince.18@iitdh.ac.in

Topics & Keywords

Publication Details

Published in: Zenodo (CERN European Organization for Nuclear Research)

DOI: 10.5281/zenodo.18680953

Command Palette

DCModelChecker 2.0: A BMC tool for Unbounded PN

Authors

Abstract

Topics & Keywords

Publication Details