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.}
  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
  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.}
  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.",
  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.}
  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].}
  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.