@comment{{B-arxiv16,
author = Bollig, Benedikt,
affiliation = aff-LSVmexico,
title = One-Counter Automata with Counter Visibility,
institution = Computing Research Repository,
number = 1602.05940,
month = feb,
nmonth = 2,
year = 2016,
type = RR,
axeLSV = mexico,
NOcontrat = "",
url = http://arxiv.org/abs/1602.05940,
PDF = "http://www.lsv.fr/Publis/PAPERS/PDF/B-arxiv16.pdf",
lsvdate-new = 20160222,
lsvdate-upd = 20160222,
lsvdate-pub = 20160222,
lsv-category = "rapl",
wwwpublic = "public and ccsb",
note = 18~pages,
abstract = "In a one-counter automaton (OCA), one can read a letter
from some finite alphabet, increment and decrement the counter by
one, or test it for zero. It is well-known that universality and
language inclusion for OCAs are undecidable. We consider here OCAs
with counter visibility: Whenever the automaton produces a letter,
it outputs the current counter value along with~it. Hence, its
language is now a set of words over an infinite alphabet. We show
that universality and inclusion for that model are in PSPACE, thus
no harder than the corresponding problems for finite automata, which
can actually be considered as a special case. In fact, we show that
OCAs with counter visibility are effectively determinizable and
closed under all boolean operations. As~a~strict generalization, we
subsequently extend our model by registers. The general nonemptiness
problem being undecidable, we impose a bound on the number of
register comparisons and show that the corresponding nonemptiness
problem is NP-complete.",
}}
@inproceedings{FHK-atpn19,
address = {Aachen, Germany},
month = jun,
year = 2019,
volume = {11522},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Susanna Donatelli and Stefan Haar},
acronym = {{PETRI~NETS}'19},
booktitle = {{P}roceedings of the 40th
{I}nternational {C}onference on
{A}pplications and {T}heory of {P}etri {N}ets
({PETRI~NETS}'19)},
author = {Finkel, Alain and Haddad, Serge and Khmelnitsky, Igor},
title = {Coverability and Termination in Recursive Petri Nets},
pages = { 429-448},
url = {https://hal.inria.fr/hal-02081019},
pdf = {https://hal.inria.fr/hal-02081019/document},
doi = {10.1007/978-3-030-21571-2_23},
abstract = {In the early two-thousands, Recursive Petri nets have been introduced in order to model distributed planning of multi-agent systems for which counters and recursivity were necessary. Although Recursive Petri nets strictly extend Petri nets and stack automata, most of the usual property problems are solvable but using non primitive recursive algorithms, even for coverability and termination. For almost all other extended Petri nets models containing a stack the complexity of coverability and termination are unknown or strictly larger than EXPSPACE. In contrast, we establish here that for Recursive Petri nets, the coverability and termination problems are EXPSPACE-complete as for Petri nets. From an expressiveness point of view, we show that coverability languages of Recursive Petri nets strictly include the union of coverability languages of Petri nets and context-free languages. Thus we get for free a more powerful model than Petri net.}
}
@article{FHK-deds20,
publisher = {Springer},
journal = {Discrete Event Dynamic Systems: Theory and Applications},
author = {Alain Finkel and Serge Haddad and Igor Khmelnitsky},
title = {{Commodification of accelerations for the Karp and Miller Construction}},
doi = {10.1007/s10626-020-00331-z},
year = {2020},
url = {https://link.springer.com/article/10.1007/s10626-020-00331-z}
}
@techreport{KY-arxiv20,
author = {Khmelnitsky, Igor and
Neider, Daniel and
Roy, Rajarshi and
Barbot, Beno{\^{\i}}t and
Bollig, Benedikt and
Finkel, Alain and
Haddad, Serge and
Leucker, Martin and
Ye, Lina },
institution = {Computing Research Repository},
month = sep,
number = {2009.10610},
type = {Research Report},
title = {Property-Directed Verification of Recurrent Neural Networks},
year = {2020},
url = {https://arxiv.org/abs/2009.10610},
pdf = {https://arxiv.org/pdf/2009.10610.pdf}
}
@inproceedings{HK-atpn20,
address = {Paris, France},
month = jun,
volume = {12152},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Ryszard Janicki and Natalia Sidorova and Thomas Chatain},
acronym = {{PETRI~NETS}'20},
booktitle = {{P}roceedings of the 41st
{I}nternational {C}onference on
{A}pplications and {T}heory of {P}etri {N}ets
({PETRI~NETS}'20)},
author = {Serge Haddad and Igor Khmelnitsky},
title = {{D}ynamic {R}ecursive {P}etri {N}ets},
pages = {345-366},
doi = {10.1007/978-3-030-51831-8\_17},
year = 2020,
url = {https://hal.inria.fr/hal-02511321}
}
@inproceedings{FHK-msr2019,
address = {Angers, France},
month = nov,
futureseries = {Journal Europ{\'e}en des Syst{\`e}mes Automatis{\'e}s},
publisher = {HAL},
editor = {Beno{\^i}t Delahaye and S{\'e}bastien Lahaye and Mehdi Lhommeau},
acronym = {{MSR}'19},
booktitle = {{A}ctes du 12{\`e}me {C}olloque sur la
{M}od{\'e}lisation des {S}yst{\`e}mes
{R}{\'e}actifs
({MSR}'19)},
author = {Alain Finkel and Serge Haddad and Igor Khmelnitsky},
title = {{R{\'e}ification des acc{\'e}l{\'e}rations pour la construction de Karp et Miller}},
year = 2019,
pdf = {https://hal.archives-ouvertes.fr/hal-02431913/file/MSR19_paper_17.pdf},
url = {https://hal.archives-ouvertes.fr/hal-02431913}
}
@inproceedings{FHK-fossacs2020,
address = {Dublin, Ireland},
month = apr,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Barbara K{\"o}nig and Jean Goubault-Larrecq},
acronym = {{FoSSaCS}'20},
booktitle = {{P}roceedings of the 23rd {I}nternational
{C}onference on {F}oundations of {S}oftware {S}cience
and {C}omputation {S}tructures
({FoSSaCS}'20)},
author = {Alain Finkel and Serge Haddad and Igor Khmelnitsky},
title = {Minimal coverability tree construction made complete and efficient},
pages = {237--256},
doi = {10.1007/978-3-030-45231-5_13},
year = 2020
}
This file was generated by bibtex2html 1.98.