S
[Saf89] Shmuel Safra. Complexity of Automata on Infinite Objects. PhD thesis, Weizmann Institute of Science, Rehovot, Israel, March 1989.
@phdthesis{phd-safra,
  author =              {Safra, Shmuel},
  title =               {Complexity of Automata on Infinite Objects},
  year =                {1989},
  month =               mar,
  school =              {Weizmann Institute of Science, Rehovot, Israel},
}
[Saf92] Shmuel Safra. Exponential Determinization for ω-Automata with Strong-Fairness Acceptance Condition. In STOC'92, pages 272-282. ACM Press, 1992.
@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},
}
[San05] Sven Sandberg. Homing and Synchronizing Sequences. In MBTRS'04, Lecture Notes in Computer Science 3472, pages 5-33. Springer-Verlag, 2005.
@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},
}
[San10] Ocan Sankur. Model-checking robuste des automates temporisés via les machines à canaux. Mémoire de master, Lab. Spécification & Vérification, ENS Cachan, France, 2010.
@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},
}
[San13] Ocan Sankur. Robustness in Timed Automata: Analysis, Synthesis, Implementation. Thèse de doctorat, Lab. Spécification & Vérification, ENS Cachan, France, May 2013.
@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},
}
[San15] Ocan Sankur. Symbolic Quantitative Robustness Analysis of Timed Automata. In TACAS'15, Lecture Notes in Computer Science 9035, pages 484-498. Springer-Verlag, April 2015.
@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},
}
[Sar93] Ramnath Sarnath. Doubly Logarithmic Time Parallel Sorting. Technical Report 93-01, suny, January 1993.
@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},
}
[Saw03] Zdeněk Sawa. Equivalence Checking of Non-flat Systems is EXPTIME-hard. In CONCUR'03, Lecture Notes in Computer Science 2761, pages 237-250. Springer-Verlag, August 2003.
@inproceedings{concur2003-Saw,
  author =              {Sawa, Zden{{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,
}
[SB00] Fabio Somenzi and Roderick Bloem. Efficient Büchi Automata from LTL Formulae. In CAV'00, Lecture Notes in Computer Science 1855, pages 248-263. Springer-Verlag, July 2000.
@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,
}
[SB11] Fabio Somenzi and Steven Bradley. IC3: where monolithic and incremental meet. In FMCAD'11, pages 3-8. October 2011.
@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,
}
[SBM11] Ocan Sankur, Patricia Bouyer, and Nicolas Markey. Shrinking Timed Automata. In FSTTCS'11, Leibniz International Proceedings in Informatics 13, pages 90-102. Leibniz-Zentrum für Informatik, December 2011.
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 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.},
}
[SBM14] Ocan Sankur, Patricia Bouyer, and Nicolas Markey. Shrinking Timed Automata. Information and Computation 234:107-132. Elsevier, February 2014.
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 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.},
}
[SBM+13] Ocan Sankur, Patricia Bouyer, Nicolas Markey, and Pierre-Alain Reynier. Robust Controller Synthesis in Timed Automata. In CONCUR'13, Lecture Notes in Computer Science 8052, pages 546-560. Springer-Verlag, August 2013.
Abstract

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.},
}
[SC85] A. Prasad Sistla and Edmund M. Clarke. The Complexity of Propositional Linear Temporal Logics. Journal of the ACM 32(3):733-749. ACM Press, July 1985.
@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,
}
[SC02] Michael Soltys and Stephen A. Cook. The Proof Complexity of Linear Algebra. In LICS'02, pages 335-344. IEEE Comp. Soc. Press, July 2002.
@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,
}
[Sch61] Marcel-Paul Schützenberger. On the Definition of a Family of Automata. Information and Control 4(2-3):245-270. Academic Press, September 1961.
@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,
}
[Sch98] Stefan Schwendimann. A New One-Pass Tableau Calculus for PLTL. In TABLEAUX'98, Lecture Notes in Computer Science 1397, pages 277-292. Springer-Verlag, May 1998.
@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,
}
[Sch01] Philippe Schnoebelen. Spécification et Vérification des Systèmes Concurrents. Mémoire d'habilitation, Lab. Spécification & Vérification, ENS Cachan, France, October 2001.
@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},
}
[Sch02] Philippe Schnoebelen. Verifying Lossy Channel Systems has Nonprimitive Recursive Complexity. Information Processing Letters 83(5):251-261. Elsevier, September 2002.
@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,
}
[Sch03] Philippe Schnoebelen. The Complexity of Temporal Logic Model Checking. In AIML'02, pages 481-517. King's College Publications, 2003.
@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},
}
[Sch03] Philippe Schnoebelen. Oracle Circuits for Branching-Time Model Checking. In ICALP'03, Lecture Notes in Computer Science 2719, pages 790-801. Springer-Verlag, June 2003.
@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,
}
[Sch04] Pierre-Yves Schobbens. Alternating-Time Logic with Imperfect Recall. In LCMAS'03, Electronic Notes in Theoretical Computer Science 85(2), pages 82-93. Elsevier, April 2004.
@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},
}
[Sch08] Sven Schewe. ATL* Satisfiability Is 2EXPTIME-Complete. In ICALP'08, Lecture Notes in Computer Science 5126, pages 373-385. Springer-Verlag, July 2008.
@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,
}
[Sch08] Sven Schewe. Synthesis of Distributed Systems. PhD thesis, Saarland University, Germany, July 2008.
@phdthesis{phd-schewe,
  author =              {Schewe, Sven},
  title =               {Synthesis of Distributed Systems},
  year =                {2008},
  month =               jul,
  school =              {Saarland University, Germany},
}
[Sch13] Sylvain Schmitz. Complexity Hierarchies Beyond Elementary. Research Report cs.CC/1312.5686, arXiv, December 2013.
@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},
}
[Sch16] Sylvain Schmitz. Complexity Hierarchies Beyond Elementary. ACM Transactions on Computation Theory 8(1):3:1-3:36. ACM Press, February 2016.
@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},
}
[SE89] Robert S. Streett and E. Allen Emerson. An Automata Theoretic Decision Procedure for the Propositional Mu-Calculus. Information and Computation 81(3):249-264. Academic Press, 1989.
@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},
}
[See76] Detlef G. Seese. Entscheidbarkeits- und Interpretierbarkeitsfragen monadischer Theorien zweiter Stufe gewisser Klassen von Graphen. PhD thesis, Humboldt-Universität zu Berlin, German Democratic Republic, 1976.
@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},
}
[Ser04] Olivier Serre. Vectorial Languages and Linear Temporal Logic. Theoretical Computer Science 310(1-3):79-116. Elsevier, January 2004.
@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,
}
[Ser06] Olivier Serre. Parity games played on transition graphs of one-counter processes. In FoSSaCS'06, Lecture Notes in Computer Science 3921, pages 337-351. Springer-Verlag, March 2006.
@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},
}
[SF06] Sven Schewe and Bernd Finkbeiner. Satisfiability and Finite Model Property for the Alternating-Time μ-Calculus. In CSL'06, Lecture Notes in Computer Science 4207, pages 591-605. Springer-Verlag, September 2006.
@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,
}
[SF07] Sven Schewe and Bernd Finkbeiner. Synthesis of Asynchronous Systems. In LOPSTR'06, Lecture Notes in Computer Science 4407, pages 127-142. Springer-Verlag, 2007.
@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},
}
[SF07] Mani Swaminathan and Martin Fränzle. A Symbolic Decision Procedure for Robust Safety of Timed Systems. In TIME'07, pages 192. IEEE Comp. Soc. Press, June 2007.
@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,
}
[SFK08] Mani Swaminathan, Martin Fränzle, and Joost-Pieter Katoen. The Surprising Robustness of (Closed) Timed Automata against Clock-Drift. In IFIPTCS'08, IFIP Conference Proceedings 273, pages 537-553. Springer-Verlag, September 2008.
@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,
}
[She59] John C. Shepherdson. The Reduction of Two-Way Automata to One-Way Automata. IBM Journal of Research and Development 3:198-200. April 1959.
@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},
  pages =               {198-200},
  year =                {1959},
  month =               apr,
}
[Sho08] Yoav Shoham. Computer Science and Game Theory. Communications of the ACM 51(8):74-79. ACM Press, August 2008.
@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},
}
[Sip80] Michael Sipser. Halting Space-bounded Computations. Theoretical Computer Science 10(3):335-338. Elsevier, 1980.
@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},
}
[Sip97] Michael Sipser. Introduction to the theory of computation. PWS Publishing Company, 1997.
@book{Sip97-ITC,
  author =              {Sipser, Michael},
  title =               {Introduction to the theory of computation},
  publisher =           {PWS Publishing Company},
  year =                {1997},
}
[Sip06] Michael Sipser. Introduction to the theory of computation. Thomson Course Technology, 2006.
@book{Sip06-ITC,
  author =              {Sipser, Michael},
  title =               {Introduction to the theory of computation},
  publisher =           {Thomson Course Technology},
  year =                {2006},
}
[Sis83] A. Prasad Sistla. Theoretical Issues in the Design and Verification of Distributed Systems. PhD thesis, Harvard University, 1983.
@phdthesis{phd-sistla,
  author =              {Sistla, A. Prasad},
  title =               {Theoretical Issues in the Design and Verification of
                         Distributed Systems},
  year =                {1983},
  school =              {Harvard University},
}
[SJ01] Zdeněk Sawa and Petr Jančar. P-hardness of Equivalence Testing on Finite State Processes. In SOFSEM'01, Lecture Notes in Computer Science 2234, pages 326-335. Springer-Verlag, November 2001.
@inproceedings{sofsem2001-SJ,
  author =              {Sawa, Zden{{e}}k and Jan{ 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,
}
[SKL06] Oleg Sokolsky, Sampath Kannan, and Insup Lee. Simulation-Based Graph Similarity. In TACAS'06, Lecture Notes in Computer Science 3920, pages 426-440. Springer-Verlag, March 2006.
@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,
}
[SKS03] Shoham Shamir, Orna Kupferman, and Eli Shamir. Branching-Depth Hierarchies. In EXPRESS'00, Electronic Notes in Theoretical Computer Science 39(1). Elsevier, February 2003.
@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},
}
[Sla05] John K. Slaney. Semipositive LTL with an Uninterpreted Past Operator. Logic Journal of the IGPL 13(2):211-229. Oxford University Press, March 2005.
@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,
}
[SLB09] Yoav Shoham and Kevin Leyton-Brown. Multiagent Systems – Algorithmic, Game-Theoretic, and Logical Foundations. Cambridge University Press, 2009.
@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},
}
[SLS+14] Youcheng Sun, Giuseppe Lipari, Romain Soulat, Laurent Fribourg, and Nicolas Markey. Component-Based Analysis of Hierarchical Scheduling using Linear Hybrid Automata. In RTCSA'14. IEEE Comp. Soc. Press, August 2014.
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.

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.},
}
[SLT98] Meera Sampath, Stéphane Lafortune, and Demosthenis Teneketzis. Active diagnosis of discrete-event systems. IEEE Transactions on Automatic Control 43(7):908-929. IEEE Comp. Soc. Press, July 1998.
@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},
}
[SM73] Larry J. Stockmeyer and Albert R. Meyer. Word Problems Requiring Exponential Time: Preliminary Report. In STOC'73, pages 1-9. ACM Press, April 1973.
@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,
}
[Sor02] Maria Sorea. A Decidable Fixpoint Logic for Time-Outs. In CONCUR'02, Lecture Notes in Computer Science 2421, pages 255-271. Springer-Verlag, August 2002.
@inproceedings{concur2002-Sor,
  author =              {Sorea, Maria},
  title =               {A Decidable Fixpoint Logic for Time-Outs},
  editor =              {Brim, Lubo{ s} and Jan{ c}ar, Petr and K{
                         r}et{\'\i}nsk{\'y}, Mojm{\'\i}r and Ku{ 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,
}
[SPN+08] P. Vijay Suman, Paritosh K. Pandya, Shankara Narayanan Krishna, and Lakshmi Manasa. Timed Automata with Integer Resets: Language Inclusion and Expressiveness. In FORMATS'08, Lecture Notes in Computer Science 5215, pages 78-92. Springer-Verlag, September 2008.
@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,
}
[SR99] Pierre-Yves Schobbens and Jean-François Raskin. The Logic of "Initially" and "Next". Information Processing Letters 69(5):221-225. Elsevier, 1999.
@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},
}
[Srb02] Jiří Srba. Undecidability of Weak Bisimulation for Pushdown Processes. In CONCUR'02, Lecture Notes in Computer Science 2421, pages 579-593. Springer-Verlag, August 2002.
@inproceedings{concur2002-Srb,
  author =              {Srba, Ji{ r}{\'\i}},
  title =               {Undecidability of Weak Bisimulation for Pushdown
                         Processes},
  editor =              {Brim, Lubo{ s} and Jan{ c}ar, Petr and K{
                         r}et{\'\i}nsk{\'y}, Mojm{\'\i}r and Ku{ 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,
}
[SRH02] Pierre-Yves Schobbens, Jean-François Raskin, and Thomas A. Henzinger. Axioms for Real-Time Logics. Theoretical Computer Science 274(1-2):151-182. Elsevier, March 2002.
@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,
}
[SRS09] Anu Singh, C. R. Ramakrishnan, and Scott A. Smolka. Query-Based Model Checking of Ad Hoc Network Protocols. In CONCUR'09, Lecture Notes in Computer Science 5710, pages 603-619. Springer-Verlag, September 2009.
@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},
}
[SS78] William J. Sakoda and Michael Sipser. Nondeterminism and the Size of Two Way Finite Automata. In STOC'78, pages 275-286. ACM Press, May 1978.
@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,
}
[SS82] James A. Storer and Thomas G. Szymanski. Data Compression via Textual Substitution. Journal of the ACM 29(4):928-951. ACM Press, October 1982.
@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,
}
[SS02] Vladimiro Sassone and Paweł Sobocoński. Deriving Bisimulationn Congruences: A 2-Categorical Approach. In EXPRESS'02, Electronic Notes in Theoretical Computer Science 68(2), pages 107-126. Elsevier, August 2002.
@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,
}
[SSL+95] Meera Sampath, Raja Sengupta, Stéphane Lafortune, Kasim Sinnamohideen, and Demosthenis Teneketzis. Diagnosability of discrete-event systems. IEEE Transactions on Automatic Control 40(9):1555-1575. IEEE Comp. Soc. Press, September 1995.
@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},
}
[SSL+96] Meera Sampath, Raja Sengupta, Stéphane Lafortune, Kasim Sinnamohideen, and Demosthenis Teneketzis. Failure diagnosis using discrete-event models. IEEE Transactions on Computers 35(1):105-124. IEEE Comp. Soc. Press, January 1996.
@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},
}
[SSS+01] Hiroshi Sakamoto, Shinichi Shimozono, Ayumi Shinohara, and Masayuki Takeda. On the Minimization Problem of Text Compression Scheme by a Reduced Grammar Transform. Technical Report 195, Department of Informatics, Kyushu University, Japan, August 2001.
@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},
}
[ST03] Roberto Sebastiani and Stefano Tonetta. "More Deterministic" vs. "Smaller" Büchi Automata for Efficient LTL Model Checking. In CHARME'03, Lecture Notes in Computer Science 2860. Springer-Verlag, October 2003.
@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,
}
[ST17] Ocan Sankur and Jean-Pierre Talpin. An Abstraction Technique For Parameterized Model Checking of Leader Election Protocols: Application to FTSP. In TACAS'17, Lecture Notes in Computer Science 10205. Springer-Verlag, April 2017.
@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},
}
[Sta17] Daniel Stan. Randomized strategies in concurrent games. Thèse de doctorat, Lab. Spécification & Vérification, ENS Cachan, France, March 2017.
@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},
}
[Sti95] Colin Stirling. Local Model Checking Games (Extended Abstract). In CONCUR'95, Lecture Notes in Computer Science 962, pages 1-11. Springer-Verlag, August 1995.
@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,
}
[Sto74] Larry J. Stockmeyer. The Complexity of Decision Problems in Automata Theory and Logic. PhD thesis, MIT, 1974.
@phdthesis{phd-stockmeyer,
  author =              {Stockmeyer, Larry J.},
  title =               {The Complexity of Decision Problems in Automata
                         Theory and Logic},
  year =                {1974},
  school =              {MIT},
}
[Sto76] Larry J. Stockmeyer. The Polynomial-Time Hierarchy. Theoretical Computer Science 3(1):1-22. Elsevier, 1976.
@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},
}
[Sto87] Larry J. Stockmeyer. Classifying the Computational Complexity of Problems. Journal of Symbolic Logic 52(1):1-43. Association for Symbolic Logic, March 1987.
@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,
}
[Str52] Arthur N. Strahler. Hypsometric (area-altitude) analysis of erosional topography. Geological Society of America Bulletin 63(11):1117-1142. Geological Society of America, November 1952.
@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},
}
[Str04] Jan Strejček. Linear Temporal Logic: Expressiveness and Model Checking. PhD thesis, Faculty of Informatics, Masaryk University, Brno, Czech Republic, 2004.
@phdthesis{phd-strejcek,
  author =              {Strej{ c}ek, Jan},
  title =               {Linear Temporal Logic: Expressiveness and Model
                         Checking},
  year =                {2004},
  school =              {Faculty of Informatics, Masaryk University, Brno,
                         Czech Republic},
}
[SU02] Marcus Schaefer and Christopher Umans. Completeness in the Polynomial-Time hierarchy: A Compendium. SIGACT News 33(3):32-49. ACM Press, September 2002.
@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,
}
[SU02] Marcus Schaefer and Christopher Umans. Completeness in the Polynomial-Time hierarchy: Part II. SIGACT News 33(4):22-36. ACM Press, December 2002.
@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,
}
[SVD01] Jan Springintveld, Frits Vaandrager, and Pedro R. D'Argenio. Testing timed automata. Theoretical Computer Science 254(1-2):225-257. Elsevier, March 2001.
@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},
}
[SVM+12] Diego V. Simões De Sousa, Henrique Viana, Nicolas Markey, and Jose Antônio F. de Macêdo. Querying Trajectories through Model Checking based on Timed Automata. In SBBD'12, pages 33-40. Sociedade Brasileira de Computação, October 2012.
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{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.},
}
[SVW85] A. Prasad Sistla, Moshe Y. Vardi, and Pierre Wolper. The Complementation Problem for Büchi Automata, with Applications to Temporal Logic. In ICALP'85, Lecture Notes in Computer Science 194, pages 465-474. Springer-Verlag, July 1985.
@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,
}
[SVW87] A. Prasad Sistla, Moshe Y. Vardi, and Pierre Wolper. The Complementation Problem for Büchi Automata with Applications to Temporal Logics. Theoretical Computer Science 49:217-237. Elsevier, 1987.
@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},
}
[SW10] Chrstoffer Sloth and Rafael Wisniewski. Timed Game Abstraction of Control Systems. Technical Report 1012.5113, arXiv, December 2010.
@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},
}
[SW13] Chrstoffer Sloth and Rafael Wisniewski. Complete abstractions of dynamical systems by timed automata. Nonlinear Analysis: Hybrid Systems 7(1):80-100. February 2013.
@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},
}
[SZH+09] Mathijs Schuts, Yunshan Zhu, Faranak Heidarian, and Frits Vaandrager. Modelling Clock Synchronization in the Chess gMAC WSN Protocol. In QFM'09, Electronic Proceedings in Theoretical Computer Science 13, pages 41-54. November 2009.
@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,
}