2012
[BMO+12] Patricia Bouyer, Nicolas Markey, Joël Ouaknine, Philippe Schnoebelen, and James Worrell. On Termination and Invariance for Faulty Channel Systems. Formal Aspects of Computing 24(4-6):595-607. Springer-Verlag, July 2012.
Abstract

A channel machine consists of a finite controller together with several fifo channels; the controller can read messages from the head of a channel and write messages to the tail of a channel. In this paper we focus on channel machines with insertion errors, i.e., machines in whose channels messages can spontaneously appear. We consider the invariance problem: does a given insertion channel machine have an infinite computation all of whose configurations satisfy a given predicate? We show that this problem is primitive-recursive if the predicate is closed under message losses. We also give a non-elementary lower bound for the invariance problem under this restriction. Finally, using the previous result, we show that the satisfiability problem for the safety fragment of Metric Temporal Logic is non-elementary.

@article{fac24(4-6)-BMOSW,
  author =              {Bouyer, Patricia and Markey, Nicolas and Ouaknine,
                         Jo{\"e}l and Schnoebelen, {\relax Ph}ilippe and
                         Worrell, James},
  title =               {On Termination and Invariance for Faulty Channel
                         Systems},
  publisher =           {Springer-Verlag},
  journal =             {Formal Aspects of Computing},
  volume =              {24},
  number =              {4-6},
  pages =               {595-607},
  year =                {2012},
  month =               jul,
  doi =                 {10.1007/s00165-012-0234-7},
  abstract =            {A~\emph{channel machine} consists of a finite
                         controller together with several fifo channels; the
                         controller can read messages from the head of a
                         channel and write messages to the tail of a channel.
                         In this paper we focus on channel machines with
                         \emph{insertion errors}, i.e., machines in whose
                         channels messages can spontaneously appear. We
                         consider the invariance problem: does a given
                         insertion channel machine have an infinite
                         computation all of whose configurations satisfy a
                         given predicate? We show that this problem is
                         primitive-recursive if the predicate is closed under
                         message losses. We also give a non-elementary lower
                         bound for the invariance problem under this
                         restriction. Finally, using the previous result, we
                         show that the satisfiability problem for the safety
                         fragment of Metric Temporal Logic is
                         non-elementary.},
}
[BBM+12] Patricia Bouyer, Romain Brenguier, Nicolas Markey, and Michael Ummels. Concurrent games with ordered objectives. In FoSSaCS'12, Lecture Notes in Computer Science 7213, pages 301-315. Springer-Verlag, March 2012.
Abstract

We consider concurrent games played on graphs, in which each player has several qualitative (e.g. reachability or Büchi) objectives, and a preorder on these objectives (for instance the counting order, where the aim is to maximise the number of objectives that are fulfilled).

We study two fundamental problems in that setting: (1) the value problem, which aims at deciding the existence of a strategy that ensures a given payoff; (2) the Nash equilibrium problem, where we want to decide the existence of a Nash equilibrium (possibly with a condition on the payoffs). We characterise the exact complexities of these problems for several relevant preorders, and several kinds of objectives.

@inproceedings{fossacs2012-BBMU,
  author =              {Bouyer, Patricia and Brenguier, Romain and Markey,
                         Nicolas and Ummels, Michael},
  title =               {Concurrent games with ordered objectives},
  editor =              {Birkedal, Lars},
  booktitle =           {{P}roceedings of the 15th {I}nternational
                         {C}onference on {F}oundations of {S}oftware
                         {S}cience and {C}omputation {S}tructure
                         ({FoSSaCS}'12)},
  acronym =             {{FoSSaCS}'12},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {7213},
  pages =               {301-315},
  year =                {2012},
  month =               mar,
  doi =                 {10.1007/978-3-642-28729-9_20},
  abstract =            {We consider concurrent games played on graphs, in
                         which each player has several qualitative (e.g.
                         reachability or B{\"u}chi) objectives, and a
                         preorder on these objectives (for instance the
                         counting order, where the aim is to maximise the
                         number of objectives that are fulfilled).\par We
                         study two fundamental problems in that setting:
                         (1)~the \emph{value problem}, which aims at deciding
                         the existence of a strategy that ensures a given
                         payoff; (2)~the \emph{Nash equilibrium problem},
                         where we want to decide the existence of a Nash
                         equilibrium (possibly with a condition on the
                         payoffs). We characterise the exact complexities of
                         these problems for several relevant preorders, and
                         several kinds of objectives.},
}
[BLM12] Patricia Bouyer, Kim Guldstrand Larsen, and Nicolas Markey. Lower-Bound Constrained Runs in Weighted Timed Automata. In QEST'12, pages 128-137. IEEE Comp. Soc. Press, September 2012.
Abstract

We investigate a number of problems related to infinite runs of weighted timed automata, subject to lower-bound constraints on the accumulated weight. Closing an open problem from [Bouyer et al., "Infinite runs in weighted timed automata with energy constraints", FORMATS'08], we show that the existence of an infinite lower-bound-constrained run is—for us somewhat unexpectedly—undecidable for weighted timed automata with four or more clocks.

This undecidability result assumes a fixed and know initial credit. We show that the related problem of existence of an initial credit for which there ex- ist a feasible run is decidable in PSPACE. We also investigate the variant of these problems where only bounded-duration runs are considered, showing that this restriction makes our original problem decidable in NEXPTIME. Finally, we prove that the universal versions of all those problems (i.e, checking that all the considered runs satisfy the lower-bound constraint) are decidable in PSPACE.

@inproceedings{qest2012-BLM,
  author =              {Bouyer, Patricia and Larsen, Kim Guldstrand and
                         Markey, Nicolas},
  title =               {Lower-Bound Constrained Runs in Weighted Timed
                         Automata},
  booktitle =           {{P}roceedings of the 9th {I}nternational
                         {C}onference on {Q}uantitative {E}valuation of
                         {S}ystems ({QEST}'12)},
  acronym =             {{QEST}'12},
  publisher =           {IEEE Comp. Soc. Press},
  pages =               {128-137},
  year =                {2012},
  month =               sep,
  doi =                 {10.1109/QEST.2012.28},
  abstract =            {We investigate a number of problems related to
                         infinite runs of weighted timed automata, subject to
                         lower-bound constraints on the accumulated weight.
                         Closing an open problem from [Bouyer
                         \textit{et~al.}, {"}Infinite runs in weighted timed
                         automata with energy constraints{"}, FORMATS'08], we
                         show that the existence of an infinite
                         lower-bound-constrained run is---for us somewhat
                         unexpectedly---undecidable for weighted timed
                         automata with four or more clocks.\par This
                         undecidability result assumes a fixed and know
                         initial credit. We show that the related problem of
                         existence of an initial credit for which there ex-
                         ist a feasible run is decidable in PSPACE. We also
                         investigate the variant of these problems where only
                         bounded-duration runs are considered, showing that
                         this restriction makes our original problem
                         decidable in NEXPTIME. Finally, we prove that the
                         universal versions of all those problems (i.e,
                         checking that all the considered runs satisfy the
                         lower-bound constraint) are decidable in PSPACE.},
}
[BMS12] Patricia Bouyer, Nicolas Markey, and Ocan Sankur. Robust reachability in timed automata: a game-based approach. In ICALP'12, Lecture Notes in Computer Science 7392, pages 128-140. Springer-Verlag, July 2012.
Abstract

Reachability checking is one of the most basic problems in verification. By solving this problem, one synthesizes a strategy that dictates the actions to be performed for ensuring that the target location is reached. In this work, we are interested in synthesizing "robust" strategies for ensuring reachability of a location in a timed automaton; with "robust", we mean that it must still ensure reachability even when the delays are perturbed by the environment. We model this perturbed semantics as a game between the controller and its environment, and solve the parameterized robust reachability problem: we show that the existence of an upper bound on the perturbations under which there is a strategy reaching a target location is EXPTIME-complete.

@inproceedings{icalp2012-BMS,
  author =              {Bouyer, Patricia and Markey, Nicolas and Sankur,
                         Ocan},
  title =               {Robust reachability in timed automata: a~game-based
                         approach},
  editor =              {Czumaj, Artur and Mehlhorn, Kurt and Pitts, Andrew
                         and Wattenhofer, Roger},
  booktitle =           {{P}roceedings of the 39th {I}nternational
                         {C}olloquium on {A}utomata, {L}anguages and
                         {P}rogramming ({ICALP}'12)~-- Part~{II}},
  acronym =             {{ICALP}'12},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {7392},
  pages =               {128-140},
  year =                {2012},
  month =               jul,
  doi =                 {10.1007/978-3-642-31585-5_15},
  abstract =            {Reachability checking is one of the most basic
                         problems in verification. By solving this problem,
                         one synthesizes a strategy that dictates the actions
                         to be performed for ensuring that the target
                         location is reached. In this work, we are interested
                         in synthesizing {"}robust{"} strategies for ensuring
                         reachability of a location in a timed automaton;
                         with {"}robust{"}, we mean that it must still ensure
                         reachability even when the delays are perturbed by
                         the environment. We model this perturbed semantics
                         as a game between the controller and its
                         environment, and solve the parameterized robust
                         reachability problem: we show that the existence of
                         an upper bound on the perturbations under which
                         there is a strategy reaching a target location is
                         EXPTIME-complete.},
}
[DLM12] Arnaud Da Costa, François Laroussinie, and Nicolas Markey. Quantified CTL: Expressiveness and Model Checking. In CONCUR'12, Lecture Notes in Computer Science 7454, pages 177-192. Springer-Verlag, September 2012.
Abstract

While it was defined long ago, the extension of CTL with quantification over atomic propositions has never been studied extensively. Considering two different semantics (depending whether propositional quantification refers to the Kripke structure or to its unwinding tree), we study its expressiveness (showing in particular that QCTL coincides with Monadic Second-Order Logic for both semantics) and characterize the complexity of its model-checking problem, depending on the number of nested propositional quantifiers (showing that the structure semantics populates the polynomial hierarchy while the tree semantics populates the exponential hierarchy). We also show how these results apply to model checking ATL-like temporal logics for games.

@inproceedings{concur2012-DLM,
  author =              {Da{~}Costa, Arnaud and Laroussinie, Fran{\c c}ois
                         and Markey, Nicolas},
  title =               {Quantified~{CTL}: Expressiveness and Model Checking},
  editor =              {Koutny, Maciej and Ulidowski, Irek},
  booktitle =           {{P}roceedings of the 23rd {I}nternational
                         {C}onference on {C}oncurrency {T}heory
                         ({CONCUR}'12)},
  acronym =             {{CONCUR}'12},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {7454},
  pages =               {177-192},
  year =                {2012},
  month =               sep,
  doi =                 {10.1007/978-3-642-32940-1_14},
  abstract =            {While it was defined long ago, the extension of CTL
                         with quantification over atomic propositions has
                         never been studied extensively. Considering two
                         different semantics (depending whether propositional
                         quantification refers to the Kripke structure or to
                         its unwinding tree), we study its expressiveness
                         (showing in particular that QCTL coincides with
                         Monadic Second-Order Logic for both semantics) and
                         characterize the complexity of its model-checking
                         problem, depending on the number of nested
                         propositional quantifiers (showing that the
                         structure semantics populates the polynomial
                         hierarchy while the tree semantics populates the
                         exponential hierarchy). We also show how these
                         results apply to model checking ATL-like temporal
                         logics for games.},
}
[BBD+12] Thomas Brihaye, Véronique Bruyère, Julie De Pril, and Hugo Gimbert. Subgame Perfection for Equilibria in Quantitative Reachability Games. In FoSSaCS'12, Lecture Notes in Computer Science 7213, pages 286-300. Springer-Verlag, March 2012. 
@inproceedings{fossacs2012-BBDG,
  author =              {Brihaye, {\relax Th}omas and Bruy{\`e}re,
                         V{\'e}ronique and De{~}Pril, Julie and Gimbert,
                         Hugo},
  title =               {Subgame Perfection for Equilibria in Quantitative
                         Reachability Games},
  editor =              {Birkedal, Lars},
  booktitle =           {{P}roceedings of the 15th {I}nternational
                         {C}onference on {F}oundations of {S}oftware
                         {S}cience and {C}omputation {S}tructure
                         ({FoSSaCS}'12)},
  acronym =             {{FoSSaCS}'12},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {7213},
  pages =               {286-300},
  year =                {2012},
  month =               mar,
}
[BBG+12] Christel Baier, Tomáš Brázdil, Marcus Größer, and Antonín Kučera. Stochastic Game Logic. Acta Informatica 49(4):203-224. Springer-Verlag, June 2012. 
@article{acta49(4)-BBGK,
  author =              {Baier, {\relax Ch}ristel and Br{\'a}zdil,
                         Tom{\'a}{\v s} and Gr{\"o}{\ss}er, Marcus and Ku{\v
                         c}era, Anton{\'\i}n},
  title =               {Stochastic Game Logic},
  publisher =           {Springer-Verlag},
  journal =             {Acta Informatica},
  volume =              {49},
  number =              {4},
  pages =               {203-224},
  year =                {2012},
  month =               jun,
  doi =                 {10.1007/s00236-012-0156-0},
}
[BDL12] Benedikt Bollig, Normann Decker, and Martin Leucker. Frequency Linear-time Temporal Logic. In TASE'12, pages 85-92. IEEE Comp. Soc. Press, July 2012. 
@inproceedings{tase2012-BDL,
  author =              {Bollig, Benedikt and Decker, Normann and Leucker,
                         Martin},
  title =               {Frequency Linear-time Temporal Logic},
  editor =              {Margaria, Tiziana and Qiu, Zongyang and Yang,
                         Hongli},
  booktitle =           {{P}roceedings of the 6th {I}nternational {S}ymposium
                         on {T}heoretical {A}spects of {S}oftware
                         {E}ngineering ({TASE}'12)},
  acronym =             {{TASE}'12},
  publisher =           {IEEE Comp. Soc. Press},
  pages =               {85-92},
  year =                {2012},
  month =               jul,
  doi =                 {10.1109/TASE.2012.43},
}
[BDL+12] Peter Bulychev, Alexandre David, Kim Guldstrand Larsen, Axel Legay, Guangyuan Li, Danny Bøgsted Poulsen, and Amélie Stainer. Monitor-based statistical model checking for weighted metric temporal logic. In LPAR'12, Lecture Notes in Computer Science 7180, pages 168-182. Springer-Verlag, March 2012. 
@inproceedings{lpar2012-BDLLLPS,
  author =              {Bulychev, Peter and David, Alexandre and Larsen, Kim
                         Guldstrand and Legay, Axel and Li, Guangyuan and
                         Poulsen, Danny B{\o}gsted and Stainer, Am{\'e}lie},
  title =               {Monitor-based statistical model checking for
                         weighted metric temporal logic},
  editor =              {Bj{\o}rner, Nikolaj and Voronkov, Andrei},
  booktitle =           {{P}roceedings of the 18th {I}nternational
                         {C}onference {L}ogic {P}rogramming and {A}utomated
                         {R}easoning ({LPAR}'12)},
  acronym =             {{LPAR}'12},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {7180},
  pages =               {168-182},
  year =                {2012},
  month =               mar,
  doi =                 {10.1007/978-3-642-28717-6_15},
}
[BDL+12] Peter Bulychev, Alexandre David, Kim Guldstrand Larsen, Axel Legay, Marius Mikučionis, and Danny Bøgsted Poulsen. Checking and Distributing Statistical Model Checking. In NFM'12, Lecture Notes in Computer Science 7226, pages 449-463. Springer-Verlag, April 2012. 
@inproceedings{nasaFM2012-BDLLMP,
  author =              {Bulychev, Peter and David, Alexandre and Larsen, Kim
                         Guldstrand and Legay, Axel and Miku{\v{c}}ionis,
                         Marius and Poulsen, Danny B{\o}gsted},
  title =               {Checking and Distributing Statistical Model
                         Checking},
  editor =              {Goodloe, Alwyn and Person, Suzette},
  booktitle =           {{P}roceedings of the 4th {NASA} {F}ormal {M}ethods
                         {S}ymposium ({NFM}'12)},
  acronym =             {{NFM}'12},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {7226},
  pages =               {449-463},
  year =                {2012},
  month =               apr,
}
[BJS+12] Nathalie Bertrand, Thierry Jéron, Amélie Stainer, and Moez Krichen. Off-line test selection with test purposes for non-deterministic timed automata. Logical Methods in Computer Science 8(4). 2012. 
@article{lmcs8(4)-BJSK,
  author =              {Bertrand, Nathalie and J{\'e}ron, Thierry and
                         Stainer, Am{\'e}lie and Krichen, Moez},
  title =               {Off-line test selection with test purposes for
                         non-deterministic timed automata},
  journal =             {Logical Methods in Computer Science},
  volume =              {8},
  number =              {4},
  year =                {2012},
  doi =                 {10.2168/LMCS-8(4:8)2012},
}
[BL12] Mikołaj Bojańczyk and Sławomir Lasota. A Machine-Independent Characterization of Timed Languages. In ICALP'12, Lecture Notes in Computer Science 7392, pages 92-103. Springer-Verlag, July 2012. 
@inproceedings{icalp2012-BL,
  author =              {Boja{\'n}czyk, Miko{\l}aj and Lasota, S{\l}awomir},
  title =               {A~Machine-Independent Characterization of Timed
                         Languages},
  editor =              {Czumaj, Artur and Mehlhorn, Kurt and Pitts, Andrew
                         and Wattenhofer, Roger},
  booktitle =           {{P}roceedings of the 39th {I}nternational
                         {C}olloquium on {A}utomata, {L}anguages and
                         {P}rogramming ({ICALP}'12)~-- Part~{II}},
  acronym =             {{ICALP}'12},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {7392},
  pages =               {92-103},
  year =                {2012},
  month =               jul,
  doi =                 {10.1007/978-3-642-31585-5_12},
}
[Bre12] Romain Brenguier. Nash Equilibria in Concurrent Games –Application to Timed Games. Thèse de doctorat, Lab. Spécification & Vérification, ENS Cachan, France, November 2012. 
@phdthesis{phd-brenguier,
  author =              {Brenguier, Romain},
  title =               {Nash Equilibria in Concurrent Games~--Application to
                         Timed Games},
  year =                {2012},
  month =               nov,
  school =              {Lab.~Sp\'ecification \& V\'erification, ENS Cachan,
                         France},
  type =                {Th\`ese de doctorat},
}
[BS12] Nathalie Bertrand and Sven Schewe. Playing Optimally on Timed Automata with Random Delays. In FORMATS'12, Lecture Notes in Computer Science 7595, pages 43-58. Springer-Verlag, September 2012. 
@inproceedings{formats2012-BS,
  author =              {Bertrand, Nathalie and Schewe, Sven},
  title =               {Playing Optimally on Timed Automata with Random
                         Delays},
  editor =              {Jurdzi{\'n}ski, Marcin and Nickovic, Dejan},
  booktitle =           {{P}roceedings of the 10th {I}nternational
                         {C}onferences on {F}ormal {M}odelling and {A}nalysis
                         of {T}imed {S}ystems ({FORMATS}'12)},
  acronym =             {{FORMATS}'12},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {7595},
  pages =               {43-58},
  year =                {2012},
  month =               sep,
  doi =                 {10.1007/978-3-642-33365-1_5},
}
[CD12] Krishnendu Chatterjee and Laurent Doyen. Energy Parity Games. Theoretical Computer Science 458:49-60. Elsevier, November 2012. 
@article{tcs458-CD,
  author =              {Chatterjee, Krishnendu and Doyen, Laurent},
  title =               {Energy Parity Games},
  publisher =           {Elsevier},
  journal =             {Theoretical Computer Science},
  volume =              {458},
  pages =               {49-60},
  year =                {2012},
  month =               nov,
  doi =                 {10.1016/j.tcs.2012.07.038},
}
[CDM12] Franck Cassez, Jérémy Dubreil, and Hervé Marchand. Synthesis of opaque systems with static and dynamic masks. Formal Methods in System Design 40(1):88-115. Springer-Verlag, February 2012. 
@article{fmsd40(1)-CDM,
  author =              {Cassez, Franck and Dubreil, J{\'e}r{\'e}my and
                         Marchand, Herv{\'e}},
  title =               {Synthesis of opaque systems with static and dynamic
                         masks},
  publisher =           {Springer-Verlag},
  journal =             {Formal Methods in System Design},
  volume =              {40},
  number =              {1},
  pages =               {88-115},
  year =                {2012},
  month =               feb,
  doi =                 {10.1007/s10703-012-0141-9},
}
[CFK+12] Taolue Chen, Vojtěch Forejt, Marta Kwiatkowska, David Parker, and Aistis Simaitis. Automatic Verification of Competitive Stochastic Systems. In TACAS'12, Lecture Notes in Computer Science 7214, pages 315-330. Springer-Verlag, March 2012. 
@inproceedings{CFKPS-tacas2012,
  author =              {Chen, Taolue and Forejt, Vojt{\v{e}}ch and
                         Kwiatkowska, Marta and Parker, David and Simaitis,
                         Aistis},
  title =               {Automatic Verification of Competitive Stochastic
                         Systems},
  editor =              {Flanagan, Cormac and K{\"o}nig, Barbara},
  booktitle =           {{P}roceedings of the 18th {I}nternational
                         {C}onference on {T}ools and {A}lgorithms for
                         {C}onstruction and {A}nalysis of {S}ystems
                         ({TACAS}'12)},
  acronym =             {{TACAS}'12},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {7214},
  pages =               {315-330},
  year =                {2012},
  month =               mar,
}
[CFK+12] Taolue Chen, Vojtěch Forejt, Marta Kwiatkowska, Aistis Simaitis, Ashutosh Trivedi, and Michael Ummels. Playing Stochastic Games Precisely. In CONCUR'12, Lecture Notes in Computer Science 7454, pages 348-363. Springer-Verlag, September 2012. 
@inproceedings{CFKSTU-concur2012,
  author =              {Chen, Taolue and Forejt, Vojt{\v{e}}ch and
                         Kwiatkowska, Marta and Simaitis, Aistis and Trivedi,
                         Ashutosh and Ummels, Michael},
  title =               {Playing Stochastic Games Precisely},
  editor =              {Koutny, Maciej and Ulidowski, Irek},
  booktitle =           {{P}roceedings of the 23rd {I}nternational
                         {C}onference on {C}oncurrency {T}heory
                         ({CONCUR}'12)},
  acronym =             {{CONCUR}'12},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {7454},
  pages =               {348-363},
  year =                {2012},
  month =               sep,
}
[CHR12] Pavol Černý, Thomas A. Henzinger, and Arjun Radhakrishna. Simulation distances. Theoretical Computer Science 413(1):21-35. Elsevier, January 2012. 
@article{tcs413(1)-CHR,
  author =              {{\v{C}}ern{\'y}, Pavol and Henzinger, Thomas A. and
                         Radhakrishna, Arjun},
  title =               {Simulation distances},
  publisher =           {Elsevier},
  journal =             {Theoretical Computer Science},
  volume =              {413},
  number =              {1},
  pages =               {21-35},
  year =                {2012},
  month =               jan,
  doi =                 {10.1016/j.tcs.2011.08.002},
}
[Col12] Thomas Colcombet. Forms of determinism for automata. In STACS'12, Leibniz International Proceedings in Informatics 14, pages 1-23. Leibniz-Zentrum für Informatik, February 2012. 
@inproceedings{stacs2012-Col,
  author =              {Colcombet, {\relax Th}omas},
  title =               {Forms of determinism for automata},
  editor =              {D{\"u}rr, Christoph and Wilke, Thomas},
  booktitle =           {{P}roceedings of the 29th {S}ymposium on
                         {T}heoretical {A}spects of {C}omputer {S}cience
                         ({STACS}'12)},
  acronym =             {{STACS}'12},
  publisher =           {Leibniz-Zentrum f{\"u}r Informatik},
  series =              {Leibniz International Proceedings in Informatics},
  volume =              {14},
  pages =               {1-23},
  year =                {2012},
  month =               feb,
  doi =                 {10.4230/LIPIcs.STACS.2012.1},
}
[CRR12] Krishnendu Chatterjee, Mickael Randour, and Jean-François Raskin. Strategy Synthesis for Multi-dimensional Quantitative Objectives. Research Report 1201.5073, arXiv, January 2012. 
@techreport{arxiv12-CRR,
  author =              {Chatterjee, Krishnendu and Randour, Mickael and
                         Raskin, Jean-Fran{\c c}ois},
  title =               {Strategy Synthesis for Multi-dimensional
                         Quantitative Objectives},
  number =              {1201.5073},
  year =                {2012},
  month =               jan,
  institution =         {arXiv},
  type =                {Research Report},
}
[CV12] Krishnendu Chatterjee and Yaron Velner. Mean-Payoff Pushdown Games. In LICS'12, pages 195-204. IEEE Comp. Soc. Press, June 2012. 
@inproceedings{lics2012-CV,
  author =              {Chatterjee, Krishnendu and Velner, Yaron},
  title =               {Mean-Payoff Pushdown Games},
  booktitle =           {{P}roceedings of the 27th {A}nnual {S}ymposium on
                         {L}ogic in {C}omputer {S}cience ({LICS}'12)},
  acronym =             {{LICS}'12},
  publisher =           {IEEE Comp. Soc. Press},
  pages =               {195-204},
  year =                {2012},
  month =               jun,
  doi =                 {10.1109/LICS.2012.30},
}
[DDD+12] Werner Damm, Henning Dierks, Stefan Disch, Willem Hagemann, Florian Pigorsch, Christoph Scholl, Uwe Waldmann, and Boris Wirtz. Exact and fully symbolic verification of linear hybrid automata with large discrete state spaces. Science of Computer Programming 77(10-11):1122-1150. Elsevier, September 2012. 
@article{scp77(10-11)-DDDHPSWW,
  author =              {Damm, Werner and Dierks, Henning and Disch, Stefan
                         and Hagemann, Willem and Pigorsch, Florian and
                         Scholl, Christoph and Waldmann, Uwe and Wirtz,
                         Boris},
  title =               {Exact and fully symbolic verification of linear
                         hybrid automata with large discrete state spaces},
  publisher =           {Elsevier},
  journal =             {Science of Computer Programming},
  volume =              {77},
  number =              {10-11},
  pages =               {1122-1150},
  year =                {2012},
  month =               sep,
  doi =                 {10.1016/j.scico.2011.07.006},
}
[DLL+12] Alexandre David, Kim Guldstrand Larsen, Axel Legay, and Marius Mikučionis. Schedulability of Herschel-Planck Revisited Using Statistical Model Checking. In ISoLA'12, Lecture Notes in Computer Science 7610, pages 293-307. Springer-Verlag, October 2012. 
@inproceedings{isola2012-DLLM,
  author =              {David, Alexandre and Larsen, Kim Guldstrand and
                         Legay, Axel and Miku{\v{c}}ionis, Marius},
  title =               {Schedulability of {H}erschel-{P}lanck Revisited
                         Using Statistical Model Checking},
  editor =              {Margaria, Tiziana and Steffen, Bernhard},
  booktitle =           {{P}roceedings of the 5th {I}nternational {S}ymposium
                         on {L}everaging {A}pplications of {F}ormal {M}ethods
                         ({IS}o{LA}'12)~-- {P}art~{II}: {A}pplications and
                         {C}ase {S}tudies},
  acronym =             {{IS}o{LA}'12},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {7610},
  pages =               {293-307},
  year =                {2012},
  month =               oct,
  doi =                 {10.1007/978-3-642-34032-1},
}
[DMS12] Laurent Doyen, Thierry Massart, and Mahsa Shirmohammadi. Infinite Synchronizing Words for Probabilistic Automata (erratum). Research Report 1206.0995, arXiv, June 2012. 
@techreport{mfcs2011-DMS-erratum,
  author =              {Doyen, Laurent and Massart, {\relax Th}ierry and
                         Shirmohammadi, Mahsa},
  title =               {Infinite Synchronizing Words for Probabilistic
                         Automata (erratum)},
  number =              {1206.0995},
  year =                {2012},
  month =               jun,
  institution =         {arXiv},
  type =                {Research Report},
}
[Doy12] Laurent Doyen. Games and Automata: From Boolean to Quantitative Verification. Mémoire d'habilitation, École Normale Supérieure de Cachan, France, March 2012. 
@phdthesis{hdr-doyen,
  author =              {Doyen, Laurent},
  title =               {Games and Automata: From Boolean to Quantitative
                         Verification},
  year =                {2012},
  month =               mar,
  school =              {{\'E}cole Normale Sup{\'e}rieure de Cachan, France},
  type =                {M\'emoire d'habilitation},
}
[DST+12] Giorgio Delzanno, Arnaud Sangnier, Riccardo Traverso, and Gianluigi Zavattaro. On the Complexity of Parameterized Reachability in Reconfigurable Broadcast Networks. In FSTTCS'12, Leibniz International Proceedings in Informatics 18, pages 289-300. Leibniz-Zentrum für Informatik, December 2012. 
@inproceedings{fsttcs12-DSTZ,
  author =              {Delzanno, Giorgio and Sangnier, Arnaud and Traverso,
                         Riccardo and Zavattaro, Gianluigi},
  title =               {On~the Complexity of Parameterized Reachability in
                         Reconfigurable Broadcast Networks},
  editor =              {D'Souza, Deepak and Kavitha, Telikepalli and
                         Radhakrishnan, Jaikumar},
  booktitle =           {{P}roceedings of the 32nd {C}onference on
                         {F}oundations of {S}oftware {T}echnology and
                         {T}heoretical {C}omputer {S}cience ({FSTTCS}'12)},
  acronym =             {{FSTTCS}'12},
  publisher =           {Leibniz-Zentrum f{\"u}r Informatik},
  series =              {Leibniz International Proceedings in Informatics},
  volume =              {18},
  pages =               {289-300},
  year =                {2012},
  month =               dec,
  doi =                 {LIPIcs.FSTTCS.2012.289},
}
[DSZ12] Giorgio Delzanno, Arnaud Sangnier, and Gianluigi Zavattaro. Verification of Ad Hoc Networks with Node and Communication Failures. In FMOODS/FORTE'12, Lecture Notes in Computer Science 7273, pages 313-327. Springer-Verlag, June 2012. 
@inproceedings{forte2012-DSZ,
  author =              {Delzanno, Giorgio and Sangnier, Arnaud and
                         Zavattaro, Gianluigi},
  title =               {Verification of Ad~Hoc Networks with Node and
                         Communication Failures},
  editor =              {Giese, Holger and Ro{\c{s}}u, Grigore},
  booktitle =           {{P}roceedings of the {J}oint 14th {IFIP} {WG~6.1}
                         {I}nternational {C}onference on {F}ormal {M}ethods
                         for {O}pen {O}bject-{B}ased {D}istributed {S}ystems
                         ({FMOODS}'12) and 32nd {IFIP} {WG~6.1}
                         {I}nternational {C}onference on {F}ormal
                         {T}echniques for {N}etworked and {D}istributed
                         {S}ystems ({FORTE}'12)},
  acronym =             {{FMOODS/FORTE}'12},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {7273},
  pages =               {313-327},
  year =                {2012},
  month =               jun,
  doi =                 {10.1007/978-3-642-15375-4_22},
}
[FS12] John Fearnley and Sven Schewe. Time and parallelizability results for parity games with bounded treewidth. In ICALP'12, Lecture Notes in Computer Science 7392, pages 189-200. Springer-Verlag, July 2012. 
@inproceedings{icalp2012-FS,
  author =              {Fearnley, John and Schewe, Sven},
  title =               {Time and parallelizability results for parity games
                         with bounded treewidth},
  editor =              {Czumaj, Artur and Mehlhorn, Kurt and Pitts, Andrew
                         and Wattenhofer, Roger},
  booktitle =           {{P}roceedings of the 39th {I}nternational
                         {C}olloquium on {A}utomata, {L}anguages and
                         {P}rogramming ({ICALP}'12)~-- Part~{II}},
  acronym =             {{ICALP}'12},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {7392},
  pages =               {189-200},
  year =                {2012},
  month =               jul,
  doi =                 {10.1007/978-3-642-31585-5_20},
}
[FZ12] Wladimir Fridman and Martin Zimmermann. Playing Pushdown Parity Games in a Hurry. In GandALF'12, Electronic Proceedings in Theoretical Computer Science 96, pages 183-196. September 2012. 
@inproceedings{gandalf2012-FZ,
  author =              {Fridman, Wladimir and Zimmermann, Martin},
  title =               {Playing Pushdown Parity Games in a Hurry},
  editor =              {Faella, Marco and Murano, Aniello},
  booktitle =           {{P}roceedings of the 3th {I}nternational {S}ymposium
                         on {G}ames, {A}utomata, {L}ogics and {F}ormal
                         {V}erification ({GandALF}'12)},
  acronym =             {{GandALF}'12},
  series =              {Electronic Proceedings in Theoretical Computer
                         Science},
  volume =              {96},
  pages =               {183-196},
  year =                {2012},
  month =               sep,
  doi =                 {10.4204/EPTCS.96.14},
}
[GC12] Arie Gurfinkel and Marsha Chechik. Robust Vacuity for Branching Temporal Logic. ACM Transactions on Computational Logic 13(1). ACM Press, January 2012. 
@article{tocl13(1)-GC,
  author =              {Gurfinkel, Arie and Chechik, Marsha},
  title =               {Robust Vacuity for Branching Temporal Logic},
  publisher =           {ACM Press},
  journal =             {ACM Transactions on Computational Logic},
  volume =              {13},
  number =              {1},
  year =                {2012},
  month =               jan,
  doi =                 {10.1145/2071368.2071369},
}
[GD12] Dimitar P. Guelev and Cătălin Dima. Epistemic ATL with Perfect Recall, Past and Strategy Contexts. In CLIMA'12, Lecture Notes in Artificial Intelligence 7486, pages 77-93. Springer-Verlag, August 2012. 
@inproceedings{clima2012-GD,
  author =              {Guelev, Dimitar P. and Dima, C{\u a}t{\u a}lin},
  title =               {Epistemic {ATL} with Perfect Recall, Past and
                         Strategy Contexts},
  editor =              {Fisher, Michael and van der Torre, Leendert W. N.
                         and Dastani, Mehdi and Governatori, Guido},
  booktitle =           {{P}roceedings of the 13th {I}nternational {W}orkshop
                         on {C}omputational {L}ogic in {M}ulti-{A}gent
                         {S}ystems ({CLIMA}'12)},
  acronym =             {{CLIMA}'12},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Artificial Intelligence},
  volume =              {7486},
  pages =               {77-93},
  year =                {2012},
  month =               aug,
  doi =                 {10.1007/978-3-642-32897-8_7},
}
[Gir12] Antoine Girard. Low-complexity switching controllers for safety using symbolic models. In ADHS'12. International Federation of Automatic Control, June 2012. 
@inproceedings{adhs2012-Gir,
  author =              {Girard, Antoine},
  title =               {Low-complexity switching controllers for safety
                         using symbolic models},
  editor =              {Giua, Alessandro and Silva, Manuel and Heemels,
                         Maurice and De{~}Schutter, Bart},
  booktitle =           {Proceedings of the 4th {IFAC} conference on
                         {A}nalysis and {D}esign of {H}ybrid {S}ystems
                         ({ADHS}'12)},
  acronym =             {{ADHS}'12},
  publisher =           {International Federation of Automatic Control},
  year =                {2012},
  month =               jun,
}
[Haa12] Christoph Haase. On the Complexity of Model Checking Counter Automata. PhD thesis, University of Oxford, UK, January 2012. 
@phdthesis{phd-haase,
  author =              {Haase, Christoph},
  title =               {On the Complexity of Model Checking Counter
                         Automata},
  year =                {2012},
  month =               jan,
  school =              {University of Oxford, UK},
}
[Hen12] Thomas A. Henzinger. Quantitative Reactive Models. In MODELS'12, Lecture Notes in Computer Science 7590, pages 1-2. Springer-Verlag, September 2012. 
@inproceedings{models2012-Hen,
  author =              {Henzinger, Thomas A.},
  title =               {Quantitative Reactive Models},
  editor =              {France, Robert B. and Kazmeier, J{\"u}rgen and Breu,
                         Ruth and Atkinson, Colin},
  booktitle =           {{P}roceedings of the 15th {I}nternational
                         {C}onference on {M}odel {D}riven {E}ngineering
                         {L}anguages and {S}ystems ({MODELS}'12)},
  acronym =             {{MODELS}'12},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {7590},
  pages =               {1-2},
  year =                {2012},
  month =               sep,
  doi =                 {10.1007/978-3-642-33666-9_1},
}
[HIM12] Thomas Dueholm Hansen, Rasmus Ibsen-Jensen, and Peter Bro Miltersen. A Faster Algorithm for Solving One-Clock Priced Timed Games. Research Report 1201.3498, arXiv, January 2012. 
@techreport{arxiv12-HIM,
  author =              {Hansen, Thomas Dueholm and Ibsen{-}Jensen, Rasmus
                         and Miltersen, Peter Bro},
  title =               {A~Faster Algorithm for Solving One-Clock Priced
                         Timed Games},
  number =              {1201.3498},
  year =                {2012},
  month =               jan,
  institution =         {arXiv},
  type =                {Research Report},
}
[HSW12] Frédéric Herbreteau, B. Srivathsan, and Igor Walukiewicz. Efficient emptiness check for timed Büchi automata. Formal Methods in System Design 40(2):122-146. Springer-Verlag, April 2012. 
@article{fmsd40(2)-HSW,
  author =              {Herbreteau, Fr{\'e}d{\'e}ric and Srivathsan, B. and
                         Walukiewicz, Igor},
  title =               {Efficient emptiness check for timed {B}{\"u}chi
                         automata},
  publisher =           {Springer-Verlag},
  journal =             {Formal Methods in System Design},
  volume =              {40},
  number =              {2},
  pages =               {122-146},
  year =                {2012},
  month =               apr,
  doi =                 {10.1007/s10703-011-0133-1},
}
[HSW12] Frédéric Herbreteau, B. Srivathsan, and Igor Walukiewicz. Better abstractions for timed automata. In LICS'12, pages 375-384. IEEE Comp. Soc. Press, June 2012. 
@inproceedings{lics2012-HSW,
  author =              {Herbreteau, Fr{\'e}d{\'e}ric and Srivathsan, B. and
                         Walukiewicz, Igor},
  title =               {Better abstractions for timed automata},
  booktitle =           {{P}roceedings of the 27th {A}nnual {S}ymposium on
                         {L}ogic in {C}omputer {S}cience ({LICS}'12)},
  acronym =             {{LICS}'12},
  publisher =           {IEEE Comp. Soc. Press},
  pages =               {375-384},
  year =                {2012},
  month =               jun,
  doi =                 {10.1109/LICS.2012.48},
}
[JLS12] Kenneth Yrke Jørgensen, Kim Guldstrand Larsen, and Jiří Srba. Time-Darts: A Data Structure for Verification of Closed Timed Automata. In SSV'12, Electronic Proceedings in Theoretical Computer Science 102, pages 141-155. November 2012. 
@inproceedings{ssv2012-JLS,
  author =              {J{\o}rgensen, Kenneth Yrke and Larsen, Kim
                         Guldstrand and Srba, Ji{\v r}{\'\i}},
  title =               {Time-Darts: A~Data Structure for Verification of
                         Closed Timed Automata},
  booktitle =           {{P}roceedings of the 7th {C}onference on {S}ystems
                         {S}oftware {V}erification ({SSV}'12)},
  acronym =             {{SSV}'12},
  series =              {Electronic Proceedings in Theoretical Computer
                         Science},
  volume =              {102},
  pages =               {141-155},
  year =                {2012},
  month =               nov,
  doi =                 {10.4204/EPTCS.102.13},
}
[KLS+12] Miroslav Klimoš, Kim Guldstrand Larsen, Filip Štefaňák, and Jeppe Thaarup. Nash Equilibria in Concurrent Priced Games. In LATA'12, Lecture Notes in Computer Science 7183, pages 363-376. Springer-Verlag, May 2012. 
@inproceedings{lata2012-KLST,
  author =              {Klimo{\v{s}}, Miroslav and Larsen, Kim Guldstrand
                         and {\v{S}}tefa{\v{n}}{\'a}k, Filip and Thaarup,
                         Jeppe},
  title =               {{N}ash Equilibria in Concurrent Priced Games},
  editor =              {Dediu, Adrian Horia and Mart{\'\i}n-Vide, Carlos},
  booktitle =           {{P}roceedings of the 6th {I}nternational
                         {C}onference on {L}anguage and {A}utomata {T}heory
                         and {A}pplications ({LATA}'12)},
  acronym =             {{LATA}'12},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {7183},
  pages =               {363-376},
  year =                {2012},
  month =               may,
}
[KP12] Elias Koutsoupias and Katia Papakonstantinopoulou. Contention Issues in Congestion Games. In ICALP'12, Lecture Notes in Computer Science 7392, pages 623-635. Springer-Verlag, July 2012. 
@inproceedings{icalp2012-KP,
  author =              {Koutsoupias, Elias and Papakonstantinopoulou, Katia},
  title =               {Contention Issues in Congestion Games},
  editor =              {Czumaj, Artur and Mehlhorn, Kurt and Pitts, Andrew
                         and Wattenhofer, Roger},
  booktitle =           {{P}roceedings of the 39th {I}nternational
                         {C}olloquium on {A}utomata, {L}anguages and
                         {P}rogramming ({ICALP}'12)~-- Part~{II}},
  acronym =             {{ICALP}'12},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {7392},
  pages =               {623-635},
  year =                {2012},
  month =               jul,
  doi =                 {10.1007/978-3-642-31585-5_55},
}
[KPV12] Orna Kupferman, Amir Pnueli, and Moshe Y. Vardi. Once and For All. Journal of Computer and System Sciences 78(3):981-996. Elsevier, May 2012. 
@article{jcss78(3)-KPV,
  author =              {Kupferman, Orna and Pnueli, Amir and Vardi, Moshe
                         Y.},
  title =               {{\emph{Once}} and {\emph{For All}}},
  publisher =           {Elsevier},
  journal =             {Journal of Computer and System Sciences},
  volume =              {78},
  number =              {3},
  pages =               {981-996},
  year =                {2012},
  month =               may,
  doi =                 {10.1016/j.jcss.2011.08.006},
}
[Kuc12] Antonín Kučera. Playing Games with Counter Automata. In RP'12, Lecture Notes in Computer Science 7550, pages 29-41. Springer-Verlag, September 2012. 
@inproceedings{rp2012-Kuc,
  author =              {Ku{\v c}era, Anton{\'\i}n},
  title =               {Playing Games with Counter Automata},
  editor =              {Finkel, Alain and Leroux, J{\'e}r{\^o}me and
                         Potapov, Igor},
  booktitle =           {{P}roceedings of the 6th {W}orkshop on
                         {R}eachability {P}roblems in {C}omputational
                         {M}odels ({RP}'12)},
  acronym =             {{RP}'12},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {7550},
  pages =               {29-41},
  year =                {2012},
  month =               sep,
  doi =                 {10.1007/978-3-642-33512-9_4},
}
[MMP+12] Fabio Mogavero, Aniello Murano, Giuseppe Perelli, and Moshe Y. Vardi. What Makes ATL* Decidable? A Decidable Fragment of Strategy Logic. In CONCUR'12, Lecture Notes in Computer Science 7454, pages 193-208. Springer-Verlag, September 2012. 
@inproceedings{concur2012-MMPV,
  author =              {Mogavero, Fabio and Murano, Aniello and Perelli,
                         Giuseppe and Vardi, Moshe Y.},
  title =               {What Makes {ATL\(^{*}\)} Decidable? {A}~Decidable
                         Fragment of Strategy Logic},
  editor =              {Koutny, Maciej and Ulidowski, Irek},
  booktitle =           {{P}roceedings of the 23rd {I}nternational
                         {C}onference on {C}oncurrency {T}heory
                         ({CONCUR}'12)},
  acronym =             {{CONCUR}'12},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {7454},
  pages =               {193-208},
  year =                {2012},
  month =               sep,
}
[MMP+12] Fabio Mogavero, Aniello Murano, Giuseppe Perelli, and Moshe Y. Vardi. Reasoning About Strategies: On the Model-Checking Problem. Research Report cs.LO/1112.6275, arXiv, December 2012. 
@techreport{arxiv-cd.LO-1112.6275,
  author =              {Mogavero, Fabio and Murano, Aniello and Perelli,
                         Giuseppe and Vardi, Moshe Y.},
  title =               {Reasoning About Strategies: On the Model-Checking
                         Problem},
  number =              {cs.LO/1112.6275},
  year =                {2012},
  month =               dec,
  institution =         {arXiv},
  type =                {Research Report},
}
[MS12] Carol A. Meyers and Andreas S. Schulz. The complexity of welfare maximization in congestion games. Networks 59(2):252-260. John Wiley & Sons, March 2012. 
@article{netw59(2)-MS,
  author =              {Meyers, Carol A. and Schulz, Andreas S.},
  title =               {The~complexity of welfare maximization in congestion
                         games},
  publisher =           {John Wiley \& Sons},
  journal =             {Networks},
  volume =              {59},
  number =              {2},
  pages =               {252-260},
  year =                {2012},
  month =               mar,
  doi =                 {10.1002/net.20439},
}
[NSL+12] Truong Khanh Nguyen, Jun Sun, Yang Liu, Jin Song Dong, and Yan Liu. Improved BDD-Based Discrete Analysis of Timed Systems. In FM'12, Lecture Notes in Computer Science 7436, pages 326-340. Springer-Verlag, August 2012. 
@inproceedings{fm2012-NSLDL,
  author =              {Nguyen, Truong Khanh and Sun, Jun and Liu, Yang and
                         Dong, Jin Song and Liu, Yan},
  title =               {Improved {BDD}-Based Discrete Analysis of Timed
                         Systems},
  editor =              {Giannakopoulou, Dimitra and M{\'e}ry, Dominique},
  booktitle =           {{P}roceedings of the 18th {I}nternational
                         {S}ymposium on {F}ormal {M}ethods ({FM}'12)},
  acronym =             {{FM}'12},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {7436},
  pages =               {326-340},
  year =                {2012},
  month =               aug,
  doi =                 {10.1007/978-3-642-32759-9_28},
}
[PST12] Renato Paes Leme, Vasilis Syrgkanis, and Éva Tardos. The curse of simultaneity. In ITCS'12, pages 60-67. ACM Press, January 2012. 
@inproceedings{itcs2012-PST,
  author =              {Paes{ }Leme, Renato and Syrgkanis, Vasilis and
                         Tardos, {\'E}va},
  title =               {The curse of simultaneity},
  editor =              {Goldwasser, Shafi},
  booktitle =           {{P}roceedings of the 3rd {C}onference on
                         {I}nnovations in {T}heoretical {C}omputer {S}cience
                         ({ITCS}'12)},
  acronym =             {{ITCS}'12},
  publisher =           {ACM Press},
  pages =               {60-67},
  year =                {2012},
  month =               jan,
  doi =                 {10.1145/2090236.2090242},
}
[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.},
}
[THH+12] Takashi Tomita, Shin Hiura, Shigeki Hagihara, and Naoki Yonezaki. A Temporal Logic with Mean-Payoff Constraints. In ICFEM'12, Lecture Notes in Computer Science 7635, pages 249-265. Springer-Verlag, November 2012. 
@inproceedings{icfem2012-THHY,
  author =              {Tomita, Takashi and Hiura, Shin and Hagihara,
                         Shigeki and Yonezaki, Naoki},
  title =               {A~Temporal Logic with Mean-Payoff Constraints},
  editor =              {Aoki, Toshiaki and Taguchi, Kenji},
  booktitle =           {{P}roceedings of the 14th {I}nternational
                         {C}onference on {F}ormal {E}ngineering {M}ethods
                         ({ICFEM}'12)},
  acronym =             {{ICFEM}'12},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {7635},
  pages =               {249-265},
  year =                {2012},
  month =               nov,
  doi =                 {10.1007/978-3-642-34281-3_19},
}
[TW12] Nicolas Troquard and Dirk Walther. On Satisfiability in ATL with Strategy Contexts. In JELIA'12, Lecture Notes in Computer Science 7519, pages 398-410. Springer-Verlag, September 2012. 
@inproceedings{jelia2012-TW,
  author =              {Troquard, Nicolas and Walther, Dirk},
  title =               {On Satisfiability in {ATL} with Strategy Contexts},
  editor =              {Fari{\~n}as{ }del{ }Cerro, Luis and Herzig, Andreas
                         and Mengin, J{\'e}r{\^o}me},
  booktitle =           {{P}roceedings of the 13th {E}uropean {C}onference in
                         {L}ogics in {A}rtificial {I}ntelligence
                         ({JELIA}'12)},
  acronym =             {{JELIA}'12},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {7519},
  pages =               {398-410},
  year =                {2012},
  month =               sep,
  doi =                 {10.1007/978-3-642-33353-8_31},
}
[Zan12] Fabio Zanasi. Expressiveness of Monadic Second-Order Logics on Infinite Trees of Arbitrary Branching Degrees. Master's thesis, Amsterdam University, the Netherlands, August 2012. 
@mastersthesis{master-zanasi,
  author =              {Zanasi, Fabio},
  title =               {Expressiveness of Monadic Second-Order Logics on
                         Infinite Trees of Arbitrary Branching Degrees},
  year =                {2012},
  month =               aug,
  school =              {Amsterdam University, the~Netherlands},
  type =                {Master's thesis},
}
List of authors