2004
[Mar04] Nicolas Markey. Past is for Free: On the Complexity of Verifying Linear Temporal Properties with Past. Acta Informatica 40(6-7):431-458. Springer-Verlag, May 2004.
Abstract

We study the complexity of satisfiability and model checking problems for fragments of linear-time temporal logic with past (PLTL). We consider many fragments of PLTL, obtained by restricting the set of allowed temporal modalities, the use of negations or the nesting of future formulas into past formulas. Our results strengthen the widely accepted fact that "past is for free", in the sense that allowing symmetric past-time modalities does not bring additional theoretical complexity. This result holds even for small fragments and even when nesting future formulas into past formulas.

@article{acta40(6-7)-Mar,
  author =              {Markey, Nicolas},
  title =               {Past is for Free: On the Complexity of Verifying
                         Linear Temporal Properties with Past},
  publisher =           {Springer-Verlag},
  journal =             {Acta Informatica},
  volume =              {40},
  number =              {6-7},
  pages =               {431-458},
  year =                {2004},
  month =               may,
  doi =                 {10.1007/s00236-003-0136-5},
  abstract =            {We study the complexity of satisfiability and model
                         checking problems for fragments of linear-time
                         temporal logic with past (PLTL). We consider many
                         fragments of PLTL, obtained by restricting the set
                         of allowed temporal modalities, the use of negations
                         or the nesting of future formulas into past
                         formulas. Our results strengthen the widely accepted
                         fact that {"}past is for free{"}, in the sense that
                         allowing symmetric past-time modalities does not
                         bring additional theoretical complexity. This result
                         holds even for small fragments and even when nesting
                         future formulas into past formulas.},
}
[MS04] Nicolas Markey and Philippe Schnoebelen. A PTIME-Complete Matching Problem for SLP-Compressed Words. Information Processing Letters 90(1):3-6. Elsevier, April 2004.
Abstract

SLP-compressed words are words given by simple deterministic grammars called "straight-line programs". We prove that the problem of deciding whether an SLP-compressed word is recognized by a FSA is complete for polynomial-time.

@article{ipl90(1)-MS,
  author =              {Markey, Nicolas and Schnoebelen, {\relax Ph}ilippe},
  title =               {A {PTIME}-Complete Matching Problem for
                         {SLP}-Compressed Words},
  publisher =           {Elsevier},
  journal =             {Information Processing Letters},
  volume =              {90},
  number =              {1},
  pages =               {3-6},
  year =                {2004},
  month =               apr,
  doi =                 {10.1016/j.ipl.2004.01.002},
  abstract =            {SLP-compressed words are words given by simple
                         deterministic grammars called {"}straight-line
                         programs{"}. We prove that the problem of deciding
                         whether an SLP-compressed word is recognized by a
                         FSA is complete for polynomial-time.},
}
[DCM+04] Jennifer M. Davoren, Vaughan Coulthard, Nicolas Markey, and Thomas Moor. Non-deterministic Temporal Logics for General Flow Systems. In HSCC'04, Lecture Notes in Computer Science 2993, pages 280-295. Springer-Verlag, March 2004.
Abstract

In this paper, we use the constructs of branching temporal logic to formalize reasoning about a class of general flow systems, including discrete-time transition systems, continuous-time differential inclusions, and hybrid-time systems such as hybrid automata. We introduce Full General Flow Logic, GFL*, which has essentially the same syntax as the well-known Full Computation Tree Logic, CTL*, but generalizes the semantics to general flow systems over arbitrary time-lines. We propose an axiomatic proof system for GFL* and establish its soundness w.r.t. the general flow semantics.

@inproceedings{hscc2004-DCMM,
  author =              {Davoren, Jennifer M. and Coulthard, Vaughan and
                         Markey, Nicolas and Moor, Thomas},
  title =               {Non-deterministic Temporal Logics for General Flow
                         Systems},
  editor =              {Alur, Rajeev and Pappas, George J.},
  booktitle =           {{P}roceedings of the 7th {I}nternational {W}orkshop
                         on {H}ybrid {S}ystems: {C}omputation and {C}ontrol
                         ({HSCC}'04)},
  acronym =             {{HSCC}'04},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {2993},
  pages =               {280-295},
  year =                {2004},
  month =               mar,
  doi =                 {10.1007/978-3-540-24743-2_19},
  abstract =            {In this paper, we use the constructs of branching
                         temporal logic to formalize reasoning about a class
                         of general flow systems, including discrete-time
                         transition systems, continuous-time differential
                         inclusions, and hybrid-time systems such as hybrid
                         automata. We introduce Full General Flow Logic,
                         GFL\(^*\), which has essentially the same syntax as
                         the well-known Full Computation Tree Logic,
                         CTL\(^*\), but generalizes the semantics to general
                         flow systems over arbitrary time-lines. We propose
                         an axiomatic proof system for GFL\(^*\) and
                         establish its soundness w.r.t. the general flow
                         semantics.},
}
[DDM+04] Martin De Wulf, Laurent Doyen, Nicolas Markey, and Jean-François Raskin. Robustness and Implementability of Timed Automata. In FORMATS-FTRTFT'04, Lecture Notes in Computer Science 3253, pages 118-133. Springer-Verlag, September 2004.
Abstract

In a former paper, we defined a new semantics for timed automata, the Almost ASAP semantics, which is parameterized by Δ to cope with the reaction delay of the controller. We showed that this semantics is implementable provided there exists a strictly positive value for the parameter Δ for which the strategy is correct. In this paper, we define the implementability problem to be the question of existence of such a Δ. We show that this question is closely related to a notion of robustness for timed automata defined in (A. Puri: Dynamical Properties of Timed Automata. FTRTFT, 1998) and prove that the implementability problem is decidable.

@inproceedings{ftrtft2004-DDMR,
  author =              {De{~}Wulf, Martin and Doyen, Laurent and Markey,
                         Nicolas and Raskin, Jean-Fran{\c c}ois},
  title =               {Robustness and Implementability of Timed Automata},
  editor =              {Lakhnech, Yassine and Yovine, Sergio},
  booktitle =           {{P}roceedings of the {J}oint {I}nternational
                         {C}onferences on {F}ormal {M}odelling and {A}nalysis
                         of {T}imed {S}ystems ({FORMATS}'04) and {F}ormal
                         {T}echniques in {R}eal-Time and {F}ault-Tolerant
                         {S}ystems ({FTRTFT}'04)},
  acronym =             {{FORMATS-FTRTFT}'04},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {3253},
  pages =               {118-133},
  year =                {2004},
  month =               sep,
  doi =                 {10.1007/978-3-540-30206-3_10},
  abstract =            {In a former paper, we defined a new semantics for
                         timed automata, the Almost ASAP semantics, which is
                         parameterized by \(\Delta\) to cope with the
                         reaction delay of the controller. We showed that
                         this semantics is implementable provided there
                         exists a strictly positive value for the parameter
                         \(\Delta\) for which the strategy is correct. In
                         this paper, we define the implementability problem
                         to be the question of existence of such a
                         \(\Delta\). We show that this question is closely
                         related to a notion of robustness for timed automata
                         defined in (A.~Puri: \textit{Dynamical Properties of
                         Timed Automata}. FTRTFT, 1998) and prove that the
                         implementability problem is decidable.},
}
[LMS04] François Laroussinie, Nicolas Markey, and Philippe Schnoebelen. Model Checking Timed Automata with One or Two Clocks. In CONCUR'04, Lecture Notes in Computer Science 3170, pages 387-401. Springer-Verlag, August 2004.
Abstract

In this paper, we study model checking of timed automata (TAs), and more precisely we aim at finding efficient model checking for subclasses of TAs. For this, we consider model checking TCTL and TCTL, over TAs with one clock or two clocks.

First we show that the reachability problem is NLOGSPACE-complete for one clock TAs (i.e. as complex as reachability in classical graphs) and we give a polynomial time algorithm for model checking TCTL, over this class of TAs. Secondly we show that model checking becomes PSPACE-complete for full TCTL over one clock TAs. We also show that model checking CTL (without any timing constraint) over two clock TAs is PSPACE-complete and that reachability is NP-hard.

@inproceedings{concur2004-LMS,
  author =              {Laroussinie, Fran{\c c}ois and Markey, Nicolas and
                         Schnoebelen, {\relax Ph}ilippe},
  title =               {Model Checking Timed Automata with One or Two
                         Clocks},
  editor =              {Gardner, {\relax Ph}ilippa and Yoshida, Nobuko},
  booktitle =           {{P}roceedings of the 15th {I}nternational
                         {C}onference on {C}oncurrency {T}heory
                         ({CONCUR}'04)},
  acronym =             {{CONCUR}'04},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {3170},
  pages =               {387-401},
  year =                {2004},
  month =               aug,
  doi =                 {10.1007/978-3-540-28644-8_25},
  abstract =            {In this paper, we study model checking of timed
                         automata (TAs), and more precisely we aim at finding
                         efficient model checking for subclasses of TAs. For
                         this, we consider model checking TCTL and TCTL, over
                         TAs with one clock or two clocks.\par First we show
                         that the reachability problem is NLOGSPACE-complete
                         for one clock TAs (i.e. as complex as reachability
                         in classical graphs) and we give a polynomial time
                         algorithm for model checking TCTL, over this class
                         of TAs. Secondly we show that model checking becomes
                         PSPACE-complete for full TCTL over one clock TAs. We
                         also show that model checking CTL (without any
                         timing constraint) over two clock TAs is
                         PSPACE-complete and that reachability is NP-hard.},
}
[MR04] Nicolas Markey and Jean-François Raskin. Model Checking Restricted Sets of Timed Paths. In CONCUR'04, Lecture Notes in Computer Science 3170, pages 432-447. Springer-Verlag, August 2004.
Abstract

In this paper, we study the complexity of model-checking formulas of three important real-time logics (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) a infinite set of finite (or infinite) timed paths defined by a finite (or ultimately periodic) path in a region graph, (iii) a infinite set of finite (or infinite) timed paths defined by a finite (or ultimately periodic) path in a zone graph.

@inproceedings{concur2004-MR,
  author =              {Markey, Nicolas and Raskin, Jean-Fran{\c c}ois},
  title =               {Model Checking Restricted Sets of Timed Paths},
  editor =              {Gardner, {\relax Ph}ilippa and Yoshida, Nobuko},
  booktitle =           {{P}roceedings of the 15th {I}nternational
                         {C}onference on {C}oncurrency {T}heory
                         ({CONCUR}'04)},
  acronym =             {{CONCUR}'04},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {3170},
  pages =               {432-447},
  year =                {2004},
  month =               aug,
  doi =                 {10.1007/978-3-540-28644-8_28},
  abstract =            {In this paper, we study the complexity of
                         model-checking formulas of three important real-time
                         logics (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)} a infinite set of finite (or infinite)
                         timed paths defined by a finite (or ultimately
                         periodic) path in a region graph, \textit{(iii)} a
                         infinite set of finite (or infinite) timed paths
                         defined by a finite (or ultimately periodic) path in
                         a zone graph.},
}
[MS04] Nicolas Markey and Philippe Schnoebelen. Symbolic Model Checking for Simply Timed Systems. In FORMATS-FTRTFT'04, Lecture Notes in Computer Science 3253, pages 102-117. Springer-Verlag, September 2004.
Abstract

We describe OBDD-based symbolic model checking algorithms for simply-timed systems, i.e. finite state graphs where transitions carry a duration. These durations can be arbitrary natural numbers. A simple and natural semantics for these systems opens the way for improved efficiency. Our algorithms have been implemented in NuSMV and perform well in practice (on standard case studies).

@inproceedings{formats2004-MS,
  author =              {Markey, Nicolas and Schnoebelen, {\relax Ph}ilippe},
  title =               {Symbolic Model Checking for Simply Timed Systems},
  editor =              {Lakhnech, Yassine and Yovine, Sergio},
  booktitle =           {{P}roceedings of the {J}oint {I}nternational
                         {C}onferences on {F}ormal {M}odelling and {A}nalysis
                         of {T}imed {S}ystems ({FORMATS}'04) and {F}ormal
                         {T}echniques in {R}eal-Time and {F}ault-Tolerant
                         {S}ystems ({FTRTFT}'04)},
  acronym =             {{FORMATS-FTRTFT}'04},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {3253},
  pages =               {102-117},
  year =                {2004},
  month =               sep,
  doi =                 {10.1007/978-3-540-30206-3_9},
  abstract =            {We describe OBDD-based symbolic model checking
                         algorithms for simply-timed systems, i.e. finite
                         state graphs where transitions carry a duration.
                         These durations can be arbitrary natural numbers.
                         A~simple and natural semantics for these systems
                         opens the way for improved efficiency. Our
                         algorithms have been implemented in NuSMV and
                         perform well in practice (on standard case
                         studies).},
}
[ABM04] Rajeev Alur, Mikhail Bernadsky, and Parthasarathy Madhusudan. Optimal Reachability for Weighted Timed Games. In ICALP'04, Lecture Notes in Computer Science, pages 122-133. Springer-Verlag, 2004. 
@inproceedings{icalp2004-ABM,
  author =              {Alur, Rajeev and Bernadsky, Mikhail and Madhusudan,
                         Parthasarathy},
  title =               {Optimal Reachability for Weighted Timed Games},
  booktitle =           {{P}roceedings of the 31st {I}nternational
                         {C}olloquium on {A}utomata, {L}anguages and
                         {P}rogramming ({ICALP}'04)},
  acronym =             {{ICALP}'04},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  pages =               {122-133},
  year =                {2004},
}
[ADK+04] Elliot Anshelevich, Anirban Dasgupta, Jon Kleinberg, Éva Tardos, Tom Wexler, and Tim Roughgarden. The Price of Stability for Network Design with Fair Cost Allocation. In FOCS'04, pages 295-304. IEEE Comp. Soc. Press, October 2004. 
@inproceedings{focs2004-ADKTWR,
  author =              {Anshelevich, Elliot and Dasgupta, Anirban and
                         Kleinberg, Jon and Tardos, {\'E}va and Wexler, Tom
                         and Roughgarden, Tim},
  title =               {The Price of Stability for Network Design with Fair
                         Cost Allocation},
  booktitle =           {{P}roceedings of the 45th {A}nnual {S}ymposium on
                         {F}oundations of {C}omputer {S}cience ({FOCS}'04)},
  acronym =             {{FOCS}'04},
  publisher =           {IEEE Comp. Soc. Press},
  pages =               {295-304},
  year =                {2004},
  month =               oct,
  doi =                 {10.1109/FOCS.2004.68},
}
[ADM04] Parosh Aziz Abdulla, Johann Deneux, and Pritha Mahata. Multi-clock timed networks. In LICS'04, pages 345-354. IEEE Comp. Soc. Press, July 2004. 
@inproceedings{lics2004-ADM,
  author =              {Abdulla, Parosh Aziz and Deneux, Johann and Mahata,
                         Pritha},
  title =               {Multi-clock timed networks},
  booktitle =           {{P}roceedings of the 19th {A}nnual {S}ymposium on
                         {L}ogic in {C}omputer {S}cience ({LICS}'04)},
  acronym =             {{LICS}'04},
  publisher =           {IEEE Comp. Soc. Press},
  pages =               {345-354},
  year =                {2004},
  month =               jul,
  doi =                 {10.1109/LICS.2004.1319629},
}
[AJN+04] Parosh Aziz Abdulla, Bengt Jonsson, Marcus Nilsson, and Mayank Saksena. A Survey of Regular Model Checking. In CONCUR'04, Lecture Notes in Computer Science 3170, pages 35-48. Springer-Verlag, August 2004. 
@inproceedings{concur2004-AJNS,
  author =              {Abdulla, Parosh Aziz and Jonsson, Bengt and Nilsson,
                         Marcus and Saksena, Mayank},
  title =               {A Survey of Regular Model Checking},
  editor =              {Gardner, {\relax Ph}ilippa and Yoshida, Nobuko},
  booktitle =           {{P}roceedings of the 15th {I}nternational
                         {C}onference on {C}oncurrency {T}heory
                         ({CONCUR}'04)},
  acronym =             {{CONCUR}'04},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {3170},
  pages =               {35-48},
  year =                {2004},
  month =               aug,
  doi =                 {10.1007/978-3-540-28644-8_3},
}
[AL04] Rajeev Alur and Salvatore La Torre. Deterministic Generators and Games for LTL Fragments. ACM Transactions on Computational Logic 5(1):297-322. ACM Press, January 2004. 
@article{tocl5(1)-AL,
  author =              {Alur, Rajeev and La{~}Torre, Salvatore},
  title =               {Deterministic Generators and Games for {LTL}
                         Fragments},
  publisher =           {ACM Press},
  journal =             {ACM Transactions on Computational Logic},
  volume =              {5},
  number =              {1},
  pages =               {297-322},
  year =                {2004},
  month =               jan,
}
[ALP04] Rajeev Alur, Salvatore La Torre, and George J. Pappas. Optimal paths in weighted timed automata. Theoretical Computer Science 318(3):297-322. Elsevier, June 2004. 
@article{tcs318(3)-ALP,
  author =              {Alur, Rajeev and La{~}Torre, Salvatore and Pappas,
                         George J.},
  title =               {Optimal paths in weighted timed automata},
  publisher =           {Elsevier},
  journal =             {Theoretical Computer Science},
  volume =              {318},
  number =              {3},
  pages =               {297-322},
  year =                {2004},
  month =               jun,
  doi =                 {10.1016/j.tcs.2003.10.038},
}
[AM04] Rajeev Alur and Parthasarathy Madhusudan. Decision Problems for Timed Automata: A Survey. In SFM-RT'04, Lecture Notes in Computer Science 3185, pages 1-24. Springer-Verlag, September 2004. 
@inproceedings{sfm2004-AM,
  author =              {Alur, Rajeev and Madhusudan, Parthasarathy},
  title =               {Decision Problems for Timed Automata: A~Survey},
  editor =              {Bernardo, Marco and Corradini, Flavio},
  booktitle =           {{F}ormal {M}ethods for the {D}esign of {R}eal-{T}ime
                         {S}ystems~--- {R}evised {L}ectures of the
                         {I}nternational {S}chool on {F}ormal {M}ethods for
                         the {D}esign of {C}omputer, {C}ommunication and
                         {S}oftware {S}ystems ({SFM-RT}'04)},
  acronym =             {{SFM-RT}'04},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {3185},
  pages =               {1-24},
  year =                {2004},
  month =               sep,
}
[AS04] Robert Airapetyan and Thorsten Schneider. Protecting Applications with Petri Nets. The Code Breaker's Journal 1(1). 2004. 
@article{cbj1(1)-AS,
  author =              {Airapetyan, Robert and Schneider, Thorsten},
  title =               {Protecting Applications with {P}etri Nets},
  journal =             {The Code Breaker's Journal},
  volume =              {1},
  number =              {1},
  year =                {2004},
}
[BB04] Laura Brandán Briones and Ed Brinksma. A Test Generation Framework for Quiescent Real-Time Systems. In FATES'04, Lecture Notes in Computer Science 3395, pages 64-78. Springer-Verlag, September 2004. 
@inproceedings{BB-fates2004,
  author =              {Briones, Laura Brand{\'a}n and Brinksma, Ed},
  title =               {A~Test Generation Framework for Quiescent Real-Time
                         Systems},
  editor =              {Grabowski, Jens and Nielsen, Brian},
  booktitle =           {{P}roceedings of the 4th {I}nternational {W}orkshop
                         on {F}ormal {A}pproaches to {S}oftware {T}esting
                         ({FATES}'04)},
  acronym =             {{FATES}'04},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {3395},
  pages =               {64-78},
  year =                {2004},
  month =               sep,
  doi =                 {10.1007/978-3-540-31848-4_5},
}
[BBL04] Patricia Bouyer, Ed Brinksma, and Kim Guldstrand Larsen. Staying Alive as Cheaply as Possible. In HSCC'04, Lecture Notes in Computer Science 2993, pages 203-218. Springer-Verlag, March 2004. 
@inproceedings{hscc2004-BBL,
  author =              {Bouyer, Patricia and Brinksma, Ed and Larsen, Kim
                         Guldstrand},
  title =               {Staying Alive as Cheaply as Possible},
  editor =              {Alur, Rajeev and Pappas, George J.},
  booktitle =           {{P}roceedings of the 7th {I}nternational {W}orkshop
                         on {H}ybrid {S}ystems: {C}omputation and {C}ontrol
                         ({HSCC}'04)},
  acronym =             {{HSCC}'04},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {2993},
  pages =               {203-218},
  year =                {2004},
  month =               mar,
}
[BBL+04] Gerd Behrmann, Patricia Bouyer, Kim Guldstrand Larsen, and Radek Pelánek. Lower and Upper Bounds in Zone-Based Abstractions of Timed Automata. In TACAS'04, Lecture Notes in Computer Science 2988, pages 312-326. Springer-Verlag, March 2004. 
@inproceedings{tacas2004-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},
  editor =              {Jensen, Kurt and Podelski, Andreas},
  booktitle =           {{P}roceedings of the 10th {I}nternational
                         {C}onference on {T}ools and {A}lgorithms for
                         {C}onstruction and {A}nalysis of {S}ystems
                         ({TACAS}'04)},
  acronym =             {{TACAS}'04},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {2988},
  pages =               {312-326},
  year =                {2004},
  month =               mar,
  doi =                 {10.1007/978-3-540-24730-2_25},
}
[BBR04] Thomas Brihaye, Véronique Bruyère, and Jean-François Raskin. Model-checking for weighted timed automata. In FORMATS-FTRTFT'04, Lecture Notes in Computer Science 3253, pages 277-292. Springer-Verlag, September 2004. 
@inproceedings{formats2004-BBR,
  author =              {Brihaye, {\relax Th}omas and Bruy{\`e}re,
                         V{\'e}ronique and Raskin, Jean-Fran{\c c}ois},
  title =               {Model-checking for weighted timed automata},
  editor =              {Lakhnech, Yassine and Yovine, Sergio},
  booktitle =           {{P}roceedings of the {J}oint {I}nternational
                         {C}onferences on {F}ormal {M}odelling and {A}nalysis
                         of {T}imed {S}ystems ({FORMATS}'04) and {F}ormal
                         {T}echniques in {R}eal-Time and {F}ault-Tolerant
                         {S}ystems ({FTRTFT}'04)},
  acronym =             {{FORMATS-FTRTFT}'04},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {3253},
  pages =               {277-292},
  year =                {2004},
  month =               sep,
}
[BCF+04] Patricia Bouyer, Franck Cassez, Emmanuel Fleury, and Kim Guldstrand Larsen. Optimal Strategies in Priced Timed Game Automata. In FSTTCS'04, Lecture Notes in Computer Science 3328, pages 148-160. Springer-Verlag, December 2004. 
@inproceedings{fsttcs2004-BCFL,
  author =              {Bouyer, Patricia and Cassez, Franck and Fleury,
                         Emmanuel and Larsen, Kim Guldstrand},
  title =               {Optimal Strategies in Priced Timed Game Automata},
  editor =              {Lodaya, Kamal and Mahajan, Meena},
  booktitle =           {{P}roceedings of the 24th {C}onference on
                         {F}oundations of {S}oftware {T}echnology and
                         {T}heoretical {C}omputer {S}cience ({FSTTCS}'04)},
  acronym =             {{FSTTCS}'04},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {3328},
  pages =               {148-160},
  year =                {2004},
  month =               dec,
}
[BCF+04] Patricia Bouyer, Franck Cassez, Emmanuel Fleury, and Kim Guldstrand Larsen. Optimal Strategies in Priced Timed Games. Research Report RS-04-4, Basic Research in Computer Science, Aalborg University, Denmark, February 2004. 
@techreport{TR-brics04-4,
  author =              {Bouyer, Patricia and Cassez, Franck and Fleury,
                         Emmanuel and Larsen, Kim Guldstrand},
  title =               {Optimal Strategies in Priced Timed Games},
  number =              {RS-04-4},
  year =                {2004},
  month =               feb,
  institution =         {Basic Research in Computer Science, Aalborg
                         University, Denmark},
  type =                {Research Report},
}
[BDF+04] Patricia Bouyer, Catherine Dufourd, Emmanuel Fleury, and Antoine Petit. Updatable timed Automata. Theoretical Computer Science 321(2-3):291-345. Elsevier, August 2004. 
@article{tcs321(2-3)-BDFP,
  author =              {Bouyer, Patricia and Dufourd, Catherine and Fleury,
                         Emmanuel and Petit, Antoine},
  title =               {Updatable timed Automata},
  publisher =           {Elsevier},
  journal =             {Theoretical Computer Science},
  volume =              {321},
  number =              {2-3},
  pages =               {291-345},
  year =                {2004},
  month =               aug,
  doi =                 {10.1016/j.tcs.2004.04.003},
}
[BDL04] Gerd Behrmann, Alexandre David, and Kim Guldstrand Larsen. A Tutorial on Uppaal. In SFM-RT'04, Lecture Notes in Computer Science 3185, pages 200-236. Springer-Verlag, September 2004. 
@inproceedings{sfm2004-BDL,
  author =              {Behrmann, Gerd and David, Alexandre and Larsen, Kim
                         Guldstrand},
  title =               {A~Tutorial on {U}ppaal},
  editor =              {Bernardo, Marco and Corradini, Flavio},
  booktitle =           {{F}ormal {M}ethods for the {D}esign of {R}eal-{T}ime
                         {S}ystems~--- {R}evised {L}ectures of the
                         {I}nternational {S}chool on {F}ormal {M}ethods for
                         the {D}esign of {C}omputer, {C}ommunication and
                         {S}oftware {S}ystems ({SFM-RT}'04)},
  acronym =             {{SFM-RT}'04},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {3185},
  pages =               {200-236},
  year =                {2004},
  month =               sep,
  doi =                 {10.1007/978-3-540-30080-9_7},
}
[BG04] Dietmar Berwanger and Erich Grädel. Fixed-Point Logics and Solitaire Games. Theory of Computing Systems 37(6):675-694. Springer-Verlag, December 2004. 
@article{TCSyst37(6)-BG,
  author =              {Berwanger, Dietmar and Gr{\"a}del, Erich},
  title =               {Fixed-Point Logics and Solitaire Games},
  publisher =           {Springer-Verlag},
  journal =             {Theory of Computing Systems},
  volume =              {37},
  number =              {6},
  pages =               {675-694},
  year =                {2004},
  month =               dec,
  doi =                 {10.1007/s00224-004-1147-5},
}
[BH04] Anne Bergeron and Sylvie Hamel. From Cascade Decompositions to Bit-Vector Algorithms. Theoretical Computer Science 313(1):3-16. Elsevier, February 2004. 
@article{tcs313(1)-BH,
  author =              {Bergeron, Anne and Hamel, Sylvie},
  title =               {From Cascade Decompositions to Bit-Vector
                         Algorithms},
  publisher =           {Elsevier},
  journal =             {Theoretical Computer Science},
  volume =              {313},
  number =              {1},
  pages =               {3-16},
  year =                {2004},
  month =               feb,
}
[BO04] Stephen J. Bellantoni and Isabel Oitavem. Separating NC along the δ axis. Theoretical Computer Science 318(1-2):57-78. Elsevier, June 2004. 
@article{tcs318(1-2)-BO,
  author =              {Bellantoni, Stephen J. and Oitavem, Isabel},
  title =               {Separating {{\(\mathrm{NC}\)}} along the
                         {{\(\delta\)}} axis},
  publisher =           {Elsevier},
  journal =             {Theoretical Computer Science},
  volume =              {318},
  number =              {1-2},
  pages =               {57-78},
  year =                {2004},
  month =               jun,
  doi =                 {10.1016/j.tcs.2003.10.021},
}
[Bou04] Patricia Bouyer. Forward Analysis of Updatable Timed Automata. Formal Methods in System Design 24(3):281-320. Kluwer Academic, May 2004. 
@article{fmsd24(3)-Bou,
  author =              {Bouyer, Patricia},
  title =               {Forward Analysis of Updatable Timed Automata},
  publisher =           {Kluwer Academic},
  journal =             {Formal Methods in System Design},
  volume =              {24},
  number =              {3},
  pages =               {281-320},
  year =                {2004},
  month =               may,
  doi =                 {10.1023/B:FORM.0000026093.21513.31},
}
[BSV04] Henrik Björklund, Sven Sandberg, and Sergei Vorobyov. Memoryless Determinacy of Parity and Mean Payoff Games: A Simple Proof. Theoretical Computer Science 310(1-3):365-378. Elsevier, January 2004. 
@article{tcs310(1-3)-BSV,
  author =              {Bj{\"o}rklund, Henrik and Sandberg, Sven and
                         Vorobyov, Sergei},
  title =               {Memoryless Determinacy of Parity and Mean Payoff
                         Games: A~Simple Proof},
  publisher =           {Elsevier},
  journal =             {Theoretical Computer Science},
  volume =              {310},
  number =              {1-3},
  pages =               {365-378},
  year =                {2004},
  month =               jan,
  doi =                 {10.1016/S0304-3975(03)00427-4},
}
[BY04] Johan Bengtsson and Wang Yi. Timed Automata: Semantics, Algorithms and Tools. In Jörg Desel, Wolfgang Reisig, and Grzegorz Rozenberg (eds.), Lectures on Concurrency and Petri Nets, Lecture Notes in Computer Science 2098, pages 87-124. Springer-Verlag, 2004. 
@incollection{lncs3098-BY,
  author =              {Bengtsson, Johan and Yi, Wang},
  title =               {Timed Automata: Semantics, Algorithms and Tools},
  editor =              {Desel, J{\"o}rg and Reisig, Wolfgang and Rozenberg,
                         Grzegorz},
  booktitle =           {Lectures on Concurrency and {P}etri Nets},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {2098},
  pages =               {87-124},
  year =                {2004},
  doi =                 {10.1007/b98282},
}
[CAM+04] Scott Cotton, Eugene Asarin, Oded Maler, and Peter Niebert. Some Progress in Satisfiability Checking for Difference Logic. In FORMATS-FTRTFT'04, Lecture Notes in Computer Science 3253, pages 263-276. Springer-Verlag, September 2004. 
@inproceedings{formats2004-CAMN,
  author =              {Cotton, Scott and Asarin, Eugene and Maler, Oded and
                         Niebert, Peter},
  title =               {Some Progress in Satisfiability Checking for
                         Difference Logic},
  editor =              {Lakhnech, Yassine and Yovine, Sergio},
  booktitle =           {{P}roceedings of the {J}oint {I}nternational
                         {C}onferences on {F}ormal {M}odelling and {A}nalysis
                         of {T}imed {S}ystems ({FORMATS}'04) and {F}ormal
                         {T}echniques in {R}eal-Time and {F}ault-Tolerant
                         {S}ystems ({FTRTFT}'04)},
  acronym =             {{FORMATS-FTRTFT}'04},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {3253},
  pages =               {263-276},
  year =                {2004},
  month =               sep,
}
[CDC04] Krishnendu Chatterjee, Pallab Dasgupta, and P. P. Chakrabarti. The power of first-order quantification over states in branching and linear time temporal logics. Information Processing Letters 91(5):201-210. Elsevier, September 2004. 
@article{ipl91(5)-CDC,
  author =              {Chatterjee, Krishnendu and Dasgupta, Pallab and
                         Chakrabarti, P. P.},
  title =               {The power of first-order quantification over states
                         in branching and linear time temporal logics},
  publisher =           {Elsevier},
  journal =             {Information Processing Letters},
  volume =              {91},
  number =              {5},
  pages =               {201-210},
  year =                {2004},
  month =               sep,
}
[CHJ04] Krishnendu Chatterjee, Thomas A. Henzinger, and Marcin Jurdziński. Games with Secure Equilibria. In LICS'04, pages 160-169. IEEE Comp. Soc. Press, July 2004. 
@inproceedings{lics2004-CHJ,
  author =              {Chatterjee, Krishnendu and Henzinger, Thomas A. and
                         Jurdzi{\'n}ski, Marcin},
  title =               {Games with Secure Equilibria},
  booktitle =           {{P}roceedings of the 19th {A}nnual {S}ymposium on
                         {L}ogic in {C}omputer {S}cience ({LICS}'04)},
  acronym =             {{LICS}'04},
  publisher =           {IEEE Comp. Soc. Press},
  pages =               {160-169},
  year =                {2004},
  month =               jul,
}
[CMJ04] Krishnendu Chatterjee, Rupak Majumdar, and Marcin Jurdziński. On Nash equilibria in stochastic games. In CSL'04, Lecture Notes in Computer Science 3210. Springer-Verlag, September 2004. 
@inproceedings{csl2004-CMJ,
  author =              {Chatterjee, Krishnendu and Majumdar, Rupak and
                         Jurdzi{\'n}ski, Marcin},
  title =               {On {N}ash equilibria in stochastic games},
  editor =              {Marcinkowski, Jerzy and Tarlecki, Andrzej},
  booktitle =           {{P}roceedings of the 18th {I}nternational {W}orkshop
                         on {C}omputer {S}cience {L}ogic ({CSL}'04)},
  acronym =             {{CSL}'04},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {3210},
  year =                {2004},
  month =               sep,
}
[CMP04] Ching-Tsun Chou, Phanindra K. Mannava, and Seungjoon Park. A Simple Method for Parameterized Verification of Cache Coherence Protocols. In FMCAD'04, Lecture Notes in Computer Science 3312, pages 382-398. Springer-Verlag, November 2004. 
@inproceedings{fmcad2004-CMP,
  author =              {Chou, Ching-Tsun and Mannava, Phanindra K. and Park,
                         Seungjoon},
  title =               {A Simple Method for Parameterized Verification of
                         Cache Coherence Protocols},
  editor =              {Hu, Alan J. and Martin, Andrew K.},
  booktitle =           {{P}roceedings of the 5th {I}nternational
                         {C}onference on {F}ormal {M}ethods in
                         {C}omputer-{A}ided {D}esign ({FMCAD}'04)},
  acronym =             {{FMCAD}'04},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {3312},
  pages =               {382-398},
  year =                {2004},
  month =               nov,
  doi =                 {10.1007/978-3-540-30494-4_27},
}
[Coo04] Stephen A. Cook. Theories for Complexity Classes and their Propositional Translations. In Jan Krajíček (eds.), Complexity of computations and proofs, Quaderni di Matematica 13, pages 175-227. Dipartimento di Matematica, Seconda Universitá degli Studi di Napoli, Italy, 2004. 
@incollection{CCP2004-cook,
  author =              {Cook, Stephen A.},
  title =               {Theories for Complexity Classes and their
                         Propositional Translations},
  editor =              {Kraj{\'\i}{\v c}ek, Jan},
  booktitle =           {Complexity of computations and proofs},
  publisher =           {Dipartimento di Matematica, Seconda Universit{\'a}
                         degli Studi di Napoli, Italy},
  series =              {Quaderni di Matematica},
  volume =              {13},
  pages =               {175-227},
  year =                {2004},
}
[Cou04] Jean-Michel Couvreur. A BDD-like Implementation of an Automaton Package. In CIAA'04, Lecture Notes in Computer Science 3317, pages 310-311. Springer-Verlag, July 2004. 
@inproceedings{ciaa2004-Cou,
  author =              {Couvreur, Jean-Michel},
  title =               {A {BDD}-like Implementation of an Automaton Package},
  editor =              {Domaratzki, Michael and Okhatin, Alexander and
                         Salomaa, Arto and Yu, Sheng},
  booktitle =           {{R}evised {S}elected {P}apers of the 9th
                         {I}nternational {C}onference on Implementation and
                         Application of Automata ({CIAA}'04)},
  acronym =             {{CIAA}'04},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {3317},
  pages =               {310-311},
  year =                {2004},
  month =               jul,
}
[Cou04] Jean-Michel Couvreur. Contribution à l'algorithmique de la vérification. Mémoire d'habilitation, Lab. Spécification & Vérification, ENS Cachan, France, July 2004. 
@phdthesis{hab-couvreur,
  author =              {Couvreur, Jean-Michel},
  title =               {Contribution {\`a} l'algorithmique de la
                         v{\'e}rification},
  year =                {2004},
  month =               jul,
  school =              {Lab.~Sp\'ecification \& V\'erification, ENS Cachan,
                         France},
  type =                {M\'emoire d'habilitation},
}
[CRV+04] Shih-Fen Cheng, Daniel M. Reeves, Yevgeniy Vorobeychik, and Michael P. Wellman. Notes on Equilibria in Symmetric Games. In GTDT'04, pages 71-78. June 2004. 
@inproceedings{gtdt2004-CRVW,
  author =              {Cheng, Shih-Fen and Reeves, Daniel M. and
                         Vorobeychik, Yevgeniy and Wellman, Michael P.},
  title =               {Notes on Equilibria in Symmetric Games},
  editor =              {Parsons, Simon and Gmytrasiewicz, Piotr},
  booktitle =           {{P}roceedings of the 6th {I}nternational {W}orkshop
                         on Game Theoretic and Decision Theoretic Agents
                         ({GTDT}'04)},
  acronym =             {{GTDT}'04},
  pages =               {71-78},
  year =                {2004},
  month =               jun,
}
[CTT+04] Edmund M. Clarke, Muralidhar Talupur, Tayssir Touili, and Helmut Veith. Verification by network decomposition. In CONCUR'04, Lecture Notes in Computer Science 3170, pages 276-291. Springer-Verlag, August 2004. 
@inproceedings{concur2004-CTTV,
  author =              {Clarke, Edmund M. and Talupur, Muralidhar and
                         Touili, Tayssir and Veith, Helmut},
  title =               {Verification by network decomposition},
  editor =              {Gardner, {\relax Ph}ilippa and Yoshida, Nobuko},
  booktitle =           {{P}roceedings of the 15th {I}nternational
                         {C}onference on {C}oncurrency {T}heory
                         ({CONCUR}'04)},
  acronym =             {{CONCUR}'04},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {3170},
  pages =               {276-291},
  year =                {2004},
  month =               aug,
  doi =                 {10.1007/978-3-540-28644-8_18},
}
[DDR04] Martin De Wulf, Laurent Doyen, and Jean-François Raskin. Almost ASAP Semantics: From Timed Models to Timed Implementations. In HSCC'04, Lecture Notes in Computer Science 2993, pages 296-310. Springer-Verlag, March 2004. 
@inproceedings{hscc2004-DDR,
  author =              {De{~}Wulf, Martin and Doyen, Laurent and Raskin,
                         Jean-Fran{\c c}ois},
  title =               {Almost {ASAP} Semantics: From Timed Models to Timed
                         Implementations},
  editor =              {Alur, Rajeev and Pappas, George J.},
  booktitle =           {{P}roceedings of the 7th {I}nternational {W}orkshop
                         on {H}ybrid {S}ystems: {C}omputation and {C}ontrol
                         ({HSCC}'04)},
  acronym =             {{HSCC}'04},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {2993},
  pages =               {296-310},
  year =                {2004},
  month =               mar,
}
[DFF+04] Erik D. Demaine, Rudolf Fleischer, Aviezri S. Fraenkel, and Richard J. Nowakowski. Appendix B: Open Problems at the 2002 Dagstuhl Seminar on Algebraic Combinatorial Game Theory. Theoretical Computer Science 313(3):539-543. Elsevier, February 2004. 
@article{tcs313(3)-DFFN,
  author =              {Demaine, Erik D. and Fleischer, Rudolf and Fraenkel,
                         Aviezri S. and Nowakowski, Richard J.},
  title =               {Appendix~{B}: {O}pen Problems at the 2002 {D}agstuhl
                         Seminar on Algebraic Combinatorial Game Theory},
  publisher =           {Elsevier},
  journal =             {Theoretical Computer Science},
  volume =              {313},
  number =              {3},
  pages =               {539-543},
  year =                {2004},
  month =               feb,
}
[DRV04] Giorgio Delzanno, Jean-François Raskin, and Laurent Van Begin. Covering sharing trees: a compact data structure for parameterized verification. International Journal on Software Tools for Technology Transfer 5(2-3):268-297. Springer-Verlag, 2004. 
@article{sttt5(2-3)-DRV,
  author =              {Delzanno, Giorgio and Raskin, Jean-Fran{\c c}ois and
                         Van{~}Begin, Laurent},
  title =               {Covering sharing trees: a compact data structure for
                         parameterized verification},
  publisher =           {Springer-Verlag},
  journal =             {International Journal on Software Tools for
                         Technology Transfer},
  volume =              {5},
  number =              {2-3},
  pages =               {268-297},
  year =                {2004},
}
[DT04] Deepak D'Souza and Nicolas Tabareau. On Timed Automata with Input-Determined Guards. In FORMATS-FTRTFT'04, Lecture Notes in Computer Science 3253, pages 68-83. Springer-Verlag, September 2004. 
@inproceedings{formats2004-DT,
  author =              {D'Souza, Deepak and Tabareau, Nicolas},
  title =               {On~Timed Automata with Input-Determined Guards},
  editor =              {Lakhnech, Yassine and Yovine, Sergio},
  booktitle =           {{P}roceedings of the {J}oint {I}nternational
                         {C}onferences on {F}ormal {M}odelling and {A}nalysis
                         of {T}imed {S}ystems ({FORMATS}'04) and {F}ormal
                         {T}echniques in {R}eal-Time and {F}ault-Tolerant
                         {S}ystems ({FTRTFT}'04)},
  acronym =             {{FORMATS-FTRTFT}'04},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {3253},
  pages =               {68-83},
  year =                {2004},
  month =               sep,
  doi =                 {10.1007/978-3-540-30206-3_7},
}
[FPT04] Alex Fabrikant, Christos H. Papadimitriou, and Kunal Talwar. The complexity of pure Nash equilibria. In STOC'04, pages 604-612. ACM Press, June 2004. 
@inproceedings{stoc2004-FPT,
  author =              {Fabrikant, Alex and Papadimitriou, {\relax Ch}ristos
                         H. and Talwar, Kunal},
  title =               {The complexity of pure {N}ash equilibria},
  editor =              {Babai, L{\'a}szl{\'o}},
  booktitle =           {{P}roceedings of the 36th {A}nnual {ACM} {S}ymposium
                         on the {T}heory of {C}omputing ({STOC}'04)},
  acronym =             {{STOC}'04},
  publisher =           {ACM Press},
  pages =               {604-612},
  year =                {2004},
  month =               jun,
  doi =                 {10.1145/1007352.1007445},
}
[FS04] Bernd Finkbeiner and Henny Sipma. Checking Finite Traces using Alternating Automata. Formal Methods in System Design 24(2):101-127. Kluwer Academic, March 2004. 
@article{fmsd24(2)-FS,
  author =              {Finkbeiner, Bernd and Sipma, Henny},
  title =               {Checking Finite Traces using Alternating Automata},
  publisher =           {Kluwer Academic},
  journal =             {Formal Methods in System Design},
  volume =              {24},
  number =              {2},
  pages =               {101-127},
  year =                {2004},
  month =               mar,
  doi =                 {10.1023/B:FORM.0000017718.28096.48},
}
[GC04] Arie Gurfinkel and Marsha Chechik. Extending extended vacuity. In FMCAD'04, Lecture Notes in Computer Science 3312, pages 306-321. Springer-Verlag, November 2004. 
@inproceedings{fmcad2004-GC,
  author =              {Gurfinkel, Arie and Chechik, Marsha},
  title =               {Extending extended vacuity},
  editor =              {Hu, Alan J. and Martin, Andrew K.},
  booktitle =           {{P}roceedings of the 5th {I}nternational
                         {C}onference on {F}ormal {M}ethods in
                         {C}omputer-{A}ided {D}esign ({FMCAD}'04)},
  acronym =             {{FMCAD}'04},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {3312},
  pages =               {306-321},
  year =                {2004},
  month =               nov,
  doi =                 {10.1007/978-3-540-30494-4_22},
}
[GJ04] Valentin Goranko and Wojciech Jamroga. Comparing Semantics of Logics for Multi-agent Systems. Synthese 139(2):241-280. Springer-Verlag, March 2004. 
@article{synthese139(2)-GJ,
  author =              {Goranko, Valentin and Jamroga, Wojciech},
  title =               {Comparing Semantics of Logics for Multi-agent
                         Systems},
  publisher =           {Springer-Verlag},
  journal =             {Synthese},
  volume =              {139},
  number =              {2},
  pages =               {241-280},
  year =                {2004},
  month =               mar,
}
[GZ04] Hugo Gimbert and Wiesław Zielonka. When Can You Play Positionnaly?. In MFCS'04, Lecture Notes in Computer Science 3153, pages 686-697. Springer-Verlag, August 2004. 
@inproceedings{mfcs2004-GZ,
  author =              {Gimbert, Hugo and Zielonka, Wies{\l}aw},
  title =               {When Can You Play Positionnaly?},
  editor =              {Fiala, Ji{\v r}{\'\i} and Koubek, V{\'a}clav and
                         Kratoch{\'\i}l, Jan},
  booktitle =           {{P}roceedings of the 29th {I}nternational
                         {S}ymposium on {M}athematical {F}oundations of
                         {C}omputer {S}cience ({MFCS}'04)},
  acronym =             {{MFCS}'04},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {3153},
  pages =               {686-697},
  year =                {2004},
  month =               aug,
}
[HJ04] Gerard J. Holzmann and Rajeev Joshi. Model-Driven Software Verification. In SPIN'04, Lecture Notes in Computer Science 2989, pages 76-91. Springer-Verlag, April 2004. 
@inproceedings{spin2004-HJ,
  author =              {Holzmann, Gerard J. and Joshi, Rajeev},
  title =               {Model-Driven Software Verification},
  editor =              {Graf, Susanne and Mounier, Laurent},
  booktitle =           {{P}roceedings of the 11th {I}nternational {SPIN}
                         {W}orkshop ({SPIN}'04)},
  acronym =             {{SPIN}'04},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {2989},
  pages =               {76-91},
  year =                {2004},
  month =               apr,
  doi =                 {10.1007/978-3-540-24732-6_6},
}
[HJM+04] Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar, and Kenneth L. McMillan. Abstractions from Proofs. In POPL'04, pages 232-244. ACM Press, January 2004. 
@inproceedings{popl2004-HJMM,
  author =              {Henzinger, Thomas A. and Jhala, Ranjit and Majumdar,
                         Rupak and McMillan, Kenneth L.},
  title =               {Abstractions from Proofs},
  editor =              {Jones, Neil D. and Leroy, Xavier},
  booktitle =           {Conference Record of the 31st {ACM}
                         {SIGPLAN}-{SIGACT} {S}ymposium on {P}rinciples of
                         {P}rogramming {L}anguages ({POPL}'04)},
  acronym =             {{POPL}'04},
  publisher =           {ACM Press},
  pages =               {232-244},
  year =                {2004},
  month =               jan,
}
[HLM+04] Thomas Hérault, Richard Lassaigne, Frédéric Magniette, and Sylvain Peyronnet. Approximate Probabilistic Model Checking. In VMCAI'04, Lecture Notes in Computer Science 2937, pages 73-84. Springer-Verlag, January 2004. 
@inproceedings{vmcai2004-HLMP,
  author =              {H{\'e}rault, {\relax Th}omas and Lassaigne, Richard
                         and Magniette, Fr{\'e}d{\'e}ric and Peyronnet,
                         Sylvain},
  title =               {Approximate Probabilistic Model Checking},
  editor =              {Steffen, Bernhard and Levi, Giorgio},
  booktitle =           {{P}roceedings of the 5th {I}nternational {W}orkshop
                         on {V}erification, {M}odel {C}hecking, and
                         {A}bstract {I}nterpretation ({VMCAI}'04)},
  acronym =             {{VMCAI}'04},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {2937},
  pages =               {73-84},
  year =                {2004},
  month =               jan,
}
[HR04] Yoram Hirshfeld and Alexander Rabinovich. Logics for Real Time: Decidability and Complexity. Fundamenta Informaticae 62(1):1-28. IOS Press, 2004. 
@article{fi62(1)-HR,
  author =              {Hirshfeld, Yoram and Rabinovich, Alexander},
  title =               {Logics for Real Time: Decidability and Complexity},
  publisher =           {IOS Press},
  journal =             {Fundamenta Informaticae},
  volume =              {62},
  number =              {1},
  pages =               {1-28},
  year =                {2004},
}
[HR04] Michael Huth and Mark D. Ryan. Logic in Computer Science. Cambridge University Press, August 2004. 
@book{lics-HR,
  author =              {Huth, Michael and Ryan, Mark D.},
  title =               {Logic in Computer Science},
  publisher =           {Cambridge University Press},
  year =                {2004},
  month =               aug,
}
[HVG04] Jinfeng Huang, Jeroen Voeten, and Marc C.W. Geilen. Real-Time Property Preservation in Concurrent Real-time Systems. In RTCSA'04. August 2004. 
@inproceedings{rtcsa2004-HVG,
  author =              {Huang, Jinfeng and Voeten, Jeroen and Geilen, Marc
                         C.W.},
  title =               {Real-Time Property Preservation in Concurrent
                         Real-time Systems},
  booktitle =           {{P}roceedings of the 10th {I}nternational
                         {C}onference on {R}eal-{T}ime {C}omputing {S}ystems
                         and {A}pplications ({RTCSA}'04)},
  acronym =             {{RTCSA}'04},
  year =                {2004},
  month =               aug,
}
[Jer04] Thierry Jéron. Contribution à la génération automatique de tests pour les systèmes réactifs. Mémoire d'habilitation, Université Rennes 1, France, February 2004. 
@phdthesis{hab-jeron,
  author =              {J{\'e}ron, Thierry},
  title =               {Contribution {\`a} la g{\'e}n{\'e}ration automatique
                         de tests pour les syst{\`e}mes r{\'e}actifs},
  year =                {2004},
  month =               feb,
  school =              {Universit{\'e} Rennes~1, France},
  type =                {M\'emoire d'habilitation},
}
[JvdH04] Wojciech Jamroga and Wiebe van der Hoek. Agents that Know How to Play. Fundamenta Informaticae 63(2-3):185-219. IOS Press, 2004. 
@article{fundi63(2-3)-JH,
  author =              {Jamroga, Wojciech and van der Hoek, Wiebe},
  title =               {Agents that Know How to Play},
  publisher =           {IOS Press},
  journal =             {Fundamenta Informaticae},
  volume =              {63},
  number =              {2-3},
  pages =               {185-219},
  year =                {2004},
}
[JL04] David Janin and Giacommo Lenzi. On the Relationship Between Monadic and Weak Monadic Second Order Logic on Arbitrary Trees. Fundamenta Informaticae 61(3-4):247-265. IOS Press, 2004. 
@article{fundi61(3-4)-JL,
  author =              {Janin, David and Lenzi, Giacommo},
  title =               {On the Relationship Between Monadic and Weak Monadic
                         Second Order Logic on Arbitrary Trees},
  publisher =           {IOS Press},
  journal =             {Fundamenta Informaticae},
  volume =              {61},
  number =              {3-4},
  pages =               {247-265},
  year =                {2004},
}
[KMS+04] Daniel Král, Vladan Majerech, Jiří Sgall, Tomáš Tichý, and Gerhard J. Woeginger. It is Tough to be a Plumber. Theoretical Computer Science 313(3):473-484. Elsevier, February 2004. 
@article{tcs313(3)-KMSTW,
  author =              {Kr{\'a}l, Daniel and Majerech, Vladan and Sgall,
                         Ji{\v r}{\'\i} and Tich{\'y}, Tom{\'a}{\v s} and
                         Woeginger, Gerhard J.},
  title =               {It is Tough to be a Plumber},
  publisher =           {Elsevier},
  journal =             {Theoretical Computer Science},
  volume =              {313},
  number =              {3},
  pages =               {473-484},
  year =                {2004},
  month =               feb,
}
[KMT+04] Pavel Krčál, Leonid Mokrushin, P. S. Thiagarajan, and Wang Yi. Timed vs. Timed-Triggered Automata. In CONCUR'04, Lecture Notes in Computer Science 3170, pages 340-354. Springer-Verlag, August 2004. 
@inproceedings{concur2004-KMTY,
  author =              {Kr{\v{c}}{\'a}l, Pavel and Mokrushin, Leonid and
                         Thiagarajan, P. S. and Yi, Wang},
  title =               {Timed vs.{} Timed-Triggered Automata},
  editor =              {Gardner, {\relax Ph}ilippa and Yoshida, Nobuko},
  booktitle =           {{P}roceedings of the 15th {I}nternational
                         {C}onference on {C}oncurrency {T}heory
                         ({CONCUR}'04)},
  acronym =             {{CONCUR}'04},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {3170},
  pages =               {340-354},
  year =                {2004},
  month =               aug,
}
[KP04] Magdalena Kacprzak and Wojciech Penczek. Unbounded Model Checking for Alternating-Time Temporal Logic. In AAMAS'04, pages 646-653. IEEE Comp. Soc. Press, August 2004. 
@inproceedings{aamas2004-KP,
  author =              {Kacprzak, Magdalena and Penczek, Wojciech},
  title =               {Unbounded Model Checking for Alternating-Time
                         Temporal Logic},
  booktitle =           {{P}roceedings of the 3rd {I}nternational {J}oint
                         {C}onference on {A}utonomous {A}gents and
                         {M}ultiagent {S}ystems ({AAMAS}'04)},
  acronym =             {{AAMAS}'04},
  publisher =           {IEEE Comp. Soc. Press},
  pages =               {646-653},
  year =                {2004},
  month =               aug,
}
[LMG04] Thomas Lévy, Olivier Marcé, and Damien Galand. Embedded BGP Routing Monitoring. In HSNMC'04, Lecture Notes in Computer Science 3079, pages 348-359. Springer-Verlag, June 2004. 
@inproceedings{hsnmc2004-LMG,
  author =              {L{\'e}vy, {\relax Th}omas and Marc{\'e}, Olivier and
                         Galand, Damien},
  title =               {Embedded {BGP} Routing Monitoring},
  editor =              {Mammeri, Zoubir and Lorenz, Pascal},
  booktitle =           {{P}roceedings of the 7th {IEEE} {I}nternational
                         {C}onference on {H}igh {S}peed {N}etworks and
                         {M}ultimedia {C}ommunications ({HSNMC}'04)},
  acronym =             {{HSNMC}'04},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {3079},
  pages =               {348-359},
  year =                {2004},
  month =               jun,
}
[LMN04] Kim Guldstrand Larsen, Marius Mikučionis, and Brian Nielsen. Online Testing of Real-time Systems Using Uppaal. In FATES'04, Lecture Notes in Computer Science 3395, pages 79-94. Springer-Verlag, September 2004. 
@inproceedings{LMN-fates2004,
  author =              {Larsen, Kim Guldstrand and Miku{\v{c}}ionis, Marius
                         and Nielsen, Brian},
  title =               {Online Testing of Real-time Systems Using {U}ppaal},
  editor =              {Grabowski, Jens and Nielsen, Brian},
  booktitle =           {{P}roceedings of the 4th {I}nternational {W}orkshop
                         on {F}ormal {A}pproaches to {S}oftware {T}esting
                         ({FATES}'04)},
  acronym =             {{FATES}'04},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {3395},
  pages =               {79-94},
  year =                {2004},
  month =               sep,
  doi =                 {10.1007/978-3-540-31848-4_6},
}
[LNZ04] Denis Lugiez, Peter Niebert, and Sarah Zennou. A partial order semantics approach to the clock explosion problem of timed automata. In TACAS'04, Lecture Notes in Computer Science 2988, pages 296-311. Springer-Verlag, March 2004. 
@inproceedings{tacas2004-LNZ,
  author =              {Lugiez, Denis and Niebert, Peter and Zennou, Sarah},
  title =               {A~partial order semantics approach to the clock
                         explosion problem of timed automata},
  editor =              {Jensen, Kurt and Podelski, Andreas},
  booktitle =           {{P}roceedings of the 10th {I}nternational
                         {C}onference on {T}ools and {A}lgorithms for
                         {C}onstruction and {A}nalysis of {S}ystems
                         ({TACAS}'04)},
  acronym =             {{TACAS}'04},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {2988},
  pages =               {296-311},
  year =                {2004},
  month =               mar,
}
[LPS04] Banjamin Lynn, Manoj Prabhakaran, and Amit Sahai. Positive Results and Techniques for Obfuscation. In EUROCRYPT'04, Lecture Notes in Computer Science 3027, pages 20-39. Springer-Verlag, August 2004. 
@inproceedings{eurocrypt2004-LPS,
  author =              {Lynn, Banjamin and Prabhakaran, Manoj and Sahai,
                         Amit},
  title =               {Positive Results and Techniques for Obfuscation},
  editor =              {Cachin, Christian and Camenisch, Jan},
  booktitle =           {{P}roceedings of the 23rd {I}nternational
                         {C}onference on the {T}heory and {A}pplications of
                         {C}ryptographic {T}echniques ({EUROCRYPT}'04)},
  acronym =             {{EUROCRYPT}'04},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {3027},
  pages =               {20-39},
  year =                {2004},
  month =               aug,
}
[Mar04] Nicolas Markey. TSMV : model-checking symbolique de systémes simplement temporisés. In AFADL'04. June 2004. 
@inproceedings{afadl2004-Mar,
  author =              {Markey, Nicolas},
  title =               {{TSMV}~: model-checking symbolique de syst{\'e}mes
                         simplement temporis{\'e}s},
  editor =              {Julliand, Jacques},
  booktitle =           {Actes de la 6\`eme Conf\'erence {A}pproches
                         {F}ormelles dans l'{A}ssistance au
                         {D}{\'e}veloppement de {L}ogiciels ({AFADL}'04)},
  acronym =             {{AFADL}'04},
  year =                {2004},
  month =               jun,
}
[MN04] Oded Maler and Dejan Nickovic. Monitoring Temporal Properties of Continuous Signals. In FORMATS-FTRTFT'04, Lecture Notes in Computer Science 3253, pages 152-166. Springer-Verlag, September 2004. 
@inproceedings{formats2004-MN,
  author =              {Maler, Oded and Nickovic, Dejan},
  title =               {Monitoring Temporal Properties of Continuous
                         Signals},
  editor =              {Lakhnech, Yassine and Yovine, Sergio},
  booktitle =           {{P}roceedings of the {J}oint {I}nternational
                         {C}onferences on {F}ormal {M}odelling and {A}nalysis
                         of {T}imed {S}ystems ({FORMATS}'04) and {F}ormal
                         {T}echniques in {R}eal-Time and {F}ault-Tolerant
                         {S}ystems ({FTRTFT}'04)},
  acronym =             {{FORMATS-FTRTFT}'04},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {3253},
  pages =               {152-166},
  year =                {2004},
  month =               sep,
}
[MS04] Nicolas Markey and Philippe Schnoebelen. TSMV: Symbolic Model Checking for Simply Timed Systems. In QEST'04, pages 330-331. IEEE Comp. Soc. Press, September 2004.
Abstract

TSMV is an extension of NuSMV, the open-source symbolic model checker, aimed at dealing with timed versions of (models of) circuits, PLC controllers, protocols, etc. The underlying model is an extension of Kripke structures, where every transition carries an integer duration (possibly zero). This simple model supports efficient symbolic algorithms for RTCTL formulae.

@inproceedings{qest2004-MS,
  author =              {Markey, Nicolas and Schnoebelen, {\relax Ph}ilippe},
  title =               {{TSMV}: Symbolic Model Checking for Simply Timed
                         Systems},
  booktitle =           {{P}roceedings of the 1st {I}nternational
                         {C}onference on {Q}uantitative {E}valuation of
                         {S}ystems ({QEST}'04)},
  acronym =             {{QEST}'04},
  publisher =           {IEEE Comp. Soc. Press},
  pages =               {330-331},
  year =                {2004},
  month =               sep,
  doi =                 {10.1109/QEST.2004.1348052},
  abstract =            {TSMV is an extension of NuSMV, the open-source
                         symbolic model checker, aimed at dealing with timed
                         versions of (models of) circuits, PLC controllers,
                         protocols, etc. The underlying model is an extension
                         of Kripke structures, where every transition carries
                         an integer duration (possibly zero). This simple
                         model supports efficient symbolic algorithms for
                         RTCTL formulae.},
}
[Osb04] Martin J. Osborne. An Introduction to Game Theory. Oxford University Press, 2004. 
@book{igt-Osb04,
  author =              {Osborne, Martin J.},
  title =               {An~Introduction to Game Theory},
  publisher =           {Oxford University Press},
  year =                {2004},
}
[OW04] Joël Ouaknine and James Worrell. On the Language Inclusion Problem for Timed Automata: Closing a Decidability Gap. In LICS'04, pages 54-63. IEEE Comp. Soc. Press, July 2004. 
@inproceedings{lics2004-OW,
  author =              {Ouaknine, Jo{\"e}l and Worrell, James},
  title =               {On the Language Inclusion Problem for Timed
                         Automata: {C}losing a Decidability Gap},
  booktitle =           {{P}roceedings of the 19th {A}nnual {S}ymposium on
                         {L}ogic in {C}omputer {S}cience ({LICS}'04)},
  acronym =             {{LICS}'04},
  publisher =           {IEEE Comp. Soc. Press},
  pages =               {54-63},
  year =                {2004},
  month =               jul,
}
[PZM+04] Dan Pei, Beichuan Zhang, Dan Massey, and Lixia Zhang. An Analysis of Path-Vector Routing Protocol Convergence Algorithms. Technical Report TR040009, Computer Science Department, University of California at Los Angeles, USA, March 2004. 
@techreport{UCLA-TR040009,
  author =              {Pei, Dan and Zhang, Beichuan and Massey, Dan and
                         Zhang, Lixia},
  title =               {An Analysis of Path-Vector Routing Protocol
                         Convergence Algorithms},
  number =              {TR040009},
  year =                {2004},
  month =               mar,
  institution =         {Computer Science Department, University of
                         California at Los~Angeles, USA},
  type =                {Technical Report},
}
[QBI04] Michael Melholt Quottrup, Thomas Bak, and Roozbeh Izadi-Zamanabadi. Multi-robot planning: a timed automata approach. In ICRA'04, pages 4417-4422. IEEE Robotics & Automation Soc., April 2004. 
@inproceedings{icra2004-QBI,
  author =              {Quottrup, Michael Melholt and Bak, Thomas and
                         Izadi{-}Zamanabadi, Roozbeh},
  title =               {Multi-robot planning: a~timed automata approach},
  booktitle =           {{P}roceedings of the 2004 {IEEE} {I}nternational
                         {C}onference on {R}obotics and {A}utomation
                         ({ICRA}'04)},
  acronym =             {{ICRA}'04},
  publisher =           {IEEE Robotics~\& Automation Soc.},
  pages =               {4417-4422},
  year =                {2004},
  month =               apr,
  doi =                 {10.1109/ROBOT.2004.1302413},
}
[Rey04] Mark Reynolds. The Complexity of the Temporal Logic with "Until" Over General Linear Time. Journal of Computer and System Sciences 66(2):393-426. Academic Press, March 2004. 
@article{jcss66(2)-Rey,
  author =              {Reynolds, Mark},
  title =               {The Complexity of the Temporal Logic with
                         {"}Until{"} Over General Linear Time},
  publisher =           {Academic Press},
  journal =             {Journal of Computer and System Sciences},
  volume =              {66},
  number =              {2},
  pages =               {393-426},
  year =                {2004},
  month =               mar,
}
[RT04] Tim Roughgarden and Éva Tardos. Bounding the inefficiency of equilibria in non-atomic congestion games. Games and Economic Behavior 47(2):389-403. May 2004. 
@article{geb47(2)-RT,
  author =              {Roughgarden, Tim and Tardos, {\'E}va},
  title =               {Bounding the inefficiency of equilibria in
                         non-atomic congestion games},
  journal =             {Games and Economic Behavior},
  volume =              {47},
  number =              {2},
  pages =               {389-403},
  year =                {2004},
  month =               may,
  doi =                 {10.1016/j.geb.2003.06.004},
}
[Sch04] Pierre-Yves Schobbens. Alternating-Time Logic with Imperfect Recall. In LCMAS'03, Electronic Notes in Theoretical Computer Science 85(2), pages 82-93. Elsevier, April 2004. 
@inproceedings{lcmas2003-Sch,
  author =              {Schobbens, Pierre-Yves},
  title =               {Alternating-Time Logic with Imperfect Recall},
  editor =              {van der Hoek, Wiebe and Lomuscio, Alessio and de
                         Vink, Erik and Wooldridge, Michael},
  booktitle =           {{P}roceedings of the {W}orkshop on Logic and
                         Communication in Multi-Agent Systems ({LCMAS}'03)},
  acronym =             {{LCMAS}'03},
  publisher =           {Elsevier},
  series =              {Electronic Notes in Theoretical Computer Science},
  volume =              {85(2)},
  pages =               {82-93},
  year =                {2004},
  month =               apr,
  confyear =            {2003},
  confmonth =           {6},
  doi =                 {10.1016/S1571-0661(05)82604-0},
}
[Ser04] Olivier Serre. Vectorial Languages and Linear Temporal Logic. Theoretical Computer Science 310(1-3):79-116. Elsevier, January 2004. 
@article{tcs310(1-3)-ser,
  author =              {Serre, Olivier},
  title =               {Vectorial Languages and Linear Temporal Logic},
  publisher =           {Elsevier},
  journal =             {Theoretical Computer Science},
  volume =              {310},
  number =              {1-3},
  pages =               {79-116},
  year =                {2004},
  month =               jan,
}
[Str04] Jan Strejček. Linear Temporal Logic: Expressiveness and Model Checking. PhD thesis, Faculty of Informatics, Masaryk University, Brno, Czech Republic, 2004. 
@phdthesis{phd-strejcek,
  author =              {Strej{\v c}ek, Jan},
  title =               {Linear Temporal Logic: Expressiveness and Model
                         Checking},
  year =                {2004},
  school =              {Faculty of Informatics, Masaryk University, Brno,
                         Czech Republic},
}
[TR04] Prasanna Thati and Grigore Roşu. Monitoring Algorithms for Metric Temporal Logic Specifications. In RV'04, Electronic Notes in Theoretical Computer Science 113, pages 131-147. Elsevier, April 2004. 
@inproceedings{rv2004-TR,
  author =              {Thati, Prasanna and Ro{\c{s}}u, Grigore},
  title =               {Monitoring Algorithms for Metric Temporal Logic
                         Specifications},
  editor =              {Havelund, Klaus and Ro{\c{s}}u, Grigore},
  booktitle =           {{P}roceedings of the 4th {I}nternational {W}orkshop
                         on {R}untime {V}erification ({RV}'04)},
  acronym =             {{RV}'04},
  publisher =           {Elsevier},
  series =              {Electronic Notes in Theoretical Computer Science},
  volume =              {113},
  pages =               {131-147},
  year =                {2004},
  month =               apr,
  doi =                 {10.1016/j.entcs.2004.12.01},
}
[Wal04] Igor Walukiewicz. A Landscape with Games in the Background. In LICS'04, pages 356-366. IEEE Comp. Soc. Press, July 2004. 
@inproceedings{lics2004-Wal,
  author =              {Walukiewicz, Igor},
  title =               {A Landscape with Games in the Background},
  booktitle =           {{P}roceedings of the 19th {A}nnual {S}ymposium on
                         {L}ogic in {C}omputer {S}cience ({LICS}'04)},
  acronym =             {{LICS}'04},
  publisher =           {IEEE Comp. Soc. Press},
  pages =               {356-366},
  year =                {2004},
  month =               jul,
}
[Wan04] Farn Wang. Efficient verification of timed automata with BDD-like data structures. International Journal on Software Tools for Technology Transfer 6(1):77-97. Springer-Verlag, July 2004. 
@article{sttt6(1)-Wan,
  author =              {Wang, Farn},
  title =               {Efficient verification of timed automata with
                         {BDD}-like data structures},
  publisher =           {Springer-Verlag},
  journal =             {International Journal on Software Tools for
                         Technology Transfer},
  volume =              {6},
  number =              {1},
  pages =               {77-97},
  year =                {2004},
  month =               jul,
  doi =                 {10.1007/s10009-003-0135-4},
}
[Wan04] Farn Wang. Model-Checking Distributed Real-Time Systems with States, Events, and Multiple Fairness Assumptions. In AMAST'04, Lecture Notes in Computer Science 3116, pages 553-567. Springer-Verlag, July 2004. 
@inproceedings{amast2004-Wan,
  author =              {Wang, Farn},
  title =               {Model-Checking Distributed Real-Time Systems with
                         States, Events, and Multiple Fairness Assumptions},
  editor =              {Rattray, Charles and Maharaj, Savi and Shankland,
                         Carron},
  booktitle =           {{P}roceedings of the 10th {I}nternational
                         {C}onference on {A}lgebraic {M}ethodology and
                         {S}oftware {T}echnology ({AMAST}'04)},
  acronym =             {{AMAST}'04},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {3116},
  pages =               {553-567},
  year =                {2004},
  month =               jul,
}
[WD04] Michael Wooldridge and Paul E. Dunne. On the Computational Complexity of Qualitative Coalition Games. Artificial Intelligence 158(1):27-73. Elsevier, September 2004. 
@article{ai158(1)-WD,
  author =              {Wooldridge, Michael and Dunne, Paul E.},
  title =               {On the Computational Complexity of Qualitative
                         Coalition Games},
  publisher =           {Elsevier},
  journal =             {Artificial Intelligence},
  volume =              {158},
  number =              {1},
  pages =               {27-73},
  year =                {2004},
  month =               sep,
  doi =                 {10.1016/j.artint.2004.04.002},
}
[Wei04] Pascal Weil. Algebraic Recognizability of Languages. In MFCS'04, Lecture Notes in Computer Science 3153, pages 149-175. Springer-Verlag, August 2004. 
@inproceedings{mfcs2004-Wei,
  author =              {Weil, Pascal},
  title =               {Algebraic Recognizability of Languages},
  editor =              {Fiala, Ji{\v r}{\'\i} and Koubek, V{\'a}clav and
                         Kratoch{\'\i}l, Jan},
  booktitle =           {{P}roceedings of the 29th {I}nternational
                         {S}ymposium on {M}athematical {F}oundations of
                         {C}omputer {S}cience ({MFCS}'04)},
  acronym =             {{MFCS}'04},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {3153},
  pages =               {149-175},
  year =                {2004},
  month =               aug,
}
[Win04] Aaron Windsor. A Simple Proof that Finding a Macimal Independent Set in a Graph is in NC. Information Processing Letters 92(4):185-187. Elsevier, November 2004. 
@article{ipl92(4)-Win,
  author =              {Windsor, Aaron},
  title =               {A Simple Proof that Finding a Macimal Independent
                         Set in a Graph is in~{\(\mathcal{NC}\)}},
  publisher =           {Elsevier},
  journal =             {Information Processing Letters},
  volume =              {92},
  number =              {4},
  pages =               {185-187},
  year =                {2004},
  month =               nov,
}
[Yan04] Mihalis Yannakakis. Testing, Optimization, and Games. In ICALP'04, Lecture Notes in Computer Science, pages 28-45. Springer-Verlag, 2004. 
@inproceedings{icalp2004-Yan,
  author =              {Yannakakis, Mihalis},
  title =               {Testing, Optimization, and Games},
  booktitle =           {{P}roceedings of the 31st {I}nternational
                         {C}olloquium on {A}utomata, {L}anguages and
                         {P}rogramming ({ICALP}'04)},
  acronym =             {{ICALP}'04},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  pages =               {28-45},
  year =                {2004},
  doi =                 {10.1007/978-3-540-27836-8_6},
}
[ZSS04] Shipei Zhang, Oleg Sokolsky, and Scott A. Smolka. On the Parallel Complexity of Model Checking in the Modal Mu-Calculus. In LICS'04, pages 154-163. IEEE Comp. Soc. Press, July 2004. 
@inproceedings{lics1994-ZSS,
  author =              {Zhang, Shipei and Sokolsky, Oleg and Smolka, Scott
                         A.},
  title =               {On the Parallel Complexity of Model Checking in the
                         Modal Mu-Calculus},
  booktitle =           {{P}roceedings of the 19th {A}nnual {S}ymposium on
                         {L}ogic in {C}omputer {S}cience ({LICS}'04)},
  acronym =             {{LICS}'04},
  publisher =           {IEEE Comp. Soc. Press},
  pages =               {154-163},
  year =                {2004},
  month =               jul,
}
List of authors