@inproceedings{JLMX-mfps30,
address = {Ithaca, New~York, USA},
month = jun,
year = 2014,
volume = 308,
series = {Electronic Notes in Theoretical Computer Science},
publisher = {Elsevier Science Publishers},
editor = {Jacobs, Bart and Silva, Alexandra and Staton, Sam},
acronym = {{MFPS}'14},
booktitle = {{P}roceedings of the 30th {C}onference on
{M}athematical {F}oundations of {P}rogramming
{S}emantics ({MFPS}'14)},
author = {Jaziri, Samy and Larsen, Kim G. and Mardare, Radu and Xue, Bingtian},
title = {Adequacy and Complete Axiomatization for Timed Modal Logic},
pages = {183-210},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/JLMX-mfps14.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/JLMX-mfps14.pdf},
doi = {10.1016/j.entcs.2014.10.011},
abstract = {In this paper we develop the metatheory for Timed Modal
Logic~(TML), which is the modal logic used for the analysis of timed
transition systems~(TTSs). We solve a series of long-standing open
problems related to~TML. Firstly, we prove that TML enjoys the
Hennessy-Milner property and solve one of the open questions in the field.
Secondly, we prove that the set of validities are not recursively
enumerable. Nevertheless, we develop a strongly-complete proof system
for~TML. Since the logic is not compact, the proof system contains
infinitary rules, but only with countable sets of instances. Thus, we~can
involve topological results regarding Stone spaces, such as the
Rasiowa-Sikorski lemma, to complete the proofs.}
}
@inproceedings{BJM-concur15,
address = {Madrid, Spain},
month = sep,
year = 2015,
volume = {42},
series = {Leibniz International Proceedings in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {Aceto, Luca and de Frutos-Escrig, David},
acronym = {{CONCUR}'15},
booktitle = {{P}roceedings of the 26th
{I}nternational {C}onference on
{C}oncurrency {T}heory
({CONCUR}'15)},
author = {Bouyer, Patricia and Jaziri, Samy and Markey, Nicolas},
title = {On~the Value Problem in Weighted Timed Games},
pages = {311-324},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BJM-concur15.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BJM-concur15.pdf},
doi = {10.4230/LIPIcs.CONCUR.2015.311},
abstract = {A~weighted timed game is a timed game with extra quantitative
information representing e.g. energy consumption. Optimizing the cost for
reaching a target is a natural question, which has been investigated for
ten years. Existence of optimal strategies is known to be undecidable in
general, and only very restricted classes of games have been described for
which optimal cost and almost-optimal strategies can be computed.\par
In this paper, we show that the value problem is undecidable in general
weighted timed games. The undecidability proof relies on that for the
existence of optimal strategies and on a diagonalization construction
recently designed in the context of quantitative temporal logics. We then
provide an algorithm to compute arbitrary approximations of the value in a
game, and almost-optimal strategies. The algorithm applies in a large
subclass of weighted timed games, and is the first approximation scheme
which is designed in the current context.}
}
@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{BJM-formats17,
address = {Berlin, Germany},
month = sep,
year = 2017,
volume = {10419},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Abate, Alessandro and Geeraerts, Gilles},
acronym = {{FORMATS}'17},
booktitle = {{P}roceedings of the 15th {I}nternational {C}onference
on {F}ormal {M}odelling and {A}nalysis of {T}imed
{S}ystems ({FORMATS}'17)},
author = {Bouyer, Patricia and Jaziri, Samy and Markey, Nicolas},
title = {On the Determinization of Timed Systems},
pages = {25-41},
url = {https://hal.archives-ouvertes.fr/hal-01566436/},
doi = {10.1007/978-3-319-65765-3_2},
abstract = {We introduce a new formalism called automata over a timed domain which provides an adequate framework for the determinization of timed systems. In this formalism, determinization w.r.t. timed language is always possible at the cost of changing the timed domain. We give a condition for determinizability of automata over a timed domain without changing the timed domain, which allows us to recover several known determinizable classes of timed systems, such as strongly-non-zeno timed automata, integer-reset timed automata, perturbed timed automata, etc. Moreover in the case of timed automata this condition encompasses most determinizability conditions from the literature.}
}
@inproceedings{BJM-rv18,
address = {Limassol, Cyprus},
month = nov,
volume = 11237,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Colombo, Christian and Leucker, Martin},
acronym = {{RV}'18},
booktitle = {{P}roceedings of the 18th {W}orkshop on {R}untime {V}erification ({RV}'18)},
author = {Bouyer, Patricia and Jaziri, Samy and Markey, Nicolas},
title = {Efficient Timed Diagnosis Using Automata with Timed Domains},
pages = {205-221},
year = {2018},
doi = {10.1007/978-3-030-03769-7_12},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BJM-rv18.pdf},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BJM-rv18.pdf},
abstract = {We consider the problems of efficiently diagnosing and predicting what did (or will) happen in a partially-observable one-clock timed automaton. We introduce timed sets as a formalism to keep track of the evolution of the reachable configurations over time, and use our previous work on automata over timed domains to build a candidate diagnoser for our timed automaton. We report on our implementation of this approach compared to the approach of [Tripakis, Fault diagnosis for timed automata, 2002].}
}
@mastersthesis{m2-Jaziri,
author = {Jaziri, Samy},
title = {{Robustness issues in priced timed automata}},
school = {{M}aster {P}arisien de {R}echerche en
{I}nformatique, Paris, France},
type = {Rapport de {M}aster},
year = {2014},
month = sep
}
@phdthesis{jaziri-phd2019,
author = {Samy Jaziri},
title = {{Automata on Timed Structures}},
school = {{\'E}cole Normale Sup{\'e}rieure Paris-Saclay, France},
type = {Th{\`e}se de doctorat},
year = 2019,
month = sep,
url = {https://tel.archives-ouvertes.fr/tel-02384274},
pdf = {https://tel.archives-ouvertes.fr/tel-02384274/document}
}
This file was generated by bibtex2html 1.98.