Nicolas Markey

@phdthesis{phd-sadhukhan,
  author =              {Sadhukhan, Suman},
  title =               {A Verification Viewpoint on Network Congestion
                         Games},
  year =                {2021},
  month =               dec,
  school =              {Universit{\'e} Rennes~1, France},
}

@phdthesis{phd-safra,
  author =              {Safra, Shmuel},
  title =               {Complexity of Automata on Infinite Objects},
  year =                {1989},
  month =               mar,
  school =              {Weizmann Institute of Science, Rehovot, Israel},
}

@inproceedings{stoc1992-Saf,
  author =              {Safra, Shmuel},
  title =               {Exponential Determinization for
                         {\(\omega\)}-Automata with Strong-Fairness
                         Acceptance Condition},
  booktitle =           {{P}roceedings of the 24th {A}nnual {ACM} {S}ymposium
                         on the {T}heory of {C}omputing ({STOC}'92)},
  acronym =             {{STOC}'92},
  publisher =           {ACM Press},
  pages =               {272-282},
  year =                {1992},
}

@inproceedings{mbtrs2004-San,
  author =              {Sandberg, Sven},
  title =               {Homing and Synchronizing Sequences},
  editor =              {Broy, Manfred and Jonsson, Bengt and Katoen,
                         Joost-Pieter and Leucker, Martin and Pretschner,
                         Alexander},
  booktitle =           {{A}dvanced {L}ectures on {M}odel-{B}ased {T}esting
                         of {R}eactive {S}ystems ({MBTRS}'04)},
  acronym =             {{MBTRS}'04},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {3472},
  pages =               {5-33},
  year =                {2005},
  confyear =            {2004},
  confmonth =           {1},
}

@mastersthesis{master10-sankur,
  author =              {Sankur, Ocan},
  title =               {Model-checking robuste des automates temporis{\'e}s
                         via les machines {\`a} canaux},
  year =                {2010},
  school =              {Lab.~Sp\'ecification \& V\'erification, ENS Cachan,
                         France},
  type =                {M\'emoire de master},
}

@phdthesis{phd-sankur,
  author =              {Sankur, Ocan},
  title =               {Robustness in Timed Automata: Analysis, Synthesis,
                         Implementation},
  year =                {2013},
  month =               may,
  school =              {Lab.~Sp\'ecification \& V\'erification, ENS Cachan,
                         France},
  type =                {Th\`ese de doctorat},
}

@inproceedings{tacas2015-San,
  author =              {Sankur, Ocan},
  title =               {Symbolic Quantitative Robustness Analysis of Timed
                         Automata},
  editor =              {Baier, {\relax Ch}ristel and Tinelli, Cesare},
  booktitle =           {{P}roceedings of the 21st {I}nternational
                         {C}onference on {T}ools and {A}lgorithms for
                         {C}onstruction and {A}nalysis of {S}ystems
                         ({TACAS}'15)},
  acronym =             {{TACAS}'15},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {9035},
  pages =               {484-498},
  year =                {2015},
  month =               apr,
  doi =                 {10.1007/978-3-662-46681-0_48},
}

@techreport{suny-93-01,
  author =              {Sarnath, Ramnath},
  title =               {Doubly Logarithmic Time Parallel Sorting},
  number =              {93-01},
  year =                {1993},
  month =               jan,
  institution =         {suny},
  type =                {Technical Report},
}

@article{jcss4(2)-Sav,
  author =              {Savitch, Walter},
  title =               {Relationships between nondeterministic and
                         deterministic tape complexities},
  publisher =           {Academic Press},
  journal =             {Journal of Computer and System Sciences},
  volume =              {4},
  number =              {2},
  pages =               {177-192},
  year =                {1970},
  month =               apr,
  doi =                 {10.1016/S0022-0000(70)80006-X},
}

@inproceedings{concur2003-Saw,
  author =              {Sawa, Zden{\v{e}}k},
  title =               {Equivalence Checking of Non-flat Systems is
                         EXPTIME-hard},
  editor =              {Amadio, Roberto and Lugiez, Denis},
  booktitle =           {{P}roceedings of the 14th {I}nternational
                         {C}onference on {C}oncurrency {T}heory
                         ({CONCUR}'03)},
  acronym =             {{CONCUR}'03},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {2761},
  pages =               {237-250},
  year =                {2003},
  month =               aug,
}

@inproceedings{cav2000-SB,
  author =              {Somenzi, Fabio and Bloem, Roderick},
  title =               {Efficient {B}{\"u}chi Automata from {LTL} Formulae},
  editor =              {Emerson, E. Allen and Sistla, A. Prasad},
  booktitle =           {{P}roceedings of the 12th {I}nternational
                         {C}onference on {C}omputer {A}ided {V}erification
                         ({CAV}'00)},
  acronym =             {{CAV}'00},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {1855},
  pages =               {248-263},
  year =                {2000},
  month =               jul,
}

@inproceedings{cav2003-SB,
  author =              {Seshia,Sanjit A. and Bryant, Randal E.},
  title =               {Unbounded, Fully Symbolic Model Checking of Timed
                         Automata using Boolean Methods},
  editor =              {Hunt, Jr, Warren A. and Somenzi, Fabio},
  booktitle =           {{P}roceedings of the 15th {I}nternational
                         {C}onference on {C}omputer {A}ided {V}erification
                         ({CAV}'03)},
  acronym =             {{CAV}'03},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {2725},
  pages =               {154-166},
  year =                {2003},
  month =               jul,
  doi =                 {10.1007/978-3-540-45069-6_16},
}

@inproceedings{fmcad2011-SB,
  author =              {Somenzi, Fabio and Bradley, Steven},
  title =               {{IC3:} where monolithic and incremental meet},
  booktitle =           {{P}roceedings of the 11th {I}nternational
                         {C}onference on {F}ormal {M}ethods in
                         {C}omputer-{A}ided {D}esign ({FMCAD}'11)},
  acronym =             {{FMCAD}'11},
  pages =               {3-8},
  year =                {2011},
  month =               oct,
}

Résumé

We define and study a new approach to the implementability of timed automata, where the semantics is perturbed by imprecisions and finite frequency of the hardware. In order to circumvent these effects, we introduce parametric shrinking of clock constraints, which corresponds to tightening the guards. We propose symbolic procedures to decide the existence of (and then compute) parameters under which the shrunk version of a given timed automaton is non-blocking and can time-abstract simulate the exact semantics. We then define an implementation semantics for timed automata with a digital clock and positive reaction times, and show that for shrinkable timed automata both properties are preserved in implementation.

@inproceedings{fsttcs2011-SBM,
  author =              {Sankur, Ocan and Bouyer, Patricia and Markey,
                         Nicolas},
  title =               {Shrinking Timed Automata},
  editor =              {Chakraborty, Supratik and Kumar, Amit},
  booktitle =           {{P}roceedings of the 31st {C}onference on
                         {F}oundations of {S}oftware {T}echnology and
                         {T}heoretical {C}omputer {S}cience ({FSTTCS}'11)},
  acronym =             {{FSTTCS}'11},
  publisher =           {Leibniz-Zentrum f{\"u}r Informatik},
  series =              {Leibniz International Proceedings in Informatics},
  volume =              {13},
  pages =               {90-102},
  year =                {2011},
  month =               dec,
  doi =                 {10.4230/LIPIcs.FSTTCS.2011.90},
  abstract =            {We define and study a new approach to the
                         implementability of timed automata, where the
                         semantics is perturbed by imprecisions and finite
                         frequency of the hardware. In order to circumvent
                         these effects, we introduce \emph{parametric
                         shrinking} of clock constraints, which corresponds
                         to tightening the guards. We propose symbolic
                         procedures to decide the existence of (and then
                         compute) parameters under which the shrunk version
                         of a given timed automaton is non-blocking and can
                         time-abstract simulate the exact semantics. We then
                         define an implementation semantics for timed
                         automata with a digital clock and positive reaction
                         times, and show that for shrinkable timed automata
                         both properties are preserved in implementation.},
}

Résumé

We define and study a new approach to the implementability of timed automata, where the semantics is perturbed by imprecisions and finite frequency of the hardware. In order to circumvent these effects, we introduce parametric shrinking of clock constraints, which corresponds to tightening the guards. We propose symbolic procedures to decide the existence of (and then compute) parameters under which the shrunk version of a given timed automaton is non-blocking and can time-abstract simulate the exact semantics. We then define an implementation semantics for timed automata with a digital clock and positive reaction times, and show that for shrinkable timed automata, non-blockingness and time-abstract simulation are preserved in implementation.

@article{icomp234()-SBM,
  author =              {Sankur, Ocan and Bouyer, Patricia and Markey,
                         Nicolas},
  title =               {Shrinking Timed Automata},
  publisher =           {Elsevier},
  journal =             {Information and Computation},
  volume =              {234},
  pages =               {107-132},
  year =                {2014},
  month =               feb,
  doi =                 {10.1016/j.ic.2014.01.002},
  abstract =            {We define and study a new approach to the
                         implementability of timed automata, where the
                         semantics is perturbed by imprecisions and finite
                         frequency of the hardware. In order to circumvent
                         these effects, we introduce \emph{parametric
                         shrinking} of clock constraints, which corresponds
                         to tightening the guards. We propose symbolic
                         procedures to decide the existence of (and then
                         compute) parameters under which the shrunk version
                         of a given timed automaton is non-blocking and can
                         time-abstract simulate the exact semantics. We then
                         define an implementation semantics for timed
                         automata with a digital clock and positive reaction
                         times, and show that for shrinkable timed automata,
                         non-blockingness and time-abstract simulation are
                         preserved in implementation.},
}

Résumé

We consider the fundamental problem of Büchi acceptance in timed automata in a robust setting. The problem is formalised in terms of controller synthesis: timed automata are equipped with a parametrised game-based semantics that models the possible perturbations of the decisions taken by the controller. We characterise timed automata that are robustly controllable for some parameter, with a simple graph theoretic condition, by showing the equivalence with the existence of an aperiodic lasso that satisfies the winning condition (aperiodicity was defined and used earlier in different contexts to characterise convergence phenomena in timed automata). We then show decidability and PSPACE-completeness of our problem.

@inproceedings{concur2013-SBMR,
  author =              {Sankur, Ocan and Bouyer, Patricia and Markey,
                         Nicolas and Reynier, Pierre-Alain},
  title =               {Robust Controller Synthesis in Timed Automata},
  editor =              {D{'}Argenio, Pedro R. and Melgratt, Hern{\'a}n C.},
  booktitle =           {{P}roceedings of the 24th {I}nternational
                         {C}onference on {C}oncurrency {T}heory
                         ({CONCUR}'13)},
  acronym =             {{CONCUR}'13},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {8052},
  pages =               {546-560},
  year =                {2013},
  month =               aug,
  doi =                 {10.1007/978-3-642-40184-8_38},
  abstract =            {We consider the fundamental problem of B{\"u}chi
                         acceptance in timed automata in a robust setting.
                         The problem is formalised in terms of controller
                         synthesis: timed automata are equipped with a
                         parametrised game-based semantics that models the
                         possible perturbations of the decisions taken by the
                         controller. We characterise timed automata that are
                         robustly controllable for some parameter, with a
                         simple graph theoretic condition, by showing the
                         equivalence with the existence of an aperiodic lasso
                         that satisfies the winning condition (aperiodicity
                         was defined and used earlier in different contexts
                         to characterise convergence phenomena in timed
                         automata). We then show decidability and
                         PSPACE-completeness of our problem.},
}

@article{jacm32(3)-SC,
  author =              {Sistla, A. Prasad and Clarke, Edmund M.},
  title =               {The Complexity of Propositional Linear Temporal
                         Logics},
  publisher =           {ACM Press},
  journal =             {Journal of the~ACM},
  volume =              {32},
  number =              {3},
  pages =               {733-749},
  year =                {1985},
  month =               jul,
  doi =                 {10.1145/3828.3837},
}

@inproceedings{lics2002-SC,
  author =              {Soltys, Michael and Cook, Stephen A.},
  title =               {The Proof Complexity of Linear Algebra},
  booktitle =           {{P}roceedings of the 17th {A}nnual {S}ymposium on
                         {L}ogic in {C}omputer {S}cience ({LICS}'02)},
  acronym =             {{LICS}'02},
  publisher =           {IEEE Comp. Soc. Press},
  pages =               {335-344},
  year =                {2002},
  month =               jul,
}

@article{icont4(2-3)-Sch,
  author =              {Sch{\"u}tzenberger, Marcel-Paul},
  title =               {On the Definition of a Family of Automata},
  publisher =           {Academic Press},
  journal =             {Information and Control},
  volume =              {4},
  number =              {2-3},
  pages =               {245-270},
  year =                {1961},
  month =               sep,
}

@inproceedings{tableaux1998-Sch,
  author =              {Schwendimann, Stefan},
  title =               {A New One-Pass Tableau Calculus for {PLTL}},
  editor =              {de Swart, Harrie C. M.},
  booktitle =           {{P}roceedings of the 7th {I}nternational
                         {C}onference on {A}utomated {R}easoning with
                         {A}nalytic {T}ableaux and {R}elated {M}ethods
                         ({TABLEAUX}'98)},
  acronym =             {{TABLEAUX}'98},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {1397},
  pages =               {277-292},
  year =                {1998},
  month =               may,
}

@phdthesis{hab-schnoebelen,
  author =              {Schnoebelen, {\relax Ph}ilippe},
  title =               {Sp{\'e}cification et V{\'e}rification des
                         Syst{\`e}mes Concurrents},
  year =                {2001},
  month =               oct,
  school =              {Lab.~Sp\'ecification \& V\'erification, ENS Cachan,
                         France},
  type =                {M\'emoire d'habilitation},
}

@article{ipl83(5)-Sch,
  author =              {Schnoebelen, {\relax Ph}ilippe},
  title =               {Verifying Lossy Channel Systems has Nonprimitive
                         Recursive Complexity},
  publisher =           {Elsevier},
  journal =             {Information Processing Letters},
  volume =              {83},
  number =              {5},
  pages =               {251-261},
  year =                {2002},
  month =               sep,
}

@inproceedings{aiml2002-Sch,
  author =              {Schnoebelen, {\relax Ph}ilippe},
  title =               {The Complexity of Temporal Logic Model Checking},
  editor =              {Balbiani, {\relax Ph}ilippe and Suzuki, Nobu-Yuki
                         and Wolter, Frank and Zakharyaschev, Michael},
  booktitle =           {{P}roceedings of the 4th {W}orkshop on {A}dvances in
                         {M}odal {L}ogic ({AIML}'02)},
  acronym =             {{AIML}'02},
  publisher =           {King's College Publications},
  pages =               {481-517},
  year =                {2003},
  confyear =            {2002},
  confmonth =           {9-10},
}

@inproceedings{icalp2003-Sch,
  author =              {Schnoebelen, {\relax Ph}ilippe},
  title =               {Oracle Circuits for Branching-Time Model Checking},
  editor =              {Baeten, Jos C. M. and Lenstra, Jan Karel and Parrow,
                         Joachim and Woeginger, Gerhard J.},
  booktitle =           {{P}roceedings of the 30th {I}nternational
                         {C}olloquium on {A}utomata, {L}anguages and
                         {P}rogramming ({ICALP}'03)},
  acronym =             {{ICALP}'03},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {2719},
  pages =               {790-801},
  year =                {2003},
  month =               jun,
}

@inproceedings{lcmas2003-Sch,
  author =              {Schobbens, Pierre-Yves},
  title =               {Alternating-Time Logic with Imperfect Recall},
  editor =              {van der Hoek, Wiebe and Lomuscio, Alessio and de
                         Vink, Erik and Wooldridge, Michael},
  booktitle =           {{P}roceedings of the {W}orkshop on Logic and
                         Communication in Multi-Agent Systems ({LCMAS}'03)},
  acronym =             {{LCMAS}'03},
  publisher =           {Elsevier},
  series =              {Electronic Notes in Theoretical Computer Science},
  volume =              {85(2)},
  pages =               {82-93},
  year =                {2004},
  month =               apr,
  confyear =            {2003},
  confmonth =           {6},
  doi =                 {10.1016/S1571-0661(05)82604-0},
}

@inproceedings{icalp2008-Sch,
  author =              {Schewe, Sven},
  title =               {{ATL}{\(^*\)} Satisfiability Is 2{EXPTIME}-Complete},
  editor =              {Aceto, Luca and Damg{\aa}rd, Ivan and Goldberg,
                         Leslie Ann and Halld{\'o}rsson, Magn{\'u}s M. and
                         Ing{\'o}lfsd{\'o}ttir, Anna and Walukiewicz, Igor},
  booktitle =           {{P}roceedings of the 35th {I}nternational
                         {C}olloquium on {A}utomata, {L}anguages and
                         {P}rogramming ({ICALP}'08)~-- Part~{II}},
  acronym =             {{ICALP}'08},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {5126},
  pages =               {373-385},
  year =                {2008},
  month =               jul,
}

@phdthesis{phd-schewe,
  author =              {Schewe, Sven},
  title =               {Synthesis of Distributed Systems},
  year =                {2008},
  month =               jul,
  school =              {Saarland University, Germany},
}

@techreport{arxiv-cs.CC/1312.5686,
  author =              {Schmitz, Sylvain},
  title =               {Complexity Hierarchies Beyond Elementary},
  number =              {cs.CC/1312.5686},
  year =                {2013},
  month =               dec,
  institution =         {arXiv},
  type =                {Research Report},
}

@article{toct8(1)-Sch,
  author =              {Schmitz, Sylvain},
  title =               {Complexity Hierarchies Beyond Elementary},
  publisher =           {ACM Press},
  journal =             {ACM Transactions on Computation Theory},
  volume =              {8},
  number =              {1},
  pages =               {3:1-3:36},
  year =                {2016},
  month =               feb,
  doi =                 {10.1145/2858784},
}

@article{icomp81(3)-SE,
  author =              {Streett, Robert S. and Emerson, E. Allen},
  title =               {An Automata Theoretic Decision Procedure for the
                         Propositional Mu-Calculus},
  publisher =           {Academic Press},
  journal =             {Information and Computation},
  volume =              {81},
  number =              {3},
  pages =               {249-264},
  year =                {1989},
}

@phdthesis{phd-seese,
  author =              {Seese, Detlef G.},
  title =               {Entscheidbarkeits- und {I}nterpretierbarkeitsfragen
                         monadischer {T}heorien zweiter {S}tufe gewisser
                         {K}lassen von {G}raphen},
  year =                {1976},
  school =              {Humboldt-Universit{\"a}t zu Berlin, German
                         Democratic Republic},
}

@article{tcs310(1-3)-ser,
  author =              {Serre, Olivier},
  title =               {Vectorial Languages and Linear Temporal Logic},
  publisher =           {Elsevier},
  journal =             {Theoretical Computer Science},
  volume =              {310},
  number =              {1-3},
  pages =               {79-116},
  year =                {2004},
  month =               jan,
}

@inproceedings{fossacs2006-Ser,
  author =              {Serre, Olivier},
  title =               {Parity games played on transition graphs of
                         one-counter processes},
  editor =              {Aceto, Luca and Ing{\'o}lfsd{\'o}ttir, Anna},
  booktitle =           {{P}roceedings of the 9th {I}nternational
                         {C}onference on {F}oundations of {S}oftware
                         {S}cience and {C}omputation {S}tructure
                         ({FoSSaCS}'06)},
  acronym =             {{FoSSaCS}'06},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {3921},
  pages =               {337-351},
  year =                {2006},
  month =               mar,
  doi =                 {10.1007/11690634_23},
}

@inproceedings{csl2006-SF,
  author =              {Schewe, Sven and Finkbeiner, Bernd},
  title =               {Satisfiability and Finite Model Property for the
                         Alternating-Time {\(\mu\)}-Calculus},
  editor =              {{\'E}sik, Zolt{\'a}n},
  booktitle =           {{P}roceedings of the 20th {I}nternational {W}orkshop
                         on {C}omputer {S}cience {L}ogic ({CSL}'06)},
  acronym =             {{CSL}'06},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {4207},
  pages =               {591-605},
  year =                {2006},
  month =               sep,
}

@inproceedings{lopstr2006-SF,
  author =              {Schewe, Sven and Finkbeiner, Bernd},
  title =               {Synthesis of Asynchronous Systems},
  editor =              {Puebla, Germ{\'a}n},
  booktitle =           {{R}evised {S}elected {P}apers of the 16th
                         {I}nternational {S}ymposium on {L}ogic-{B}ased
                         {P}rogram {S}ynthesis and {T}ransformation
                         ({LOPSTR}'06)},
  acronym =             {{LOPSTR}'06},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {4407},
  pages =               {127-142},
  year =                {2007},
  confyear =            {2006},
  confmonth =           {7},
}

@inproceedings{time2007-SF,
  author =              {Swaminathan, Mani and Fr{\"a}nzle, Martin},
  title =               {A Symbolic Decision Procedure for Robust Safety of
                         Timed Systems},
  booktitle =           {{P}roceedings of the 14th {I}nternational
                         {S}ymposium on {T}emporal {R}epresentation and
                         {R}easoning ({TIME}'07)},
  acronym =             {{TIME}'07},
  publisher =           {IEEE Comp. Soc. Press},
  pages =               {192},
  year =                {2007},
  month =               jun,
}

@inproceedings{ifiptcs2008-SFK,
  author =              {Swaminathan, Mani and Fr{\"a}nzle, Martin and
                         Katoen, Joost-Pieter},
  title =               {The Surprising Robustness of (Closed) Timed Automata
                         against Clock-Drift},
  editor =              {Karhum{\"a}ki, Juhani and Ong, Luke},
  booktitle =           {{P}roceedings of the 5th {IFIP} {I}nternational
                         {C}onference on {T}heoretical {C}omputer {S}cience
                         ({IFIPTCS}'08)},
  acronym =             {{IFIPTCS}'08},
  publisher =           {Springer-Verlag},
  series =              {IFIP Conference Proceedings},
  volume =              {273},
  pages =               {537-553},
  year =                {2008},
  month =               sep,
}

@article{pnas39(10)-Sha,
  author =              {Shapley, Lloyd S.},
  title =               {Stochastic games},
  publisher =           {National Academy of Sciences of the United States of
                         America},
  journal =             {Proceedings of the National Academy of Sciences},
  volume =              {39},
  number =              {10},
  pages =               {1095-1100},
  year =                {1953},
  month =               oct,
  doi =                 {10.1073/pnas.39.10.1095},
}

@article{IBM-JRD3-She,
  author =              {Shepherdson, John C.},
  title =               {The Reduction of Two-Way Automata to One-Way
                         Automata},
  journal =             {IBM Journal of Research and Development},
  volume =              {3},
  number =              {2},
  pages =               {198-200},
  year =                {1959},
  month =               apr,
}

@phdthesis{phd-shirmohammadi,
  author =              {Shirmohammadi, Mahsa},
  title =               {Qualitative analysis of synchronizing probabilistic
                         systems},
  year =                {2014},
  month =               dec,
  school =              {Lab.~Sp\'ecification \& V\'erification, ENS Cachan,
                         France and D{\'e}partement d'Informatique,
                         Universit{\'e} Libre de Bruxelles, Belgium},
  type =                {Th\`ese de doctorat},
}

@article{jalc24(2-4)-Shi,
  author =              {Shitov, Yaroslav},
  title =               {An Improvement to a Recent Upper Bound for
                         Synchronizing Words of Finite Automata},
  journal =             {Journal of Automata, Languages and Combinatorics},
  volume =              {24},
  number =              {2-4},
  pages =               {367-373},
  year =                {2019},
  doi =                 {10.25596/jalc-2019-367},
}

@article{cacm51(8)-Sho,
  author =              {Shoham, Yoav},
  title =               {Computer Science and Game Theory},
  publisher =           {ACM Press},
  journal =             {Communications of the ACM},
  volume =              {51},
  number =              {8},
  pages =               {74-79},
  year =                {2008},
  month =               aug,
  doi =                 {10.1145/1378704.1378721},
}

@phdthesis{phd-sickert,
  author =              {Sickert, Salomon},
  title =               {A~unified translation of Linear Temporal Logic to
                         {\(\omega\)}-automata},
  year =                {2019},
  month =               jul,
  school =              {Technischen Universit{\"a}t M{\"u}nchen, Germany},
}

@article{tcs10(3)-Sip,
  author =              {Sipser, Michael},
  title =               {Halting Space-bounded Computations},
  publisher =           {Elsevier},
  journal =             {Theoretical Computer Science},
  volume =              {10},
  number =              {3},
  pages =               {335-338},
  year =                {1980},
}

@book{Sip97-ITC,
  author =              {Sipser, Michael},
  title =               {Introduction to the theory of computation},
  publisher =           {PWS Publishing Company},
  year =                {1997},
}

@book{Sip06-ITC,
  author =              {Sipser, Michael},
  title =               {Introduction to the theory of computation},
  publisher =           {Thomson Course Technology},
  year =                {2006},
}

@book{Sip13-ITC,
  author =              {Sipser, Michael},
  title =               {Introduction to the theory of computation},
  publisher =           {Cengage Learning},
  year =                {2013},
}

@phdthesis{phd-sistla,
  author =              {Sistla, A. Prasad},
  title =               {Theoretical Issues in the Design and Verification of
                         Distributed Systems},
  year =                {1983},
  school =              {Harvard University},
}

@inproceedings{sofsem2001-SJ,
  author =              {Sawa, Zden{\v{e}}k and Jan{\v c}ar, Petr},
  title =               {{P}-hardness of Equivalence Testing on Finite State
                         Processes},
  editor =              {Pacholski, Leszek and Ruzicka, Peter},
  booktitle =           {{P}roceedings of the 28th {C}onference on {C}urrent
                         {T}rends in {T}heory and {P}ractice of {I}nformatics
                         ({SOFSEM}'01)},
  acronym =             {{SOFSEM}'01},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {2234},
  pages =               {326-335},
  year =                {2001},
  month =               nov,
}

Résumé

We consider the automatic online synthesis of black-box test cases from functional requirements specified as automata for reactive implementations. The goal of the tester is to reach some given state, so as to satisfy a coverage criterion, while monitoring the violation of the requirements. We develop an approach based on Monte Carlo Tree Search, which is a classical technique in reinforcement learning for efficiently selecting promising inputs. Seeing the automata requirements as a game between the implementation and the tester, we develop a heuristic by biasing the search towards inputs that are promising in this game. We experimentally show that our heuristic accelerates the convergence of the Monte Carlo Tree Search algorithm, thus improving the performance of testing.

@techreport{2407.18994-SJMMN,
  author =              {Sankur, Ocan and J{\'e}ron, Thierry and Markey,
                         Nicolas and Mentr{\'e}, David and Noguchi, Reiya},
  title =               {Online Test Synthesis From Requirements: Enhancing
                         Reinforcement Learning with Game Theory},
  number =              {2407-18994},
  year =                {2024},
  month =               jul,
  doi =                 {10.48550/arXiv.2407-18994},
  institution =         {arXiv},
  abstract =            {We consider the automatic online synthesis of
                         black-box test cases from functional requirements
                         specified as automata for reactive implementations.
                         The goal of the tester is to reach some given state,
                         so as to satisfy a coverage criterion, while
                         monitoring the violation of the requirements. We
                         develop an approach based on Monte~Carlo Tree
                         Search, which is a classical technique in
                         reinforcement learning for efficiently selecting
                         promising inputs. Seeing the automata requirements
                         as a game between the implementation and the tester,
                         we develop a heuristic by biasing the search towards
                         inputs that are promising in this game.
                         We~experimentally show that our heuristic
                         accelerates the convergence of the Monte~Carlo Tree
                         Search algorithm, thus improving the performance of
                         testing.},
}

@inproceedings{sbmf2021-SK,
  author =              {Saeedloei, Neda and Klu{\'z}niak, Feliks},
  title =               {Minimization of the Number of Clocks for Timed
                         Scenarios},
  editor =              {Campos, S{\'e}rgio Vale Aguiar and Minea, Marius},
  booktitle =           {{P}roceedings of the24th {B}razilian {S}ymposium on
                         {F}ormal {M}ethods ({SBMF}'21)},
  acronym =             {{SBMF}'21},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {13130},
  pages =               {122-139},
  year =                {2021},
  confmonth =           {12},
  doi =                 {10.1007/978-3-030-92137-8_8},
}

@inproceedings{tacas2006-SKL,
  author =              {Sokolsky, Oleg and Kannan, Sampath and Lee, Insup},
  title =               {Simulation-Based Graph Similarity},
  editor =              {Hermanns, Holger and Palsberg, Jens},
  booktitle =           {{P}roceedings of the 12th {I}nternational
                         {C}onference on {T}ools and {A}lgorithms for
                         {C}onstruction and {A}nalysis of {S}ystems
                         ({TACAS}'06)},
  acronym =             {{TACAS}'06},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {3920},
  pages =               {426-440},
  year =                {2006},
  month =               mar,
}

@inproceedings{express2000-SKS,
  author =              {Shamir, Shoham and Kupferman, Orna and Shamir, Eli},
  title =               {Branching-Depth Hierarchies},
  editor =              {Aceto, Luca and Victor, Bjorn},
  booktitle =           {{P}roceedings of the 7th {I}nternational {W}orkshop
                         on {E}xpressiveness in {C}oncurrency ({EXPRESS}'00)},
  acronym =             {{EXPRESS}'00},
  publisher =           {Elsevier},
  series =              {Electronic Notes in Theoretical Computer Science},
  volume =              {39},
  number =              {1},
  year =                {2003},
  month =               feb,
  confyear =            {2000},
  confmonth =           {8},
}

@article{jigpl13(2)-Sla,
  author =              {Slaney, John K.},
  title =               {Semipositive {LTL} with an Uninterpreted Past
                         Operator},
  publisher =           {Oxford University Press},
  journal =             {Logic Journal of the IGPL},
  volume =              {13},
  number =              {2},
  pages =               {211-229},
  year =                {2005},
  month =               mar,
}

@book{mas-SL09,
  author =              {Shoham, Yoav and Leyton-Brown, Kevin},
  title =               {Multiagent Systems~-- Algorithmic, Game-Theoretic,
                         and Logical Foundations},
  publisher =           {Cambridge University Press},
  year =                {2009},
}

Résumé

Formal methods (e.g. Timed Automata or Linear Hybrid Automata) can be used to analyse a real-time system by performing a reachability analysis on the model. The advantage of using formal methods is that they are more expressive than classical analytic models used in schedulability analysis. For example, it is possible to express state-dependent behaviour, arbitrary activation patterns, etc.

In this paper we use the formalism of Linear Hybrid Automata to encode a hierarchical scheduling system. In particular, we model a dynamic server algorithm and the tasks contained within, abstracting away the rest of the system, thus enabling component-based scheduling analysis. We prove the correctness of the model and the decidability of the reachability analysis for the case of periodic tasks. Then, we compare the results of our model against classical schedulability analysis techniques, showing that our analysis performs better than analytic methods in terms of resource utilisation. We further present two case studies: a component with state-dependent tasks, and a simplified model of a real avionics system. Finally, through extensive tests with various configurations, we demonstrate that this approach is usable for medium size components.

@inproceedings{rtcsa2014-SLSFM,
  author =              {Sun, Youcheng and Lipari, Giuseppe and Soulat,
                         Romain and Fribourg, Laurent and Markey, Nicolas},
  title =               {Component-Based Analysis of Hierarchical Scheduling
                         using Linear Hybrid Automata},
  booktitle =           {{P}roceedings of the 20th {I}nternational
                         {C}onference on {R}eal-{T}ime {C}omputing {S}ystems
                         and {A}pplications ({RTCSA}'14)},
  acronym =             {{RTCSA}'14},
  publisher =           {IEEE Comp. Soc. Press},
  year =                {2014},
  month =               aug,
  doi =                 {10.1109/RTCSA.2014.6910502},
  abstract =            {Formal methods (e.g. Timed Automata or Linear Hybrid
                         Automata) can be used to analyse a real-time system
                         by performing a reachability analysis on the model.
                         The advantage of using formal methods is that they
                         are more expressive than classical analytic models
                         used in schedulability analysis. For example, it is
                         possible to express state-dependent behaviour,
                         arbitrary activation patterns,~etc.\par In this
                         paper we use the formalism of Linear Hybrid Automata
                         to encode a hierarchical scheduling system. In
                         particular, we model a dynamic server algorithm and
                         the tasks contained within, abstracting away the
                         rest of the system, thus enabling component-based
                         scheduling analysis. We prove the correctness of the
                         model and the decidability of the reachability
                         analysis for the case of periodic tasks. Then, we
                         compare the results of our model against classical
                         schedulability analysis techniques, showing that our
                         analysis performs better than analytic methods in
                         terms of resource utilisation. We further present
                         two case studies: a~component with state-dependent
                         tasks, and a simplified model of a real avionics
                         system. Finally, through extensive tests with
                         various configurations, we demonstrate that this
                         approach is usable for medium size components.},
}

@article{tac43(7)-SLT,
  author =              {Sampath, Meera and Lafortune, St{\'e}phane and
                         Teneketzis, Demosthenis},
  title =               {Active diagnosis of discrete-event systems},
  publisher =           {IEEE Comp. Soc. Press},
  journal =             {IEEE Transactions on Automatic Control},
  volume =              {43},
  number =              {7},
  pages =               {908-929},
  year =                {1998},
  month =               jul,
  doi =                 {10.1109/9.701089},
}

@inproceedings{stoc1973-SM,
  author =              {Stockmeyer, Larry J. and Meyer, Albert R.},
  title =               {Word Problems Requiring Exponential Time:
                         Preliminary Report},
  booktitle =           {{P}roceedings of the 5th {A}nnual {ACM} {S}ymposium
                         on the {T}heory of {C}omputing ({STOC}'73)},
  acronym =             {{STOC}'73},
  publisher =           {ACM Press},
  pages =               {1-9},
  year =                {1973},
  month =               apr,
}

@inproceedings{concur2002-Sor,
  author =              {Sorea, Maria},
  title =               {A Decidable Fixpoint Logic for Time-Outs},
  editor =              {Brim, Lubo{\v s} and Jan{\v c}ar, Petr and K{\v
                         r}et{\'\i}nsk{\'y}, Mojm{\'\i}r and Ku{\v c}era,
                         Anton{\'\i}n},
  booktitle =           {{P}roceedings of the 13th {I}nternational
                         {C}onference on {C}oncurrency {T}heory
                         ({CONCUR}'02)},
  acronym =             {{CONCUR}'02},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {2421},
  pages =               {255-271},
  year =                {2002},
  month =               aug,
}

@mastersthesis{sorensen-master14,
  author =              {S{\o}rensen, Mathias Grund},
  title =               {Controller synthesis for home automation},
  year =                {2014},
  school =              {Computer Science Department, Aalborg University,
                         Denmark},
}

@article{mmor71(2)-Spe,
  author =              {Sperber, Heike},
  title =               {How to find {N}ash equilibria with extreme total
                         latency in network congestion games?},
  publisher =           {Springer-Verlag},
  journal =             {Mathematical Methods of Operations Research},
  volume =              {71},
  number =              {2},
  pages =               {245-265},
  year =                {2010},
  month =               apr,
  doi =                 {10.1007/s00186-009-0293-6},
}

@inproceedings{formats2008-SPNM,
  author =              {Suman, P. Vijay and Pandya, Paritosh K. and
                         Narayanan Krishna, Shankara and Manasa, Lakshmi},
  title =               {Timed Automata with Integer Resets: Language
                         Inclusion and Expressiveness},
  editor =              {Cassez, Franck and Jard, Claude},
  booktitle =           {{P}roceedings of the 6th {I}nternational
                         {C}onferences on {F}ormal {M}odelling and {A}nalysis
                         of {T}imed {S}ystems ({FORMATS}'08)},
  acronym =             {{FORMATS}'08},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {5215},
  pages =               {78-92},
  year =                {2008},
  month =               sep,
}

@article{ipl69(5)-SR,
  author =              {Schobbens, Pierre-Yves and Raskin, Jean-Fran{\c
                         c}ois},
  title =               {The Logic of {"}Initially{"} and {"}Next{"}},
  publisher =           {Elsevier},
  journal =             {Information Processing Letters},
  volume =              {69},
  number =              {5},
  pages =               {221-225},
  year =                {1999},
}

@inproceedings{concur2002-Srb,
  author =              {Srba, Ji{\v r}{\'\i}},
  title =               {Undecidability of Weak Bisimulation for Pushdown
                         Processes},
  editor =              {Brim, Lubo{\v s} and Jan{\v c}ar, Petr and K{\v
                         r}et{\'\i}nsk{\'y}, Mojm{\'\i}r and Ku{\v c}era,
                         Anton{\'\i}n},
  booktitle =           {{P}roceedings of the 13th {I}nternational
                         {C}onference on {C}oncurrency {T}heory
                         ({CONCUR}'02)},
  acronym =             {{CONCUR}'02},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {2421},
  pages =               {579-593},
  year =                {2002},
  month =               aug,
}

@article{tcs274(1-2)-SRH,
  author =              {Schobbens, Pierre-Yves and Raskin, Jean-Fran{\c
                         c}ois and Henzinger, Thomas A.},
  title =               {Axioms for Real-Time Logics},
  publisher =           {Elsevier},
  journal =             {Theoretical Computer Science},
  volume =              {274},
  number =              {1-2},
  pages =               {151-182},
  year =                {2002},
  month =               mar,
}

@inproceedings{concur2009-SRS,
  author =              {Singh, Anu and Ramakrishnan, C. R. and Smolka, Scott
                         A.},
  title =               {Query-Based Model Checking of Ad~Hoc Network
                         Protocols},
  editor =              {Bravetti, Mario and Zavattaro, Gianluigi},
  booktitle =           {{P}roceedings of the 20th {I}nternational
                         {C}onference on {C}oncurrency {T}heory
                         ({CONCUR}'09)},
  acronym =             {{CONCUR}'09},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {5710},
  pages =               {603-619},
  year =                {2009},
  month =               sep,
  doi =                 {10.1007/978-3-642-04081-8_40},
}

@inproceedings{stoc1978-SS,
  author =              {Sakoda, William J. and Sipser, Michael},
  title =               {Nondeterminism and the Size of Two Way Finite
                         Automata},
  booktitle =           {{P}roceedings of the 10th {A}nnual {ACM} {S}ymposium
                         on the {T}heory of {C}omputing ({STOC}'78)},
  acronym =             {{STOC}'78},
  publisher =           {ACM Press},
  pages =               {275-286},
  year =                {1978},
  month =               may,
}

@article{jacm29(4)-SS,
  author =              {Storer, James A. and Szymanski, Thomas G.},
  title =               {Data Compression via Textual Substitution},
  publisher =           {ACM Press},
  journal =             {Journal of the~ACM},
  volume =              {29},
  number =              {4},
  pages =               {928-951},
  year =                {1982},
  month =               oct,
}

@inproceedings{express2002-SS,
  author =              {Sassone, Vladimiro and Soboco{\'n}ski, Pawe{\l}},
  title =               {Deriving Bisimulationn Congruences:
                         A~{\(2\)}-Categorical Approach},
  editor =              {Nestmann, Uwe and Panangaden, Prakash},
  booktitle =           {{P}roceedings of the 9th {I}nternational {W}orkshop
                         on {E}xpressiveness in {C}oncurrency ({EXPRESS}'02)},
  acronym =             {{EXPRESS}'02},
  publisher =           {Elsevier},
  series =              {Electronic Notes in Theoretical Computer Science},
  volume =              {68},
  number =              {2},
  pages =               {107-126},
  year =                {2002},
  month =               aug,
}

@article{tac40(9)-SSLST,
  author =              {Sampath, Meera and Sengupta, Raja and Lafortune,
                         St{\'e}phane and Sinnamohideen, Kasim and
                         Teneketzis, Demosthenis},
  title =               {Diagnosability of discrete-event systems},
  publisher =           {IEEE Comp. Soc. Press},
  journal =             {IEEE Transactions on Automatic Control},
  volume =              {40},
  number =              {9},
  pages =               {1555-1575},
  year =                {1995},
  month =               sep,
  doi =                 {10.1109/9.412626},
}

@article{tocst4(2)-SSLST,
  author =              {Sampath, Meera and Sengupta, Raja and Lafortune,
                         St{\'e}phane and Sinnamohideen, Kasim and
                         Teneketzis, Demosthenis},
  title =               {Failure diagnosis using discrete-event models},
  publisher =           {IEEE Comp. Soc. Press},
  journal =             {IEEE Transactions on Computers},
  volume =              {35},
  number =              {1},
  pages =               {105-124},
  year =                {1996},
  month =               jan,
  doi =                 {10.1109/87.486338},
}

@techreport{kyushu-TR195,
  author =              {Sakamoto, Hiroshi and Shimozono, Shinichi and
                         Shinohara, Ayumi and Takeda, Masayuki},
  title =               {On the Minimization Problem of Text Compression
                         Scheme by a Reduced Grammar Transform},
  number =              {195},
  year =                {2001},
  month =               aug,
  institution =         {Department of Informatics, Kyushu University, Japan},
  type =                {Technical Report},
}

@article{jacm32(3)-ST,
  author =              {Sleator, Daniel Dominic and Tarjan, Robert Endre},
  title =               {Self-adjusting binary search trees},
  publisher =           {ACM Press},
  journal =             {Journal of the~ACM},
  volume =              {32},
  number =              {3},
  pages =               {652-686},
  year =                {1985},
  month =               jul,
  doi =                 {10.1145/3828.3835},
}

@inproceedings{charme2003-ST,
  author =              {Sebastiani, Roberto and Tonetta, Stefano},
  title =               {{"}More Deterministic{"} vs. {"}Smaller{"} B{\"u}chi
                         Automata for Efficient {LTL} Model Checking},
  editor =              {Geist, Daniel and Tronci, Enrico},
  booktitle =           {{P}roceedings of the 12th {C}orrect {H}ardware
                         {D}esign and {V}erification {M}ethods ({CHARME}'03)},
  acronym =             {{CHARME}'03},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {2860},
  year =                {2003},
  month =               oct,
}

@inproceedings{tacas2017-ST,
  author =              {Sankur, Ocan and Talpin, Jean-Pierre},
  title =               {An~Abstraction Technique For Parameterized Model
                         Checking of Leader Election Protocols: Application
                         to~{FTSP}},
  editor =              {Legay, Axel and Margaria, Tiziana},
  booktitle =           {{P}roceedings of the 23rd {I}nternational
                         {C}onference on {T}ools and {A}lgorithms for
                         {C}onstruction and {A}nalysis of {S}ystems
                         ({TACAS}'17)~-- {P}art~{I}},
  acronym =             {{TACAS}'17},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {10205},
  year =                {2017},
  month =               apr,
  doi =                 {10.1007/978-3-662-54577-5_2},
}

@phdthesis{phd-stan,
  author =              {Stan, Daniel},
  title =               {Randomized strategies in concurrent games},
  year =                {2017},
  month =               mar,
  school =              {Lab.~Sp\'ecification \& V\'erification, ENS Cachan,
                         France},
  type =                {Th\`ese de doctorat},
}

@inproceedings{concur1995-Sti,
  author =              {Stirling, Colin},
  title =               {Local Model Checking Games (Extended Abstract)},
  editor =              {Lee, Insup and Smolka, Scott A.},
  booktitle =           {{P}roceedings of the 6th {I}nternational
                         {C}onference on {C}oncurrency {T}heory
                         ({CONCUR}'95)},
  acronym =             {{CONCUR}'95},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {962},
  pages =               {1-11},
  year =                {1995},
  month =               aug,
}

@phdthesis{phd-stockmeyer,
  author =              {Stockmeyer, Larry J.},
  title =               {The Complexity of Decision Problems in Automata
                         Theory and Logic},
  year =                {1974},
  school =              {MIT},
}

@article{tcs3(1)-Sto,
  author =              {Stockmeyer, Larry J.},
  title =               {The Polynomial-Time Hierarchy},
  publisher =           {Elsevier},
  journal =             {Theoretical Computer Science},
  volume =              {3},
  number =              {1},
  pages =               {1-22},
  year =                {1976},
}

@article{jsl52(1)-Sto,
  author =              {Stockmeyer, Larry J.},
  title =               {Classifying the Computational Complexity of
                         Problems},
  publisher =           {Association for Symbolic Logic},
  journal =             {Journal of Symbolic Logic},
  volume =              {52},
  number =              {1},
  pages =               {1-43},
  year =                {1987},
  month =               mar,
}

@article{gsab63(11)-Str,
  author =              {Strahler, Arthur N.},
  title =               {Hypsometric (area-altitude) analysis of erosional
                         topography},
  publisher =           {Geological Society of America},
  journal =             {Geological Society of America Bulletin},
  volume =              {63},
  number =              {11},
  pages =               {1117-1142},
  year =                {1952},
  month =               nov,
  doi =                 {10.1130/0016-7606(1952)63[1117:HAAOET]2.0.CO;2},
}

@phdthesis{phd-strejcek,
  author =              {Strej{\v c}ek, Jan},
  title =               {Linear Temporal Logic: Expressiveness and Model
                         Checking},
  year =                {2004},
  school =              {Faculty of Informatics, Masaryk University, Brno,
                         Czech Republic},
}

@article{alga2007-STZ,
  author =              {Suri, Subhash and T{\'o}th, Csaba D. and Zhou,
                         Yunhong},
  title =               {Selfish Load Balancing and Atomic Congestion Games},
  publisher =           {Springer-Verlag},
  journal =             {Algorithmica},
  volume =              {47},
  number =              {1},
  pages =               {79-96},
  year =                {2007},
  month =               jan,
  doi =                 {10.1007/s00453-006-1211-4},
}

@article{sigact-news-33(3)-SU,
  author =              {Schaefer, Marcus and Umans, Christopher},
  title =               {Completeness in the Polynomial-Time hierarchy: A
                         Compendium},
  publisher =           {ACM Press},
  journal =             {SIGACT News},
  volume =              {33},
  number =              {3},
  pages =               {32-49},
  year =                {2002},
  month =               sep,
}

@article{sigact-news33(4)-SU,
  author =              {Schaefer, Marcus and Umans, Christopher},
  title =               {Completeness in the Polynomial-Time hierarchy:
                         Part~II},
  publisher =           {ACM Press},
  journal =             {SIGACT News},
  volume =              {33},
  number =              {4},
  pages =               {22-36},
  year =                {2002},
  month =               dec,
}

@article{sigact-news33(4)-SU,
  author =              {Schaefer, Marcus and Umans, Christopher},
  title =               {Completeness in the Polynomial-Time hierarchy:
                         Part~II},
  publisher =           {ACM Press},
  journal =             {SIGACT News},
  volume =              {33},
  number =              {4},
  pages =               {22-36},
  year =                {2002},
  month =               dec,
}

@article{tcs254(1-2)-SVD,
  author =              {Springintveld, Jan and Vaandrager, Frits and
                         D{'}Argenio, Pedro R.},
  title =               {Testing timed automata},
  publisher =           {Elsevier},
  journal =             {Theoretical Computer Science},
  volume =              {254},
  number =              {1-2},
  pages =               {225-257},
  year =                {2001},
  month =               mar,
  doi =                 {10.1016/S0304-3975(99)00134-6},
}

Résumé

The popularization of geographical position devices (e.g. GPS) creates new opportunities for analyzing behavior of moving objects. However, such analysis are hindered by a lack of semantic information associated to the basic information provided by GPS. Previous works propose semantic enrichment of trajectories. Through the semantic enrichment, we could check which trajectories have a given moving sequence in an application. Often, this sequence is expressed according to the semantic application, using the approach of semantic trajectories proposed in the literature. This trajectory can be represented as a sequence of predicates that holds in some time interval. However, the solutions for querying moving sequence proposed by previous works have a high computational cost. In this paper, we propose an expressive query language to semantic trajectories that allows temporal constraints. To evaluate a query we will use model checking based on timed automata, that can be performed in polynomial time. As this model checking algorithm is not implemented yet, we propose to use UPPAAL tool, that can be more expensive theoretically, but we expected that will be ecient for our approach. In addition, we will present a query example that demonstrates the expressive power of our language. Although in this paper we will focus on semantic trajectories data, our approach is general enough for being applied to other purposes.

@inproceedings{sbbd2012-SVMM,
  author =              {Sim{\~o}es{ }De{~}Sousa, Diego V. and Viana,
                         Henrique and Markey, Nicolas and de Mac{\^e}do, Jose
                         Ant{\^o}nio F.},
  title =               {Querying Trajectories through Model Checking based
                         on Timed Automata},
  editor =              {Casanova, Marco A.},
  booktitle =           {{P}roceedings of the 27th {B}razilian {S}ymposium on
                         {D}atabases ({SBBD}'12)},
  acronym =             {{SBBD}'12},
  publisher =           {Sociedade Brasileira de Computa{\c c}{\~a}o},
  pages =               {33-40},
  year =                {2012},
  month =               oct,
  abstract =            {The popularization of geographical position devices
                         (e.g.~GPS) creates new opportunities for analyzing
                         behavior of moving objects. However, such analysis
                         are hindered by a lack of semantic information
                         associated to the basic information provided by~GPS.
                         Previous works propose semantic enrichment of
                         trajectories. Through the semantic enrichment,
                         we~could check which trajectories have a given
                         moving sequence in an application. Often,
                         this~sequence is expressed according to the semantic
                         application, using the approach of semantic
                         trajectories proposed in the literature.
                         This~trajectory can be represented as a sequence of
                         predicates that holds in some time interval.
                         However, the solutions for querying moving sequence
                         proposed by previous works have a high computational
                         cost. In~this paper, we~propose an expressive query
                         language to semantic trajectories that allows
                         temporal constraints. To~evaluate a query we will
                         use model checking based on timed automata, that can
                         be performed in polynomial time. As~this model
                         checking algorithm is not implemented yet, we
                         propose to use UPPAAL tool, that can be more
                         expensive theoretically, but we expected that will
                         be ecient for our approach. In addition, we will
                         present a query example that demonstrates the
                         expressive power of our language. Although in this
                         paper we will focus on semantic trajectories data,
                         our approach is general enough for being applied to
                         other purposes.},
}

@inproceedings{icalp1985-SVW,
  author =              {Sistla, A. Prasad and Vardi, Moshe Y. and Wolper,
                         Pierre},
  title =               {The Complementation Problem for {B}{\"u}chi
                         Automata, with Applications to Temporal Logic},
  editor =              {Brauer, Wilfried},
  booktitle =           {{P}roceedings of the 12th {I}nternational
                         {C}olloquium on {A}utomata, {L}anguages and
                         {P}rogramming ({ICALP}'85)},
  acronym =             {{ICALP}'85},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {194},
  pages =               {465-474},
  year =                {1985},
  month =               jul,
}

@article{tcs49()-SVW,
  author =              {Sistla, A. Prasad and Vardi, Moshe Y. and Wolper,
                         Pierre},
  title =               {The Complementation Problem for {B}{\"u}chi Automata
                         with Applications to Temporal Logics},
  publisher =           {Elsevier},
  journal =             {Theoretical Computer Science},
  volume =              {49},
  pages =               {217-237},
  year =                {1987},
}

@techreport{arxiv1012.5113-SW,
  author =              {Sloth, Chrstoffer and Wisniewski, Rafael},
  title =               {Timed Game Abstraction of Control Systems},
  number =              {1012.5113},
  year =                {2010},
  month =               dec,
  institution =         {arXiv},
}

@article{nahs7(1)-SW,
  author =              {Sloth, Chrstoffer and Wisniewski, Rafael},
  title =               {Complete abstractions of dynamical systems by timed
                         automata},
  journal =             {Nonlinear Analysis: Hybrid Systems},
  volume =              {7},
  number =              {1},
  pages =               {80-100},
  year =                {2013},
  month =               feb,
  doi =                 {10.1007/s10703-011-0118-0},
}

@inproceedings{qfm2009-SZHV,
  author =              {Schuts, Mathijs and Zhu, Yunshan and Heidarian,
                         Faranak and Vaandrager, Frits},
  title =               {Modelling Clock Synchronization in the Chess g{MAC}
                         {WSN} Protocol},
  editor =              {Andova, Suzana and McIver, Annabelle K. and
                         D{'}Argenio, Pedro R. and Cuijpers, Pieter J. L. and
                         Markovski, Jasen and Morgan, Carroll C. and
                         N{\'u}{\~n}ez, Manuel},
  booktitle =           {{P}roceedings of the 1st {W}orkshop on
                         {Q}uantitative {F}ormal {M}ethods: {T}heory and
                         {A}pplications ({QFM}'09)},
  acronym =             {{QFM}'09},
  series =              {Electronic Proceedings in Theoretical Computer
                         Science},
  volume =              {13},
  pages =               {41-54},
  year =                {2009},
  month =               nov,
}

@inproceedings{stacs2018-Szy,
  author =              {Szyku{\l}a, Marek},
  title =               {Improving the Upper Bound on the Length of the
                         Shortest Reset Word},
  editor =              {Niedermeier, Rolf and Vall{\'e}e, Brigitte},
  booktitle =           {{P}roceedings of the 35th {S}ymposium on
                         {T}heoretical {A}spects of {C}omputer {S}cience
                         ({STACS}'18)},
  acronym =             {{STACS}'18},
  publisher =           {Leibniz-Zentrum f{\"u}r Informatik},
  series =              {Leibniz International Proceedings in Informatics},
  volume =              {96},
  pages =               {56:1-56:13},
  year =                {2018},
  month =               feb,
  doi =                 {10.4230/LIPIcs.STACS.2018.56},
}