Automated Polyhedral Abstraction Proving

Autor: Nicolas Amat, Silvano Dal Zilio, Didier Le Botlan

Publikováno v: Application and Theory of Petri Nets and Concurrency ISBN: 9783031336195
Application and Theory of Petri Nets and Concurrency. PETRI NETS 2023
44th International Conference on Application and Theory of Petri Nets and Concurrency (Petri Nets 2023)
44th International Conference on Application and Theory of Petri Nets and Concurrency (Petri Nets 2023), Jun 2023, Lisbon, Portugal. pp.324-345, ⟨10.1007/978-3-031-33620-1_18⟩

International audience; We propose an automated procedure to prove polyhedral abstractions for Petri nets. Polyhedral abstraction is a new type of state-space equivalence based on the use of linear integer constraints. Our approach relies on an encod

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::7cabce154f332efecde76c8bafa58d4d
https://doi.org/10.1007/978-3-031-33620-1_18

A New Product Construction for the Diagnosability of Patterns in Time Petri Net

Autor: Éric Lubat, Silvano Dal Zilio, Audine Subias, Yannick Pencolé, Didier Le Botlan

Publikováno v: 59th Conference on Decision and Control (CDC) 2020
59th Conference on Decision and Control (CDC) 2020, Dec 2020, Jeju Island (virtual conference), South Korea. ⟨10.1109/CDC42340.2020.9303826⟩
HAL
CDC

International audience; We propose a method to decide the diagnosability of patterns in labeled Time Petri nets (TPN) that gracefully extends a classic approach for the diagnosability of single faults. Our approach is based on a new technique for com

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::7f0b02860a307caa3edf7696d52ba356
https://hal.laas.fr/hal-02989834/document

Counting Petri net markings from reduction equations

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

Publikováno v: International Journal on Software Tools for Technology Transfer
International Journal on Software Tools for Technology Transfer, Springer Verlag, 2020, 22, pp.163-181. ⟨10.1007/s10009-019-00519-1⟩
International Journal on Software Tools for Technology Transfer, 2020, 22, pp.163-181. ⟨10.1007/s10009-019-00519-1⟩

International audience; We propose a method to count the number of reachable markings of a Petri net without having to enumerate these first. The method relies on a structural reduction system that reduces the number of places and transitions of the

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

Presentation of the 9th Edition of the Model Checking Contest

Autor: Lom Messan Hillah, Fabrice Kordon, Silvano Dal Zilio, Bernard Berthomieu, Jeroen Meijer, Loïg Jezequel, Andrew S. Miner, Peter Gjøl Jensen, Didier Le Botlan, Gianfranco Ciardo, Elvio Gilberto Amparore, Tom van Dijk, Yann Thierry-Mieg, Torsten Liebke, Francis Hulin-Hubard, Karsten Wolf, Emmanuel Paviot-Adet, Jiří Srba, Francesco Gallà

Publikováno v: Tools and Algorithms for the Construction and Analysis of Systems-25 Years of TACAS: TOOLympics, Held as Part of ETAPS 2019, Proceedings, Part III
Tools and Algorithms for the Construction and Analysis of Systems-25 Years of TACAS: TOOLympics, Held as Part of ETAPS 2019, Proceedings, Part III, Apr 2019, Prague, Czech Republic. pp.50-68, ⟨10.1007/978-3-030-17502-3_4⟩
Tools and Algorithms for the Construction and Analysis of Systems ISBN: 9783030175016
TACAS (3)
Amparore, E, Berthomieu, B, Ciardo, G, Dal Zilio, S, Gallà, F, Hillah, L M, Hulin-Hubard, F, Jensen, P G, Jezequel, L, Kordon, F, Le Botlan, D, Liebke, T, Meijer, J, Miner, A, Paviot-Adet, E, Srba, J, Thierry-Mieg, Y, van Dijk, T & Wolf, K 2019, Presentation of the 9th Edition of the Model Checking Contest . in F Kordon, M Huisman, B Steffen & D Beyer (eds), International Conference on Tools and Algorithms for the Construction and Analysis of Systems : TACAS 2019: Tools and Algorithms for the Construction and Analysis of Systems . Springer, Lecture Notes in Computer Science, vol. 11429, pp. 50-68, 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems conference series, TACAS 2019 held as part of the 22nd European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Prague, Czech Republic, 06/04/2019 . https://doi.org/10.1007/978-3-030-17502-3_4
Tools and Algorithms for the Construction and Analysis of Systems-25 Years of TACAS: TOOLympics, Held as Part of ETAPS 2019, Proceedings, 50-68
STARTPAGE=50;ENDPAGE=68;TITLE=Tools and Algorithms for the Construction and Analysis of Systems-25 Years of TACAS

International audience; The Model Checking Contest (MCC) is an annual competition of software tools for model checking. Tools must process an increasing benchmark gathered from the whole community and may participate in various examinations: state sp

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::83d20bac4d677364c4f761e84dd91386
https://hal.sorbonne-universite.fr/hal-02094047

A Verified Approach for Checking Real-Time Specification Patterns

Autor: Nouha Abid, Silvano Dal Zilio, Didier Le Botlan

Publikováno v: Electronic Workshops in Computing (eWiC)
VECoS 2012, 6th International Workshop on Verification and Evaluation of Computer and Communication Systems
VECoS 2012, 6th International Workshop on Verification and Evaluation of Computer and Communication Systems, Aug 2012, France. pp.11
HAL

We propose a verified approach to the formal verification of timed properties using model-checking techniques. We focus on properties expressed using real-time specification patterns, which can be viewed as a subset of timed temporal logics that incl

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::fa23424e5dd1480f92896d94c2026d3d
https://hal.science/hal-00782647v2/file/article.pdf