Forward Analysis for WSTS, Part II: Complete WSTS

Alain Finkel; Jean Goubault-Larrecq

doi:10.2168/LMCS-8(3:28)2012

Alain Finkel ; Jean Goubault-Larrecq - Forward Analysis for WSTS, Part II: Complete WSTS

lmcs:1217 - Logical Methods in Computer Science, September 29, 2012, Volume 8, Issue 3 - https://doi.org/10.2168/LMCS-8(3:28)2012

Forward Analysis for WSTS, Part II: Complete WSTSArticle

Authors: Alain Finkel ; Jean Goubault-Larrecq

We describe a simple, conceptual forward analysis procedure for infinity-complete WSTS S. This computes the so-called clover of a state. When S is the completion of a WSTS X, the clover in S is a finite description of the downward closure of the reachability set. We show that such completions are infinity-complete exactly when 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 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.

Comment: 35 pages, 6 figures. An extended abstract already appeared in Proc.
36th Intl. Coll. Automata, Languages and Programming (ICALP'09)

https://doi.org/10.2168/LMCS-8(3:28)2012

Source: arXiv.org:1208.4549

Volume: Volume 8, Issue 3

Secondary volumes: Selected Papers of the 36th International Colloquium on Automata, Languages and Programming (ICALP 2009)

Published on: September 29, 2012

Imported on: November 24, 2009

Keywords: Computer Science - Logic in Computer Science, D.2.4, F.3.1

Licence: arXiv.org - Non-exclusive license to distribute

Classifications

Mathematics Subject Classification 2020¹

Sources:

[1] zbMATH Open.

Bibliographic References

14 Documents citing this article

Alain Finkel;Mathieu Hilaire, 2023, Resilience and Home-Space for WSTS, Lecture notes in computer science, pp. 147-168, 10.1007/978-3-031-50524-9_7.

Alain Finkel;Serge Haddad;Igor Khmelnitsky, 2020, Commodification of accelerations for the Karp and Miller Construction, Discrete Event Dynamic Systems, 31, 2, pp. 251-270, 10.1007/s10626-020-00331-z.

Alain Finkel;Serge Haddad;Igor Khmelnitsky, 2020, Minimal Coverability Tree Construction Made Complete and Efficient, Lecture notes in computer science, pp. 237-256, 10.1007/978-3-030-45231-5_13, https://doi.org/10.1007/978-3-030-45231-5_13.

Alain Finkel;Jean Goubault-Larrecq, 2020, Forward analysis for WSTS, part I: completions, arXiv (Cornell University), 30, 7, pp. 752-832, 10.1017/s0960129520000195, https://arxiv.org/pdf/0902.1587v1.

Ranko Lazić;Sylvain Schmitz, 2020, The ideal view on Rackoff's coverability technique, Information and Computation, 277, pp. 104582, 10.1016/j.ic.2020.104582.

Petr Jančar;David Purser, 2019, Structural liveness of Petri nets is ExpSpace-hard and decidable, Warwick Research Archive Portal (University of Warwick), 56, 6, pp. 537-552, 10.1007/s00236-019-00338-6.

Pierre-Alain Reynier;Frédéric Servais, 2019, On the Computation of the Minimal Coverability Set of Petri Nets, pp. 164-177, 10.1007/978-3-030-30806-3_13, https://hal.science/hal-02442611.

Petr Jančar, 2017, Deciding Structural Liveness of Petri Nets, Lecture notes in computer science, pp. 91-102, 10.1007/978-3-319-51963-0_8.

Mitsuharu Yamamoto;Shogo Sekine;Saki Matsumoto, 2016, Formalization of Karp-Miller tree construction on petri nets, Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, pp. 66-78, 10.1145/3018610.3018626.

Pierre Chambart;Alain Finkel;Sylvain Schmitz, 2016, Forward analysis and model checking for trace bounded WSTS, Theoretical Computer Science, 637, pp. 1-29, 10.1016/j.tcs.2016.04.020.

Piotr Hofman;Sławomir Lasota;Ranko Lazić;Jérôme Leroux;Sylvain Schmitz;Patrick Totzke, 2016, Coverability Trees for Petri Nets with Unordered Data, pp. 445-461, 10.1007/978-3-662-49630-5_26, https://inria.hal.science/hal-01252674.

Jean Goubault-Larrecq, 2013, A Constructive Proof of the Topological Kruskal Theorem, Lecture notes in computer science, pp. 22-41, 10.1007/978-3-642-40313-2_3.

Sylvain Schmitz;Philippe Schnoebelen, 2013, The Power of Well-Structured Systems, arXiv (Cornell University), pp. 5-24, 10.1007/978-3-642-40184-8_2, http://arxiv.org/abs/1402.2908.

Alain Finkel;Jean Goubault-Larrecq, 2012, The Theory of WSTS: The Case of Complete WSTS, Lecture notes in computer science, pp. 3-31, 10.1007/978-3-642-31131-4_2.

Sources : OpenCitations, OpenAlex & Crossref

Share and export

Consultation statistics

This page has been seen 3395 times.

This article's PDF has been downloaded 617 times.