Commodification of accelerations for the Karp and Miller Construction

Autor: Igor Khmelnitsky, Serge Haddad, Alain Finkel

Publikováno v: Discrete Event Dynamic Systems. 31:251-270

Karp and Miller’s algorithm is based on an exploration of the reachability tree of a Petri net where, the sequences of transitions with positive incidence are accelerated. The tree nodes of Karp and Miller are labeled with ω-markings representing

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_________::f871e065eeda0ea115fb04cf74619305
https://doi.org/10.1007/s10626-020-00331-z

Revisiting Reachability in Polynomial Interrupt Timed Automata

Autor: Serge Haddad, Béatrice Bérard

Publikováno v: Information Processing Letters
Information Processing Letters, Elsevier, 2022, 174, pp.106208. ⟨10.1016/j.ipl.2021.106208⟩
Information Processing Letters, 2022, 174, pp.106208. ⟨10.1016/j.ipl.2021.106208⟩

International audience; Polynomial Interrupt Timed Automata (PolITA) are finite automata with clocks organized along hierarchical levels. These clocks are equipped with an interruption mechanism, well suited to the modeling of real-time operating sys

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::8a4cbda7876413b83679ac061811009b
https://hal.sorbonne-universite.fr/hal-03390569/document

Analyzing Robustness of Angluin's L* Algorithm in Presence of Noise

Autor: Igor Khmelnitsky, Serge Haddad, Lina Ye, Benoît Barbot, Benedikt Bollig, Martin Leucker, Daniel Neider, Rajarshi Roy

Publikováno v: GandALF 2022-13th International Symposium on Games, Automata, Logics and Formal Verification
GandALF 2022-13th International Symposium on Games, Automata, Logics and Formal Verification, Sep 2022, Madrid, Spain. pp.81-96, ⟨10.4204/EPTCS.370.6⟩
Electronic Proceedings in Theoretical Computer Science
Proceedings of the 13th International Symposium on Games, Automata, Logics and Formal Verification

Angluin's L$^*$ algorithm learns the minimal deterministic finite automaton (DFA) of a regular language using membership and equivalence queries. Its probabilistic approximatively correct (PAC) version substitutes an equivalence query by numerous ran

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::2a76d6763e21219fdb367fee8c88d14f

Polynomial interrupt timed automata: Verification and expressiveness

Autor: Mathieu Sassolas, Claudine Picaronny, Serge Haddad, M. Safey El Din, Béatrice Bérard

Publikováno v: Information and Computation
Information and Computation, 2021, 277, pp.104580. ⟨10.1016/j.ic.2020.104580⟩
Information and Computation, Elsevier, 2021, 277, pp.104580. ⟨10.1016/j.ic.2020.104580⟩

Interrupt Timed Automata ( ITA ) form a subclass of stopwatch automata where reachability and some variants of timed model checking are decidable even in presence of parameters. They are well suited to model and analyze real-time operating systems. H

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

Property-Directed Verification and Robustness Certification of Recurrent Neural Networks

Autor: Lina Ye, Benoît Barbot, Igor Khmelnitsky, Alain Finkel, Benedikt Bollig, Serge Haddad, Rajarshi Roy, Martin Leucker, Xuan Xie, Daniel Neider

Publikováno v: Automated Technology for Verification and Analysis ISBN: 9783030888848
ATVA

This paper presents a property-directed approach to verifying recurrent neural networks (RNNs). To this end, we learn a deterministic finite automaton as a surrogate model from a given RNN using active automata learning. This model may then be analyz

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_________::d0365ec06e8f0da8d5bffbd75b5b952b
https://doi.org/10.1007/978-3-030-88885-5_24