Selected publications at LSV

We describe a simple, conceptual forward analysis procedure for ∈fty-complete WSTS mathfrakS. This computes the so-called clover of a state. When mathfrakS is the completion of a WSTS mathfrakX, the clover in mathfrakS is a finite description of the downward closure of the reachability set. We show that such completions are infinity-complete exactly when mathfrakX is an ω2-WSTS, a new robust class of WSTS. We show that our procedure terminates in more cases than the generalized Karp-Miller procedure on extensions of Petri nets and on lossy channel systems. We characterize the WSTS where our procedure terminates as those that are clover-flattable. Finally, we apply this to well-structured counter systems.

   author = {Finkel, Alain and Goubault{-}Larrecq, Jean},
   DOI = {10.2168/LMCS-8(3:28)2012},
   journal = {Logical Methods in Computer Science},
   month = sep,
   number = {3:28},
   title = {Forward Analysis for {WSTS}, Part~{II}: Complete {WSTS}},
   url = {},
   volume = {8},
   year = {2012},

About LSV

Select by Year