Forward analysis for WSTS. II: Complete WSTS. (English) Zbl 1248.68352

Finkel, Alain; Goubault-Larrecq, Jean

Albers, Susanne (ed.) et al., Automata, languages and programming. 36th international colloquium, ICALP 2009, Rhodes, Greece, July 5–12, 2009. Proceedings, Part II. Berlin: Springer (ISBN 978-3-642-02929-5/pbk). Lecture Notes in Computer Science 5556, 188-199 (2009).

Summary: We describe a simple, conceptual forward analysis procedure for \(\infty \)-complete WSTS \(\mathfrak S\). This computes the clover of a state \(s _{0}\), i.e., a finite description of the closure of the cover of \(s _{0}\). When \(\mathfrak S\) is the completion of a WSTS \(\mathfrak X\), the clover in \(\mathfrak S\) is a finite description of the cover in \(\mathfrak X\). We show that this applies exactly when \(\mathfrak X\) is an \(\omega ^{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. We characterize the WSTS where our procedure terminates as those that are clover-flattable. Finally, we apply this to well-structured counter systems.
For Part I see [the authors, LIPIcs – Leibniz Int. Proc. Inform. 3, 433–444 (2009; Zbl 1236.68183)].
For the entire collection see [Zbl 1166.68002].

MSC:

68Q85	Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
68Q55	Semantics in the theory of computing
68Q60	Specification and verification (program logics, model checking, etc.)

Citations:

Zbl 1236.68183