Property Directed Reachability for Generalized Petri Nets

Autor: Silvano Dal Zilio, Nicolas Amat, Thomas Hujsa

Publikováno v: Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2022
Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2022, Apr 2022, Munich, Germany. ⟨10.1007/978-3-030-99524-9_28⟩
Tools and Algorithms for the Construction and Analysis of Systems ISBN: 9783030995232

We propose a semi-decision procedure for checking generalized reachability properties, on generalized Petri nets, that is based on the Property Directed Reachability (PDR) method. We actually define three different versions, that vary depending on th

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::b499303cd9d345711aabb81d7fd4a753
http://arxiv.org/abs/2208.03043

Checking marking reachability with the state equation in Petri net subclasses

Autor: Thomas Hujsa, Bernard Berthomieu, Silvano Dal Zilio, Didier Le Botlan

Publikováno v: HAL

Although decidable, the marking reachability problem for Petri nets is well-known to be intractable in general, and a non-elementary lower bound has been recently uncovered. In order to alleviate this difficulty, various structural and behavioral res

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::fcbdd13bbd47858550634fa1f9b136af
https://hal.laas.fr/hal-02992521

Synthesis of Weighted Marked Graphs from Constrained Labelled Transition Systems: A Geometric Approach

Autor: Thomas Hujsa, Raymond Devillers, Evgeny Erofeev

Publikováno v: Transactions on Petri Nets and Other Models of Concurrency XIV
Transactions on Petri Nets and Other Models of Concurrency XIV, Springer, pp.172-191, 2019, 978-3-662-60650-6. ⟨10.1007/978-3-662-60651-3_7⟩
Transactions on Petri Nets and Other Models of Concurrency XIV ISBN: 9783662606506

22 pages; International audience; Recent studies investigated the problems of analysing Petri nets and synthesising them from labelled transition systems (LTS) with two labels (transitions) only. In this paper, we extend these works by providing new

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::1f943eadaaa0bd2e6449c52a2a0ee09c
https://hal.laas.fr/hal-02348962

Sufficient conditions for the marked graph realisability of labelled transition systems

Autor: Harro Wimmel, Eike Best, Thomas Hujsa

Publikováno v: Theoretical Computer Science
Theoretical Computer Science, Elsevier, 2018, 750, pp.101-116. ⟨10.1016/j.tcs.2017.10.006⟩

This paper describes two results within the context of Petri net synthesis from labelled transition systems. We consider a set of structural properties of transition systems, and we show that, given such properties, it is possible to re-engineer a Pe

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::524bf7c699a431fed90daa55e3ca38f6
https://hal.archives-ouvertes.fr/hal-02127711

Proposition of an Action Layer for Electrum

Autor: David Chemouil, Alcino Cunha, Thomas Hujsa, Nuno Macedo, Jeanne Tawa, Julien Brunel

Publikováno v: 6th International ABZ Conference ASM, Alloy, B, TLA, VDM, Z
6th International ABZ Conference ASM, Alloy, B, TLA, VDM, Z, Jun 2018, Southampton, United Kingdom. pp.397-402, ⟨10.1007/978-3-319-91271-4_30⟩
Lecture Notes in Computer Science ISBN: 9783319912707
ABZ

Electrum is an extension of Alloy that adds (1) mutable signatures and fields to the modeling layer; and (2) connectives from linear temporal logic (with past) and primed variables à la TLA+ to the constraint language. The analysis of models can the

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::3b74ce25376c51fc644f65a0b96d48f2
https://hal.archives-ouvertes.fr/hal-01774920