Searching for just a few words should be enough to get started. If you need to make more complex queries, use the tips below to guide you.
Issue title: Application and Theory of Petri Nets and Concurrency 2023: Special Issue of Selected Papers
Guest editors: Robert Lorenz and Sławomir Lasota
Article type: Research Article
Authors: Amat, Nicolasa; * | Dal Zilio, Silvanob | Le Botlan, Didierb
Affiliations: [a] IMDEA Software Institute, Madrid, Spain. [email protected] | [b] LAAS-CNRS, Université de Toulouse, INSA, CNRS, Toulouse, France
Correspondence: [*] Address for correspondence: IMDEA Software Institute Campus Montegancedo s/n, 28223 Pozuelo de Alarcon, Madrid, Spain
Abstract: We propose an automated procedure to prove polyhedral abstractions (also known as polyhedral reductions) for Petri nets. Polyhedral abstraction is a new type of state space equivalence, between Petri nets, based on the use of linear integer constraints between the marking of places. In addition to defining an automated proof method, this paper aims to better characterize polyhedral reductions, and to give an overview of their application to reachability problems. Our approach relies on encoding the equivalence problem into a set of SMT formulas whose satisfaction implies that the equivalence holds. The difficulty, in this context, arises from the fact that we need to handle infinite-state systems. For completeness, we exploit a connection with a class of Petri nets, called flat nets, that have Presburger-definable reachability sets. We have implemented our procedure, and we illustrate its use on several examples.
Keywords: Automated reasoning, Abstraction techniques, Reachability problems, Petri nets
DOI: 10.3233/FI-242197
Journal: Fundamenta Informaticae, vol. 192, no. 3-4, pp. 363-394, 2024
IOS Press, Inc.
6751 Tepper Drive
Clifton, VA 20124
USA
Tel: +1 703 830 6300
Fax: +1 703 830 2300
[email protected]
For editorial issues, like the status of your submitted paper or proposals, write to [email protected]
IOS Press
Nieuwe Hemweg 6B
1013 BG Amsterdam
The Netherlands
Tel: +31 20 688 3355
Fax: +31 20 687 0091
[email protected]
For editorial issues, permissions, book requests, submissions and proceedings, contact the Amsterdam office [email protected]
Inspirees International (China Office)
Ciyunsi Beili 207(CapitaLand), Bld 1, 7-901
100025, Beijing
China
Free service line: 400 661 8717
Fax: +86 10 8446 7947
[email protected]
For editorial issues, like the status of your submitted paper or proposals, write to [email protected]
如果您在出版方面需要帮助或有任何建, 件至: [email protected]