@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}, futureseries = {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 }

*This file was generated by
bibtex2html 1.98.*