MPI-INF Logo
Campus Event Calendar

Event Entry

What and Who

Incremental, Inductive Coverability

Johannes Kloos
Max Planck Institute for Software Systems
SWS Student Defense Talks - Qualifying Exam
  
MPI Audience
English

Date, Time and Location

Monday, 11 March 2013
15:00
60 Minutes
G26
318
Kaiserslautern

Abstract

We give an incremental, inductive (IC3) procedure to check

coverability of well-structured transition systems. Our procedure generalizes
the IC3 procedure for safety verification that has been successfully
applied in finite-state hardware verification to infinite-state wellstructured
transition systems. We show that our procedure is sound,
complete, and terminating for downward-finite well-structured transition
systems —where each state has a finite number of states below it— a
class that contains extensions of Petri nets, broadcast protocols, and
lossy channel systems.
We have implemented our algorithm for checking coverability of Petri
nets. We describe how the algorithm can be efficiently implemented
without the use of SMT solvers. Our experiments on standard Petri
net benchmarks show that IC3 is competitive with state-of-the-art implementations
for coverability based on symbolic backward analysis or
expand-enlarge-and-check algorithms both in time taken and space usage.

Contact

--email hidden
passcode not visible
logged in users only

Maria-Louise Maggio, 04/04/2013 10:02 -- Created document.