2006
[BBM06] Patricia Bouyer, Thomas Brihaye, and Nicolas Markey. Improved Undecidability Results on Weighted Timed Automata. Information Processing Letters 98(5):188-194. Elsevier, June 2006.
Abstract

In this paper, we improve two recent undecidability results of Brihaye, Bruyère and Raskin about weighted timed automata, an extension of timed automata with a cost variable. Our results rely on a new encoding of the two counters of a Minsky machine that only require three clocks and one stopwatch cost, while previous reductions required five clocks and one stopwatch cost.

@article{ipl98(5)-BBM,
  author =              {Bouyer, Patricia and Brihaye, {\relax Th}omas and
                         Markey, Nicolas},
  title =               {Improved Undecidability Results on Weighted Timed
                         Automata},
  publisher =           {Elsevier},
  journal =             {Information Processing Letters},
  volume =              {98},
  number =              {5},
  pages =               {188-194},
  year =                {2006},
  month =               jun,
  doi =                 {10.1016/j.ipl.2006.01.012},
  abstract =            {In this paper, we improve two recent undecidability
                         results of Brihaye, Bruy{\`e}re and Raskin about
                         weighted timed automata, an extension of timed
                         automata with a cost variable. Our results rely on a
                         new encoding of the two counters of a Minsky machine
                         that only require three clocks and one stopwatch
                         cost, while previous reductions required five clocks
                         and one stopwatch cost.},
}
[LMS06] François Laroussinie, Nicolas Markey, and Philippe Schnoebelen. Efficient timed model checking for discrete-time systems. Theoretical Computer Science 353(1-3):249-271. Elsevier, March 2006.
Abstract

We consider model checking of timed temporal formulae in durational transition graphs (DTGs), i.e., Kripke structures where transitions have integer durations. Two semantics for DTGs are presented and motivated. We consider timed versions of CTL where subscripts put quantitative constraints on the time it takes before a property is satisfied.

We exhibit an important gap between logics where subscripts of the form "= c" (exact duration) are allowed, and simpler logics that only allow subscripts of the form "≤ c" or "≥ c" (bounded duration).

Without exact durations, model checking can be done in polynomial time, but with exact durations, it becomes Δ2P-complete or PSPACE-complete depending on the considered semantics.

@article{tcs353(1-3)-LMS,
  author =              {Laroussinie, Fran{\c c}ois and Markey, Nicolas and
                         Schnoebelen, {\relax Ph}ilippe},
  title =               {Efficient timed model checking for discrete-time
                         systems},
  publisher =           {Elsevier},
  journal =             {Theoretical Computer Science},
  volume =              {353},
  number =              {1-3},
  pages =               {249-271},
  year =                {2006},
  month =               mar,
  doi =                 {10.1016/j.tcs.2005.11.020},
  abstract =            {We consider model checking of timed temporal
                         formulae in \emph{durational transition graphs}
                         (DTGs), \emph{i.e.}, Kripke structures where
                         transitions have integer durations. Two semantics
                         for DTGs are presented and motivated. We consider
                         timed versions of CTL where subscripts put
                         quantitative constraints on the time it takes before
                         a property is satisfied. \par We exhibit an
                         important gap between logics where subscripts of the
                         form {"}\(= c\){"} (exact duration) are allowed, and
                         simpler logics that only allow subscripts of the
                         form {"}\(\leq c\){"} or {"}\(\geq c\){"} (bounded
                         duration).\par Without exact durations, model
                         checking can be done in polynomial time, but with
                         exact durations, it becomes
                         \(\Delta_{2}^{P}\)-complete or PSPACE-complete
                         depending on the considered semantics.},
}
[MR06] Nicolas Markey and Jean-François Raskin. Model Checking Restricted Sets of Timed Paths. Theoretical Computer Science 358(2-3):273-292. Elsevier, August 2006.
Abstract

In this paper, we study the complexity of model-checking formulas of four important real-time logics (TPTL, MTL, MITL, and TCTL) over restricted sets of timed paths. The classes of restricted sets of timed paths that we consider are (i) a single finite (or ultimately periodic) timed path, (ii) an infinite set of finite (or infinite) timed paths defined by a finite (or ultimately periodic) path in a region graph, (iii) an infinite set of finite (or infinite) timed paths defined by a finite (or ultimately periodic) path in a zone graph.

Several results are quite negative: TPTL and MTL remain undecidable along region- and zone-paths. On the other hand, we obtained PTIME algorithms for model checking TCTL along a region path, and for MTL along a single timed path.

@article{tcs358(2-3)-MR,
  author =              {Markey, Nicolas and Raskin, Jean-Fran{\c c}ois},
  title =               {Model Checking Restricted Sets of Timed Paths},
  publisher =           {Elsevier},
  journal =             {Theoretical Computer Science},
  volume =              {358},
  number =              {2-3},
  pages =               {273-292},
  year =                {2006},
  month =               aug,
  doi =                 {10.1016/j.tcs.2006.01.019},
  abstract =            {In this paper, we study the complexity of
                         model-checking formulas of four important real-time
                         logics (TPTL, MTL, MITL, and TCTL) over restricted
                         sets of timed paths. The classes of restricted sets
                         of timed paths that we consider are
                         \textit{(i)}~a~single finite (or ultimately
                         periodic) timed path, \textit{(ii)}~an~infinite set
                         of finite (or infinite) timed paths defined by a
                         finite (or ultimately periodic) path in a region
                         graph, \textit{(iii)}~an~infinite set of finite (or
                         infinite) timed paths defined by a finite (or
                         ultimately periodic) path in a zone graph. \par
                         Several results are quite negative: TPTL and MTL
                         remain undecidable along region- and zone-paths. On
                         the other hand, we obtained PTIME algorithms for
                         model checking TCTL along a region path, and for MTL
                         along a single timed path.},
}
[MS06] Nicolas Markey and Philippe Schnoebelen. Mu-calculus path checking. Information Processing Letters 97(6):225-230. Elsevier, March 2006.
Abstract

We investigate the path model checking problem for the μ-calculus. Surprisingly, restricting to deterministic structures does not allow for more efficient model checking algorithm, as we prove that it can encode any instance of the standard model checking problem for the μ-calculus.

@article{ipl97(6)-MS,
  author =              {Markey, Nicolas and Schnoebelen, {\relax Ph}ilippe},
  title =               {Mu-calculus path checking},
  publisher =           {Elsevier},
  journal =             {Information Processing Letters},
  volume =              {97},
  number =              {6},
  pages =               {225-230},
  year =                {2006},
  month =               mar,
  doi =                 {10.1016/j.ipl.2005.11.010},
  abstract =            {We investigate the path model checking problem for
                         the \(\mu\)-calculus. Surprisingly, restricting to
                         deterministic structures does not allow for more
                         efficient model checking algorithm, as we prove that
                         it can encode any instance of the standard model
                         checking problem for the \(\mu\)-calculus.},
}
[BLM+06] Patricia Bouyer, Kim Guldstrand Larsen, Nicolas Markey, and Jacob Illum Rasmussen. Almost Optimal Strategies in One-Clock Priced Timed Automata. In FSTTCS'06, Lecture Notes in Computer Science 4337, pages 345-356. Springer-Verlag, December 2006.
Abstract

We consider timed games extended with cost information, and prove computability of the optimal cost and of ε-optimal memoryless strategies in timed games with one clock. In contrast, this problem has recently been proved undecidable for timed games with three clocks.

@inproceedings{fsttcs2006-BLMR,
  author =              {Bouyer, Patricia and Larsen, Kim Guldstrand and
                         Markey, Nicolas and Rasmussen, Jacob Illum},
  title =               {Almost Optimal Strategies in One-Clock Priced Timed
                         Automata},
  editor =              {Arun-Kumar, S. and Garg, Naveen},
  booktitle =           {{P}roceedings of the 26th {C}onference on
                         {F}oundations of {S}oftware {T}echnology and
                         {T}heoretical {C}omputer {S}cience ({FSTTCS}'06)},
  acronym =             {{FSTTCS}'06},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {4337},
  pages =               {345-356},
  year =                {2006},
  month =               dec,
  doi =                 {10.1007/11944836_32},
  abstract =            {We consider timed games extended with cost
                         information, and prove computability of the optimal
                         cost and of \(\epsilon\)-optimal memoryless
                         strategies in timed games with one~clock.
                         In~contrast, this problem has recently been proved
                         undecidable for timed games with three clocks.},
}
[BMR06] Patricia Bouyer, Nicolas Markey, and Pierre-Alain Reynier. Robust Model-Checking of Linear-Time Properties in Timed Automata. In LATIN'06, Lecture Notes in Computer Science 3887, pages 238-249. Springer-Verlag, March 2006.
Abstract

Formal verification of timed systems is well understood, but their implementation is still challenging. Recent works by Raskin et al. have brought out a model of parameterized timed automata that can be used to prove implementability of timed systems for safety properties. We define here a more general notion of robust model-checking for linear-time properties, which consists in verifying whether a property still holds even if the transitions are slightly delayed or expedited. We provide PSPACE algorithms for the robust model-checking of Büchi-like and LTL properties. We also verify bounded-response-time properties.

@inproceedings{latin2006-BMR,
  author =              {Bouyer, Patricia and Markey, Nicolas and Reynier,
                         Pierre-Alain},
  title =               {Robust Model-Checking of Linear-Time Properties in
                         Timed Automata},
  editor =              {Correa, Jos{\'e} R. and Hevia, Alejandro and Kiwi,
                         Marcos},
  booktitle =           {{P}roceedings of the 7th {L}atin {A}merican
                         {S}ymposium on {T}heoretical {IN}formatics
                         ({LATIN}'06)},
  acronym =             {{LATIN}'06},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {3887},
  pages =               {238-249},
  year =                {2006},
  month =               mar,
  doi =                 {10.1007/11682462_25},
  abstract =            {Formal verification of timed systems is well
                         understood, but their \emph{implementation} is still
                         challenging. Recent works by Raskin \emph{et al.}
                         have brought out a model of parameterized timed
                         automata that can be used to prove
                         \emph{implementability} of timed systems for safety
                         properties. We define here a more general notion of
                         robust model-checking for linear-time properties,
                         which consists in verifying whether a property still
                         holds even if the transitions are slightly delayed
                         or expedited. We provide PSPACE algorithms for the
                         robust model-checking of B{\"u}chi-like and LTL
                         properties. We also verify bounded-response-time
                         properties.},
}
[LMO06] François Laroussinie, Nicolas Markey, and Ghassan Oreiby. Model-Checking Timed ATL for Durational Concurrent Game Structures. In FORMATS'06, Lecture Notes in Computer Science 4202, pages 245-259. Springer-Verlag, September 2006.
Abstract

We extend the framework of ATL model-checking to "simply timed" concurrent game structures, i.e., multi-agent structures where each transition carry an integral duration (or interval thereof). While the case of single durations is easily handled from the semantics point of view, intervals of durations raise several interesting questions. Moreover subtle algorithmic problems have to be handled when dealing with model checking. We propose a semantics for which we develop efficient (PTIME) algorithms for timed ATL without equality constraints, while the general case is shown to be EXPTIME-complete.

@inproceedings{formats2006-LMO,
  author =              {Laroussinie, Fran{\c c}ois and Markey, Nicolas and
                         Oreiby, Ghassan},
  title =               {Model-Checking Timed~{ATL} for Durational Concurrent
                         Game Structures},
  editor =              {Asarin, Eugene and Bouyer, Patricia},
  booktitle =           {{P}roceedings of the 4th {I}nternational
                         {C}onferences on {F}ormal {M}odelling and {A}nalysis
                         of {T}imed {S}ystems ({FORMATS}'06)},
  acronym =             {{FORMATS}'06},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {4202},
  pages =               {245-259},
  year =                {2006},
  month =               sep,
  doi =                 {10.1007/11867340_18},
  abstract =            {We extend the framework of ATL model-checking to
                         {"}simply timed{"} concurrent game structures, i.e.,
                         multi-agent structures where each transition carry
                         an integral duration (or interval thereof). While
                         the case of single durations is easily handled from
                         the semantics point of view, intervals of durations
                         raise several interesting questions. Moreover subtle
                         algorithmic problems have to be handled when dealing
                         with model checking. We propose a semantics for
                         which we develop efficient (PTIME) algorithms for
                         timed ATL without equality constraints, while the
                         general case is shown to be EXPTIME-complete.},
}
[AAD+06] Dana Angluin, James Aspnes, Zoë Diamadi, Michael J. Fischer, and René Peralta. Computation in Networks of Passively Mobile Finite-State Sensors. Distributed Computing 18(4):235-253. Springer-Verlag, March 2006. 
@article{discomp18(4)-AADFP,
  author =              {Angluin, Dana and Aspnes, James and Diamadi, Zo{\"e}
                         and Fischer, Michael J. and Peralta, Ren{\'e}},
  title =               {Computation in Networks of Passively Mobile
                         Finite-State Sensors},
  publisher =           {Springer-Verlag},
  journal =             {Distributed Computing},
  volume =              {18},
  number =              {4},
  pages =               {235-253},
  year =                {2006},
  month =               mar,
  doi =                 {10.1007/s00446-005-0138-3},
}
[AAM06] Yasmina Abdeddaïm, Eugene Asarin, and Oded Maler. Scheduling with timed automata. Theoretical Computer Science 354(2):272-300. Elsevier, March 2006. 
@article{tcs354(2)-AAM,
  author =              {Abdedda{\"\i}m, Yasmina and Asarin, Eugene and
                         Maler, Oded},
  title =               {Scheduling with timed automata},
  publisher =           {Elsevier},
  journal =             {Theoretical Computer Science},
  volume =              {354},
  number =              {2},
  pages =               {272-300},
  year =                {2006},
  month =               mar,
}
[And06] Daniel Andersson. An improved algorithm for discounted payoff games. In Proceedings of the 11th ESSLLI Student Session, pages 91-98. August 2006. 
@inproceedings{esslli2006-students-And,
  author =              {Andersson, Daniel},
  title =               {An improved algorithm for discounted payoff games},
  editor =              {Huitink, Janneke and Katrenko, Sophia},
  booktitle =           {{P}roceedings of the 11th {ESSLLI} {S}tudent
                         {S}ession},
  pages =               {91-98},
  year =                {2006},
  month =               aug,
}
[AP06] Horacio Arló-Costa and Eric Pacuit. First-Order Classical Modal Logic. Studia Logica 84(2):171-210. Kluwer Academic, November 2006. 
@article{studlog84(2)-AP,
  author =              {Arl{\'o}{-}Costa, Horacio and Pacuit, Eric},
  title =               {First-Order Classical Modal Logic},
  publisher =           {Kluwer Academic},
  journal =             {Studia Logica},
  volume =              {84},
  number =              {2},
  pages =               {171-210},
  year =                {2006},
  month =               nov,
  doi =                 {10.1007/s11225-006-9010-0},
}
[BBF+06] Tomáš Brázdil, Václav Brožek, Vojtěch Forejt, and Antonín Kučera. Stochastic Games with Branching-Time Winning Objectives. In LICS'06, pages 349-358. IEEE Comp. Soc. Press, July 2006. 
@inproceedings{lics2006-BBFK,
  author =              {Br{\'a}zdil, Tom{\'a}{\v s} and V{\'a}clav
                         Bro{\v{z}}ek and Forejt, Vojt{\v{e}}ch and Ku{\v
                         c}era, Anton{\'\i}n},
  title =               {Stochastic Games with Branching-Time Winning
                         Objectives},
  booktitle =           {{P}roceedings of the 21st {A}nnual {S}ymposium on
                         {L}ogic in {C}omputer {S}cience ({LICS}'06)},
  acronym =             {{LICS}'06},
  publisher =           {IEEE Comp. Soc. Press},
  pages =               {349-358},
  year =                {2006},
  month =               jul,
}
[BBL+06] Gerd Behrmann, Patricia Bouyer, Kim Guldstrand Larsen, and Radek Pelánek. Lower and Upper Bounds in Zone-Based Abstractions of Timed Automata. International Journal on Software Tools for Technology Transfer 8(3):204-215. Springer-Verlag, June 2006. 
@article{sttt8(3)-BBLP,
  author =              {Behrmann, Gerd and Bouyer, Patricia and Larsen, Kim
                         Guldstrand and Pel{\'a}nek, Radek},
  title =               {Lower and Upper Bounds in Zone-Based Abstractions of
                         Timed Automata},
  publisher =           {Springer-Verlag},
  journal =             {International Journal on Software Tools for
                         Technology Transfer},
  volume =              {8},
  number =              {3},
  pages =               {204-215},
  year =                {2006},
  month =               jun,
  doi =                 {10.1007/s10009-005-0190-0},
}
[BBM06] Ramzi Ben Salah, Marius Bozga, and Oded Maler. On Interleaving in Timed Automata. In CONCUR'06, Lecture Notes in Computer Science 4137, pages 465-476. Springer-Verlag, August 2006. 
@inproceedings{concur2006-BBM,
  author =              {Ben{~}Salah, Ramzi and Bozga, Marius and Maler,
                         Oded},
  title =               {On Interleaving in Timed Automata},
  editor =              {Baier, {\relax Ch}ristel and Hermanns, Holger},
  booktitle =           {{P}roceedings of the 17th {I}nternational
                         {C}onference on {C}oncurrency {T}heory
                         ({CONCUR}'06)},
  acronym =             {{CONCUR}'06},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {4137},
  pages =               {465-476},
  year =                {2006},
  month =               aug,
}
[BC06] Patricia Bouyer and Fabrice Chevalier. On the Control of Timed and Hybrid Systems. EATCS Bulletin 89:79-96. EATCS, June 2006. 
@article{eatcs-bull89()-BC,
  author =              {Bouyer, Patricia and Chevalier, Fabrice},
  title =               {On the Control of Timed and Hybrid Systems},
  publisher =           {EATCS},
  journal =             {EATCS Bulletin},
  volume =              {89},
  pages =               {79-96},
  year =                {2006},
  month =               jun,
}
[BDH+06] Dietmar Berwanger, Anuj Dawar, Paul Hunter, and Stephan Kreutzer. DAG-Width and Parity Games. In STACS'06, Lecture Notes in Computer Science 3884, pages 524-536. Springer-Verlag, February 2006. 
@inproceedings{stacs2006-BDHK,
  author =              {Berwanger, Dietmar and Dawar, Anuj and Hunter, Paul
                         and Kreutzer, Stephan},
  title =               {{DAG}-Width and Parity Games},
  editor =              {Durand, Bruno and Thomas, Wolfgang},
  booktitle =           {{P}roceedings of the 23rd {S}ymposium on
                         {T}heoretical {A}spects of {C}omputer {S}cience
                         ({STACS}'06)},
  acronym =             {{STACS}'06},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {3884},
  pages =               {524-536},
  year =                {2006},
  month =               feb,
  doi =                 {10.1007/11672142_43},
}
[BDL+06] Gerd Behrmann, Alexandre David, Kim Guldstrand Larsen, John Håkansson, Paul Pettersson, Wang Yi, and Martijn Hendriks. UPPAAL 4.0. In QEST'06, pages 125-126. IEEE Comp. Soc. Press, September 2006. 
@inproceedings{qest2006-BDLHPYH,
  author =              {Behrmann, Gerd and David, Alexandre and Larsen, Kim
                         Guldstrand and H{\aa}kansson, John and Pettersson,
                         Paul and Yi, Wang and Hendriks, Martijn},
  title =               {UPPAAL~4.0},
  booktitle =           {{P}roceedings of the 3rd {I}nternational
                         {C}onference on {Q}uantitative {E}valuation of
                         {S}ystems ({QEST}'06)},
  acronym =             {{QEST}'06},
  publisher =           {IEEE Comp. Soc. Press},
  pages =               {125-126},
  year =                {2006},
  month =               sep,
  doi =                 {10.1109/QEST.2006.59},
}
[Bel06] Houda Bel Mokadem. Vérification des propriétés temporisées des automates programmables industriels. Thèse de doctorat, Lab. Spécification & Vérification, ENS Cachan, France, September 2006. 
@phdthesis{phd-belmokadem,
  author =              {Bel{~}Mokadem, Houda},
  title =               {V{\'e}rification des propri{\'e}t{\'e}s
                         temporis{\'e}es des automates programmables
                         industriels},
  year =                {2006},
  month =               sep,
  school =              {Lab.~Sp\'ecification \& V\'erification, ENS Cachan,
                         France},
  type =                {Th\`ese de doctorat},
}
[BH06] Bernard Boigelot and Frédéric Herbreteau. The Power of Hybrid Acceleration. In CAV'06, Lecture Notes in Computer Science 4144, pages 438-451. Springer-Verlag, July 2006. 
@inproceedings{cav2006-BH,
  author =              {Boigelot, Bernard and Herbreteau, Fr{\'e}d{\'e}ric},
  title =               {The Power of Hybrid Acceleration},
  editor =              {Ball, Thomas and Jones, Robert},
  booktitle =           {{P}roceedings of the 18th {I}nternational
                         {C}onference on {C}omputer {A}ided {V}erification
                         ({CAV}'06)},
  acronym =             {{CAV}'06},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {4144},
  pages =               {438-451},
  year =                {2006},
  month =               jul,
  doi =                 {10.1007/11817963_40},
}
[BHR06] Patricia Bouyer, Serge Haddad, and Pierre-Alain Reynier. Timed Unfoldings for Networks of Timed Automata. In ATVA'06, Lecture Notes in Computer Science 4218, pages 292-306. Springer-Verlag, October 2006. 
@inproceedings{atva2006-BHR,
  author =              {Bouyer, Patricia and Haddad, Serge and Reynier,
                         Pierre-Alain},
  title =               {Timed Unfoldings for Networks of Timed Automata},
  editor =              {Graf, Susanne and Zhang, Wenhui},
  booktitle =           {{P}roceedings of the 4th {I}nternational {S}ymposium
                         on {A}utomated {T}echnology for {V}erification and
                         {A}nalysis ({ATVA}'06)},
  acronym =             {{ATVA}'06},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {4218},
  pages =               {292-306},
  year =                {2006},
  month =               oct,
  doi =                 {10.1007/11901914_23},
}
[BIL06] Marius Bozga, Radu Iosif, and Yassine Lakhnech. Flat Parametric Counter Automata. Research Report TR-2005-15, Lab. VERIMAG, Grenoble, France, March 2006. 
@techreport{TR-verimag2005-15,
  author =              {Bozga, Marius and Iosif, Radu and Lakhnech, Yassine},
  title =               {Flat Parametric Counter Automata},
  number =              {TR-2005-15},
  year =                {2006},
  month =               mar,
  institution =         {Lab. VERIMAG, Grenoble, France},
  type =                {Research Report},
}
[BIL06] Marius Bozga, Radu Iosif, and Yassine Lakhnech. Flat Parametric Counter Automata. In ICALP'06, Lecture Notes in Computer Science 4052, pages 577-588. Springer-Verlag, July 2006. 
@inproceedings{icalp2006-BIL,
  author =              {Bozga, Marius and Iosif, Radu and Lakhnech, Yassine},
  title =               {Flat Parametric Counter Automata},
  editor =              {Bugliesi, Michele and Preneel, Bart and Sassone,
                         Vladimiro and Wegener, Ingo},
  booktitle =           {{P}roceedings of the 33rd {I}nternational
                         {C}olloquium on {A}utomata, {L}anguages and
                         {P}rogramming ({ICALP}'06))~-- Part~{II}},
  acronym =             {{ICALP}'06},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {4052},
  pages =               {577-588},
  year =                {2006},
  month =               jul,
  doi =                 {10.1007/11787006_49},
}
[BKM+06] Jeremy W. Bryans, Maciej Koutny, Laurent Mazaré, and Peter Y. A. Ryan. Opacity generalised to transition systems. In FAST'05, Lecture Notes in Computer Science 3866, pages 81-95. Springer-Verlag, 2006. 
@inproceedings{fast2005-BKMR,
  author =              {Bryans, Jeremy W. and Koutny, Maciej and Mazar{\'e},
                         Laurent and Ryan, Peter Y. A.},
  title =               {Opacity generalised to transition systems},
  editor =              {Dimitrakos, Theo and Martinelli, Fabio and Ryan,
                         Peter Y. A. and Schneider, Steve},
  booktitle =           {{R}evised {S}elected {P}apers of the 3rd
                         {I}nternational {W}orkshop on {F}ormal {A}spects in
                         {S}ecurity and {T}rust ({FAST}'05)},
  acronym =             {{FAST}'05},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {3866},
  pages =               {81-95},
  year =                {2006},
  confyear =            {2005},
  confmonth =           {7},
  doi =                 {10.1007/11679219_7},
}
[tC06] Balder ten Cate. Expressivity of Second Order Propositional Modal Logic. Journal of Philosophical Logic 35(2):209-223. Springer-Verlag, September 2006. 
@article{jpl35(2)-Cat,
  author =              {ten Cate, Balder},
  title =               {Expressivity of Second Order Propositional Modal
                         Logic},
  publisher =           {Springer-Verlag},
  journal =             {Journal of Philosophical Logic},
  volume =              {35},
  number =              {2},
  pages =               {209-223},
  year =                {2006},
  month =               sep,
}
[Cac06] Thierry Cachat. Tree Automata Make Ordinal Theory Easy. In FSTTCS'06, Lecture Notes in Computer Science 4337, pages 285-296. Springer-Verlag, December 2006. 
@inproceedings{fsttcs2006-Cac,
  author =              {Cachat, Thierry},
  title =               {Tree Automata Make Ordinal Theory Easy},
  editor =              {Arun-Kumar, S. and Garg, Naveen},
  booktitle =           {{P}roceedings of the 26th {C}onference on
                         {F}oundations of {S}oftware {T}echnology and
                         {T}heoretical {C}omputer {S}cience ({FSTTCS}'06)},
  acronym =             {{FSTTCS}'06},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {4337},
  pages =               {285-296},
  year =                {2006},
  month =               dec,
}
[CdA+06] Krishnendu Chatterjee, Luca de Alfaro, and Thomas A. Henzinger. The Complexity of Quantitative Concurrent Parity Games. In SODA'06, pages 678-687. Society for Industrial and Applied Math., January 2006. 
@inproceedings{soda2006-CdAH,
  author =              {Chatterjee, Krishnendu and de Alfaro, Luca and
                         Henzinger, Thomas A.},
  title =               {The Complexity of Quantitative Concurrent Parity
                         Games},
  booktitle =           {{P}roceedings of the 17th {A}nnual {ACM}-{SIAM}
                         {S}ymposium on {D}iscrete {A}lgorithms ({SODA}'06)},
  acronym =             {{SODA}'06},
  publisher =           {Society for Industrial and Applied Math.},
  pages =               {678-687},
  year =                {2006},
  month =               jan,
  doi =                 {10.1145/1109557.1109631},
}
[CdA+06] Krishnendu Chatterjee, Luca de Alfaro, and Thomas A. Henzinger. Strategy Improvement for Concurrent Reachability Games. In QEST'06, pages 291-300. IEEE Comp. Soc. Press, September 2006. 
@inproceedings{qest2006-CdAH,
  author =              {Chatterjee, Krishnendu and de Alfaro, Luca and
                         Henzinger, Thomas A.},
  title =               {Strategy Improvement for Concurrent Reachability
                         Games},
  booktitle =           {{P}roceedings of the 3rd {I}nternational
                         {C}onference on {Q}uantitative {E}valuation of
                         {S}ystems ({QEST}'06)},
  acronym =             {{QEST}'06},
  publisher =           {IEEE Comp. Soc. Press},
  pages =               {291-300},
  year =                {2006},
  month =               sep,
  doi =                 {10.1109/QEST.2006.48},
}
[CCJ06] Franck Cassez, Thomas Chatain, and Claude Jard. Symbolic Unfoldings for Networks of Timed Automata. In ATVA'06, Lecture Notes in Computer Science 4218, pages 307-321. Springer-Verlag, October 2006. 
@inproceedings{atva2006-CCJ,
  author =              {Cassez, Franck and Chatain, {\relax Th}omas and
                         Jard, Claude},
  title =               {Symbolic Unfoldings for Networks of Timed Automata},
  editor =              {Graf, Susanne and Zhang, Wenhui},
  booktitle =           {{P}roceedings of the 4th {I}nternational {S}ymposium
                         on {A}utomated {T}echnology for {V}erification and
                         {A}nalysis ({ATVA}'06)},
  acronym =             {{ATVA}'06},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {4218},
  pages =               {307-321},
  year =                {2006},
  month =               oct,
  doi =                 {10.1007/11901914_24},
}
[CDH+06] Krishnendu Chatterjee, Laurent Doyen, Thomas A. Henzinger, and Jean-François Raskin. Algorithms for Omega-Regular Games with Imperfect Information. In CSL'06, Lecture Notes in Computer Science 4207, pages 287-302. Springer-Verlag, September 2006. 
@inproceedings{csl2006-CDHR,
  author =              {Chatterjee, Krishnendu and Doyen, Laurent and
                         Henzinger, Thomas A. and Raskin, Jean-Fran{\c c}ois},
  title =               {Algorithms for Omega-Regular Games with Imperfect
                         Information},
  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 =               {287-302},
  year =                {2006},
  month =               sep,
}
[CHJ06] Krishnendu Chatterjee, Thomas A. Henzinger, and Marcin Jurdziński. Games with Secure Equilibria. Theoretical Computer Science 365(1-2):67-82. Elsevier, November 2006. 
@article{tcs365(1-2)-CHJ,
  author =              {Chatterjee, Krishnendu and Henzinger, Thomas A. and
                         Jurdzi{\'n}ski, Marcin},
  title =               {Games with Secure Equilibria},
  publisher =           {Elsevier},
  journal =             {Theoretical Computer Science},
  volume =              {365},
  number =              {1-2},
  pages =               {67-82},
  year =                {2006},
  month =               nov,
}
[CM06] Scott Cotton and Oded Maler. Fast and Flexible Difference Constraint Propagation for DPLL(T). In SAT'06, Lecture Notes in Computer Science 4121, pages 170-183. Springer-Verlag, August 2006. 
@inproceedings{sat2006-CM,
  author =              {Cotton, Scott and Maler, Oded},
  title =               {Fast and Flexible Difference Constraint Propagation
                         for {DPLL(T)}},
  editor =              {Biere, Armin and Gomes, Carla P.},
  booktitle =           {{P}roceedings of the 15th {I}nternational
                         {C}onference on {T}heory and {A}pplications of
                         {S}atisfiability {T}esting ({SAT}'06)},
  acronym =             {{SAT}'06},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {4121},
  pages =               {170-183},
  year =                {2006},
  month =               aug,
}
[CT06] Thomas M. Cover and Joy A. Thomas. Elements of Information Theory. John Wiley & Sons, 2006. 
@book{EIT2006-CT,
  author =              {Cover, Thomas M. and Thomas, Joy A.},
  title =               {Elements of Information Theory},
  publisher =           {John Wiley \& Sons},
  edition =             {2},
  year =                {2006},
}
[CTV06] Edmund M. Clarke, Muralidhar Talupur, and Helmut Veith. Environment Abstraction for Parameterized Verification. In VMCAI'06, Lecture Notes in Computer Science 3855, pages 126-141. Springer-Verlag, January 2006. 
@inproceedings{vmcai2006-CTV,
  author =              {Clarke, Edmund M. and Talupur, Muralidhar and Veith,
                         Helmut},
  title =               {Environment Abstraction for Parameterized
                         Verification},
  editor =              {Emerson, E. Allen and Namjoshi, Kedar},
  booktitle =           {{P}roceedings of the 7th {I}nternational {W}orkshop
                         on {V}erification, {M}odel {C}hecking, and
                         {A}bstract {I}nterpretation ({VMCAI}'06)},
  acronym =             {{VMCAI}'06},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {3855},
  pages =               {126-141},
  year =                {2006},
  month =               jan,
  doi =                 {10.1007/11609773_9},
}
[De06] Martin De Wulf. From Timed Models to Timed Implementations. Thèse de doctorat, Département d'Informatique, Université Libre de Bruxelles, Belgium, December 2006. 
@phdthesis{phd-dewulf,
  author =              {De{~}Wulf, Martin},
  title =               {From Timed Models to Timed Implementations},
  year =                {2006},
  month =               dec,
  school =              {D{\'e}partement d'Informatique, Universit{\'e} Libre
                         de Bruxelles, Belgium},
  type =                {Th\`ese de doctorat},
}
[DHL+06] Alexandre David, John Håkansson, Kim Guldstrand Larsen, and Paul Pettersson. Model Checking Timed Automata with Priorities Using DBM Subtraction. In FORMATS'06, Lecture Notes in Computer Science 4202, pages 128-142. Springer-Verlag, September 2006. 
@inproceedings{formats2006-DHLP,
  author =              {David, Alexandre and H{\aa}kansson, John and Larsen,
                         Kim Guldstrand and Pettersson, Paul},
  title =               {Model Checking Timed Automata with Priorities Using
                         {DBM} Subtraction},
  editor =              {Asarin, Eugene and Bouyer, Patricia},
  booktitle =           {{P}roceedings of the 4th {I}nternational
                         {C}onferences on {F}ormal {M}odelling and {A}nalysis
                         of {T}imed {S}ystems ({FORMATS}'06)},
  acronym =             {{FORMATS}'06},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {4202},
  pages =               {128-142},
  year =                {2006},
  month =               sep,
  doi =                 {10.1007/11867340_10},
}
[DK06] Conrado Daws and Piotr Kordy. Symbolic robustness analysis of timed automata. In FORMATS'06, Lecture Notes in Computer Science 4202, pages 143-155. Springer-Verlag, September 2006. 
@inproceedings{formats06-DK,
  author =              {Daws, Conrado and Kordy, Piotr},
  title =               {Symbolic robustness analysis of timed automata},
  editor =              {Asarin, Eugene and Bouyer, Patricia},
  booktitle =           {{P}roceedings of the 4th {I}nternational
                         {C}onferences on {F}ormal {M}odelling and {A}nalysis
                         of {T}imed {S}ystems ({FORMATS}'06)},
  acronym =             {{FORMATS}'06},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {4202},
  pages =               {143-155},
  year =                {2006},
  month =               sep,
}
[Doy06] Laurent Doyen. Algorithmic Analysis of Complex Semantics for Timed and Hybrid Automata. Thèse de doctorat, Département d'Informatique, Université Libre de Bruxelles, Belgium, June 2006. 
@phdthesis{phd-doyen,
  author =              {Doyen, Laurent},
  title =               {Algorithmic Analysis of Complex Semantics for Timed
                         and Hybrid Automata},
  year =                {2006},
  month =               jun,
  school =              {D{\'e}partement d'Informatique, Universit{\'e} Libre
                         de Bruxelles, Belgium},
  type =                {Th\`ese de doctorat},
}
[DPV06] Sanjoy Dasgupta, Christos H. Papadimitriou, and Vijay V. Vazirani. Algorithms. McGraw-Hill, 2006. 
@book{DPV06,
  author =              {Dasgupta, Sanjoy and Papadimitriou, {\relax
                         Ch}ristos H. and Vazirani, Vijay V.},
  title =               {Algorithms},
  publisher =           {McGraw-Hill},
  year =                {2006},
}
[FHB06] Márk Félegyházi, Jean-Pierre Hubaux, and Levente Buttyán. Nash Equilibria of Packet Forwarding Strategies in Wireless Ad Hoc Networks. IEEE Transactions on Mobile Computing 5(5):463-476. IEEE, May 2006. 
@article{tmc5(5)-FHB,
  author =              {F{\'e}legyh{\'a}zi, M{\'a}rk and Hubaux, Jean-Pierre
                         and Butty{\'a}n, Levente},
  title =               {{N}ash Equilibria of Packet Forwarding Strategies in
                         Wireless Ad~Hoc Networks},
  publisher =           {IEEE},
  journal =             {IEEE Transactions on Mobile Computing},
  volume =              {5},
  number =              {5},
  pages =               {463-476},
  year =                {2006},
  month =               may,
}
[Fin06] Olivier Finkel. Undecidable Problems About Timed Automata. In FORMATS'06, Lecture Notes in Computer Science 4202, pages 187-199. Springer-Verlag, September 2006. 
@inproceedings{formats2006-Fin,
  author =              {Finkel, Olivier},
  title =               {Undecidable Problems About Timed Automata},
  editor =              {Asarin, Eugene and Bouyer, Patricia},
  booktitle =           {{P}roceedings of the 4th {I}nternational
                         {C}onferences on {F}ormal {M}odelling and {A}nalysis
                         of {T}imed {S}ystems ({FORMATS}'06)},
  acronym =             {{FORMATS}'06},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {4202},
  pages =               {187-199},
  year =                {2006},
  month =               sep,
  doi =                 {10.1007/11867340_14},
}
[FKV06] Ehud Friedgut, Orna Kupferman, and Moshe Y. Vardi. Büchi Complementation Made Tighter. International Journal of Foundations of Computer Science 17(4):851-868. August 2006. 
@article{ijfcs17(4)-FKV,
  author =              {Friedgut, Ehud and Kupferman, Orna and Vardi, Moshe
                         Y.},
  title =               {B{\"u}chi Complementation Made Tighter},
  journal =             {International Journal of Foundations of Computer
                         Science},
  volume =              {17},
  number =              {4},
  pages =               {851-868},
  year =                {2006},
  month =               aug,
  doi =                 {10.1142/S0129054106004145},
}
[FMP+06] Elena Fersman, Leonid Mokrushin, Paul Pettersson, and Wang Yi. Schedulability analysis of fixed-priority systems using timed automata. Theoretical Computer Science 354(2):301-317. Elsevier, March 2006. 
@article{tcs354(2)-FMPY,
  author =              {Fersman, Elena and Mokrushin, Leonid and Pettersson,
                         Paul and Yi, Wang},
  title =               {Schedulability analysis of fixed-priority systems
                         using timed automata},
  publisher =           {Elsevier},
  journal =             {Theoretical Computer Science},
  volume =              {354},
  number =              {2},
  pages =               {301-317},
  year =                {2006},
  month =               mar,
}
[Fre06] Tim French. Bisimulation Quantifiers for Modal Logics. PhD thesis, School of Computer Science & Software Engineering, University of Western Australia, December 2006. 
@phdthesis{phd-french,
  author =              {French, Tim},
  title =               {Bisimulation Quantifiers for Modal Logics},
  year =                {2006},
  month =               dec,
  school =              {School of Computer Science \& Software Engineering,
                         University of Western Australia},
  type =                {{PhD} thesis},
}
[GvD06] Valentin Goranko and Govert van Drimmelen. Complete Axiomatization and decidability of Alternating-time Temporal Logic. Theoretical Computer Science 353(1-3):93-117. Elsevier, March 2006. 
@article{tcs353(1-3)-GvD,
  author =              {Goranko, Valentin and van Drimmelen, Govert},
  title =               {Complete Axiomatization and decidability of
                         Alternating-time Temporal Logic},
  publisher =           {Elsevier},
  journal =             {Theoretical Computer Science},
  volume =              {353},
  number =              {1-3},
  pages =               {93-117},
  year =                {2006},
  month =               mar,
}
[Gim06] Hugo Gimbert. Jeux positionnels. Thèse de doctorat, Lab. Informatique Algorithmique: Fondements et Applications, Université Paris 7, France, December 2006. 
@phdthesis{phd-gimbert,
  author =              {Gimbert, Hugo},
  title =               {Jeux positionnels},
  year =                {2006},
  month =               dec,
  school =              {Lab.~Informatique Algorithmique: Fondements et
                         Applications, Universit{\'e} Paris~7, France},
  type =                {Th\`ese de doctorat},
}
[GRV06] Gilles Geeraerts, Jean-François Raskin, and Laurent Van Begin. Expand, Enlarge and Check: New algorithms for the coverability problem of WSTS. Journal of Computer and System Sciences 72(1):180-203. Elsevier, February 2006. 
@article{jcss72(1)-GRV,
  author =              {Geeraerts, Gilles and Raskin, Jean-Fran{\c c}ois and
                         Van{~}Begin, Laurent},
  title =               {Expand, Enlarge and Check: New algorithms for the
                         coverability problem of~{WSTS}},
  publisher =           {Elsevier},
  journal =             {Journal of Computer and System Sciences},
  volume =              {72},
  number =              {1},
  pages =               {180-203},
  year =                {2006},
  month =               feb,
}
[GS06] Martin Grohe and Nicole Schweikardt. The Succinctness of First-Order Logic on Linear Orders. Logical Methods in Computer Science 1(1):1-25. June 2006. 
@article{lmcs1(1)-GS,
  author =              {Grohe, Martin and Schweikardt, Nicole},
  title =               {The Succinctness of First-Order Logic on Linear
                         Orders},
  journal =             {Logical Methods in Computer Science},
  volume =              {1},
  number =              {1},
  pages =               {1-25},
  year =                {2006},
  month =               jun,
}
[HKN+06] Andrew Hinton, Marta Kwiatkowska, Gethin Norman, and David Parker. PRISM: A Tool for Automatic Verification of Probabilistic Systems. In TACAS'06, Lecture Notes in Computer Science 3920, pages 441-444. Springer-Verlag, March 2006. 
@inproceedings{tacas2006-HKNP,
  author =              {Hinton, Andrew and Kwiatkowska, Marta and Norman,
                         Gethin and Parker, David},
  title =               {{PRISM}: A~Tool for Automatic Verification of
                         Probabilistic Systems},
  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 =               {441-444},
  year =                {2006},
  month =               mar,
}
[vdH+06] Wiebe van der Hoek, Alessio Lomuscio, and Michael Wooldridge. On the Complexity of Practical ATL Model Checking. In AAMAS'06, pages 201-208. ACM Press, May 2006. 
@inproceedings{aamas2006-HLW,
  author =              {van der Hoek, Wiebe and Lomuscio, Alessio and
                         Wooldridge, Michael},
  title =               {On the Complexity of Practical {ATL} Model Checking},
  editor =              {Nakashima, Hideyuki and Wellman, Michael P. and
                         Weiss, Gerhard and Stone, Peter},
  booktitle =           {{P}roceedings of the 5th {I}nternational {J}oint
                         {C}onference on {A}utonomous {A}gents and
                         {M}ultiagent {S}ystems ({AAMAS}'06)},
  acronym =             {{AAMAS}'06},
  publisher =           {ACM Press},
  pages =               {201-208},
  year =                {2006},
  month =               may,
}
[HvdN+06] Martijn Hendriks, Barend van den Nieuwelaar, and Frits Vaandrager. Model checker aided design of a controller for a wafer scanner. International Journal on Software Tools for Technology Transfer 8(6):633-647. Springer-Verlag, November 2006. 
@article{sttt8(6)-HVN,
  author =              {Hendriks, Martijn and van den Nieuwelaar, Barend and
                         Vaandrager, Frits},
  title =               {Model checker aided design of a controller for a
                         wafer scanner},
  publisher =           {Springer-Verlag},
  journal =             {International Journal on Software Tools for
                         Technology Transfer},
  volume =              {8},
  number =              {6},
  pages =               {633-647},
  year =                {2006},
  month =               nov,
}
[HP06] Thomas A. Henzinger and Vinayak S. Prabhu. Timed Alternating-Time Temporal Logic. In FORMATS'06, Lecture Notes in Computer Science 4202, pages 1-17. Springer-Verlag, September 2006. 
@inproceedings{formats2006-HP,
  author =              {Henzinger, Thomas A. and Prabhu, Vinayak S.},
  title =               {Timed Alternating-Time Temporal Logic},
  editor =              {Asarin, Eugene and Bouyer, Patricia},
  booktitle =           {{P}roceedings of the 4th {I}nternational
                         {C}onferences on {F}ormal {M}odelling and {A}nalysis
                         of {T}imed {S}ystems ({FORMATS}'06)},
  acronym =             {{FORMATS}'06},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {4202},
  pages =               {1-17},
  year =                {2006},
  month =               sep,
}
[HP06] Thomas A. Henzinger and Nir Piterman. Solving Games without Determinization. In CSL'06, Lecture Notes in Computer Science 4207, pages 395-410. Springer-Verlag, September 2006. 
@inproceedings{csl2006-HP,
  author =              {Henzinger, Thomas A. and Piterman, Nir},
  title =               {Solving Games without Determinization},
  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 =               {395-410},
  year =                {2006},
  month =               sep,
  doi =                 {10.1007/11874683_26},
}
[HR06] Yoram Hirshfeld and Alexander Rabinovich. An Expressive Temporal Logic for Real Time. In MFCS'06, Lecture Notes in Computer Science 4162, pages 492-504. Springer-Verlag, August 2006. 
@inproceedings{mfcs2006-HR,
  author =              {Hirshfeld, Yoram and Rabinovich, Alexander},
  title =               {An Expressive Temporal Logic for Real Time},
  editor =              {Kr{\'a}lovi{\v{c}}, Rastislav and Urzyczyn, Pawel},
  booktitle =           {{P}roceedings of the 31st {I}nternational
                         {S}ymposium on {M}athematical {F}oundations of
                         {C}omputer {S}cience ({MFCS}'06)},
  acronym =             {{MFCS}'06},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {4162},
  pages =               {492-504},
  year =                {2006},
  month =               aug,
}
[HS06] Thomas A. Henzinger and Joseph Sifakis. The Embedded Systems Design Challenge. In FM'06, Lecture Notes in Computer Science 4085, pages 1-15. Springer-Verlag, August 2006. 
@inproceedings{fm2006-HS,
  author =              {Henzinger, Thomas A. and Sifakis, Joseph},
  title =               {The Embedded Systems Design Challenge},
  editor =              {Misra, Jayadev and Nipkow, Tobias and Sekerinski,
                         Emil},
  booktitle =           {{P}roceedings of the 14th {I}nternational
                         {S}ymposium on {F}ormal {M}ethods ({FM}'06)},
  acronym =             {{FM}'06},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {4085},
  pages =               {1-15},
  year =                {2006},
  month =               aug,
  doi =                 {10.1007/11813040_1},
}
[JD06] Wojciech Jamroga and Jürgen Dix. Model Checking Abilities of Agents: A Closer Look. Technical Report IfI-06-02, Institut fúr Informatik, Technische Universität Clausthal, Germany, 2006. 
@techreport{IfI-06-02-JD,
  author =              {Jamroga, Wojciech and Dix, J{\"u}rgen},
  title =               {Model Checking Abilities of Agents: A Closer Look},
  number =              {IfI-06-02},
  year =                {2006},
  institution =         {Institut f{\'u}r Informatik, Technische
                         Universit{\"a}t Clausthal, Germany},
  type =                {Technical Report},
}
[KNP06] Marta Kwiatkowska, Gethin Norman, and David Parker. Symmetry Reduction for Probabilistic Model Checking. In CAV'06, Lecture Notes in Computer Science 4144, pages 234-248. Springer-Verlag, July 2006. 
@inproceedings{cav2006-KNP,
  author =              {Kwiatkowska, Marta and Norman, Gethin and Parker,
                         David},
  title =               {Symmetry Reduction for Probabilistic Model Checking},
  editor =              {Ball, Thomas and Jones, Robert},
  booktitle =           {{P}roceedings of the 18th {I}nternational
                         {C}onference on {C}omputer {A}ided {V}erification
                         ({CAV}'06)},
  acronym =             {{CAV}'06},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {4144},
  pages =               {234-248},
  year =                {2006},
  month =               jul,
  doi =                 {10.1007/11817963_23},
}
[Kop06] Eryk Kopczynski. Half-Positional Determinacy of Infinite Games. In ICALP'06, Lecture Notes in Computer Science 4052, pages 336-347. Springer-Verlag, July 2006. 
@inproceedings{icalp2006-Kop,
  author =              {Kopczynski, Eryk},
  title =               {Half-Positional Determinacy of Infinite Games},
  editor =              {Bugliesi, Michele and Preneel, Bart and Sassone,
                         Vladimiro and Wegener, Ingo},
  booktitle =           {{P}roceedings of the 33rd {I}nternational
                         {C}olloquium on {A}utomata, {L}anguages and
                         {P}rogramming ({ICALP}'06))~-- Part~{II}},
  acronym =             {{ICALP}'06},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {4052},
  pages =               {336-347},
  year =                {2006},
  month =               jul,
  doi =                 {10.1007/11787006_29},
}
[Koz06] Dexter C. Kozen. Coinductive Proof Principles for Stochastic Processes. In LICS'06, pages 359-366. IEEE Comp. Soc. Press, July 2006. 
@inproceedings{lics2006-koz,
  author =              {Kozen, Dexter C.},
  title =               {Coinductive Proof Principles for Stochastic
                         Processes},
  booktitle =           {{P}roceedings of the 21st {A}nnual {S}ymposium on
                         {L}ogic in {C}omputer {S}cience ({LICS}'06)},
  acronym =             {{LICS}'06},
  publisher =           {IEEE Comp. Soc. Press},
  pages =               {359-366},
  year =                {2006},
  month =               jul,
}
[KSV06] Orna Kupferman, Shmuel Safra, and Moshe Y. Vardi. Relating Word and Tree Automata. Annals of Pure and Applied Logic 138(1-3):126-146. Elsevier, March 2006. 
@article{apal138(1-3)-KSV,
  author =              {Kupferman, Orna and Safra, Shmuel and Vardi, Moshe
                         Y.},
  title =               {Relating Word and Tree Automata},
  publisher =           {Elsevier},
  journal =             {Annals of Pure and Applied Logic},
  volume =              {138},
  number =              {1-3},
  pages =               {126-146},
  year =                {2006},
  month =               mar,
}
[KV06] Orna Kupferman and Moshe Y. Vardi. Memoryful Branching-Time Logic. In LICS'06, pages 265-274. IEEE Comp. Soc. Press, July 2006. 
@inproceedings{lics2006-KV,
  author =              {Kupferman, Orna and Vardi, Moshe Y.},
  title =               {Memoryful Branching-Time Logic},
  booktitle =           {{P}roceedings of the 21st {A}nnual {S}ymposium on
                         {L}ogic in {C}omputer {S}cience ({LICS}'06)},
  acronym =             {{LICS}'06},
  publisher =           {IEEE Comp. Soc. Press},
  pages =               {265-274},
  year =                {2006},
  month =               jul,
}
[LP06] Kamal Lodaya and Paritosh K. Pandya. A Dose of Timed Logic, in Guarded Measure. In FORMATS'06, Lecture Notes in Computer Science 4202, pages 260-273. Springer-Verlag, September 2006. 
@inproceedings{formats2006-LP,
  author =              {Lodaya, Kamal and Pandya, Paritosh K.},
  title =               {A Dose of Timed Logic, in Guarded Measure},
  editor =              {Asarin, Eugene and Bouyer, Patricia},
  booktitle =           {{P}roceedings of the 4th {I}nternational
                         {C}onferences on {F}ormal {M}odelling and {A}nalysis
                         of {T}imed {S}ystems ({FORMATS}'06)},
  acronym =             {{FORMATS}'06},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {4202},
  pages =               {260-273},
  year =                {2006},
  month =               sep,
}
[McM06] Kenneth L. McMillan. Lazy Abstraction with Interpolants. In CAV'06, Lecture Notes in Computer Science 4144, pages 123-136. Springer-Verlag, July 2006. 
@inproceedings{cav2006-McM,
  author =              {McMillan, Kenneth L.},
  title =               {Lazy Abstraction with Interpolants},
  editor =              {Ball, Thomas and Jones, Robert},
  booktitle =           {{P}roceedings of the 18th {I}nternational
                         {C}onference on {C}omputer {A}ided {V}erification
                         ({CAV}'06)},
  acronym =             {{CAV}'06},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {4144},
  pages =               {123-136},
  year =                {2006},
  month =               jul,
  doi =                 {10.1007/11817963_14},
}
[MNP06] Oded Maler, Dejan Nickovic, and Amir Pnueli. From MITL to Timed Automata. In FORMATS'06, Lecture Notes in Computer Science 4202, pages 274-289. Springer-Verlag, September 2006. 
@inproceedings{formats2006-MNP,
  author =              {Maler, Oded and Nickovic, Dejan and Pnueli, Amir},
  title =               {From {MITL} to Timed Automata},
  editor =              {Asarin, Eugene and Bouyer, Patricia},
  booktitle =           {{P}roceedings of the 4th {I}nternational
                         {C}onferences on {F}ormal {M}odelling and {A}nalysis
                         of {T}imed {S}ystems ({FORMATS}'06)},
  acronym =             {{FORMATS}'06},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {4202},
  pages =               {274-289},
  year =                {2006},
  month =               sep,
}
[OW06] Joël Ouaknine and James Worrell. Safety Metric Temporal Logic is Fully Decidable. In TACAS'06, Lecture Notes in Computer Science 3920, pages 411-425. Springer-Verlag, March 2006. 
@inproceedings{tacas2006-OW,
  author =              {Ouaknine, Jo{\"e}l and Worrell, James},
  title =               {Safety Metric Temporal Logic is Fully Decidable},
  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 =               {411-425},
  year =                {2006},
  month =               mar,
}
[OW06] Joël Ouaknine and James Worrell. On Metric Temporal Logic and Faulty Turing Machines. In FoSSaCS'06, Lecture Notes in Computer Science 3921, pages 217-230. Springer-Verlag, March 2006. 
@inproceedings{fossacs2006-OW,
  author =              {Ouaknine, Jo{\"e}l and Worrell, James},
  title =               {On Metric Temporal Logic and Faulty {T}uring
                         Machines},
  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 =               {217-230},
  year =                {2006},
  month =               mar,
}
[QYZ+06] Lili Qiu, Richard Yang, Yin Zhang, and Scott Shenker. On selfish routing in internet-like environments. IEEE Transactions on Computers 14(4):725-738. IEEE Comp. Soc. Press, August 2006. 
@article{tn14(4)-QYZS,
  author =              {Qiu, Lili and Yang, Richard and Zhang, Yin and
                         Shenker, Scott},
  title =               {On selfish routing in internet-like environments},
  publisher =           {IEEE Comp. Soc. Press},
  journal =             {IEEE Transactions on Computers},
  volume =              {14},
  number =              {4},
  pages =               {725-738},
  year =                {2006},
  month =               aug,
  doi =                 {10.1109/TNET.2006.880179},
}
[RLS06] Jacob Illum Rasmussen, Kim Guldstrand Larsen, and K. Subramani. On using priced timed automata to achieve optimal scheduling. Formal Methods in System Design 29(1):97-114. Springer-Verlag, July 2006. 
@article{fmsd29(1)-RLS,
  author =              {Rasmussen, Jacob Illum and Larsen, Kim Guldstrand
                         and Subramani, K.},
  title =               {On using priced timed automata to achieve optimal
                         scheduling},
  publisher =           {Springer-Verlag},
  journal =             {Formal Methods in System Design},
  volume =              {29},
  number =              {1},
  pages =               {97-114},
  year =                {2006},
  month =               jul,
  doi =                 {10.1007/s10703-006-0014-1},
}
[RS06] Alexander Rabinovich and Philippe Schnoebelen. BTL2 and Expressive Completeness for ECTL+. Information and Computation 204(7):1023-1044. Elsevier, July 2006. 
@article{icomp204(7)-RS,
  author =              {Rabinovich, Alexander and Schnoebelen, {\relax
                         Ph}ilippe},
  title =               {{BTL}{\(_2\)} and Expressive Completeness for
                         {ECTL}{\(^+\)}},
  publisher =           {Elsevier},
  journal =             {Information and Computation},
  volume =              {204},
  number =              {7},
  pages =               {1023-1044},
  year =                {2006},
  month =               jul,
}
[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,
}
[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},
}
[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,
}
[Tau06] Heikko Tauriainen. Automata and Linear Temporal Logic: Translations with Transition-based Acceptance. Technical Report HUT-TCS-A104, Helsinki University of Technology, Finland, 2006. 
@techreport{hut-tcs-a104-Tau,
  author =              {Tauriainen, Heikko},
  title =               {Automata and Linear Temporal Logic: Translations
                         with Transition-based Acceptance},
  number =              {HUT-TCS-A104},
  year =                {2006},
  institution =         {Helsinki University of Technology, Finland},
}
[Tri06] Stavros Tripakis. Folk theorems on the determinization and minimization of timed automata. Information Processing Letters 99(6):222-226. Elsevier, September 2006. 
@article{ipl99(6)-Tri,
  author =              {Tripakis, Stavros},
  title =               {Folk theorems on the determinization and
                         minimization of timed automata},
  publisher =           {Elsevier},
  journal =             {Information Processing Letters},
  volume =              {99},
  number =              {6},
  pages =               {222-226},
  year =                {2006},
  month =               sep,
  doi =                 {10.1016/j.ipl.2006.04.015},
}
[Umm06] Michael Ummels. Rational Behavior and Strategy Construction in Infinite Multiplayer Games. In FSTTCS'06, Lecture Notes in Computer Science 4337, pages 212-223. Springer-Verlag, December 2006. 
@inproceedings{fsttcs2006-Umm,
  author =              {Ummels, Michael},
  title =               {Rational Behavior and Strategy Construction in
                         Infinite Multiplayer Games},
  editor =              {Arun-Kumar, S. and Garg, Naveen},
  booktitle =           {{P}roceedings of the 26th {C}onference on
                         {F}oundations of {S}oftware {T}echnology and
                         {T}heoretical {C}omputer {S}cience ({FSTTCS}'06)},
  acronym =             {{FSTTCS}'06},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {4337},
  pages =               {212-223},
  year =                {2006},
  month =               dec,
}
[Val06] Antti Valmari. What the Small Rubik's Cube Taught Me on Data Structures, Information Theory and Randomization. International Journal on Software Tools for Technology Transfer 8(3):180-194. Springer-Verlag, June 2006. 
@article{sttt8(3)-Val,
  author =              {Valmari, Antti},
  title =               {What the Small {R}ubik's Cube Taught Me on Data
                         Structures, Information Theory and Randomization},
  publisher =           {Springer-Verlag},
  journal =             {International Journal on Software Tools for
                         Technology Transfer},
  volume =              {8},
  number =              {3},
  pages =               {180-194},
  year =                {2006},
  month =               jun,
}
[VV06] Daniele Varacca and Hagen Völzer. Temporal Logics and Model Checking for Fairly Correct Systems. In LICS'06, pages 389-398. IEEE Comp. Soc. Press, July 2006. 
@inproceedings{lics2006-VV,
  author =              {Varacca, Daniele and V{\"o}lzer, Hagen},
  title =               {Temporal Logics and Model Checking for Fairly
                         Correct Systems},
  booktitle =           {{P}roceedings of the 21st {A}nnual {S}ymposium on
                         {L}ogic in {C}omputer {S}cience ({LICS}'06)},
  acronym =             {{LICS}'06},
  publisher =           {IEEE Comp. Soc. Press},
  pages =               {389-398},
  year =                {2006},
  month =               jul,
  doi =                 {10.1109/LICS.2006.49},
}
[WHY06] Farn Wang, Geng-Dian Huang, and Fang Yu. TCTL Inevitability Analysis of Dense-Time Systems: From Theory to Engineering. IEEE Transactions on Software Engineering 32(7):510-526. IEEE Comp. Soc. Press, July 2006. 
@article{tse32(7)-WHY,
  author =              {Wang, Farn and Huang, Geng-Dian and Yu, Fang},
  title =               {{TCTL} Inevitability Analysis of Dense-Time Systems:
                         From Theory to Engineering},
  publisher =           {IEEE Comp. Soc. Press},
  journal =             {IEEE Transactions on Software Engineering},
  volume =              {32},
  number =              {7},
  pages =               {510-526},
  year =                {2006},
  month =               jul,
}
[WLW+06] Dirk Walther, Carsten Lutz, Frank Wolter, and Michael Wooldridge. ATL Satisfiability is Indeed EXPTIME-Complete. Journal of Logic and Computation 16(6):765-787. Oxford University Press, December 2006. 
@article{jlc16(6)-WLWW,
  author =              {Walther, Dirk and Lutz, Carsten and Wolter, Frank
                         and Wooldridge, Michael},
  title =               {{ATL} Satisfiability is Indeed {EXPTIME}-Complete},
  publisher =           {Oxford University Press},
  journal =             {Journal of Logic and Computation},
  volume =              {16},
  number =              {6},
  pages =               {765-787},
  year =                {2006},
  month =               dec,
  doi =                 {10.1093/logcom/exl009},
}
[Yap06] Chee Yap. Is it Really Zero?. KIAS Newsletter 33. 2006. 
@article{kias33-Yap,
  author =              {Yap, Chee},
  title =               {Is it Really Zero?},
  journal =             {KIAS Newsletter},
  volume =              {33},
  year =                {2006},
}
List of authors