Nicolas Markey

2002
[LMS02]	François Laroussinie, Nicolas Markey, and Philippe Schnoebelen. On Model Checking Durational Kripke Structures (Extended Abstract). In FoSSaCS'02, Lecture Notes in Computer Science 2303, pages 264-279. Springer-Verlag, April 2002. 10.1007/3-540-45931-6_19 PDF Abstract + BibTeX Abstract We consider quantitative model checking in durational Kripke structures (Kripke structures where transitions have integer durations) with timed temporal logics where subscripts put quantitative constraints on the time it takes before a property is satisfied. We investigate the conditions that allow polynomial-time model checking algorithms for timed versions of CTL and 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). A surprising outcome of this study is that it provides the second example of a Δ2P-complete model checking problem. @inproceedings{fossacs2002-LMS, author = {Laroussinie, Fran{\c c}ois and Markey, Nicolas and Schnoebelen, {\relax Ph}ilippe}, title = {On Model Checking Durational {K}ripke Structures (Extended Abstract)}, editor = {Nielsen, Mogens and Engberg, Uffe}, booktitle = {{P}roceedings of the 5th {I}nternational {C}onference on {F}oundations of {S}oftware {S}cience and {C}omputation {S}tructure ({FoSSaCS}'02)}, acronym = {{FoSSaCS}'02}, publisher = {Springer-Verlag}, series = {Lecture Notes in Computer Science}, volume = {2303}, pages = {264-279}, year = {2002}, month = apr, doi = {10.1007/3-540-45931-6_19}, abstract = {We consider quantitative model checking in \emph{durational Kripke structures} (Kripke structures where transitions have integer durations) with timed temporal logics where subscripts put quantitative constraints on the time it takes before a property is satisfied. We investigate the conditions that allow polynomial-time model checking algorithms for timed versions of CTL and 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 A surprising outcome of this study is that it provides the second example of a \(\Delta_2^P\)-complete model checking problem.}, }
[LMS02]	François Laroussinie, Nicolas Markey, and Philippe Schnoebelen. Temporal Logic with Forgettable Past. In LICS'02, pages 383-392. IEEE Comp. Soc. Press, July 2002. 10.1109/LICS.2002.1029846 PDFTest-of-time award Abstract + BibTeX Abstract We investigate NLTL, a linear-time temporal logic with forgettable past. NLTL can be exponentially more succinct than LTL + Past (which in turn can be more succinct than LTL). We study satisfiability and model checking for NLTL and provide optimal automata-theoretic algorithms for these EXPSPACE-complete problems. @inproceedings{lics2002-LMS, author = {Laroussinie, Fran{\c c}ois and Markey, Nicolas and Schnoebelen, {\relax Ph}ilippe}, title = {Temporal Logic with Forgettable Past}, booktitle = {{P}roceedings of the 17th {A}nnual {S}ymposium on {L}ogic in {C}omputer {S}cience ({LICS}'02)}, acronym = {{LICS}'02}, publisher = {IEEE Comp. Soc. Press}, pages = {383-392}, year = {2002}, month = jul, doi = {10.1109/LICS.2002.1029846}, abstract = {We investigate NLTL, a linear-time temporal logic with forgettable past. NLTL can be exponentially more succinct than LTL + Past (which in turn can be more succinct than LTL). We study satisfiability and model checking for NLTL and provide optimal automata-theoretic algorithms for these EXPSPACE-complete problems.}, }
[Mar02]	Nicolas Markey. Past is for Free: On the Complexity of Verifying Linear Temporal Properties with Past. In EXPRESS'02, Electronic Notes in Theoretical Computer Science 68(2), pages 89-106. Elsevier, August 2002. 10.1016/S1571-0661(05)80366-4 PDF Abstract + BibTeX Abstract We study the complexity of satisfiability and model-checking of the linear-time temporal logic with past (PLTL). More precisely, we consider several fragments of PLTL, depending on the allowed set of temporal modalities, the use of negations or the nesting of future formulae into past formulae. Our results show that "past is for free", that is it does not bring additional theoretical complexity, even for small fragments, and even when nesting future formulae into past formulae. We also remark that existential and universal model-checking can have different complexity for certain fragments. @inproceedings{express2002-Mar, author = {Markey, Nicolas}, title = {Past is for Free: On the Complexity of Verifying Linear Temporal Properties with Past}, editor = {Nestmann, Uwe and Panangaden, Prakash}, booktitle = {{P}roceedings of the 9th {I}nternational {W}orkshop on {E}xpressiveness in {C}oncurrency ({EXPRESS}'02)}, acronym = {{EXPRESS}'02}, publisher = {Elsevier}, series = {Electronic Notes in Theoretical Computer Science}, volume = {68}, number = {2}, pages = {89-106}, year = {2002}, month = aug, doi = {10.1016/S1571-0661(05)80366-4}, abstract = {We study the complexity of satisfiability and model-checking of the linear-time temporal logic with past~(PLTL). More precisely, we consider several fragments of PLTL, depending on the allowed set of temporal modalities, the use of negations or the nesting of future formulae into past formulae. Our~results show that {"}past is for free{"}, that is it does not bring additional theoretical complexity, even for small fragments, and even when nesting future formulae into past formulae. We~also remark that existential and universal model-checking can have different complexity for certain fragments.}, }
[AC02]	Jean-Pierre Aubin and Francine Catté. Bilateral Fixed-point and Algebraic Properties of Viability Kernels and Capture Basins of Sets. Technical Report 02-10, CeReMaDe, Université Paris 9, Paris, France, April 2002. BibTeX @techreport{TR-Ceremade0210, author = {Aubin, Jean-Pierre and Catt{\'e}, Francine}, title = {Bilateral Fixed-point and Algebraic Properties of Viability Kernels and Capture Basins of Sets}, number = {02-10}, year = {2002}, month = apr, institution = {CeReMaDe, Universit\'e Paris 9, Paris, France}, }
[AFF+02]	Roy Armoni, Limor Fix, Alon Flaisher, Rob Gerth, Boris Ginsburg, Tomer Kanza, Avner Landver, Sela Mador-Haim, Eli Singerman, Andreas Tiemeyer, Moshe Y. Vardi, and Yael Zbar. The ForSpec Temporal Logic: A New Temporal Property-Specification Language. In TACAS'02, Lecture Notes in Computer Science 2280, pages 296-311. Springer-Verlag, April 2002. BibTeX @inproceedings{tacas2002-AFFGGKLMSTVZ, author = {Armoni, Roy and Fix, Limor and Flaisher, Alon and Gerth, Rob and Ginsburg, Boris and Kanza, Tomer and Landver, Avner and Mador{-}Haim, Sela and Singerman, Eli and Tiemeyer, Andreas and Vardi, Moshe Y. and Zbar, Yael}, title = {The {ForSpec} Temporal Logic: A New Temporal Property-Specification Language}, editor = {Katoen, Joost-Pieter and Stevens, Perdita}, booktitle = {{P}roceedings of the 8th {I}nternational {C}onference on {T}ools and {A}lgorithms for {C}onstruction and {A}nalysis of {S}ystems ({TACAS}'02)}, acronym = {{TACAS}'02}, publisher = {Springer-Verlag}, series = {Lecture Notes in Computer Science}, volume = {2280}, pages = {296-311}, year = {2002}, month = apr, }
[AFM+02]	Tobias Amnell, Elena Fersman, Leonid Mokrushin, Paul Pettersson, and Wang Yi. TIMES – A Tool for Modelling and Implementation of Embedded Systems. In TACAS'02, Lecture Notes in Computer Science 2280, pages 460-464. Springer-Verlag, April 2002. BibTeX @inproceedings{tacas2002-AFMPY, author = {Amnell, Tobias and Fersman, Elena and Mokrushin, Leonid and Pettersson, Paul and Yi, Wang}, title = {TIMES~-- A~Tool for Modelling and Implementation of Embedded Systems}, editor = {Katoen, Joost-Pieter and Stevens, Perdita}, booktitle = {{P}roceedings of the 8th {I}nternational {C}onference on {T}ools and {A}lgorithms for {C}onstruction and {A}nalysis of {S}ystems ({TACAS}'02)}, acronym = {{TACAS}'02}, publisher = {Springer-Verlag}, series = {Lecture Notes in Computer Science}, volume = {2280}, pages = {460-464}, year = {2002}, month = apr, }
[AH02]	Henrik Reif Andersen and Henrik Hulgaard. Boolean Expression Diagrams. Information and Computation 179(2):194-212. Academic Press, December 2002. 10.1006/inco.2001.2948 BibTeX @article{icomp179(2)-AH, author = {Andersen, Henrik Reif and Hulgaard, Henrik}, title = {Boolean Expression Diagrams}, publisher = {Academic Press}, journal = {Information and Computation}, volume = {179}, number = {2}, pages = {194-212}, year = {2002}, month = dec, doi = {10.1006/inco.2001.2948}, }
[AHK02]	Rajeev Alur, Thomas A. Henzinger, and Orna Kupferman. Alternating-time Temporal Logic. Journal of the ACM 49(5):672-713. ACM Press, September 2002. 10.1145/585265.585270 PDF BibTeX @article{jacm49(5)-AHK, author = {Alur, Rajeev and Henzinger, Thomas A. and Kupferman, Orna}, title = {Alternating-time Temporal Logic}, publisher = {ACM Press}, journal = {Journal of the~ACM}, volume = {49}, number = {5}, pages = {672-713}, year = {2002}, month = sep, doi = {10.1145/585265.585270}, }
[AL02]	Luca Aceto and François Laroussinie. Is your Model Checker on Time?. Journal of Logic and Algebraic Programming 52-53:3-51. Elsevier, June 2002. PDF BibTeX @article{jlap52-53()-AL, author = {Aceto, Luca and Laroussinie, Fran{\c c}ois}, title = {Is your Model Checker on Time?}, publisher = {Elsevier}, journal = {Journal of Logic and Algebraic Programming}, volume = {52-53}, pages = {3-51}, year = {2002}, month = jun, }
[AM02]	Yasmina Abdeddaïm and Oded Maler. Preemptive Job-Shop Scheduling using Stopwatch Automata. In TACAS'02, Lecture Notes in Computer Science 2280, pages 113-126. Springer-Verlag, April 2002. BibTeX @inproceedings{tacas2002-AM, author = {Abdedda{\"\i}m, Yasmina and Maler, Oded}, title = {Preemptive Job-Shop Scheduling using Stopwatch Automata}, editor = {Katoen, Joost-Pieter and Stevens, Perdita}, booktitle = {{P}roceedings of the 8th {I}nternational {C}onference on {T}ools and {A}lgorithms for {C}onstruction and {A}nalysis of {S}ystems ({TACAS}'02)}, acronym = {{TACAS}'02}, publisher = {Springer-Verlag}, series = {Lecture Notes in Computer Science}, volume = {2280}, pages = {113-126}, year = {2002}, month = apr, }
[AS02]	Eugene Asarin and Gerardo Schneider. Widening the Boundary between Decidable and Undecidable Hybrid Systems. In CONCUR'02, Lecture Notes in Computer Science 2421, pages 193-208. Springer-Verlag, August 2002. BibTeX @inproceedings{concur2002-AS, author = {Asarin, Eugene and Schneider, Gerardo}, title = {Widening the Boundary between Decidable and Undecidable Hybrid Systems}, editor = {Brim, Lubo{\v s} and Jan{\v c}ar, Petr and K{\v r}et{\'\i}nsk{\'y}, Mojm{\'\i}r and Ku{\v c}era, Anton{\'\i}n}, booktitle = {{P}roceedings of the 13th {I}nternational {C}onference on {C}oncurrency {T}heory ({CONCUR}'02)}, acronym = {{CONCUR}'02}, publisher = {Springer-Verlag}, series = {Lecture Notes in Computer Science}, volume = {2421}, pages = {193-208}, year = {2002}, month = aug, }
[Asp02]	James Aspnes. Fast deterministic consensus in a noisy environment. Journal of Algorithms 45(1):16-39. Elsevier, October 2002. 10.1016/S0196-6774(02)00220-1 PDF BibTeX @article{ja45(1)-Asp, author = {Aspnes, James}, title = {Fast deterministic consensus in a noisy environment}, publisher = {Elsevier}, journal = {Journal of Algorithms}, volume = {45}, number = {1}, pages = {16-39}, year = {2002}, month = oct, doi = {10.1016/S0196-6774(02)00220-1}, }
[AT02]	Karine Altisen and Stavros Tripakis. Tools for Controller Synthesis of Timed Systems. In RT-TOOLS'02. August 2002. BibTeX @inproceedings{rttools2002-AT, author = {Altisen, Karine and Tripakis, Stavros}, title = {Tools for Controller Synthesis of Timed Systems}, editor = {Pettersson, Paul and Yi, Wang}, booktitle = {{P}roceedings of the 2nd {W}orkshop on {R}eal-Time {T}ools ({RT-TOOLS}'02)}, acronym = {{RT-TOOLS}'02}, year = {2002}, month = aug, }
[Ats02]	Albert Atserias. Unsatisfiable Random Formulas are Hard to Certify. In LICS'02, pages 325-334. IEEE Comp. Soc. Press, July 2002. BibTeX @inproceedings{lics2002-Ats, author = {Atserias, Albert}, title = {Unsatisfiable Random Formulas are Hard to Certify}, booktitle = {{P}roceedings of the 17th {A}nnual {S}ymposium on {L}ogic in {C}omputer {S}cience ({LICS}'02)}, acronym = {{LICS}'02}, publisher = {IEEE Comp. Soc. Press}, pages = {325-334}, year = {2002}, month = jul, }
[BAS02]	Armin Biere, Cyrille Artho, and Viktor Schuppan. Liveness Checking as Safety Checking. In FMICS'02, Electronic Notes in Theoretical Computer Science 66(2). Elsevier, July 2002. BibTeX @inproceedings{fmics2002-BAS, author = {Biere, Armin and Artho, Cyrille and Schuppan, Viktor}, title = {Liveness Checking as Safety Checking}, editor = {Cleaveland, Rance and Garavel, Hubert}, booktitle = {{P}roceedings of the 7th {I}nternational {ERCIM} {W}orkshop in {F}ormal {M}ethods for {I}ndustrial {C}ritical {S}ystems ({FMICS}'02)}, acronym = {{FMICS}'02}, publisher = {Elsevier}, series = {Electronic Notes in Theoretical Computer Science}, volume = {66}, number = {2}, year = {2002}, month = jul, }
[BB02]	Dietmar Berwanger and Achim Blumensath. The Monadic Theory of Tree-like Structures. In Erich Grädel, Wolfgang Thomas, and Thomas Wilke (eds.), Automata, Logics, and Infinite Games, Lecture Notes in Computer Science 2500, pages 285-302. Springer-Verlag, 2002. PDF BibTeX @incollection{lncs2500-BB, author = {Berwanger, Dietmar and Blumensath, Achim}, title = {The Monadic Theory of Tree-like Structures}, editor = {Gr{\"a}del, Erich and Thomas, Wolfgang and Wilke, Thomas}, booktitle = {Automata, Logics, and Infinite Games}, publisher = {Springer-Verlag}, series = {Lecture Notes in Computer Science}, volume = {2500}, pages = {285-302}, year = {2002}, }
[BBD+02]	Gerd Behrmann, Johan Bengtsson, Alexandre David, Kim Guldstrand Larsen, Paul Pettersson, and Wang Yi. UPPAAL Implementation Secrets. In FTRTFT'02, Lecture Notes in Computer Science 2469, pages 3-22. Springer-Verlag, September 2002. 10.1007/3-540-45739-9_1 BibTeX @inproceedings{ftrtft2002-BBDLPY, author = {Behrmann, Gerd and Bengtsson, Johan and David, Alexandre and Larsen, Kim Guldstrand and Pettersson, Paul and Yi, Wang}, title = {UPPAAL Implementation Secrets}, editor = {Damm, Werner and Olderog, Ernst R{\"u}diger}, booktitle = {{P}roceedings of the 7th {F}ormal {T}echniques in {R}eal-Time and {F}ault-Tolerant {S}ystems ({FTRTFT}'02)}, acronym = {{FTRTFT}'02}, publisher = {Springer-Verlag}, series = {Lecture Notes in Computer Science}, volume = {2469}, pages = {3-22}, year = {2002}, month = sep, doi = {10.1007/3-540-45739-9_1}, }
[BFD02]	Alexander Bolotov, Michael J. Fischer, and Clare Dixon. On the Relationship between ω-Automata and Temporal Logic Normal Forms. Journal of Logic and Computation 12(4):561-581. Oxford University Press, August 2002. BibTeX @article{jlc12(4)-BFD, author = {Bolotov, Alexander and Fischer, Michael J. and Dixon, Clare}, title = {On the Relationship between {\(\omega\)}-Automata and Temporal Logic Normal Forms}, publisher = {Oxford University Press}, journal = {Journal of Logic and Computation}, volume = {12}, number = {4}, pages = {561-581}, year = {2002}, month = aug, }
[BG02]	Robert Baumgartner and Georg Gottlob. Propositional Default Logics made Easier: Computational Complexity of Model Checking. Theoretical Computer Science 289(1):591-627. Elsevier, October 2002. BibTeX @article{tcs289(1)-BG, author = {Baumgartner, Robert and Gottlob, Georg}, title = {Propositional Default Logics made Easier: Computational Complexity of Model Checking}, publisher = {Elsevier}, journal = {Theoretical Computer Science}, volume = {289}, number = {1}, pages = {591-627}, year = {2002}, month = oct, }
[BHR+02]	Danièle Beauquier, Yoram Hirshfeld, Alexander Rabinovich, and Anatol Slissenko. The Probablity Nesting Game. In EXPRESS'02, Electronic Notes in Theoretical Computer Science 68(2), pages 3-13. Elsevier, August 2002. BibTeX @inproceedings{express2002-BHRS, author = {Beauquier, Dani{\`e}le and Hirshfeld, Yoram and Rabinovich, Alexander and Slissenko, Anatol}, title = {The Probablity Nesting Game}, editor = {Nestmann, Uwe and Panangaden, Prakash}, booktitle = {{P}roceedings of the 9th {I}nternational {W}orkshop on {E}xpressiveness in {C}oncurrency ({EXPRESS}'02)}, acronym = {{EXPRESS}'02}, publisher = {Elsevier}, series = {Electronic Notes in Theoretical Computer Science}, volume = {68}, number = {2}, pages = {3-13}, year = {2002}, month = aug, }
[BJM+02]	Marius Bozga, Hou Jianmin, Oded Maler, and Sergio Yovine. Verification of Asynchronous Circuits using Timed Automata. In TPTS'02, Electronic Notes in Theoretical Computer Science 65(6), pages 47-59. Elsevier, April 2002. BibTeX @inproceedings{tpts2002-BJMY, author = {Bozga, Marius and Jianmin, Hou and Maler, Oded and Yovine, Sergio}, title = {Verification of Asynchronous Circuits using Timed Automata}, editor = {Asarin, Eugene and Maler, Oded and Yovine, Sergio}, booktitle = {{P}roceedings of the 1st {W}orkshop on {T}heory and {P}ractice of {T}imed {S}ystems ({TPTS}'02)}, acronym = {{TPTS}'02}, publisher = {Elsevier}, series = {Electronic Notes in Theoretical Computer Science}, volume = {65}, number = {6}, pages = {47-59}, year = {2002}, month = apr, }
[BJW02]	Julien Bernet, David Janin, and Igor Walukiewicz. Permissive strategies: from parity games to safety games. RAIRO – Theoretical Informatics and Applications 36(3):261-275. EDP Sciences, 2002. BibTeX @article{rairo-tia36(3)-BJW, author = {Bernet, Julien and Janin, David and Walukiewicz, Igor}, title = {Permissive strategies: from parity games to safety games}, publisher = {EDP Sciences}, journal = {RAIRO~-- Theoretical Informatics and Applications}, volume = {36}, number = {3}, pages = {261-275}, year = {2002}, }
[BMF02]	Ed Brinksma, Angelika Mader, and Ansgar Fehnker. Verification and Optimization of a PLC Control Schedule. International Journal on Software Tools for Technology Transfer 4(1):21-33. Springer-Verlag, 2002. BibTeX @article{sttt4(1)-BMF, author = {Brinksma, Ed and Mader, Angelika and Fehnker, Ansgar}, title = {Verification and Optimization of a {PLC} Control Schedule}, publisher = {Springer-Verlag}, journal = {International Journal on Software Tools for Technology Transfer}, volume = {4}, number = {1}, pages = {21-33}, year = {2002}, }
[Bou02]	Patricia Bouyer. Timed Automata May Cause some Troubles. Research Report LSV-02-09, Lab. Spécification & Vérification, ENS Cachan, France, July 2002. BibTeX @techreport{LSV0209-Bou, author = {Bouyer, Patricia}, title = {Timed Automata May Cause some Troubles}, number = {LSV-02-09}, year = {2002}, month = jul, institution = {Lab.~Sp\'ecification \& V\'erification, ENS Cachan, France}, type = {Research Report}, }
[BR02]	Danièle Beauquier and Alexander Rabinovich. Monadic Logic of Order over Naturals has no Finite Base. Journal of Logic and Computation 12(2):243-253. Oxford University Press, April 2002. BibTeX @article{jlc12(2)-BR, author = {Beauquier, Dani{\`e}le and Rabinovich, Alexander}, title = {Monadic Logic of Order over Naturals has no Finite Base}, publisher = {Oxford University Press}, journal = {Journal of Logic and Computation}, volume = {12}, number = {2}, pages = {243-253}, year = {2002}, month = apr, }
[BTK+02]	Cécile Bui Thanh, Hanna Klaudel, and Franck Pommereau. Petri Nets with Causal Time for System Verification. In MTCS'02, Electronic Notes in Theoretical Computer Science 68(5). Elsevier, August 2002. BibTeX @inproceedings{mtcs2003-BKP, author = {Bui Thanh, C{\'e}cile and Klaudel, Hanna and Pommereau, Franck}, title = {{P}etri Nets with Causal Time for System Verification}, editor = {Vogler, Walter and Larsen, Kim Guldstrand}, booktitle = {{P}roceedings of the 3rd {I}nternational {W}orkshop on {M}odels for {T}ime-Critical {S}ystems ({MTCS}'02)}, acronym = {{MTCS}'02}, publisher = {Elsevier}, series = {Electronic Notes in Theoretical Computer Science}, volume = {68}, number = {5}, year = {2002}, month = aug, }
[CC02]	Cristian S. Calude and Elena Calude. The Bridge Crossing Problem. EATCS Bulletin 77:180-190. EATCS, June 2002. BibTeX @article{eatcs-bull77()-CC, author = {Calude, Cristian S. and Calude, Elena}, title = {The Bridge Crossing Problem}, publisher = {EATCS}, journal = {EATCS Bulletin}, volume = {77}, pages = {180-190}, year = {2002}, month = jun, }
[CCG+02]	Alessandro Cimatti, Edmund M. Clarke, Enrico Giunchiglia, Fausto Giunchiglia, Marco Pistore, Marco Roveri, Roberto Sebastiani, and Armando Tacchella. NuSMV2: An OpenSource Tool for Symbolic Model Checking. In CAV'02, Lecture Notes in Computer Science 2404, pages 359-364. Springer-Verlag, July 2002. BibTeX @inproceedings{cav2002-CCGGPRST, author = {Cimatti, Alessandro and Clarke, Edmund M. and Giunchiglia, Enrico and Giunchiglia, Fausto and Pistore, Marco and Roveri, Marco and Sebastiani, Roberto and Tacchella, Armando}, title = {{NuSMV2}: An OpenSource Tool for Symbolic Model Checking}, editor = {Brinksma, Ed and Larsen, Kim Guldstrand}, booktitle = {{P}roceedings of the 14th {I}nternational {C}onference on {C}omputer {A}ided {V}erification ({CAV}'02)}, acronym = {{CAV}'02}, publisher = {Springer-Verlag}, series = {Lecture Notes in Computer Science}, volume = {2404}, pages = {359-364}, year = {2002}, month = jul, }
[CDV02]	Diego Calvanese, Giuseppe De Giacomo, and Moshe Y. Vardi. Reasoning about Actions and Planning in LTL Action Theories. In KR'02, pages 593-602. Morgan Kaufmann Publishers, April 2002. BibTeX @inproceedings{kr2002-CDV, author = {Calvanese, Diego and De{~}Giacomo, Giuseppe and Vardi, Moshe Y.}, title = {Reasoning about Actions and Planning in {LTL} Action Theories}, editor = {Giunchiglia, Fausto}, booktitle = {{P}roceedings of the 8th {I}nternational {C}onference on {P}rinciples of {K}nowledge {R}epresentation and {R}easoning ({KR}'02)}, acronym = {{KR}'02}, publisher = {Morgan Kaufmann Publishers}, pages = {593-602}, year = {2002}, month = apr, }
[CGP+02]	Alessandro Cimatti, Enrico Giunchiglia, Marco Pistore, Marco Roveri, Roberto Sebastiani, and Armando Tacchella. Integrating BDD-based and SAT-based Symbolic Model Checking. In FroCoS'02, Lecture Notes in Computer Science 2309, pages 49-56. Springer-Verlag, April 2002. BibTeX @inproceedings{frocos2002-CGPRST, author = {Cimatti, Alessandro and Giunchiglia, Enrico and Pistore, Marco and Roveri, Marco and Sebastiani, Roberto and Tacchella, Armando}, title = {Integrating {BDD}-based and {SAT}-based Symbolic Model Checking}, editor = {Armando, Alessandro}, booktitle = {{P}roceedings of the 4th {I}nternational {W}orkshop on {F}rontiers of {C}ombining {S}ystems ({FroCoS}'02)}, acronym = {{FroCoS}'02}, publisher = {Springer-Verlag}, series = {Lecture Notes in Computer Science}, volume = {2309}, pages = {49-56}, year = {2002}, month = apr, }
[CHR02]	Franck Cassez, Thomas A. Henzinger, and Jean-François Raskin. A Comparison of Control Problems for Timed and Hybrid Systems. In HSCC'02, Lecture Notes in Computer Science 2289, pages 134-148. Springer-Verlag, March 2002. PDF BibTeX @inproceedings{hscc2002-CHR, author = {Cassez, Franck and Henzinger, Thomas A. and Raskin, Jean-Fran{\c c}ois}, title = {A Comparison of Control Problems for Timed and Hybrid Systems}, editor = {Tomlin, Claire and Greenstreet, Mark R.}, booktitle = {{P}roceedings of the 5th {I}nternational {W}orkshop on {H}ybrid {S}ystems: {C}omputation and {C}ontrol ({HSCC}'02)}, acronym = {{HSCC}'02}, publisher = {Springer-Verlag}, series = {Lecture Notes in Computer Science}, volume = {2289}, pages = {134-148}, year = {2002}, month = mar, }
[CJL+02]	Edmund M. Clarke, Somesh Jha, Yuan Lu, and Helmut Veith. Tree-Like Counterexamples in Model Checking. In LICS'02, pages 19-29. IEEE Comp. Soc. Press, July 2002. BibTeX @inproceedings{lics2002-CJLV, author = {Clarke, Edmund M. and Jha, Somesh and Lu, Yuan and Veith, Helmut}, title = {Tree-Like Counterexamples in Model Checking}, booktitle = {{P}roceedings of the 17th {A}nnual {S}ymposium on {L}ogic in {C}omputer {S}cience ({LICS}'02)}, acronym = {{LICS}'02}, publisher = {IEEE Comp. Soc. Press}, pages = {19-29}, year = {2002}, month = jul, }
[CL02]	Rance Cleaveland and Gerald Lüttgen. A Logical Process Calculi. In EXPRESS'02, Electronic Notes in Theoretical Computer Science 68(2), pages 33-50. Elsevier, August 2002. BibTeX @inproceedings{express2002-CL, author = {Cleaveland, Rance and L{\"u}ttgen, Gerald}, title = {A Logical Process Calculi}, editor = {Nestmann, Uwe and Panangaden, Prakash}, booktitle = {{P}roceedings of the 9th {I}nternational {W}orkshop on {E}xpressiveness in {C}oncurrency ({EXPRESS}'02)}, acronym = {{EXPRESS}'02}, publisher = {Elsevier}, series = {Electronic Notes in Theoretical Computer Science}, volume = {68}, number = {2}, pages = {33-50}, year = {2002}, month = aug, }
[CM02]	Marco Carbone and Sergio Maffeis. On the Expressive Power of Polyadic Synchronisation in π-calculus. In EXPRESS'02, Electronic Notes in Theoretical Computer Science 68(2), pages 15-32. Elsevier, August 2002. BibTeX @inproceedings{express2002-CM, author = {Carbone, Marco and Maffeis, Sergio}, title = {On the Expressive Power of Polyadic Synchronisation in {\(\pi\)}-calculus}, editor = {Nestmann, Uwe and Panangaden, Prakash}, booktitle = {{P}roceedings of the 9th {I}nternational {W}orkshop on {E}xpressiveness in {C}oncurrency ({EXPRESS}'02)}, acronym = {{EXPRESS}'02}, publisher = {Elsevier}, series = {Electronic Notes in Theoretical Computer Science}, volume = {68}, number = {2}, pages = {15-32}, year = {2002}, month = aug, }
[CPR+02]	Alessandro Cimatti, Marco Pistore, Marco Roveri, and Roberto Sebastiani. Improving the Encoding of LTL Model Checking into SAT. In VMCAI'02, Lecture Notes in Computer Science 2294, pages 196-207. Springer-Verlag, January 2002. BibTeX @inproceedings{vmcai2002-CPRS, author = {Cimatti, Alessandro and Pistore, Marco and Roveri, Marco and Sebastiani, Roberto}, title = {Improving the Encoding of {LTL} Model Checking into {SAT}}, editor = {Cortesi, Agostino}, booktitle = {{P}roceedings of the 3rd {I}nternational {W}orkshop on {V}erification, {M}odel {C}hecking, and {A}bstract {I}nterpretation ({VMCAI}'02)}, acronym = {{VMCAI}'02}, publisher = {Springer-Verlag}, series = {Lecture Notes in Computer Science}, volume = {2294}, pages = {196-207}, year = {2002}, month = jan, }
[DG02]	Jennifer M. Davoren and Rajeev Prabhakar Gore. Bimodal Logics for Reasoning about Continuous Dynamics. In AIML'00. World Scientific, 2002. BibTeX @inproceedings{aiml2000-DG, author = {Davoren, Jennifer M. and Gore, Rajeev Prabhakar}, title = {Bimodal Logics for Reasoning about Continuous Dynamics}, editor = {de Rijke, Marteen and Wansing, Heinrich and Wolter, Frank and Zakharyaschev, Michael}, booktitle = {{P}roceedings of the 3rd {W}orkshop on {A}dvances in {M}odal {L}ogic ({AIML}'00)}, acronym = {{AIML}'00}, publisher = {World Scientific}, year = {2002}, confyear = {2000}, confmonth = {10}, }
[Dim02]	Cătălin Dima. Computing Reachability Relations in Timed Automata. In LICS'02, pages 177-186. IEEE Comp. Soc. Press, July 2002. BibTeX @inproceedings{lics2002-Dim, author = {Dima, C{\u a}t{\u a}lin}, title = {Computing Reachability Relations in Timed Automata}, booktitle = {{P}roceedings of the 17th {A}nnual {S}ymposium on {L}ogic in {C}omputer {S}cience ({LICS}'02)}, acronym = {{LICS}'02}, publisher = {IEEE Comp. Soc. Press}, pages = {177-186}, year = {2002}, month = jul, }
[DLS02]	Stéphane Demri, François Laroussinie, and Philippe Schnoebelen. A Parametric Analysis of the State Explosion Problem in Model Checking (Extended Abstract). In STACS'02, Lecture Notes in Computer Science 2285, pages 620-631. Springer-Verlag, March 2002. BibTeX @inproceedings{stacs2002-DLS, author = {Demri, St{\'e}phane and Laroussinie, Fran{\c c}ois and Schnoebelen, {\relax Ph}ilippe}, title = {A Parametric Analysis of the State Explosion Problem in Model Checking (Extended Abstract)}, editor = {Alt, Helmut and Ferreira, Afonso}, booktitle = {{P}roceedings of the 19th {S}ymposium on {T}heoretical {A}spects of {C}omputer {S}cience ({STACS}'02)}, acronym = {{STACS}'02}, publisher = {Springer-Verlag}, series = {Lecture Notes in Computer Science}, volume = {2285}, pages = {620-631}, year = {2002}, month = mar, }
[DM02]	Deepak D'Souza and Parthasarathy Madhusudan. Timed Control Synthesis for External Specifications. In STACS'02, Lecture Notes in Computer Science 2285, pages 571-582. Springer-Verlag, March 2002. BibTeX @inproceedings{stacs2002-DM, author = {D'Souza, Deepak and Madhusudan, Parthasarathy}, title = {Timed Control Synthesis for External Specifications}, editor = {Alt, Helmut and Ferreira, Afonso}, booktitle = {{P}roceedings of the 19th {S}ymposium on {T}heoretical {A}spects of {C}omputer {S}cience ({STACS}'02)}, acronym = {{STACS}'02}, publisher = {Springer-Verlag}, series = {Lecture Notes in Computer Science}, volume = {2285}, pages = {571-582}, year = {2002}, month = mar, }
[DS02]	Stéphane Demri and Philippe Schnoebelen. The Complexity of Propositional Linear Temporal Logics in Simple Cases. Information and Computation 174(1):84-103. Academic Press, April 2002. BibTeX @article{icomp174(1)-DS, author = {Demri, St{\'e}phane and Schnoebelen, {\relax Ph}ilippe}, title = {The Complexity of Propositional Linear Temporal Logics in Simple Cases}, publisher = {Academic Press}, journal = {Information and Computation}, volume = {174}, number = {1}, pages = {84-103}, year = {2002}, month = apr, }
[DS02]	Stéphane Demri and Ulrike Sattler. Automata-Theoretic Decision Procedures for Information Logics. Fundamenta Informaticae 53(1):1-22. IOS Press, 2002. BibTeX @article{fundi53(1)-DS, author = {Demri, St{\'e}phane and Sattler, Ulrike}, title = {Automata-Theoretic Decision Procedures for Information Logics}, publisher = {IOS Press}, journal = {Fundamenta Informaticae}, volume = {53}, number = {1}, pages = {1-22}, year = {2002}, }
[END+02]	Abdeslam En-Nouaary, Radhida Dssouli, and Ferhat Khendek. Timed Wp-Method: Testing Real-Time Systems. IEEE Transactions on Software Engineering 28(11):1023-1038. IEEE Comp. Soc. Press, November 2002. 10.1109/TSE.2002.1049402 BibTeX @article{tse28(11)-EDK, author = {En-Nouaary, Abdeslam and Dssouli, Radhida and Khendek, Ferhat}, title = {Timed Wp-Method: Testing Real-Time Systems}, publisher = {IEEE Comp. Soc. Press}, journal = {IEEE Transactions on Software Engineering}, volume = {28}, number = {11}, pages = {1023-1038}, year = {2002}, month = nov, doi = {10.1109/TSE.2002.1049402}, }
[Ete02]	Kousha Etessami. A Hierarchy of Polynomial-Time Computable Simulations for Automata. In CONCUR'02, Lecture Notes in Computer Science 2421, pages 131-144. Springer-Verlag, August 2002. BibTeX @inproceedings{concur2002-Ete, author = {Etessami, Kousha}, title = {A Hierarchy of Polynomial-Time Computable Simulations for Automata}, editor = {Brim, Lubo{\v s} and Jan{\v c}ar, Petr and K{\v r}et{\'\i}nsk{\'y}, Mojm{\'\i}r and Ku{\v c}era, Anton{\'\i}n}, booktitle = {{P}roceedings of the 13th {I}nternational {C}onference on {C}oncurrency {T}heory ({CONCUR}'02)}, acronym = {{CONCUR}'02}, publisher = {Springer-Verlag}, series = {Lecture Notes in Computer Science}, volume = {2421}, pages = {131-144}, year = {2002}, month = aug, }
[EVW02]	Kousha Etessami, Moshe Y. Vardi, and Thomas Wilke. First-Order Logic with Two Variables and Unary Temporal Logic. Information and Computation 179(2):279-295. Academic Press, December 2002. PDF BibTeX @article{icomp179(2)-EVW, author = {Etessami, Kousha and Vardi, Moshe Y. and Wilke, Thomas}, title = {First-Order Logic with Two Variables and Unary Temporal Logic}, publisher = {Academic Press}, journal = {Information and Computation}, volume = {179}, number = {2}, pages = {279-295}, year = {2002}, month = dec, }
[Far02]	Berndt Farwer. ω-automata. In Erich Grädel, Wolfgang Thomas, and Thomas Wilke (eds.), Automata, Logics, and Infinite Games, Lecture Notes in Computer Science 2500, pages 3-21. Springer-Verlag, 2002. BibTeX @incollection{lncs2500-Far, author = {Farwer, Berndt}, title = {{{\(\omega\)}}-automata}, editor = {Gr{\"a}del, Erich and Thomas, Wolfgang and Wilke, Thomas}, booktitle = {Automata, Logics, and Infinite Games}, publisher = {Springer-Verlag}, series = {Lecture Notes in Computer Science}, volume = {2500}, pages = {3-21}, year = {2002}, }
[FG02]	Jörg Flum and Martin Grohe. Describing Parameterized Complexity Classes. In STACS'02, Lecture Notes in Computer Science 2285, pages 359-371. Springer-Verlag, March 2002. BibTeX @inproceedings{stacs2002-FG, author = {Flum, J{\"o}rg and Grohe, Martin}, title = {Describing Parameterized Complexity Classes}, editor = {Alt, Helmut and Ferreira, Afonso}, booktitle = {{P}roceedings of the 19th {S}ymposium on {T}heoretical {A}spects of {C}omputer {S}cience ({STACS}'02)}, acronym = {{STACS}'02}, publisher = {Springer-Verlag}, series = {Lecture Notes in Computer Science}, volume = {2285}, pages = {359-371}, year = {2002}, month = mar, }
[FG02]	Markus Frick and Martin Grohe. The Complexity of First-Order and Monadic Second-Order Logic Revisited. In LICS'02, pages 215-224. IEEE Comp. Soc. Press, July 2002. BibTeX @inproceedings{lics2002-FG, author = {Frick, Markus and Grohe, Martin}, title = {The Complexity of First-Order and Monadic Second-Order Logic Revisited}, booktitle = {{P}roceedings of the 17th {A}nnual {S}ymposium on {L}ogic in {C}omputer {S}cience ({LICS}'02)}, acronym = {{LICS}'02}, publisher = {IEEE Comp. Soc. Press}, pages = {215-224}, year = {2002}, month = jul, }
[FHN02]	Ulrik Frendrup, Hans Hüttel, and Jesper Nyholm Jensen. Modal Logic for Cryptographic Systems. In EXPRESS'02, Electronic Notes in Theoretical Computer Science 68(2), pages 127-144. Elsevier, August 2002. BibTeX @inproceedings{express2002-FHN, author = {Frendrup, Ulrik and H{\"u}ttel, Hans and Nyholm{ }Jensen, Jesper}, title = {Modal Logic for Cryptographic Systems}, editor = {Nestmann, Uwe and Panangaden, Prakash}, booktitle = {{P}roceedings of the 9th {I}nternational {W}orkshop on {E}xpressiveness in {C}oncurrency ({EXPRESS}'02)}, acronym = {{EXPRESS}'02}, publisher = {Elsevier}, series = {Electronic Notes in Theoretical Computer Science}, volume = {68}, number = {2}, pages = {127-144}, year = {2002}, month = aug, }
[FL02]	Alain Finkel and Jérôme Leroux. How to Compose Presburger-Accelerations: Applications to Broadcast Protocols. Research Report, Lab. Spécification & Vérification, ENS Cachan, France, September 2002. BibTeX @techreport{LSV-02-14, author = {Finkel, Alain and Leroux, J{\'e}r{\^o}me}, title = {How to Compose {P}resburger-Accelerations: Applications to Broadcast Protocols}, year = {2002}, month = sep, institution = {Lab.~Sp\'ecification \& V\'erification, ENS Cachan, France}, type = {Research Report}, }
[FLM02]	Marco Faella, Salvatore La Torre, and Aniello Murano. Dense Real-Time Games. In LICS'02, pages 167-176. IEEE Comp. Soc. Press, July 2002. BibTeX @inproceedings{lics2002-FLM, author = {Faella, Marco and La{~}Torre, Salvatore and Murano, Aniello}, title = {Dense Real-Time Games}, booktitle = {{P}roceedings of the 17th {A}nnual {S}ymposium on {L}ogic in {C}omputer {S}cience ({LICS}'02)}, acronym = {{LICS}'02}, publisher = {IEEE Comp. Soc. Press}, pages = {167-176}, year = {2002}, month = jul, }
[FLM02]	Marco Faella, Salvatore La Torre, and Aniello Murano. Automata-Theoretic Decision of Timed Games. In VMCAI'02, Lecture Notes in Computer Science 2294, pages 94-108. Springer-Verlag, January 2002. BibTeX @inproceedings{vmcai2002-FLM, author = {Faella, Marco and La{~}Torre, Salvatore and Murano, Aniello}, title = {Automata-Theoretic Decision of Timed Games}, editor = {Cortesi, Agostino}, booktitle = {{P}roceedings of the 3rd {I}nternational {W}orkshop on {V}erification, {M}odel {C}hecking, and {A}bstract {I}nterpretation ({VMCAI}'02)}, acronym = {{VMCAI}'02}, publisher = {Springer-Verlag}, series = {Lecture Notes in Computer Science}, volume = {2294}, pages = {94-108}, year = {2002}, month = jan, }
[FPY02]	Elena Fersman, Paul Pettersson, and Wang Yi. Timed Automata with Asynchronous Processes: Schedulability and Decidability. In TACAS'02, Lecture Notes in Computer Science 2280, pages 67-82. Springer-Verlag, April 2002. BibTeX @inproceedings{tacas2002-FPY, author = {Fersman, Elena and Pettersson, Paul and Yi, Wang}, title = {Timed Automata with Asynchronous Processes: Schedulability and Decidability}, editor = {Katoen, Joost-Pieter and Stevens, Perdita}, booktitle = {{P}roceedings of the 8th {I}nternational {C}onference on {T}ools and {A}lgorithms for {C}onstruction and {A}nalysis of {S}ystems ({TACAS}'02)}, acronym = {{TACAS}'02}, publisher = {Springer-Verlag}, series = {Lecture Notes in Computer Science}, volume = {2280}, pages = {67-82}, year = {2002}, month = apr, }
[FSS02]	Bernd Finkbeiner, Sriram Sankaranarayanan, and Henny Sipma. Collecting Statistics over Runtime Executions. In RV'02, Electronic Notes in Theoretical Computer Science 70(4). Elsevier, July 2002. BibTeX @inproceedings{rv2002-FSS, author = {Finkbeiner, Bernd and Sankaranarayanan, Sriram and Sipma, Henny}, title = {Collecting Statistics over Runtime Executions}, editor = {Havelund, Klaus and Ro{\c{s}}u, Grigore}, booktitle = {{P}roceedings of the 2nd {I}nternational {W}orkshop on {R}untime {V}erification ({RV}'02)}, acronym = {{RV}'02}, publisher = {Elsevier}, series = {Electronic Notes in Theoretical Computer Science}, volume = {70}, number = {4}, year = {2002}, month = jul, }
[GBD02]	Vijay Ganesh, Sergey Berezin, and David L. Dill. Deciding Presburger Arithmetic by Model Checking and Comparisons with Other Methods. In FMCAD'02, Lecture Notes in Computer Science 2517, pages 171-398. Springer-Verlag, November 2002. BibTeX @inproceedings{fmcad2002-GBD, author = {Ganesh, Vijay and Berezin, Sergey and Dill, David L.}, title = {Deciding {P}resburger Arithmetic by Model Checking and Comparisons with Other Methods}, editor = {Aagaard, Mark D. and O'Leary, John W.}, booktitle = {{P}roceedings of the 4th {I}nternational {C}onference on {F}ormal {M}ethods in {C}omputer-{A}ided {D}esign ({FMCAD}'02)}, acronym = {{FMCAD}'02}, publisher = {Springer-Verlag}, series = {Lecture Notes in Computer Science}, volume = {2517}, pages = {171-398}, year = {2002}, month = nov, }
[GK02]	Georg Gottlob and Christoph Koch. Monadic Queries over Tree-Structured Data. In LICS'02, pages 189-202. IEEE Comp. Soc. Press, July 2002. BibTeX @inproceedings{lics2002-GK, author = {Gottlob, Georg and Koch, Christoph}, title = {Monadic Queries over Tree-Structured Data}, booktitle = {{P}roceedings of the 17th {A}nnual {S}ymposium on {L}ogic in {C}omputer {S}cience ({LICS}'02)}, acronym = {{LICS}'02}, publisher = {IEEE Comp. Soc. Press}, pages = {189-202}, year = {2002}, month = jul, }
[GL02]	Dimitra Giannakopoulou and Flavio Lerda. From States to Transitions: Improving Translation of LTL Formulae to Büchi Automata. In FORTE'02, Lecture Notes in Computer Science 2529, pages 308-326. Springer-Verlag, November 2002. BibTeX @inproceedings{forte2002-GL, author = {Giannakopoulou, Dimitra and Lerda, Flavio}, title = {From States to Transitions: Improving Translation of {LTL} Formulae to {B}{\"u}chi Automata}, editor = {Peled, Doron A. and Vardi, Moshe Y.}, booktitle = {{P}roceedings of the 22th {IFIP} {WG}6.1 {I}nternational {C}onference on {F}ormal {T}echniques for {N}etworked and {D}istributed {S}ystems ({FORTE}'02)}, acronym = {{FORTE}'02}, publisher = {Springer-Verlag}, series = {Lecture Notes in Computer Science}, volume = {2529}, pages = {308-326}, year = {2002}, month = nov, }
[GP02]	Elsa Gunter and Doron A. Peled. Tracing the Executions of Concurrent Programs. In RV'02, Electronic Notes in Theoretical Computer Science 70(4). Elsevier, July 2002. BibTeX @inproceedings{rv2002-GP, author = {Gunter, Elsa and Peled, Doron A.}, title = {Tracing the Executions of Concurrent Programs}, editor = {Havelund, Klaus and Ro{\c{s}}u, Grigore}, booktitle = {{P}roceedings of the 2nd {I}nternational {W}orkshop on {R}untime {V}erification ({RV}'02)}, acronym = {{RV}'02}, publisher = {Elsevier}, series = {Electronic Notes in Theoretical Computer Science}, volume = {70}, number = {4}, year = {2002}, month = jul, }
[GTW02]	Erich Grädel, Wolfgang Thomas, and Thomas Wilke. Automata Logics, and Infinite Games – A Guide to Current Research. Lecture Notes in Computer Science 2500. Springer-Verlag, 2002. 10.1007/3-540-36387-4 BibTeX @book{GTW-lncs2500, title = {Automata Logics, and Infinite Games~-- A~Guide to Current Research}, editor = {Gr{\"a}del, Erich and Thomas, Wolfgang and Wilke, Thomas}, publisher = {Springer-Verlag}, series = {Lecture Notes in Computer Science}, volume = {2500}, year = {2002}, doi = {10.1007/3-540-36387-4}, }
[HAB02]	William Hesse, Eric Allender, and David A. Mix Barrington. Uniform constant-depth threshold circuits for division and iterated multiplication. Journal of Computer and System Sciences 65(4):695-716. Academic Press, December 2002. BibTeX @article{jcss65(4)-HAB, author = {Hesse, William and Allender, Eric and Barrington, David A. Mix}, title = {Uniform constant-depth threshold circuits for division and iterated multiplication}, publisher = {Academic Press}, journal = {Journal of Computer and System Sciences}, volume = {65}, number = {4}, pages = {695-716}, year = {2002}, month = dec, }
[HI02]	William Hesse and Neil Immerman. Complete Problems for Dynamic Complexity Classes. In LICS'02, pages 313-322. IEEE Comp. Soc. Press, July 2002. PDF BibTeX @inproceedings{lics2002-HI, author = {Hesse, William and Immerman, Neil}, title = {Complete Problems for Dynamic Complexity Classes}, booktitle = {{P}roceedings of the 17th {A}nnual {S}ymposium on {L}ogic in {C}omputer {S}cience ({LICS}'02)}, acronym = {{LICS}'02}, publisher = {IEEE Comp. Soc. Press}, pages = {313-322}, year = {2002}, month = jul, }
[HJM+02]	Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar, and Grégoire Sutre. Lazy abstraction. In POPL'02, ACM SIGPLAN Notices 37(1), pages 58-70. ACM Press, January 2002. BibTeX @inproceedings{popl2002-HJMS, author = {Henzinger, Thomas A. and Jhala, Ranjit and Majumdar, Rupak and Sutre, Gr{\'e}goire}, title = {Lazy abstraction}, booktitle = {Conference Record of the 29th {ACM} {SIGPLAN}-{SIGACT} {S}ymposium on {P}rinciples of {P}rogramming {L}anguages ({POPL}'02)}, acronym = {{POPL}'02}, publisher = {ACM Press}, series = {ACM SIGPLAN Notices}, volume = {37}, number = {1}, pages = {58-70}, year = {2002}, month = jan, }
[HJR02]	Alan J. Hoffman, Kate Jenkins, and Tim Roughgarden. On a game in directed graphs. Information Processing Letters 83(1):13-16. Elsevier, July 2002. BibTeX @article{ipl83(1)-HJR, author = {Hoffman, Alan J. and Jenkins, Kate and Roughgarden, Tim}, title = {On a game in directed graphs}, publisher = {Elsevier}, journal = {Information Processing Letters}, volume = {83}, number = {1}, pages = {13-16}, year = {2002}, month = jul, }
[HL02]	Martijn Hendriks and Kim Guldstrand Larsen. Exact Acceleration of real-Time Model Checking. In TPTS'02, Electronic Notes in Theoretical Computer Science 65(6). Elsevier, April 2002. BibTeX @inproceedings{tpts2002-HL, author = {Hendriks, Martijn and Larsen, Kim Guldstrand}, title = {Exact Acceleration of real-Time Model Checking}, editor = {Asarin, Eugene and Maler, Oded and Yovine, Sergio}, booktitle = {{P}roceedings of the 1st {W}orkshop on {T}heory and {P}ractice of {T}imed {S}ystems ({TPTS}'02)}, acronym = {{TPTS}'02}, publisher = {Elsevier}, series = {Electronic Notes in Theoretical Computer Science}, volume = {65}, number = {6}, year = {2002}, month = apr, }
[HR02]	Klaus Havelund and Grigore Roşu. Synthesizing monitors for safety properties. In TACAS'02, Lecture Notes in Computer Science 2280, pages 342-356. Springer-Verlag, April 2002. BibTeX @inproceedings{tacas2002-HR, author = {Havelund, Klaus and Ro{\c{s}}u, Grigore}, title = {Synthesizing monitors for safety properties}, editor = {Katoen, Joost-Pieter and Stevens, Perdita}, booktitle = {{P}roceedings of the 8th {I}nternational {C}onference on {T}ools and {A}lgorithms for {C}onstruction and {A}nalysis of {S}ystems ({TACAS}'02)}, acronym = {{TACAS}'02}, publisher = {Springer-Verlag}, series = {Lecture Notes in Computer Science}, volume = {2280}, pages = {342-356}, year = {2002}, month = apr, }
[HRS02]	Aidan Harding, Mark D. Ryan, and Pierre-Yves Schobbens. Approximating ATL* in ATL (Extended Abstract). In VMCAI'02, Lecture Notes in Computer Science 2294, pages 289-301. Springer-Verlag, January 2002. BibTeX @inproceedings{vmcai2002-HRS, author = {Harding, Aidan and Ryan, Mark D. and Schobbens, Pierre-Yves}, title = {Approximating {ATL}{\(^*\)} in~{ATL} (Extended Abstract)}, editor = {Cortesi, Agostino}, booktitle = {{P}roceedings of the 3rd {I}nternational {W}orkshop on {V}erification, {M}odel {C}hecking, and {A}bstract {I}nterpretation ({VMCAI}'02)}, acronym = {{VMCAI}'02}, publisher = {Springer-Verlag}, series = {Lecture Notes in Computer Science}, volume = {2294}, pages = {289-301}, year = {2002}, month = jan, }
[HRS+02]	Thomas Hune, Judi Romijn, Mariëlle Stoelinga, and Frits Vaandrager. Linear parametric model checking of timed automata. Journal of Logic and Algebraic Programming 52-53:183-220. Elsevier, June 2002. BibTeX @article{jlap52-53-hrsv, author = {Hune, Thomas and Romijn, Judi and Stoelinga, Mari{\"e}lle and Vaandrager, Frits}, title = {Linear parametric model checking of timed automata}, publisher = {Elsevier}, journal = {Journal of Logic and Algebraic Programming}, volume = {52-53}, pages = {183-220}, year = {2002}, month = jun, }
[HWZ02]	Ian Hodkinson, Frank Wolter, and Michael Zakharyaschev. Decidable and Undecidable Fragments of First-Order Branching Temporal Logics. In LICS'02, pages 393-402. IEEE Comp. Soc. Press, July 2002. BibTeX @inproceedings{lics2002-HWZ, author = {Hodkinson, Ian and Wolter, Frank and Zakharyaschev, Michael}, title = {Decidable and Undecidable Fragments of First-Order Branching Temporal Logics}, booktitle = {{P}roceedings of the 17th {A}nnual {S}ymposium on {L}ogic in {C}omputer {S}cience ({LICS}'02)}, acronym = {{LICS}'02}, publisher = {IEEE Comp. Soc. Press}, pages = {393-402}, year = {2002}, month = jul, }
[IKO+02]	Satoshi Ikeda, Izumi Kubo, Norihiro Okumoto, and Masafumi Yamashita. Local Topological Information and Cover Time. IPSJ SIG Notes 88:27-34. Information Processing Society of Japan, September 2002. BibTeX @article{ipsj88-IKOY, author = {Ikeda, Satoshi and Kubo, Izumi and Okumoto, Norihiro and Yamashita, Masafumi}, title = {Local Topological Information and Cover Time}, publisher = {Information Processing Society of Japan}, journal = {IPSJ SIG Notes}, volume = {88}, pages = {27-34}, year = {2002}, month = sep, }
[Kir02]	Daniel Kirsten. Alternating tree automata and parity games. In Erich Grädel, Wolfgang Thomas, and Thomas Wilke (eds.), Automata, Logics, and Infinite Games, Lecture Notes in Computer Science 2500, pages 153-167. Springer-Verlag, 2002. PDF BibTeX @incollection{lncs2500-kirsten, author = {Kirsten, Daniel}, title = {Alternating tree automata and parity games}, editor = {Gr{\"a}del, Erich and Thomas, Wolfgang and Wilke, Thomas}, booktitle = {Automata, Logics, and Infinite Games}, publisher = {Springer-Verlag}, series = {Lecture Notes in Computer Science}, volume = {2500}, pages = {153-167}, year = {2002}, }
[KJJ02]	Andrei A. Krokhin, Peter Jeavons, and Peter Jonsson. The Complexity of Constraints on Intervals and Lengths. In STACS'02, Lecture Notes in Computer Science 2285, pages 443-454. Springer-Verlag, March 2002. BibTeX @inproceedings{stacs2002-KJJ, author = {Krokhin, Andrei A. and Jeavons, Peter and Jonsson, Peter}, title = {The Complexity of Constraints on Intervals and Lengths}, editor = {Alt, Helmut and Ferreira, Afonso}, booktitle = {{P}roceedings of the 19th {S}ymposium on {T}heoretical {A}spects of {C}omputer {S}cience ({STACS}'02)}, acronym = {{STACS}'02}, publisher = {Springer-Verlag}, series = {Lecture Notes in Computer Science}, volume = {2285}, pages = {443-454}, year = {2002}, month = mar, }
[KM02]	Antonín Kučera and Richard Mayr. Why is Simulation Harder than Bisimulation?. In CONCUR'02, Lecture Notes in Computer Science 2421, pages 594-609. Springer-Verlag, August 2002. BibTeX @inproceedings{concur2002-KM, author = {Ku{\v c}era, Anton{\'\i}n and Mayr, Richard}, title = {Why is Simulation Harder than Bisimulation?}, editor = {Brim, Lubo{\v s} and Jan{\v c}ar, Petr and K{\v r}et{\'\i}nsk{\'y}, Mojm{\'\i}r and Ku{\v c}era, Anton{\'\i}n}, booktitle = {{P}roceedings of the 13th {I}nternational {C}onference on {C}oncurrency {T}heory ({CONCUR}'02)}, acronym = {{CONCUR}'02}, publisher = {Springer-Verlag}, series = {Lecture Notes in Computer Science}, volume = {2421}, pages = {594-609}, year = {2002}, month = aug, }
[KNS+02]	Marta Kwiatkowska, Gethin Norman, Roberto Segala, and Jeremy Sproston. Automatic verification of real-time systems with discrete probability distributions. Theoretical Computer Science 282(1):101-150. Elsevier, June 2002. 10.1016/S0304-3975(01)00046-9 BibTeX @article{tcs282(1)-KNSS, author = {Kwiatkowska, Marta and Norman, Gethin and Segala, Roberto and Sproston, Jeremy}, title = {Automatic verification of real-time systems with discrete probability distributions}, publisher = {Elsevier}, journal = {Theoretical Computer Science}, volume = {282}, number = {1}, pages = {101-150}, year = {2002}, month = jun, doi = {10.1016/S0304-3975(01)00046-9}, }
[KP02]	Yonit Kesten and Amir Pnueli. Complete Proof System for QPTL. Journal of Logic and Computation 12(5):701-745. Oxford University Press, October 2002. 10.1093/logcom/12.5.701 BibTeX @article{jlc12(5)-KP, author = {Kesten, Yonit and Pnueli, Amir}, title = {Complete Proof System for~{QPTL}}, publisher = {Oxford University Press}, journal = {Journal of Logic and Computation}, volume = {12}, number = {5}, pages = {701-745}, year = {2002}, month = oct, doi = {10.1093/logcom/12.5.701}, }
[KP02]	Beata Konikowska and Wojciech Penczek. Reducing Model Checking from Multi-Valued CTL* to CTL. In CONCUR'02, Lecture Notes in Computer Science 2421, pages 226-239. Springer-Verlag, August 2002. BibTeX @inproceedings{concur2002-KP, author = {Konikowska, Beata and Penczek, Wojciech}, title = {Reducing Model Checking from Multi-Valued {CTL}{\(^\)} to {CTL}{\(^*\)}}, editor = {Brim, Lubo{\v s} and Jan{\v c}ar, Petr and K{\v r}et{\'\i}nsk{\'y}, Mojm{\'\i}r and Ku{\v c}era, Anton{\'\i}n}, booktitle = {{P}roceedings of the 13th {I}nternational {C}onference on {C}oncurrency {T}heory ({CONCUR}'02)}, acronym = {{CONCUR}'02}, publisher = {Springer-Verlag}, series = {Lecture Notes in Computer Science}, volume = {2421}, pages = {226-239}, year = {2002}, month = aug, }
[KPS+02]	Yonit Kesten, Amir Pnueli, Elad Shahar, and Lenore D. Zuck. Network Invariants in Action. In CONCUR'02, Lecture Notes in Computer Science 2421, pages 101-115. Springer-Verlag, August 2002. BibTeX @inproceedings{concur2002-KPSZ, author = {Kesten, Yonit and Pnueli, Amir and Shahar, Elad and Zuck, Lenore D.}, title = {Network Invariants in Action}, editor = {Brim, Lubo{\v s} and Jan{\v c}ar, Petr and K{\v r}et{\'\i}nsk{\'y}, Mojm{\'\i}r and Ku{\v c}era, Anton{\'\i}n}, booktitle = {{P}roceedings of the 13th {I}nternational {C}onference on {C}oncurrency {T}heory ({CONCUR}'02)}, acronym = {{CONCUR}'02}, publisher = {Springer-Verlag}, series = {Lecture Notes in Computer Science}, volume = {2421}, pages = {101-115}, year = {2002}, month = aug, }
[KS02]	Antonín Kučera and Jan Strejček. The Stuterring Principle Revisited: On the Expressiveness of Nested X and U Operators in the Logic LTL. Technical Report FIMU-RS-2002-03, Faculty of Informatics, Masaryk University, Brno, Czech Republic, July 2002. BibTeX @techreport{fimu-rs-2002-03-KS, author = {Ku{\v c}era, Anton{\'\i}n and Strej{\v c}ek, Jan}, title = {The Stuterring Principle Revisited: On the Expressiveness of Nested~{X} and~{U} Operators in the Logic {LTL}}, number = {FIMU-RS-2002-03}, year = {2002}, month = jul, institution = {Faculty of Informatics, Masaryk University, Brno, Czech Republic}, type = {Technical Report}, }
[Kur02]	Agi Kurucz. S5 × S5 × S5 lacks the finite model property. In AIML'00, pages 321-327. World Scientific, 2002. BibTeX @inproceedings{aiml2000-Kur, author = {Kurucz, Agi}, title = {{{\(S5\times S5\times S5\)}} lacks the finite model property}, editor = {de Rijke, Marteen and Wansing, Heinrich and Wolter, Frank and Zakharyaschev, Michael}, booktitle = {{P}roceedings of the 3rd {W}orkshop on {A}dvances in {M}odal {L}ogic ({AIML}'00)}, acronym = {{AIML}'00}, publisher = {World Scientific}, pages = {321-327}, year = {2002}, confyear = {2000}, confmonth = {10}, }
[Lan02]	Martin Lange. Local Model Checking Games for Fixed Point Logic with Chop. In CONCUR'02, Lecture Notes in Computer Science 2421, pages 240-254. Springer-Verlag, August 2002. BibTeX @inproceedings{concur2002-Lan, author = {Lange, Martin}, title = {Local Model Checking Games for Fixed Point Logic with Chop}, editor = {Brim, Lubo{\v s} and Jan{\v c}ar, Petr and K{\v r}et{\'\i}nsk{\'y}, Mojm{\'\i}r and Ku{\v c}era, Anton{\'\i}n}, booktitle = {{P}roceedings of the 13th {I}nternational {C}onference on {C}oncurrency {T}heory ({CONCUR}'02)}, acronym = {{CONCUR}'02}, publisher = {Springer-Verlag}, series = {Lecture Notes in Computer Science}, volume = {2421}, pages = {240-254}, year = {2002}, month = aug, }
[Lan02]	Martin Lange. Alternating Context-Free Languages and Linear Time μ-calculus with Sequential Composition. In EXPRESS'02, Electronic Notes in Theoretical Computer Science 68(2), pages 71-87. Elsevier, August 2002. BibTeX @inproceedings{express2002-Lan, author = {Lange, Martin}, title = {Alternating Context-Free Languages and Linear Time {\(\mu\)}-calculus with Sequential Composition}, editor = {Nestmann, Uwe and Panangaden, Prakash}, booktitle = {{P}roceedings of the 9th {I}nternational {W}orkshop on {E}xpressiveness in {C}oncurrency ({EXPRESS}'02)}, acronym = {{EXPRESS}'02}, publisher = {Elsevier}, series = {Electronic Notes in Theoretical Computer Science}, volume = {68}, number = {2}, pages = {71-87}, year = {2002}, month = aug, }
[Las02]	Sławomir Lasota. Decidability of Strong Bisimilarity for Timed BPP. In CONCUR'02, Lecture Notes in Computer Science 2421, pages 562-579. Springer-Verlag, August 2002. BibTeX @inproceedings{concur2002-Las, author = {Lasota, S{\l}awomir}, title = {Decidability of Strong Bisimilarity for Timed {BPP}}, editor = {Brim, Lubo{\v s} and Jan{\v c}ar, Petr and K{\v r}et{\'\i}nsk{\'y}, Mojm{\'\i}r and Ku{\v c}era, Anton{\'\i}n}, booktitle = {{P}roceedings of the 13th {I}nternational {C}onference on {C}oncurrency {T}heory ({CONCUR}'02)}, acronym = {{CONCUR}'02}, publisher = {Springer-Verlag}, series = {Lecture Notes in Computer Science}, volume = {2421}, pages = {562-579}, year = {2002}, month = aug, }
[LM02]	Christopher Lynch and Barbara Morawska. Automatic Decidability. In LICS'02, pages 9-16. IEEE Comp. Soc. Press, July 2002. BibTeX @inproceedings{lics2002-LM, author = {Lynch, Christopher and Morawska, Barbara}, title = {Automatic Decidability}, booktitle = {{P}roceedings of the 17th {A}nnual {S}ymposium on {L}ogic in {C}omputer {S}cience ({LICS}'02)}, acronym = {{LICS}'02}, publisher = {IEEE Comp. Soc. Press}, pages = {9-16}, year = {2002}, month = jul, }
[LS02]	Martin Lange and Colin Stirling. Model Checking Fixed Point Logic with Chop. In FoSSaCS'02, Lecture Notes in Computer Science 2303, pages 250-263. Springer-Verlag, April 2002. BibTeX @inproceedings{fossacs2002-LS, author = {Lange, Martin and Stirling, Colin}, title = {Model Checking Fixed Point Logic with Chop}, editor = {Nielsen, Mogens and Engberg, Uffe}, booktitle = {{P}roceedings of the 5th {I}nternational {C}onference on {F}oundations of {S}oftware {S}cience and {C}omputation {S}tructure ({FoSSaCS}'02)}, acronym = {{FoSSaCS}'02}, publisher = {Springer-Verlag}, series = {Lecture Notes in Computer Science}, volume = {2303}, pages = {250-263}, year = {2002}, month = apr, }
[Mal02]	Oded Maler. Control from Computer Science. Annual Reviews in Control 26(2):175-187. Elsevier, 2002. BibTeX @article{aric26(2)-Mal, author = {Maler, Oded}, title = {Control from Computer Science}, publisher = {Elsevier}, journal = {Annual Reviews in Control}, volume = {26}, number = {2}, pages = {175-187}, year = {2002}, }
[Mat02]	Radu Mateescu. Local Model-Checking of Modal Mu-Calculus on Acyclic Labeled Transition Systems. Research Report 4430, INRIA Rhône-Alpes, Montbonnot, France, April 2002. BibTeX @techreport{inria-4430, author = {Mateescu, Radu}, title = {Local Model-Checking of Modal Mu-Calculus on Acyclic Labeled Transition Systems}, number = {4430}, year = {2002}, month = apr, institution = {INRIA Rh\^one-Alpes, Montbonnot, France}, type = {Research Report}, }
[Maz02]	René Mazala. Infinite Games. In Erich Grädel, Wolfgang Thomas, and Thomas Wilke (eds.), Automata, Logics, and Infinite Games, Lecture Notes in Computer Science 2500, pages 23-42. Springer-Verlag, 2002. BibTeX @incollection{lncs2500-mazala, author = {Mazala, Ren{\'e}}, title = {Infinite Games}, editor = {Gr{\"a}del, Erich and Thomas, Wolfgang and Wilke, Thomas}, booktitle = {Automata, Logics, and Infinite Games}, publisher = {Springer-Verlag}, series = {Lecture Notes in Computer Science}, volume = {2500}, pages = {23-42}, year = {2002}, }
[McM02]	Kenneth L. McMillan. Applying SAT Methods in Unbounded Symbolic Model Checking. In CAV'02, Lecture Notes in Computer Science 2404, pages 250-264. Springer-Verlag, July 2002. BibTeX @inproceedings{cav2002-McM, author = {McMillan, Kenneth L.}, title = {Applying {SAT} Methods in Unbounded Symbolic Model Checking}, editor = {Brinksma, Ed and Larsen, Kim Guldstrand}, booktitle = {{P}roceedings of the 14th {I}nternational {C}onference on {C}omputer {A}ided {V}erification ({CAV}'02)}, acronym = {{CAV}'02}, publisher = {Springer-Verlag}, series = {Lecture Notes in Computer Science}, volume = {2404}, pages = {250-264}, year = {2002}, month = jul, }
[MM02]	Annabelle K. McIver and Carroll C. Morgan. Games, Probability and the Quantitative μ-calculus. In LPAR'02, Lecture Notes in Computer Science 2514, pages 292-310. Springer-Verlag, October 2002. BibTeX @inproceedings{lpar2002-MM, author = {McIver, Annabelle K. and Morgan, Carroll C.}, title = {Games, Probability and the Quantitative {\(\mu\)}-calculus}, editor = {Baaz, Matthias and Voronkov, Andrei}, booktitle = {{P}roceedings of the 9th {I}nternational {C}onference {L}ogic {P}rogramming and {A}utomated {R}easoning ({LPAR}'02)}, acronym = {{LPAR}'02}, publisher = {Springer-Verlag}, series = {Lecture Notes in Computer Science}, volume = {2514}, pages = {292-310}, year = {2002}, month = oct, }
[MS02]	Paolo Maggi and Riccardo Sisto. Using SPIN to verify security properties of cryptographic protocols. In SPIN'02, Lecture Notes in Computer Science 2318, pages 187-204. Springer-Verlag, April 2002. BibTeX @inproceedings{spin2002-MS, author = {Maggi, Paolo and Sisto, Riccardo}, title = {Using SPIN to verify security properties of cryptographic protocols}, editor = {Bosnacki, Dragan and Leue, Stefan}, booktitle = {{P}roceedings of the 9th {I}nternational {SPIN} {W}orkshop ({SPIN}'02)}, acronym = {{SPIN}'02}, publisher = {Springer-Verlag}, series = {Lecture Notes in Computer Science}, volume = {2318}, pages = {187-204}, year = {2002}, month = apr, }
[Nie02]	Frank Nießner. Non-deterministic tree automata. In Erich Grädel, Wolfgang Thomas, and Thomas Wilke (eds.), Automata, Logics, and Infinite Games, Lecture Notes in Computer Science 2500, pages 227-232. Springer-Verlag, 2002. BibTeX @incollection{lncs2500-niessner, author = {Nie{\ss}ner, Frank}, title = {Non-deterministic tree automata}, editor = {Gr{\"a}del, Erich and Thomas, Wolfgang and Wilke, Thomas}, booktitle = {Automata, Logics, and Infinite Games}, publisher = {Springer-Verlag}, series = {Lecture Notes in Computer Science}, volume = {2500}, pages = {227-232}, year = {2002}, }
[Niw02]	Damian Niwiński. μ-calculus via Games. In CSL'02, Lecture Notes in Computer Science 2471, pages 27-43. Springer-Verlag, September 2002. BibTeX @inproceedings{csl2002-Niw, author = {Niwi{\'n}ski, Damian}, title = {{\(\mu\)}-calculus via Games}, booktitle = {{P}roceedings of the 16th {I}nternational {W}orkshop on {C}omputer {S}cience {L}ogic ({CSL}'02)}, acronym = {{CSL}'02}, publisher = {Springer-Verlag}, series = {Lecture Notes in Computer Science}, volume = {2471}, pages = {27-43}, year = {2002}, month = sep, }
[NU02]	Matti Nykänen and Esko Ukkonen. The Exact Path Length Problem. Journal of Algorithms 42(1):41-53. Elsevier, January 2002. 10.1006/jagm.2001.1201 BibTeX @article{ja42(1)-NU, author = {Nyk{\"a}nen, Matti and Ukkonen, Esko}, title = {The Exact Path Length Problem}, publisher = {Elsevier}, journal = {Journal of Algorithms}, volume = {42}, number = {1}, pages = {41-53}, year = {2002}, month = jan, doi = {10.1006/jagm.2001.1201}, }
[OW02]	Joël Ouaknine and James Worrell. Timed CSP = Closed Timed Safety Automata. In EXPRESS'02, Electronic Notes in Theoretical Computer Science 68(2), pages 145-162. Elsevier, August 2002. BibTeX @inproceedings{express2002-OW, author = {Ouaknine, Jo{\"e}l and Worrell, James}, title = {Timed {CSP} = Closed Timed Safety Automata}, editor = {Nestmann, Uwe and Panangaden, Prakash}, booktitle = {{P}roceedings of the 9th {I}nternational {W}orkshop on {E}xpressiveness in {C}oncurrency ({EXPRESS}'02)}, acronym = {{EXPRESS}'02}, publisher = {Elsevier}, series = {Electronic Notes in Theoretical Computer Science}, volume = {68}, number = {2}, pages = {145-162}, year = {2002}, month = aug, }
[PBD+02]	Anindya C. Patthak, Indrajit Bhattacharya, Anirban Dasgupta, Pallab Dasgupta, and P. P. Chakrabarti. Quantified Computation Tree Logic. Information Processing Letters 82(3):123-129. Elsevier, 2002. PDF BibTeX @article{ipl82(3)-PBDDC, author = {Patthak, Anindya C. and Bhattacharya, Indrajit and Dasgupta, Anirban and Dasgupta, Pallab and Chakrabarti, P. P.}, title = {Quantified Computation Tree Logic}, publisher = {Elsevier}, journal = {Information Processing Letters}, volume = {82}, number = {3}, pages = {123-129}, year = {2002}, }
[Pet02]	Holger Petersen. Expressions with Intersection Is Complete in LOGCFL. In STACS'02, Lecture Notes in Computer Science 2285, pages 513-522. Springer-Verlag, March 2002. BibTeX @inproceedings{stacs2002-Pet, author = {Petersen, Holger}, title = {Expressions with Intersection Is Complete in {LOGCFL}}, editor = {Alt, Helmut and Ferreira, Afonso}, booktitle = {{P}roceedings of the 19th {S}ymposium on {T}heoretical {A}spects of {C}omputer {S}cience ({STACS}'02)}, acronym = {{STACS}'02}, publisher = {Springer-Verlag}, series = {Lecture Notes in Computer Science}, volume = {2285}, pages = {513-522}, year = {2002}, month = mar, }
[PK02]	Amir Pnueli and Yonit Kesten. A Deductive Proof System for CTL. In CONCUR'02, Lecture Notes in Computer Science 2421, pages 24-40. Springer-Verlag, August 2002. BibTeX @inproceedings{concur2002-PK, author = {Pnueli, Amir and Kesten, Yonit}, title = {A~Deductive Proof System for~{CTL}}, editor = {Brim, Lubo{\v s} and Jan{\v c}ar, Petr and K{\v r}et{\'\i}nsk{\'y}, Mojm{\'\i}r and Ku{\v c}era, Anton{\'\i}n}, booktitle = {{P}roceedings of the 13th {I}nternational {C}onference on {C}oncurrency {T}heory ({CONCUR}'02)}, acronym = {{CONCUR}'02}, publisher = {Springer-Verlag}, series = {Lecture Notes in Computer Science}, volume = {2421}, pages = {24-40}, year = {2002}, month = aug, }
[PXZ02]	Amir Pnueli, Jessie Xu, and Lenore D. Zuck. Liveness with (0,1,infty)-Counter Abstraction. In CAV'02, Lecture Notes in Computer Science 2404, pages 107-122. Springer-Verlag, July 2002. 10.1007/3-540-45657-0_9 PDF BibTeX @inproceedings{cav2002-PXZ, author = {Pnueli, Amir and Xu, Jessie and Zuck, Lenore D.}, title = {Liveness with {{\((0,1,infty)\)}}-Counter Abstraction}, editor = {Brinksma, Ed and Larsen, Kim Guldstrand}, booktitle = {{P}roceedings of the 14th {I}nternational {C}onference on {C}omputer {A}ided {V}erification ({CAV}'02)}, acronym = {{CAV}'02}, publisher = {Springer-Verlag}, series = {Lecture Notes in Computer Science}, volume = {2404}, pages = {107-122}, year = {2002}, month = jul, doi = {10.1007/3-540-45657-0_9}, }
[Rab02]	Alexander Rabinovich. Expressive Power of Temporal Logic. In CONCUR'02, Lecture Notes in Computer Science 2421, pages 57-75. Springer-Verlag, August 2002. BibTeX @inproceedings{concur2002-Rab, author = {Rabinovich, Alexander}, title = {Expressive Power of Temporal Logic}, editor = {Brim, Lubo{\v s} and Jan{\v c}ar, Petr and K{\v r}et{\'\i}nsk{\'y}, Mojm{\'\i}r and Ku{\v c}era, Anton{\'\i}n}, booktitle = {{P}roceedings of the 13th {I}nternational {C}onference on {C}oncurrency {T}heory ({CONCUR}'02)}, acronym = {{CONCUR}'02}, publisher = {Springer-Verlag}, series = {Lecture Notes in Computer Science}, volume = {2421}, pages = {57-75}, year = {2002}, month = aug, }
[Rot02]	Günter Rote. Crossing the Bridge at Night. EATCS Bulletin 78:241-246. EATCS, October 2002. BibTeX @article{eatcs-bull78()-Rot, author = {Rote, G{\"u}nter}, title = {Crossing the Bridge at Night}, publisher = {EATCS}, journal = {EATCS Bulletin}, volume = {78}, pages = {241-246}, year = {2002}, month = oct, }
[RT02]	Tim Roughgarden and Éva Tardos. How bad is selfish routing?. Journal of the ACM 49(2):236-259. ACM Press, March 2002. 10.1145/506147.506153 PDF BibTeX @article{jacm49(2)-RT, author = {Roughgarden, Tim and Tardos, {\'E}va}, title = {How bad is selfish routing?}, publisher = {ACM Press}, journal = {Journal of the~ACM}, volume = {49}, number = {2}, pages = {236-259}, year = {2002}, month = mar, doi = {10.1145/506147.506153}, }
[SC02]	Michael Soltys and Stephen A. Cook. The Proof Complexity of Linear Algebra. In LICS'02, pages 335-344. IEEE Comp. Soc. Press, July 2002. BibTeX @inproceedings{lics2002-SC, author = {Soltys, Michael and Cook, Stephen A.}, title = {The Proof Complexity of Linear Algebra}, booktitle = {{P}roceedings of the 17th {A}nnual {S}ymposium on {L}ogic in {C}omputer {S}cience ({LICS}'02)}, acronym = {{LICS}'02}, publisher = {IEEE Comp. Soc. Press}, pages = {335-344}, year = {2002}, month = jul, }
[Sch02]	Philippe Schnoebelen. Verifying Lossy Channel Systems has Nonprimitive Recursive Complexity. Information Processing Letters 83(5):251-261. Elsevier, September 2002. BibTeX @article{ipl83(5)-Sch, author = {Schnoebelen, {\relax Ph}ilippe}, title = {Verifying Lossy Channel Systems has Nonprimitive Recursive Complexity}, publisher = {Elsevier}, journal = {Information Processing Letters}, volume = {83}, number = {5}, pages = {251-261}, year = {2002}, month = sep, }
[Sor02]	Maria Sorea. A Decidable Fixpoint Logic for Time-Outs. In CONCUR'02, Lecture Notes in Computer Science 2421, pages 255-271. Springer-Verlag, August 2002. BibTeX @inproceedings{concur2002-Sor, author = {Sorea, Maria}, title = {A Decidable Fixpoint Logic for Time-Outs}, editor = {Brim, Lubo{\v s} and Jan{\v c}ar, Petr and K{\v r}et{\'\i}nsk{\'y}, Mojm{\'\i}r and Ku{\v c}era, Anton{\'\i}n}, booktitle = {{P}roceedings of the 13th {I}nternational {C}onference on {C}oncurrency {T}heory ({CONCUR}'02)}, acronym = {{CONCUR}'02}, publisher = {Springer-Verlag}, series = {Lecture Notes in Computer Science}, volume = {2421}, pages = {255-271}, year = {2002}, month = aug, }
[Srb02]	Jiří Srba. Undecidability of Weak Bisimulation for Pushdown Processes. In CONCUR'02, Lecture Notes in Computer Science 2421, pages 579-593. Springer-Verlag, August 2002. BibTeX @inproceedings{concur2002-Srb, author = {Srba, Ji{\v r}{\'\i}}, title = {Undecidability of Weak Bisimulation for Pushdown Processes}, editor = {Brim, Lubo{\v s} and Jan{\v c}ar, Petr and K{\v r}et{\'\i}nsk{\'y}, Mojm{\'\i}r and Ku{\v c}era, Anton{\'\i}n}, booktitle = {{P}roceedings of the 13th {I}nternational {C}onference on {C}oncurrency {T}heory ({CONCUR}'02)}, acronym = {{CONCUR}'02}, publisher = {Springer-Verlag}, series = {Lecture Notes in Computer Science}, volume = {2421}, pages = {579-593}, year = {2002}, month = aug, }
[SRH02]	Pierre-Yves Schobbens, Jean-François Raskin, and Thomas A. Henzinger. Axioms for Real-Time Logics. Theoretical Computer Science 274(1-2):151-182. Elsevier, March 2002. BibTeX @article{tcs274(1-2)-SRH, author = {Schobbens, Pierre-Yves and Raskin, Jean-Fran{\c c}ois and Henzinger, Thomas A.}, title = {Axioms for Real-Time Logics}, publisher = {Elsevier}, journal = {Theoretical Computer Science}, volume = {274}, number = {1-2}, pages = {151-182}, year = {2002}, month = mar, }
[SS02]	Vladimiro Sassone and Paweł Sobocoński. Deriving Bisimulationn Congruences: A 2-Categorical Approach. In EXPRESS'02, Electronic Notes in Theoretical Computer Science 68(2), pages 107-126. Elsevier, August 2002. BibTeX @inproceedings{express2002-SS, author = {Sassone, Vladimiro and Soboco{\'n}ski, Pawe{\l}}, title = {Deriving Bisimulationn Congruences: A~{\(2\)}-Categorical Approach}, editor = {Nestmann, Uwe and Panangaden, Prakash}, booktitle = {{P}roceedings of the 9th {I}nternational {W}orkshop on {E}xpressiveness in {C}oncurrency ({EXPRESS}'02)}, acronym = {{EXPRESS}'02}, publisher = {Elsevier}, series = {Electronic Notes in Theoretical Computer Science}, volume = {68}, number = {2}, pages = {107-126}, year = {2002}, month = aug, }
[SU02]	Marcus Schaefer and Christopher Umans. Completeness in the Polynomial-Time hierarchy: A Compendium. SIGACT News 33(3):32-49. ACM Press, September 2002. BibTeX @article{sigact-news-33(3)-SU, author = {Schaefer, Marcus and Umans, Christopher}, title = {Completeness in the Polynomial-Time hierarchy: A Compendium}, publisher = {ACM Press}, journal = {SIGACT News}, volume = {33}, number = {3}, pages = {32-49}, year = {2002}, month = sep, }
[SU02]	Marcus Schaefer and Christopher Umans. Completeness in the Polynomial-Time hierarchy: Part II. SIGACT News 33(4):22-36. ACM Press, December 2002. BibTeX @article{sigact-news33(4)-SU, author = {Schaefer, Marcus and Umans, Christopher}, title = {Completeness in the Polynomial-Time hierarchy: Part~II}, publisher = {ACM Press}, journal = {SIGACT News}, volume = {33}, number = {4}, pages = {22-36}, year = {2002}, month = dec, }
[Tan02]	Till Tantau. Comparing Verboseness for Finite Automata and Turing Machines. In STACS'02, Lecture Notes in Computer Science 2285, pages 465-476. Springer-Verlag, March 2002. BibTeX @inproceedings{stacs2002-Tan, author = {Tantau, Till}, title = {Comparing Verboseness for Finite Automata and Turing Machines}, editor = {Alt, Helmut and Ferreira, Afonso}, booktitle = {{P}roceedings of the 19th {S}ymposium on {T}heoretical {A}spects of {C}omputer {S}cience ({STACS}'02)}, acronym = {{STACS}'02}, publisher = {Springer-Verlag}, series = {Lecture Notes in Computer Science}, volume = {2285}, pages = {465-476}, year = {2002}, month = mar, }
[Tho02]	Wolfgang Thomas. Infinite Games and Verification (Extended Abstract of a Tutoral). In CAV'02, Lecture Notes in Computer Science 2404, pages 58-64. Springer-Verlag, July 2002. BibTeX @inproceedings{cav2002-Tho, author = {Thomas, Wolfgang}, title = {Infinite Games and Verification (Extended Abstract of a Tutoral)}, editor = {Brinksma, Ed and Larsen, Kim Guldstrand}, booktitle = {{P}roceedings of the 14th {I}nternational {C}onference on {C}omputer {A}ided {V}erification ({CAV}'02)}, acronym = {{CAV}'02}, publisher = {Springer-Verlag}, series = {Lecture Notes in Computer Science}, volume = {2404}, pages = {58-64}, year = {2002}, month = jul, }
[Tri02]	Stavros Tripakis. Description and Schedulability Analysis of the Software Architecture of an Automated Vehicle Control System. In EMSOFT'02, Lecture Notes in Computer Science 2491, pages 123-137. Springer-Verlag, October 2002. BibTeX @inproceedings{emsoft2002-Tri, author = {Tripakis, Stavros}, title = {Description and Schedulability Analysis of the Software Architecture of an Automated Vehicle Control System}, editor = {Sangiovani{-}Vincentelli, Alberto L. and Sifakis, Joseph}, booktitle = {{P}roceedings of the 2nd {I}nternational {C}onference on {E}mbedded {S}oftware ({EMSOFT}'02)}, acronym = {{EMSOFT}'02}, publisher = {Springer-Verlag}, series = {Lecture Notes in Computer Science}, volume = {2491}, pages = {123-137}, year = {2002}, month = oct, }
[TW02]	Denis Thérien and Thomas Wilke. Nesting Until and Since in Linear Temporal Logic. In STACS'02, Lecture Notes in Computer Science 2285, pages 455-464. Springer-Verlag, March 2002. BibTeX @inproceedings{stacs2002-TW, author = {Th{\'e}rien, Denis and Wilke, Thomas}, title = {Nesting Until and Since in Linear Temporal Logic}, editor = {Alt, Helmut and Ferreira, Afonso}, booktitle = {{P}roceedings of the 19th {S}ymposium on {T}heoretical {A}spects of {C}omputer {S}cience ({STACS}'02)}, acronym = {{STACS}'02}, publisher = {Springer-Verlag}, series = {Lecture Notes in Computer Science}, volume = {2285}, pages = {455-464}, year = {2002}, month = mar, }
[TW02]	P. S. Thiagarajan and Igor Walukiewicz. An Expressively Complete Linear Time Temporal Logic for Mazurkiewicz Traces. Information and Computation 179(2):230-249. Academic Press, December 2002. BibTeX @article{icomp179(2)-TW, author = {Thiagarajan, P. S. and Walukiewicz, Igor}, title = {An Expressively Complete Linear Time Temporal Logic for {M}azurkiewicz Traces}, publisher = {Academic Press}, journal = {Information and Computation}, volume = {179}, number = {2}, pages = {230-249}, year = {2002}, month = dec, }
[Wal02]	Igor Walukiewicz. Monadic second order logic on tree-like structures. Theoretical Computer Science 275(1-2):311-346. Elsevier, March 2002. PDF BibTeX @article{tcs275(1-2)-Wal, author = {Walukiewicz, Igor}, title = {Monadic second order logic on tree-like structures}, publisher = {Elsevier}, journal = {Theoretical Computer Science}, volume = {275}, number = {1-2}, pages = {311-346}, year = {2002}, month = mar, }

[LMS02]

François Laroussinie, Nicolas Markey, and Philippe Schnoebelen. On Model Checking Durational Kripke Structures (Extended Abstract). In FoSSaCS'02, Lecture Notes in Computer Science 2303, pages 264-279. Springer-Verlag, April 2002.

10.1007/3-540-45931-6_19

PDF

Abstract + BibTeX

Abstract: We consider quantitative model checking in durational Kripke structures (Kripke structures where transitions have integer durations) with timed temporal logics where subscripts put quantitative constraints on the time it takes before a property is satisfied. We investigate the conditions that allow polynomial-time model checking algorithms for timed versions of CTL and 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).
A surprising outcome of this study is that it provides the second example of a Δ2P-complete model checking problem.

@inproceedings{fossacs2002-LMS,
  author =              {Laroussinie, Fran{\c c}ois and Markey, Nicolas and
                         Schnoebelen, {\relax Ph}ilippe},
  title =               {On Model Checking Durational {K}ripke Structures
                         (Extended Abstract)},
  editor =              {Nielsen, Mogens and Engberg, Uffe},
  booktitle =           {{P}roceedings of the 5th {I}nternational
                         {C}onference on {F}oundations of {S}oftware
                         {S}cience and {C}omputation {S}tructure
                         ({FoSSaCS}'02)},
  acronym =             {{FoSSaCS}'02},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {2303},
  pages =               {264-279},
  year =                {2002},
  month =               apr,
  doi =                 {10.1007/3-540-45931-6_19},
  abstract =            {We consider quantitative model checking in
                         \emph{durational Kripke structures} (Kripke
                         structures where transitions have integer durations)
                         with timed temporal logics where subscripts put
                         quantitative constraints on the time it takes before
                         a property is satisfied. We investigate the
                         conditions that allow polynomial-time model checking
                         algorithms for timed versions of CTL and 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 A surprising outcome of this study is
                         that it provides the second example of a
                         \(\Delta_2^P\)-complete model checking problem.},
}

[LMS02]

François Laroussinie, Nicolas Markey, and Philippe Schnoebelen. Temporal Logic with Forgettable Past. In LICS'02, pages 383-392. IEEE Comp. Soc. Press, July 2002.

10.1109/LICS.2002.1029846

PDF

Test-of-time award

Abstract + BibTeX

Abstract: We investigate NLTL, a linear-time temporal logic with forgettable past. NLTL can be exponentially more succinct than LTL + Past (which in turn can be more succinct than LTL). We study satisfiability and model checking for NLTL and provide optimal automata-theoretic algorithms for these EXPSPACE-complete problems.

@inproceedings{lics2002-LMS,
  author =              {Laroussinie, Fran{\c c}ois and Markey, Nicolas and
                         Schnoebelen, {\relax Ph}ilippe},
  title =               {Temporal Logic with Forgettable Past},
  booktitle =           {{P}roceedings of the 17th {A}nnual {S}ymposium on
                         {L}ogic in {C}omputer {S}cience ({LICS}'02)},
  acronym =             {{LICS}'02},
  publisher =           {IEEE Comp. Soc. Press},
  pages =               {383-392},
  year =                {2002},
  month =               jul,
  doi =                 {10.1109/LICS.2002.1029846},
  abstract =            {We investigate NLTL, a linear-time temporal logic
                         with forgettable past. NLTL can be exponentially
                         more succinct than LTL + Past (which in turn can be
                         more succinct than LTL). We study satisfiability and
                         model checking for NLTL and provide optimal
                         automata-theoretic algorithms for these
                         EXPSPACE-complete problems.},
}

[Mar02]

Nicolas Markey. Past is for Free: On the Complexity of Verifying Linear Temporal Properties with Past. In EXPRESS'02, Electronic Notes in Theoretical Computer Science 68(2), pages 89-106. Elsevier, August 2002.

10.1016/S1571-0661(05)80366-4

PDF

Abstract + BibTeX

Abstract: We study the complexity of satisfiability and model-checking of the linear-time temporal logic with past (PLTL). More precisely, we consider several fragments of PLTL, depending on the allowed set of temporal modalities, the use of negations or the nesting of future formulae into past formulae. Our results show that "past is for free", that is it does not bring additional theoretical complexity, even for small fragments, and even when nesting future formulae into past formulae. We also remark that existential and universal model-checking can have different complexity for certain fragments.

@inproceedings{express2002-Mar,
  author =              {Markey, Nicolas},
  title =               {Past is for Free: On the Complexity of Verifying
                         Linear Temporal Properties with Past},
  editor =              {Nestmann, Uwe and Panangaden, Prakash},
  booktitle =           {{P}roceedings of the 9th {I}nternational {W}orkshop
                         on {E}xpressiveness in {C}oncurrency ({EXPRESS}'02)},
  acronym =             {{EXPRESS}'02},
  publisher =           {Elsevier},
  series =              {Electronic Notes in Theoretical Computer Science},
  volume =              {68},
  number =              {2},
  pages =               {89-106},
  year =                {2002},
  month =               aug,
  doi =                 {10.1016/S1571-0661(05)80366-4},
  abstract =            {We study the complexity of satisfiability and
                         model-checking of the linear-time temporal logic
                         with past~(PLTL). More precisely, we consider
                         several fragments of PLTL, depending on the allowed
                         set of temporal modalities, the use of negations or
                         the nesting of future formulae into past formulae.
                         Our~results show that {"}past is for free{"}, that
                         is it does not bring additional theoretical
                         complexity, even for small fragments, and even when
                         nesting future formulae into past formulae. We~also
                         remark that existential and universal model-checking
                         can have different complexity for certain
                         fragments.},
}

[AC02]

Jean-Pierre Aubin and Francine Catté. Bilateral Fixed-point and Algebraic Properties of Viability Kernels and Capture Basins of Sets. Technical Report 02-10, CeReMaDe, Université Paris 9, Paris, France, April 2002.

BibTeX

@techreport{TR-Ceremade0210,
  author =              {Aubin, Jean-Pierre and Catt{\'e}, Francine},
  title =               {Bilateral Fixed-point and Algebraic Properties of
                         Viability Kernels and Capture Basins of Sets},
  number =              {02-10},
  year =                {2002},
  month =               apr,
  institution =         {CeReMaDe, Universit\'e Paris 9, Paris, France},
}

[AFF+02]

Roy Armoni, Limor Fix, Alon Flaisher, Rob Gerth, Boris Ginsburg, Tomer Kanza, Avner Landver, Sela Mador-Haim, Eli Singerman, Andreas Tiemeyer, Moshe Y. Vardi, and Yael Zbar. The ForSpec Temporal Logic: A New Temporal Property-Specification Language. In TACAS'02, Lecture Notes in Computer Science 2280, pages 296-311. Springer-Verlag, April 2002.

BibTeX

@inproceedings{tacas2002-AFFGGKLMSTVZ,
  author =              {Armoni, Roy and Fix, Limor and Flaisher, Alon and
                         Gerth, Rob and Ginsburg, Boris and Kanza, Tomer and
                         Landver, Avner and Mador{-}Haim, Sela and Singerman,
                         Eli and Tiemeyer, Andreas and Vardi, Moshe Y. and
                         Zbar, Yael},
  title =               {The {ForSpec} Temporal Logic: A New Temporal
                         Property-Specification Language},
  editor =              {Katoen, Joost-Pieter and Stevens, Perdita},
  booktitle =           {{P}roceedings of the 8th {I}nternational
                         {C}onference on {T}ools and {A}lgorithms for
                         {C}onstruction and {A}nalysis of {S}ystems
                         ({TACAS}'02)},
  acronym =             {{TACAS}'02},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {2280},
  pages =               {296-311},
  year =                {2002},
  month =               apr,
}

[AFM+02]

Tobias Amnell, Elena Fersman, Leonid Mokrushin, Paul Pettersson, and Wang Yi. TIMES – A Tool for Modelling and Implementation of Embedded Systems. In TACAS'02, Lecture Notes in Computer Science 2280, pages 460-464. Springer-Verlag, April 2002.

BibTeX

@inproceedings{tacas2002-AFMPY,
  author =              {Amnell, Tobias and Fersman, Elena and Mokrushin,
                         Leonid and Pettersson, Paul and Yi, Wang},
  title =               {TIMES~-- A~Tool for Modelling and Implementation of
                         Embedded Systems},
  editor =              {Katoen, Joost-Pieter and Stevens, Perdita},
  booktitle =           {{P}roceedings of the 8th {I}nternational
                         {C}onference on {T}ools and {A}lgorithms for
                         {C}onstruction and {A}nalysis of {S}ystems
                         ({TACAS}'02)},
  acronym =             {{TACAS}'02},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {2280},
  pages =               {460-464},
  year =                {2002},
  month =               apr,
}

[AH02]

Henrik Reif Andersen and Henrik Hulgaard. Boolean Expression Diagrams. Information and Computation 179(2):194-212. Academic Press, December 2002.

10.1006/inco.2001.2948

BibTeX

@article{icomp179(2)-AH,
  author =              {Andersen, Henrik Reif and Hulgaard, Henrik},
  title =               {Boolean Expression Diagrams},
  publisher =           {Academic Press},
  journal =             {Information and Computation},
  volume =              {179},
  number =              {2},
  pages =               {194-212},
  year =                {2002},
  month =               dec,
  doi =                 {10.1006/inco.2001.2948},
}

[AHK02]

Rajeev Alur, Thomas A. Henzinger, and Orna Kupferman. Alternating-time Temporal Logic. Journal of the ACM 49(5):672-713. ACM Press, September 2002.

10.1145/585265.585270

PDF

BibTeX

@article{jacm49(5)-AHK,
  author =              {Alur, Rajeev and Henzinger, Thomas A. and Kupferman,
                         Orna},
  title =               {Alternating-time Temporal Logic},
  publisher =           {ACM Press},
  journal =             {Journal of the~ACM},
  volume =              {49},
  number =              {5},
  pages =               {672-713},
  year =                {2002},
  month =               sep,
  doi =                 {10.1145/585265.585270},
}

[AL02]

Luca Aceto and François Laroussinie. Is your Model Checker on Time?. Journal of Logic and Algebraic Programming 52-53:3-51. Elsevier, June 2002.

PDF

BibTeX

@article{jlap52-53()-AL,
  author =              {Aceto, Luca and Laroussinie, Fran{\c c}ois},
  title =               {Is your Model Checker on Time?},
  publisher =           {Elsevier},
  journal =             {Journal of Logic and Algebraic Programming},
  volume =              {52-53},
  pages =               {3-51},
  year =                {2002},
  month =               jun,
}

[AM02]

Yasmina Abdeddaïm and Oded Maler. Preemptive Job-Shop Scheduling using Stopwatch Automata. In TACAS'02, Lecture Notes in Computer Science 2280, pages 113-126. Springer-Verlag, April 2002.

BibTeX

@inproceedings{tacas2002-AM,
  author =              {Abdedda{\"\i}m, Yasmina and Maler, Oded},
  title =               {Preemptive Job-Shop Scheduling using Stopwatch
                         Automata},
  editor =              {Katoen, Joost-Pieter and Stevens, Perdita},
  booktitle =           {{P}roceedings of the 8th {I}nternational
                         {C}onference on {T}ools and {A}lgorithms for
                         {C}onstruction and {A}nalysis of {S}ystems
                         ({TACAS}'02)},
  acronym =             {{TACAS}'02},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {2280},
  pages =               {113-126},
  year =                {2002},
  month =               apr,
}

[AS02]

Eugene Asarin and Gerardo Schneider. Widening the Boundary between Decidable and Undecidable Hybrid Systems. In CONCUR'02, Lecture Notes in Computer Science 2421, pages 193-208. Springer-Verlag, August 2002.

BibTeX

@inproceedings{concur2002-AS,
  author =              {Asarin, Eugene and Schneider, Gerardo},
  title =               {Widening the Boundary between Decidable and
                         Undecidable Hybrid Systems},
  editor =              {Brim, Lubo{\v s} and Jan{\v c}ar, Petr and K{\v
                         r}et{\'\i}nsk{\'y}, Mojm{\'\i}r and Ku{\v c}era,
                         Anton{\'\i}n},
  booktitle =           {{P}roceedings of the 13th {I}nternational
                         {C}onference on {C}oncurrency {T}heory
                         ({CONCUR}'02)},
  acronym =             {{CONCUR}'02},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {2421},
  pages =               {193-208},
  year =                {2002},
  month =               aug,
}

[Asp02]

James Aspnes. Fast deterministic consensus in a noisy environment. Journal of Algorithms 45(1):16-39. Elsevier, October 2002.

10.1016/S0196-6774(02)00220-1

PDF

BibTeX

@article{ja45(1)-Asp,
  author =              {Aspnes, James},
  title =               {Fast deterministic consensus in a noisy environment},
  publisher =           {Elsevier},
  journal =             {Journal of Algorithms},
  volume =              {45},
  number =              {1},
  pages =               {16-39},
  year =                {2002},
  month =               oct,
  doi =                 {10.1016/S0196-6774(02)00220-1},
}

[AT02]

Karine Altisen and Stavros Tripakis. Tools for Controller Synthesis of Timed Systems. In RT-TOOLS'02. August 2002.

BibTeX

@inproceedings{rttools2002-AT,
  author =              {Altisen, Karine and Tripakis, Stavros},
  title =               {Tools for Controller Synthesis of Timed Systems},
  editor =              {Pettersson, Paul and Yi, Wang},
  booktitle =           {{P}roceedings of the 2nd {W}orkshop on {R}eal-Time
                         {T}ools ({RT-TOOLS}'02)},
  acronym =             {{RT-TOOLS}'02},
  year =                {2002},
  month =               aug,
}

[Ats02]

Albert Atserias. Unsatisfiable Random Formulas are Hard to Certify. In LICS'02, pages 325-334. IEEE Comp. Soc. Press, July 2002.

BibTeX

@inproceedings{lics2002-Ats,
  author =              {Atserias, Albert},
  title =               {Unsatisfiable Random Formulas are Hard to Certify},
  booktitle =           {{P}roceedings of the 17th {A}nnual {S}ymposium on
                         {L}ogic in {C}omputer {S}cience ({LICS}'02)},
  acronym =             {{LICS}'02},
  publisher =           {IEEE Comp. Soc. Press},
  pages =               {325-334},
  year =                {2002},
  month =               jul,
}

[BAS02]

Armin Biere, Cyrille Artho, and Viktor Schuppan. Liveness Checking as Safety Checking. In FMICS'02, Electronic Notes in Theoretical Computer Science 66(2). Elsevier, July 2002.

BibTeX

@inproceedings{fmics2002-BAS,
  author =              {Biere, Armin and Artho, Cyrille and Schuppan,
                         Viktor},
  title =               {Liveness Checking as Safety Checking},
  editor =              {Cleaveland, Rance and Garavel, Hubert},
  booktitle =           {{P}roceedings of the 7th {I}nternational {ERCIM}
                         {W}orkshop in {F}ormal {M}ethods for {I}ndustrial
                         {C}ritical {S}ystems ({FMICS}'02)},
  acronym =             {{FMICS}'02},
  publisher =           {Elsevier},
  series =              {Electronic Notes in Theoretical Computer Science},
  volume =              {66},
  number =              {2},
  year =                {2002},
  month =               jul,
}

[BB02]

Dietmar Berwanger and Achim Blumensath. The Monadic Theory of Tree-like Structures. In Erich Grädel, Wolfgang Thomas, and Thomas Wilke (eds.), Automata, Logics, and Infinite Games, Lecture Notes in Computer Science 2500, pages 285-302. Springer-Verlag, 2002.

PDF

BibTeX

@incollection{lncs2500-BB,
  author =              {Berwanger, Dietmar and Blumensath, Achim},
  title =               {The Monadic Theory of Tree-like Structures},
  editor =              {Gr{\"a}del, Erich and Thomas, Wolfgang and Wilke,
                         Thomas},
  booktitle =           {Automata, Logics, and Infinite Games},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {2500},
  pages =               {285-302},
  year =                {2002},
}

[BBD+02]

Gerd Behrmann, Johan Bengtsson, Alexandre David, Kim Guldstrand Larsen, Paul Pettersson, and Wang Yi. UPPAAL Implementation Secrets. In FTRTFT'02, Lecture Notes in Computer Science 2469, pages 3-22. Springer-Verlag, September 2002.

10.1007/3-540-45739-9_1

BibTeX

@inproceedings{ftrtft2002-BBDLPY,
  author =              {Behrmann, Gerd and Bengtsson, Johan and David,
                         Alexandre and Larsen, Kim Guldstrand and Pettersson,
                         Paul and Yi, Wang},
  title =               {UPPAAL Implementation Secrets},
  editor =              {Damm, Werner and Olderog, Ernst R{\"u}diger},
  booktitle =           {{P}roceedings of the 7th {F}ormal {T}echniques in
                         {R}eal-Time and {F}ault-Tolerant {S}ystems
                         ({FTRTFT}'02)},
  acronym =             {{FTRTFT}'02},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {2469},
  pages =               {3-22},
  year =                {2002},
  month =               sep,
  doi =                 {10.1007/3-540-45739-9_1},
}

[BFD02]

Alexander Bolotov, Michael J. Fischer, and Clare Dixon. On the Relationship between ω-Automata and Temporal Logic Normal Forms. Journal of Logic and Computation 12(4):561-581. Oxford University Press, August 2002.

BibTeX

@article{jlc12(4)-BFD,
  author =              {Bolotov, Alexander and Fischer, Michael J. and
                         Dixon, Clare},
  title =               {On the Relationship between {\(\omega\)}-Automata
                         and Temporal Logic Normal Forms},
  publisher =           {Oxford University Press},
  journal =             {Journal of Logic and Computation},
  volume =              {12},
  number =              {4},
  pages =               {561-581},
  year =                {2002},
  month =               aug,
}

[BG02]

Robert Baumgartner and Georg Gottlob. Propositional Default Logics made Easier: Computational Complexity of Model Checking. Theoretical Computer Science 289(1):591-627. Elsevier, October 2002.

BibTeX

@article{tcs289(1)-BG,
  author =              {Baumgartner, Robert and Gottlob, Georg},
  title =               {Propositional Default Logics made Easier:
                         Computational Complexity of Model Checking},
  publisher =           {Elsevier},
  journal =             {Theoretical Computer Science},
  volume =              {289},
  number =              {1},
  pages =               {591-627},
  year =                {2002},
  month =               oct,
}

[BHR+02]

Danièle Beauquier, Yoram Hirshfeld, Alexander Rabinovich, and Anatol Slissenko. The Probablity Nesting Game. In EXPRESS'02, Electronic Notes in Theoretical Computer Science 68(2), pages 3-13. Elsevier, August 2002.

BibTeX

@inproceedings{express2002-BHRS,
  author =              {Beauquier, Dani{\`e}le and Hirshfeld, Yoram and
                         Rabinovich, Alexander and Slissenko, Anatol},
  title =               {The Probablity Nesting Game},
  editor =              {Nestmann, Uwe and Panangaden, Prakash},
  booktitle =           {{P}roceedings of the 9th {I}nternational {W}orkshop
                         on {E}xpressiveness in {C}oncurrency ({EXPRESS}'02)},
  acronym =             {{EXPRESS}'02},
  publisher =           {Elsevier},
  series =              {Electronic Notes in Theoretical Computer Science},
  volume =              {68},
  number =              {2},
  pages =               {3-13},
  year =                {2002},
  month =               aug,
}

[BJM+02]

Marius Bozga, Hou Jianmin, Oded Maler, and Sergio Yovine. Verification of Asynchronous Circuits using Timed Automata. In TPTS'02, Electronic Notes in Theoretical Computer Science 65(6), pages 47-59. Elsevier, April 2002.

BibTeX

@inproceedings{tpts2002-BJMY,
  author =              {Bozga, Marius and Jianmin, Hou and Maler, Oded and
                         Yovine, Sergio},
  title =               {Verification of Asynchronous Circuits using Timed
                         Automata},
  editor =              {Asarin, Eugene and Maler, Oded and Yovine, Sergio},
  booktitle =           {{P}roceedings of the 1st {W}orkshop on {T}heory and
                         {P}ractice of {T}imed {S}ystems ({TPTS}'02)},
  acronym =             {{TPTS}'02},
  publisher =           {Elsevier},
  series =              {Electronic Notes in Theoretical Computer Science},
  volume =              {65},
  number =              {6},
  pages =               {47-59},
  year =                {2002},
  month =               apr,
}

[BJW02]

Julien Bernet, David Janin, and Igor Walukiewicz. Permissive strategies: from parity games to safety games. RAIRO – Theoretical Informatics and Applications 36(3):261-275. EDP Sciences, 2002.

BibTeX

@article{rairo-tia36(3)-BJW,
  author =              {Bernet, Julien and Janin, David and Walukiewicz,
                         Igor},
  title =               {Permissive strategies: from parity games to safety
                         games},
  publisher =           {EDP Sciences},
  journal =             {RAIRO~-- Theoretical Informatics and Applications},
  volume =              {36},
  number =              {3},
  pages =               {261-275},
  year =                {2002},
}

[BMF02]

Ed Brinksma, Angelika Mader, and Ansgar Fehnker. Verification and Optimization of a PLC Control Schedule. International Journal on Software Tools for Technology Transfer 4(1):21-33. Springer-Verlag, 2002.

BibTeX

@article{sttt4(1)-BMF,
  author =              {Brinksma, Ed and Mader, Angelika and Fehnker,
                         Ansgar},
  title =               {Verification and Optimization of a {PLC} Control
                         Schedule},
  publisher =           {Springer-Verlag},
  journal =             {International Journal on Software Tools for
                         Technology Transfer},
  volume =              {4},
  number =              {1},
  pages =               {21-33},
  year =                {2002},
}

[Bou02]

Patricia Bouyer. Timed Automata May Cause some Troubles. Research Report LSV-02-09, Lab. Spécification & Vérification, ENS Cachan, France, July 2002.

BibTeX

@techreport{LSV0209-Bou,
  author =              {Bouyer, Patricia},
  title =               {Timed Automata May Cause some Troubles},
  number =              {LSV-02-09},
  year =                {2002},
  month =               jul,
  institution =         {Lab.~Sp\'ecification \& V\'erification, ENS Cachan,
                         France},
  type =                {Research Report},
}

[BR02]

Danièle Beauquier and Alexander Rabinovich. Monadic Logic of Order over Naturals has no Finite Base. Journal of Logic and Computation 12(2):243-253. Oxford University Press, April 2002.

BibTeX

@article{jlc12(2)-BR,
  author =              {Beauquier, Dani{\`e}le and Rabinovich, Alexander},
  title =               {Monadic Logic of Order over Naturals has no Finite
                         Base},
  publisher =           {Oxford University Press},
  journal =             {Journal of Logic and Computation},
  volume =              {12},
  number =              {2},
  pages =               {243-253},
  year =                {2002},
  month =               apr,
}

[BTK+02]

Cécile Bui Thanh, Hanna Klaudel, and Franck Pommereau. Petri Nets with Causal Time for System Verification. In MTCS'02, Electronic Notes in Theoretical Computer Science 68(5). Elsevier, August 2002.

BibTeX

@inproceedings{mtcs2003-BKP,
  author =              {Bui Thanh, C{\'e}cile and Klaudel, Hanna and
                         Pommereau, Franck},
  title =               {{P}etri Nets with Causal Time for System
                         Verification},
  editor =              {Vogler, Walter and Larsen, Kim Guldstrand},
  booktitle =           {{P}roceedings of the 3rd {I}nternational {W}orkshop
                         on {M}odels for {T}ime-Critical {S}ystems
                         ({MTCS}'02)},
  acronym =             {{MTCS}'02},
  publisher =           {Elsevier},
  series =              {Electronic Notes in Theoretical Computer Science},
  volume =              {68},
  number =              {5},
  year =                {2002},
  month =               aug,
}

[CC02]

Cristian S. Calude and Elena Calude. The Bridge Crossing Problem. EATCS Bulletin 77:180-190. EATCS, June 2002.

BibTeX

@article{eatcs-bull77()-CC,
  author =              {Calude, Cristian S. and Calude, Elena},
  title =               {The Bridge Crossing Problem},
  publisher =           {EATCS},
  journal =             {EATCS Bulletin},
  volume =              {77},
  pages =               {180-190},
  year =                {2002},
  month =               jun,
}

[CCG+02]

Alessandro Cimatti, Edmund M. Clarke, Enrico Giunchiglia, Fausto Giunchiglia, Marco Pistore, Marco Roveri, Roberto Sebastiani, and Armando Tacchella. NuSMV2: An OpenSource Tool for Symbolic Model Checking. In CAV'02, Lecture Notes in Computer Science 2404, pages 359-364. Springer-Verlag, July 2002.

BibTeX

@inproceedings{cav2002-CCGGPRST,
  author =              {Cimatti, Alessandro and Clarke, Edmund M. and
                         Giunchiglia, Enrico and Giunchiglia, Fausto and
                         Pistore, Marco and Roveri, Marco and Sebastiani,
                         Roberto and Tacchella, Armando},
  title =               {{NuSMV2}: An OpenSource Tool for Symbolic Model
                         Checking},
  editor =              {Brinksma, Ed and Larsen, Kim Guldstrand},
  booktitle =           {{P}roceedings of the 14th {I}nternational
                         {C}onference on {C}omputer {A}ided {V}erification
                         ({CAV}'02)},
  acronym =             {{CAV}'02},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {2404},
  pages =               {359-364},
  year =                {2002},
  month =               jul,
}

[CDV02]

Diego Calvanese, Giuseppe De Giacomo, and Moshe Y. Vardi. Reasoning about Actions and Planning in LTL Action Theories. In KR'02, pages 593-602. Morgan Kaufmann Publishers, April 2002.

BibTeX

@inproceedings{kr2002-CDV,
  author =              {Calvanese, Diego and De{~}Giacomo, Giuseppe and
                         Vardi, Moshe Y.},
  title =               {Reasoning about Actions and Planning in {LTL} Action
                         Theories},
  editor =              {Giunchiglia, Fausto},
  booktitle =           {{P}roceedings of the 8th {I}nternational
                         {C}onference on {P}rinciples of {K}nowledge
                         {R}epresentation and {R}easoning ({KR}'02)},
  acronym =             {{KR}'02},
  publisher =           {Morgan Kaufmann Publishers},
  pages =               {593-602},
  year =                {2002},
  month =               apr,
}

[CGP+02]

Alessandro Cimatti, Enrico Giunchiglia, Marco Pistore, Marco Roveri, Roberto Sebastiani, and Armando Tacchella. Integrating BDD-based and SAT-based Symbolic Model Checking. In FroCoS'02, Lecture Notes in Computer Science 2309, pages 49-56. Springer-Verlag, April 2002.

BibTeX

@inproceedings{frocos2002-CGPRST,
  author =              {Cimatti, Alessandro and Giunchiglia, Enrico and
                         Pistore, Marco and Roveri, Marco and Sebastiani,
                         Roberto and Tacchella, Armando},
  title =               {Integrating {BDD}-based and {SAT}-based Symbolic
                         Model Checking},
  editor =              {Armando, Alessandro},
  booktitle =           {{P}roceedings of the 4th {I}nternational {W}orkshop
                         on {F}rontiers of {C}ombining {S}ystems
                         ({FroCoS}'02)},
  acronym =             {{FroCoS}'02},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {2309},
  pages =               {49-56},
  year =                {2002},
  month =               apr,
}

[CHR02]

Franck Cassez, Thomas A. Henzinger, and Jean-François Raskin. A Comparison of Control Problems for Timed and Hybrid Systems. In HSCC'02, Lecture Notes in Computer Science 2289, pages 134-148. Springer-Verlag, March 2002.

PDF

BibTeX

@inproceedings{hscc2002-CHR,
  author =              {Cassez, Franck and Henzinger, Thomas A. and Raskin,
                         Jean-Fran{\c c}ois},
  title =               {A Comparison of Control Problems for Timed and
                         Hybrid Systems},
  editor =              {Tomlin, Claire and Greenstreet, Mark R.},
  booktitle =           {{P}roceedings of the 5th {I}nternational {W}orkshop
                         on {H}ybrid {S}ystems: {C}omputation and {C}ontrol
                         ({HSCC}'02)},
  acronym =             {{HSCC}'02},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {2289},
  pages =               {134-148},
  year =                {2002},
  month =               mar,
}

[CJL+02]

Edmund M. Clarke, Somesh Jha, Yuan Lu, and Helmut Veith. Tree-Like Counterexamples in Model Checking. In LICS'02, pages 19-29. IEEE Comp. Soc. Press, July 2002.

BibTeX

@inproceedings{lics2002-CJLV,
  author =              {Clarke, Edmund M. and Jha, Somesh and Lu, Yuan and
                         Veith, Helmut},
  title =               {Tree-Like Counterexamples in Model Checking},
  booktitle =           {{P}roceedings of the 17th {A}nnual {S}ymposium on
                         {L}ogic in {C}omputer {S}cience ({LICS}'02)},
  acronym =             {{LICS}'02},
  publisher =           {IEEE Comp. Soc. Press},
  pages =               {19-29},
  year =                {2002},
  month =               jul,
}

[CL02]

Rance Cleaveland and Gerald Lüttgen. A Logical Process Calculi. In EXPRESS'02, Electronic Notes in Theoretical Computer Science 68(2), pages 33-50. Elsevier, August 2002.

BibTeX

@inproceedings{express2002-CL,
  author =              {Cleaveland, Rance and L{\"u}ttgen, Gerald},
  title =               {A Logical Process Calculi},
  editor =              {Nestmann, Uwe and Panangaden, Prakash},
  booktitle =           {{P}roceedings of the 9th {I}nternational {W}orkshop
                         on {E}xpressiveness in {C}oncurrency ({EXPRESS}'02)},
  acronym =             {{EXPRESS}'02},
  publisher =           {Elsevier},
  series =              {Electronic Notes in Theoretical Computer Science},
  volume =              {68},
  number =              {2},
  pages =               {33-50},
  year =                {2002},
  month =               aug,
}

[CM02]

Marco Carbone and Sergio Maffeis. On the Expressive Power of Polyadic Synchronisation in π-calculus. In EXPRESS'02, Electronic Notes in Theoretical Computer Science 68(2), pages 15-32. Elsevier, August 2002.

BibTeX

@inproceedings{express2002-CM,
  author =              {Carbone, Marco and Maffeis, Sergio},
  title =               {On the Expressive Power of Polyadic Synchronisation
                         in {\(\pi\)}-calculus},
  editor =              {Nestmann, Uwe and Panangaden, Prakash},
  booktitle =           {{P}roceedings of the 9th {I}nternational {W}orkshop
                         on {E}xpressiveness in {C}oncurrency ({EXPRESS}'02)},
  acronym =             {{EXPRESS}'02},
  publisher =           {Elsevier},
  series =              {Electronic Notes in Theoretical Computer Science},
  volume =              {68},
  number =              {2},
  pages =               {15-32},
  year =                {2002},
  month =               aug,
}

[CPR+02]

Alessandro Cimatti, Marco Pistore, Marco Roveri, and Roberto Sebastiani. Improving the Encoding of LTL Model Checking into SAT. In VMCAI'02, Lecture Notes in Computer Science 2294, pages 196-207. Springer-Verlag, January 2002.

BibTeX

@inproceedings{vmcai2002-CPRS,
  author =              {Cimatti, Alessandro and Pistore, Marco and Roveri,
                         Marco and Sebastiani, Roberto},
  title =               {Improving the Encoding of {LTL} Model Checking into
                         {SAT}},
  editor =              {Cortesi, Agostino},
  booktitle =           {{P}roceedings of the 3rd {I}nternational {W}orkshop
                         on {V}erification, {M}odel {C}hecking, and
                         {A}bstract {I}nterpretation ({VMCAI}'02)},
  acronym =             {{VMCAI}'02},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {2294},
  pages =               {196-207},
  year =                {2002},
  month =               jan,
}

[DG02]

Jennifer M. Davoren and Rajeev Prabhakar Gore. Bimodal Logics for Reasoning about Continuous Dynamics. In AIML'00. World Scientific, 2002.

BibTeX

@inproceedings{aiml2000-DG,
  author =              {Davoren, Jennifer M. and Gore, Rajeev Prabhakar},
  title =               {Bimodal Logics for Reasoning about Continuous
                         Dynamics},
  editor =              {de Rijke, Marteen and Wansing, Heinrich and Wolter,
                         Frank and Zakharyaschev, Michael},
  booktitle =           {{P}roceedings of the 3rd {W}orkshop on {A}dvances in
                         {M}odal {L}ogic ({AIML}'00)},
  acronym =             {{AIML}'00},
  publisher =           {World Scientific},
  year =                {2002},
  confyear =            {2000},
  confmonth =           {10},
}

[Dim02]

Cătălin Dima. Computing Reachability Relations in Timed Automata. In LICS'02, pages 177-186. IEEE Comp. Soc. Press, July 2002.

BibTeX

@inproceedings{lics2002-Dim,
  author =              {Dima, C{\u a}t{\u a}lin},
  title =               {Computing Reachability Relations in Timed Automata},
  booktitle =           {{P}roceedings of the 17th {A}nnual {S}ymposium on
                         {L}ogic in {C}omputer {S}cience ({LICS}'02)},
  acronym =             {{LICS}'02},
  publisher =           {IEEE Comp. Soc. Press},
  pages =               {177-186},
  year =                {2002},
  month =               jul,
}

[DLS02]

Stéphane Demri, François Laroussinie, and Philippe Schnoebelen. A Parametric Analysis of the State Explosion Problem in Model Checking (Extended Abstract). In STACS'02, Lecture Notes in Computer Science 2285, pages 620-631. Springer-Verlag, March 2002.

BibTeX

@inproceedings{stacs2002-DLS,
  author =              {Demri, St{\'e}phane and Laroussinie, Fran{\c c}ois
                         and Schnoebelen, {\relax Ph}ilippe},
  title =               {A Parametric Analysis of the State Explosion Problem
                         in Model Checking (Extended Abstract)},
  editor =              {Alt, Helmut and Ferreira, Afonso},
  booktitle =           {{P}roceedings of the 19th {S}ymposium on
                         {T}heoretical {A}spects of {C}omputer {S}cience
                         ({STACS}'02)},
  acronym =             {{STACS}'02},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {2285},
  pages =               {620-631},
  year =                {2002},
  month =               mar,
}

[DM02]

Deepak D'Souza and Parthasarathy Madhusudan. Timed Control Synthesis for External Specifications. In STACS'02, Lecture Notes in Computer Science 2285, pages 571-582. Springer-Verlag, March 2002.

BibTeX

@inproceedings{stacs2002-DM,
  author =              {D'Souza, Deepak and Madhusudan, Parthasarathy},
  title =               {Timed Control Synthesis for External Specifications},
  editor =              {Alt, Helmut and Ferreira, Afonso},
  booktitle =           {{P}roceedings of the 19th {S}ymposium on
                         {T}heoretical {A}spects of {C}omputer {S}cience
                         ({STACS}'02)},
  acronym =             {{STACS}'02},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {2285},
  pages =               {571-582},
  year =                {2002},
  month =               mar,
}

[DS02]

Stéphane Demri and Philippe Schnoebelen. The Complexity of Propositional Linear Temporal Logics in Simple Cases. Information and Computation 174(1):84-103. Academic Press, April 2002.

BibTeX

@article{icomp174(1)-DS,
  author =              {Demri, St{\'e}phane and Schnoebelen, {\relax
                         Ph}ilippe},
  title =               {The Complexity of Propositional Linear Temporal
                         Logics in Simple Cases},
  publisher =           {Academic Press},
  journal =             {Information and Computation},
  volume =              {174},
  number =              {1},
  pages =               {84-103},
  year =                {2002},
  month =               apr,
}

[DS02]

Stéphane Demri and Ulrike Sattler. Automata-Theoretic Decision Procedures for Information Logics. Fundamenta Informaticae 53(1):1-22. IOS Press, 2002.

BibTeX

@article{fundi53(1)-DS,
  author =              {Demri, St{\'e}phane and Sattler, Ulrike},
  title =               {Automata-Theoretic Decision Procedures for
                         Information Logics},
  publisher =           {IOS Press},
  journal =             {Fundamenta Informaticae},
  volume =              {53},
  number =              {1},
  pages =               {1-22},
  year =                {2002},
}

[END+02]

Abdeslam En-Nouaary, Radhida Dssouli, and Ferhat Khendek. Timed Wp-Method: Testing Real-Time Systems. IEEE Transactions on Software Engineering 28(11):1023-1038. IEEE Comp. Soc. Press, November 2002.

10.1109/TSE.2002.1049402

BibTeX

@article{tse28(11)-EDK,
  author =              {En-Nouaary, Abdeslam and Dssouli, Radhida and
                         Khendek, Ferhat},
  title =               {Timed Wp-Method: Testing Real-Time Systems},
  publisher =           {IEEE Comp. Soc. Press},
  journal =             {IEEE Transactions on Software Engineering},
  volume =              {28},
  number =              {11},
  pages =               {1023-1038},
  year =                {2002},
  month =               nov,
  doi =                 {10.1109/TSE.2002.1049402},
}

[Ete02]

Kousha Etessami. A Hierarchy of Polynomial-Time Computable Simulations for Automata. In CONCUR'02, Lecture Notes in Computer Science 2421, pages 131-144. Springer-Verlag, August 2002.

BibTeX

@inproceedings{concur2002-Ete,
  author =              {Etessami, Kousha},
  title =               {A Hierarchy of Polynomial-Time Computable
                         Simulations for Automata},
  editor =              {Brim, Lubo{\v s} and Jan{\v c}ar, Petr and K{\v
                         r}et{\'\i}nsk{\'y}, Mojm{\'\i}r and Ku{\v c}era,
                         Anton{\'\i}n},
  booktitle =           {{P}roceedings of the 13th {I}nternational
                         {C}onference on {C}oncurrency {T}heory
                         ({CONCUR}'02)},
  acronym =             {{CONCUR}'02},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {2421},
  pages =               {131-144},
  year =                {2002},
  month =               aug,
}

[EVW02]

Kousha Etessami, Moshe Y. Vardi, and Thomas Wilke. First-Order Logic with Two Variables and Unary Temporal Logic. Information and Computation 179(2):279-295. Academic Press, December 2002.

PDF

BibTeX

@article{icomp179(2)-EVW,
  author =              {Etessami, Kousha and Vardi, Moshe Y. and Wilke,
                         Thomas},
  title =               {First-Order Logic with Two Variables and Unary
                         Temporal Logic},
  publisher =           {Academic Press},
  journal =             {Information and Computation},
  volume =              {179},
  number =              {2},
  pages =               {279-295},
  year =                {2002},
  month =               dec,
}

[Far02]

Berndt Farwer. ω-automata. In Erich Grädel, Wolfgang Thomas, and Thomas Wilke (eds.), Automata, Logics, and Infinite Games, Lecture Notes in Computer Science 2500, pages 3-21. Springer-Verlag, 2002.

BibTeX

@incollection{lncs2500-Far,
  author =              {Farwer, Berndt},
  title =               {{{\(\omega\)}}-automata},
  editor =              {Gr{\"a}del, Erich and Thomas, Wolfgang and Wilke,
                         Thomas},
  booktitle =           {Automata, Logics, and Infinite Games},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {2500},
  pages =               {3-21},
  year =                {2002},
}

[FG02]

Jörg Flum and Martin Grohe. Describing Parameterized Complexity Classes. In STACS'02, Lecture Notes in Computer Science 2285, pages 359-371. Springer-Verlag, March 2002.

BibTeX

@inproceedings{stacs2002-FG,
  author =              {Flum, J{\"o}rg and Grohe, Martin},
  title =               {Describing Parameterized Complexity Classes},
  editor =              {Alt, Helmut and Ferreira, Afonso},
  booktitle =           {{P}roceedings of the 19th {S}ymposium on
                         {T}heoretical {A}spects of {C}omputer {S}cience
                         ({STACS}'02)},
  acronym =             {{STACS}'02},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {2285},
  pages =               {359-371},
  year =                {2002},
  month =               mar,
}

[FG02]

Markus Frick and Martin Grohe. The Complexity of First-Order and Monadic Second-Order Logic Revisited. In LICS'02, pages 215-224. IEEE Comp. Soc. Press, July 2002.

BibTeX

@inproceedings{lics2002-FG,
  author =              {Frick, Markus and Grohe, Martin},
  title =               {The Complexity of First-Order and Monadic
                         Second-Order Logic Revisited},
  booktitle =           {{P}roceedings of the 17th {A}nnual {S}ymposium on
                         {L}ogic in {C}omputer {S}cience ({LICS}'02)},
  acronym =             {{LICS}'02},
  publisher =           {IEEE Comp. Soc. Press},
  pages =               {215-224},
  year =                {2002},
  month =               jul,
}

[FHN02]

Ulrik Frendrup, Hans Hüttel, and Jesper Nyholm Jensen. Modal Logic for Cryptographic Systems. In EXPRESS'02, Electronic Notes in Theoretical Computer Science 68(2), pages 127-144. Elsevier, August 2002.

BibTeX

@inproceedings{express2002-FHN,
  author =              {Frendrup, Ulrik and H{\"u}ttel, Hans and Nyholm{
                         }Jensen, Jesper},
  title =               {Modal Logic for Cryptographic Systems},
  editor =              {Nestmann, Uwe and Panangaden, Prakash},
  booktitle =           {{P}roceedings of the 9th {I}nternational {W}orkshop
                         on {E}xpressiveness in {C}oncurrency ({EXPRESS}'02)},
  acronym =             {{EXPRESS}'02},
  publisher =           {Elsevier},
  series =              {Electronic Notes in Theoretical Computer Science},
  volume =              {68},
  number =              {2},
  pages =               {127-144},
  year =                {2002},
  month =               aug,
}

[FL02]

Alain Finkel and Jérôme Leroux. How to Compose Presburger-Accelerations: Applications to Broadcast Protocols. Research Report, Lab. Spécification & Vérification, ENS Cachan, France, September 2002.

BibTeX

@techreport{LSV-02-14,
  author =              {Finkel, Alain and Leroux, J{\'e}r{\^o}me},
  title =               {How to Compose {P}resburger-Accelerations:
                         Applications to Broadcast Protocols},
  year =                {2002},
  month =               sep,
  institution =         {Lab.~Sp\'ecification \& V\'erification, ENS Cachan,
                         France},
  type =                {Research Report},
}

[FLM02]

Marco Faella, Salvatore La Torre, and Aniello Murano. Dense Real-Time Games. In LICS'02, pages 167-176. IEEE Comp. Soc. Press, July 2002.

BibTeX

@inproceedings{lics2002-FLM,
  author =              {Faella, Marco and La{~}Torre, Salvatore and Murano,
                         Aniello},
  title =               {Dense Real-Time Games},
  booktitle =           {{P}roceedings of the 17th {A}nnual {S}ymposium on
                         {L}ogic in {C}omputer {S}cience ({LICS}'02)},
  acronym =             {{LICS}'02},
  publisher =           {IEEE Comp. Soc. Press},
  pages =               {167-176},
  year =                {2002},
  month =               jul,
}

[FLM02]

Marco Faella, Salvatore La Torre, and Aniello Murano. Automata-Theoretic Decision of Timed Games. In VMCAI'02, Lecture Notes in Computer Science 2294, pages 94-108. Springer-Verlag, January 2002.

BibTeX

@inproceedings{vmcai2002-FLM,
  author =              {Faella, Marco and La{~}Torre, Salvatore and Murano,
                         Aniello},
  title =               {Automata-Theoretic Decision of Timed Games},
  editor =              {Cortesi, Agostino},
  booktitle =           {{P}roceedings of the 3rd {I}nternational {W}orkshop
                         on {V}erification, {M}odel {C}hecking, and
                         {A}bstract {I}nterpretation ({VMCAI}'02)},
  acronym =             {{VMCAI}'02},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {2294},
  pages =               {94-108},
  year =                {2002},
  month =               jan,
}

[FPY02]

Elena Fersman, Paul Pettersson, and Wang Yi. Timed Automata with Asynchronous Processes: Schedulability and Decidability. In TACAS'02, Lecture Notes in Computer Science 2280, pages 67-82. Springer-Verlag, April 2002.

BibTeX

@inproceedings{tacas2002-FPY,
  author =              {Fersman, Elena and Pettersson, Paul and Yi, Wang},
  title =               {Timed Automata with Asynchronous Processes:
                         Schedulability and Decidability},
  editor =              {Katoen, Joost-Pieter and Stevens, Perdita},
  booktitle =           {{P}roceedings of the 8th {I}nternational
                         {C}onference on {T}ools and {A}lgorithms for
                         {C}onstruction and {A}nalysis of {S}ystems
                         ({TACAS}'02)},
  acronym =             {{TACAS}'02},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {2280},
  pages =               {67-82},
  year =                {2002},
  month =               apr,
}

[FSS02]

Bernd Finkbeiner, Sriram Sankaranarayanan, and Henny Sipma. Collecting Statistics over Runtime Executions. In RV'02, Electronic Notes in Theoretical Computer Science 70(4). Elsevier, July 2002.

BibTeX

@inproceedings{rv2002-FSS,
  author =              {Finkbeiner, Bernd and Sankaranarayanan, Sriram and
                         Sipma, Henny},
  title =               {Collecting Statistics over Runtime Executions},
  editor =              {Havelund, Klaus and Ro{\c{s}}u, Grigore},
  booktitle =           {{P}roceedings of the 2nd {I}nternational {W}orkshop
                         on {R}untime {V}erification ({RV}'02)},
  acronym =             {{RV}'02},
  publisher =           {Elsevier},
  series =              {Electronic Notes in Theoretical Computer Science},
  volume =              {70},
  number =              {4},
  year =                {2002},
  month =               jul,
}

[GBD02]

Vijay Ganesh, Sergey Berezin, and David L. Dill. Deciding Presburger Arithmetic by Model Checking and Comparisons with Other Methods. In FMCAD'02, Lecture Notes in Computer Science 2517, pages 171-398. Springer-Verlag, November 2002.

BibTeX

@inproceedings{fmcad2002-GBD,
  author =              {Ganesh, Vijay and Berezin, Sergey and Dill, David
                         L.},
  title =               {Deciding {P}resburger Arithmetic by Model Checking
                         and Comparisons with Other Methods},
  editor =              {Aagaard, Mark D. and O'Leary, John W.},
  booktitle =           {{P}roceedings of the 4th {I}nternational
                         {C}onference on {F}ormal {M}ethods in
                         {C}omputer-{A}ided {D}esign ({FMCAD}'02)},
  acronym =             {{FMCAD}'02},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {2517},
  pages =               {171-398},
  year =                {2002},
  month =               nov,
}

[GK02]

Georg Gottlob and Christoph Koch. Monadic Queries over Tree-Structured Data. In LICS'02, pages 189-202. IEEE Comp. Soc. Press, July 2002.

BibTeX

@inproceedings{lics2002-GK,
  author =              {Gottlob, Georg and Koch, Christoph},
  title =               {Monadic Queries over Tree-Structured Data},
  booktitle =           {{P}roceedings of the 17th {A}nnual {S}ymposium on
                         {L}ogic in {C}omputer {S}cience ({LICS}'02)},
  acronym =             {{LICS}'02},
  publisher =           {IEEE Comp. Soc. Press},
  pages =               {189-202},
  year =                {2002},
  month =               jul,
}

[GL02]

Dimitra Giannakopoulou and Flavio Lerda. From States to Transitions: Improving Translation of LTL Formulae to Büchi Automata. In FORTE'02, Lecture Notes in Computer Science 2529, pages 308-326. Springer-Verlag, November 2002.

BibTeX

@inproceedings{forte2002-GL,
  author =              {Giannakopoulou, Dimitra and Lerda, Flavio},
  title =               {From States to Transitions: Improving Translation of
                         {LTL} Formulae to {B}{\"u}chi Automata},
  editor =              {Peled, Doron A. and Vardi, Moshe Y.},
  booktitle =           {{P}roceedings of the 22th {IFIP} {WG}6.1
                         {I}nternational {C}onference on {F}ormal
                         {T}echniques for {N}etworked and {D}istributed
                         {S}ystems ({FORTE}'02)},
  acronym =             {{FORTE}'02},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {2529},
  pages =               {308-326},
  year =                {2002},
  month =               nov,
}

[GP02]

Elsa Gunter and Doron A. Peled. Tracing the Executions of Concurrent Programs. In RV'02, Electronic Notes in Theoretical Computer Science 70(4). Elsevier, July 2002.

BibTeX

@inproceedings{rv2002-GP,
  author =              {Gunter, Elsa and Peled, Doron A.},
  title =               {Tracing the Executions of Concurrent Programs},
  editor =              {Havelund, Klaus and Ro{\c{s}}u, Grigore},
  booktitle =           {{P}roceedings of the 2nd {I}nternational {W}orkshop
                         on {R}untime {V}erification ({RV}'02)},
  acronym =             {{RV}'02},
  publisher =           {Elsevier},
  series =              {Electronic Notes in Theoretical Computer Science},
  volume =              {70},
  number =              {4},
  year =                {2002},
  month =               jul,
}

[GTW02]

Erich Grädel, Wolfgang Thomas, and Thomas Wilke. Automata Logics, and Infinite Games – A Guide to Current Research. Lecture Notes in Computer Science 2500. Springer-Verlag, 2002.

10.1007/3-540-36387-4

BibTeX

@book{GTW-lncs2500,
  title =               {Automata Logics, and Infinite Games~-- A~Guide to
                         Current Research},
  editor =              {Gr{\"a}del, Erich and Thomas, Wolfgang and Wilke,
                         Thomas},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {2500},
  year =                {2002},
  doi =                 {10.1007/3-540-36387-4},
}

[HAB02]

William Hesse, Eric Allender, and David A. Mix Barrington. Uniform constant-depth threshold circuits for division and iterated multiplication. Journal of Computer and System Sciences 65(4):695-716. Academic Press, December 2002.

BibTeX

@article{jcss65(4)-HAB,
  author =              {Hesse, William and Allender, Eric and Barrington,
                         David A. Mix},
  title =               {Uniform constant-depth threshold circuits for
                         division and iterated multiplication},
  publisher =           {Academic Press},
  journal =             {Journal of Computer and System Sciences},
  volume =              {65},
  number =              {4},
  pages =               {695-716},
  year =                {2002},
  month =               dec,
}

[HI02]

William Hesse and Neil Immerman. Complete Problems for Dynamic Complexity Classes. In LICS'02, pages 313-322. IEEE Comp. Soc. Press, July 2002.

PDF

BibTeX

@inproceedings{lics2002-HI,
  author =              {Hesse, William and Immerman, Neil},
  title =               {Complete Problems for Dynamic Complexity Classes},
  booktitle =           {{P}roceedings of the 17th {A}nnual {S}ymposium on
                         {L}ogic in {C}omputer {S}cience ({LICS}'02)},
  acronym =             {{LICS}'02},
  publisher =           {IEEE Comp. Soc. Press},
  pages =               {313-322},
  year =                {2002},
  month =               jul,
}

[HJM+02]

Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar, and Grégoire Sutre. Lazy abstraction. In POPL'02, ACM SIGPLAN Notices 37(1), pages 58-70. ACM Press, January 2002.

BibTeX

@inproceedings{popl2002-HJMS,
  author =              {Henzinger, Thomas A. and Jhala, Ranjit and Majumdar,
                         Rupak and Sutre, Gr{\'e}goire},
  title =               {Lazy abstraction},
  booktitle =           {Conference Record of the 29th {ACM}
                         {SIGPLAN}-{SIGACT} {S}ymposium on {P}rinciples of
                         {P}rogramming {L}anguages ({POPL}'02)},
  acronym =             {{POPL}'02},
  publisher =           {ACM Press},
  series =              {ACM SIGPLAN Notices},
  volume =              {37},
  number =              {1},
  pages =               {58-70},
  year =                {2002},
  month =               jan,
}

[HJR02]

Alan J. Hoffman, Kate Jenkins, and Tim Roughgarden. On a game in directed graphs. Information Processing Letters 83(1):13-16. Elsevier, July 2002.

BibTeX

@article{ipl83(1)-HJR,
  author =              {Hoffman, Alan J. and Jenkins, Kate and Roughgarden,
                         Tim},
  title =               {On a game in directed graphs},
  publisher =           {Elsevier},
  journal =             {Information Processing Letters},
  volume =              {83},
  number =              {1},
  pages =               {13-16},
  year =                {2002},
  month =               jul,
}

[HL02]

Martijn Hendriks and Kim Guldstrand Larsen. Exact Acceleration of real-Time Model Checking. In TPTS'02, Electronic Notes in Theoretical Computer Science 65(6). Elsevier, April 2002.

BibTeX

@inproceedings{tpts2002-HL,
  author =              {Hendriks, Martijn and Larsen, Kim Guldstrand},
  title =               {Exact Acceleration of real-Time Model Checking},
  editor =              {Asarin, Eugene and Maler, Oded and Yovine, Sergio},
  booktitle =           {{P}roceedings of the 1st {W}orkshop on {T}heory and
                         {P}ractice of {T}imed {S}ystems ({TPTS}'02)},
  acronym =             {{TPTS}'02},
  publisher =           {Elsevier},
  series =              {Electronic Notes in Theoretical Computer Science},
  volume =              {65},
  number =              {6},
  year =                {2002},
  month =               apr,
}

[HR02]

Klaus Havelund and Grigore Roşu. Synthesizing monitors for safety properties. In TACAS'02, Lecture Notes in Computer Science 2280, pages 342-356. Springer-Verlag, April 2002.

BibTeX

@inproceedings{tacas2002-HR,
  author =              {Havelund, Klaus and Ro{\c{s}}u, Grigore},
  title =               {Synthesizing monitors for safety properties},
  editor =              {Katoen, Joost-Pieter and Stevens, Perdita},
  booktitle =           {{P}roceedings of the 8th {I}nternational
                         {C}onference on {T}ools and {A}lgorithms for
                         {C}onstruction and {A}nalysis of {S}ystems
                         ({TACAS}'02)},
  acronym =             {{TACAS}'02},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {2280},
  pages =               {342-356},
  year =                {2002},
  month =               apr,
}

[HRS02]

Aidan Harding, Mark D. Ryan, and Pierre-Yves Schobbens. Approximating ATL* in ATL (Extended Abstract). In VMCAI'02, Lecture Notes in Computer Science 2294, pages 289-301. Springer-Verlag, January 2002.

BibTeX

@inproceedings{vmcai2002-HRS,
  author =              {Harding, Aidan and Ryan, Mark D. and Schobbens,
                         Pierre-Yves},
  title =               {Approximating {ATL}{\(^*\)} in~{ATL} (Extended
                         Abstract)},
  editor =              {Cortesi, Agostino},
  booktitle =           {{P}roceedings of the 3rd {I}nternational {W}orkshop
                         on {V}erification, {M}odel {C}hecking, and
                         {A}bstract {I}nterpretation ({VMCAI}'02)},
  acronym =             {{VMCAI}'02},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {2294},
  pages =               {289-301},
  year =                {2002},
  month =               jan,
}

[HRS+02]

Thomas Hune, Judi Romijn, Mariëlle Stoelinga, and Frits Vaandrager. Linear parametric model checking of timed automata. Journal of Logic and Algebraic Programming 52-53:183-220. Elsevier, June 2002.

BibTeX

@article{jlap52-53-hrsv,
  author =              {Hune, Thomas and Romijn, Judi and Stoelinga,
                         Mari{\"e}lle and Vaandrager, Frits},
  title =               {Linear parametric model checking of timed automata},
  publisher =           {Elsevier},
  journal =             {Journal of Logic and Algebraic Programming},
  volume =              {52-53},
  pages =               {183-220},
  year =                {2002},
  month =               jun,
}

[HWZ02]

Ian Hodkinson, Frank Wolter, and Michael Zakharyaschev. Decidable and Undecidable Fragments of First-Order Branching Temporal Logics. In LICS'02, pages 393-402. IEEE Comp. Soc. Press, July 2002.

BibTeX

@inproceedings{lics2002-HWZ,
  author =              {Hodkinson, Ian and Wolter, Frank and Zakharyaschev,
                         Michael},
  title =               {Decidable and Undecidable Fragments of First-Order
                         Branching Temporal Logics},
  booktitle =           {{P}roceedings of the 17th {A}nnual {S}ymposium on
                         {L}ogic in {C}omputer {S}cience ({LICS}'02)},
  acronym =             {{LICS}'02},
  publisher =           {IEEE Comp. Soc. Press},
  pages =               {393-402},
  year =                {2002},
  month =               jul,
}

[IKO+02]

Satoshi Ikeda, Izumi Kubo, Norihiro Okumoto, and Masafumi Yamashita. Local Topological Information and Cover Time. IPSJ SIG Notes 88:27-34. Information Processing Society of Japan, September 2002.

BibTeX

@article{ipsj88-IKOY,
  author =              {Ikeda, Satoshi and Kubo, Izumi and Okumoto, Norihiro
                         and Yamashita, Masafumi},
  title =               {Local Topological Information and Cover Time},
  publisher =           {Information Processing Society of Japan},
  journal =             {IPSJ SIG Notes},
  volume =              {88},
  pages =               {27-34},
  year =                {2002},
  month =               sep,
}

[Kir02]

Daniel Kirsten. Alternating tree automata and parity games. In Erich Grädel, Wolfgang Thomas, and Thomas Wilke (eds.), Automata, Logics, and Infinite Games, Lecture Notes in Computer Science 2500, pages 153-167. Springer-Verlag, 2002.

PDF

BibTeX

@incollection{lncs2500-kirsten,
  author =              {Kirsten, Daniel},
  title =               {Alternating tree automata and parity games},
  editor =              {Gr{\"a}del, Erich and Thomas, Wolfgang and Wilke,
                         Thomas},
  booktitle =           {Automata, Logics, and Infinite Games},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {2500},
  pages =               {153-167},
  year =                {2002},
}

[KJJ02]

Andrei A. Krokhin, Peter Jeavons, and Peter Jonsson. The Complexity of Constraints on Intervals and Lengths. In STACS'02, Lecture Notes in Computer Science 2285, pages 443-454. Springer-Verlag, March 2002.

BibTeX

@inproceedings{stacs2002-KJJ,
  author =              {Krokhin, Andrei A. and Jeavons, Peter and Jonsson,
                         Peter},
  title =               {The Complexity of Constraints on Intervals and
                         Lengths},
  editor =              {Alt, Helmut and Ferreira, Afonso},
  booktitle =           {{P}roceedings of the 19th {S}ymposium on
                         {T}heoretical {A}spects of {C}omputer {S}cience
                         ({STACS}'02)},
  acronym =             {{STACS}'02},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {2285},
  pages =               {443-454},
  year =                {2002},
  month =               mar,
}

[KM02]

Antonín Kučera and Richard Mayr. Why is Simulation Harder than Bisimulation?. In CONCUR'02, Lecture Notes in Computer Science 2421, pages 594-609. Springer-Verlag, August 2002.

BibTeX

@inproceedings{concur2002-KM,
  author =              {Ku{\v c}era, Anton{\'\i}n and Mayr, Richard},
  title =               {Why is Simulation Harder than Bisimulation?},
  editor =              {Brim, Lubo{\v s} and Jan{\v c}ar, Petr and K{\v
                         r}et{\'\i}nsk{\'y}, Mojm{\'\i}r and Ku{\v c}era,
                         Anton{\'\i}n},
  booktitle =           {{P}roceedings of the 13th {I}nternational
                         {C}onference on {C}oncurrency {T}heory
                         ({CONCUR}'02)},
  acronym =             {{CONCUR}'02},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {2421},
  pages =               {594-609},
  year =                {2002},
  month =               aug,
}

[KNS+02]

Marta Kwiatkowska, Gethin Norman, Roberto Segala, and Jeremy Sproston. Automatic verification of real-time systems with discrete probability distributions. Theoretical Computer Science 282(1):101-150. Elsevier, June 2002.

10.1016/S0304-3975(01)00046-9

BibTeX

@article{tcs282(1)-KNSS,
  author =              {Kwiatkowska, Marta and Norman, Gethin and Segala,
                         Roberto and Sproston, Jeremy},
  title =               {Automatic verification of real-time systems with
                         discrete probability distributions},
  publisher =           {Elsevier},
  journal =             {Theoretical Computer Science},
  volume =              {282},
  number =              {1},
  pages =               {101-150},
  year =                {2002},
  month =               jun,
  doi =                 {10.1016/S0304-3975(01)00046-9},
}

[KP02]

Yonit Kesten and Amir Pnueli. Complete Proof System for QPTL. Journal of Logic and Computation 12(5):701-745. Oxford University Press, October 2002.

10.1093/logcom/12.5.701

BibTeX

@article{jlc12(5)-KP,
  author =              {Kesten, Yonit and Pnueli, Amir},
  title =               {Complete Proof System for~{QPTL}},
  publisher =           {Oxford University Press},
  journal =             {Journal of Logic and Computation},
  volume =              {12},
  number =              {5},
  pages =               {701-745},
  year =                {2002},
  month =               oct,
  doi =                 {10.1093/logcom/12.5.701},
}

[KP02]

Beata Konikowska and Wojciech Penczek. Reducing Model Checking from Multi-Valued CTL* to CTL*. In CONCUR'02, Lecture Notes in Computer Science 2421, pages 226-239. Springer-Verlag, August 2002.

BibTeX

@inproceedings{concur2002-KP,
  author =              {Konikowska, Beata and Penczek, Wojciech},
  title =               {Reducing Model Checking from Multi-Valued
                         {CTL}{\(^*\)} to {CTL}{\(^*\)}},
  editor =              {Brim, Lubo{\v s} and Jan{\v c}ar, Petr and K{\v
                         r}et{\'\i}nsk{\'y}, Mojm{\'\i}r and Ku{\v c}era,
                         Anton{\'\i}n},
  booktitle =           {{P}roceedings of the 13th {I}nternational
                         {C}onference on {C}oncurrency {T}heory
                         ({CONCUR}'02)},
  acronym =             {{CONCUR}'02},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {2421},
  pages =               {226-239},
  year =                {2002},
  month =               aug,
}

[KPS+02]

Yonit Kesten, Amir Pnueli, Elad Shahar, and Lenore D. Zuck. Network Invariants in Action. In CONCUR'02, Lecture Notes in Computer Science 2421, pages 101-115. Springer-Verlag, August 2002.

BibTeX

@inproceedings{concur2002-KPSZ,
  author =              {Kesten, Yonit and Pnueli, Amir and Shahar, Elad and
                         Zuck, Lenore D.},
  title =               {Network Invariants in Action},
  editor =              {Brim, Lubo{\v s} and Jan{\v c}ar, Petr and K{\v
                         r}et{\'\i}nsk{\'y}, Mojm{\'\i}r and Ku{\v c}era,
                         Anton{\'\i}n},
  booktitle =           {{P}roceedings of the 13th {I}nternational
                         {C}onference on {C}oncurrency {T}heory
                         ({CONCUR}'02)},
  acronym =             {{CONCUR}'02},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {2421},
  pages =               {101-115},
  year =                {2002},
  month =               aug,
}

[KS02]

Antonín Kučera and Jan Strejček. The Stuterring Principle Revisited: On the Expressiveness of Nested X and U Operators in the Logic LTL. Technical Report FIMU-RS-2002-03, Faculty of Informatics, Masaryk University, Brno, Czech Republic, July 2002.

BibTeX

@techreport{fimu-rs-2002-03-KS,
  author =              {Ku{\v c}era, Anton{\'\i}n and Strej{\v c}ek, Jan},
  title =               {The Stuterring Principle Revisited: On the
                         Expressiveness of Nested~{X} and~{U} Operators in
                         the Logic {LTL}},
  number =              {FIMU-RS-2002-03},
  year =                {2002},
  month =               jul,
  institution =         {Faculty of Informatics, Masaryk University, Brno,
                         Czech Republic},
  type =                {Technical Report},
}

[Kur02]

Agi Kurucz. S5 × S5 × S5 lacks the finite model property. In AIML'00, pages 321-327. World Scientific, 2002.

BibTeX

@inproceedings{aiml2000-Kur,
  author =              {Kurucz, Agi},
  title =               {{{\(S5\times S5\times S5\)}} lacks the finite model
                         property},
  editor =              {de Rijke, Marteen and Wansing, Heinrich and Wolter,
                         Frank and Zakharyaschev, Michael},
  booktitle =           {{P}roceedings of the 3rd {W}orkshop on {A}dvances in
                         {M}odal {L}ogic ({AIML}'00)},
  acronym =             {{AIML}'00},
  publisher =           {World Scientific},
  pages =               {321-327},
  year =                {2002},
  confyear =            {2000},
  confmonth =           {10},
}

[Lan02]

Martin Lange. Local Model Checking Games for Fixed Point Logic with Chop. In CONCUR'02, Lecture Notes in Computer Science 2421, pages 240-254. Springer-Verlag, August 2002.

BibTeX

@inproceedings{concur2002-Lan,
  author =              {Lange, Martin},
  title =               {Local Model Checking Games for Fixed Point Logic
                         with Chop},
  editor =              {Brim, Lubo{\v s} and Jan{\v c}ar, Petr and K{\v
                         r}et{\'\i}nsk{\'y}, Mojm{\'\i}r and Ku{\v c}era,
                         Anton{\'\i}n},
  booktitle =           {{P}roceedings of the 13th {I}nternational
                         {C}onference on {C}oncurrency {T}heory
                         ({CONCUR}'02)},
  acronym =             {{CONCUR}'02},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {2421},
  pages =               {240-254},
  year =                {2002},
  month =               aug,
}

[Lan02]

Martin Lange. Alternating Context-Free Languages and Linear Time μ-calculus with Sequential Composition. In EXPRESS'02, Electronic Notes in Theoretical Computer Science 68(2), pages 71-87. Elsevier, August 2002.

BibTeX

@inproceedings{express2002-Lan,
  author =              {Lange, Martin},
  title =               {Alternating Context-Free Languages and Linear Time
                         {\(\mu\)}-calculus with Sequential Composition},
  editor =              {Nestmann, Uwe and Panangaden, Prakash},
  booktitle =           {{P}roceedings of the 9th {I}nternational {W}orkshop
                         on {E}xpressiveness in {C}oncurrency ({EXPRESS}'02)},
  acronym =             {{EXPRESS}'02},
  publisher =           {Elsevier},
  series =              {Electronic Notes in Theoretical Computer Science},
  volume =              {68},
  number =              {2},
  pages =               {71-87},
  year =                {2002},
  month =               aug,
}

[Las02]

Sławomir Lasota. Decidability of Strong Bisimilarity for Timed BPP. In CONCUR'02, Lecture Notes in Computer Science 2421, pages 562-579. Springer-Verlag, August 2002.

BibTeX

@inproceedings{concur2002-Las,
  author =              {Lasota, S{\l}awomir},
  title =               {Decidability of Strong Bisimilarity for Timed {BPP}},
  editor =              {Brim, Lubo{\v s} and Jan{\v c}ar, Petr and K{\v
                         r}et{\'\i}nsk{\'y}, Mojm{\'\i}r and Ku{\v c}era,
                         Anton{\'\i}n},
  booktitle =           {{P}roceedings of the 13th {I}nternational
                         {C}onference on {C}oncurrency {T}heory
                         ({CONCUR}'02)},
  acronym =             {{CONCUR}'02},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {2421},
  pages =               {562-579},
  year =                {2002},
  month =               aug,
}

[LM02]

Christopher Lynch and Barbara Morawska. Automatic Decidability. In LICS'02, pages 9-16. IEEE Comp. Soc. Press, July 2002.

BibTeX

@inproceedings{lics2002-LM,
  author =              {Lynch, Christopher and Morawska, Barbara},
  title =               {Automatic Decidability},
  booktitle =           {{P}roceedings of the 17th {A}nnual {S}ymposium on
                         {L}ogic in {C}omputer {S}cience ({LICS}'02)},
  acronym =             {{LICS}'02},
  publisher =           {IEEE Comp. Soc. Press},
  pages =               {9-16},
  year =                {2002},
  month =               jul,
}

[LS02]

Martin Lange and Colin Stirling. Model Checking Fixed Point Logic with Chop. In FoSSaCS'02, Lecture Notes in Computer Science 2303, pages 250-263. Springer-Verlag, April 2002.

BibTeX

@inproceedings{fossacs2002-LS,
  author =              {Lange, Martin and Stirling, Colin},
  title =               {Model Checking Fixed Point Logic with Chop},
  editor =              {Nielsen, Mogens and Engberg, Uffe},
  booktitle =           {{P}roceedings of the 5th {I}nternational
                         {C}onference on {F}oundations of {S}oftware
                         {S}cience and {C}omputation {S}tructure
                         ({FoSSaCS}'02)},
  acronym =             {{FoSSaCS}'02},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {2303},
  pages =               {250-263},
  year =                {2002},
  month =               apr,
}

[Mal02]

Oded Maler. Control from Computer Science. Annual Reviews in Control 26(2):175-187. Elsevier, 2002.

BibTeX

@article{aric26(2)-Mal,
  author =              {Maler, Oded},
  title =               {Control from Computer Science},
  publisher =           {Elsevier},
  journal =             {Annual Reviews in Control},
  volume =              {26},
  number =              {2},
  pages =               {175-187},
  year =                {2002},
}

[Mat02]

Radu Mateescu. Local Model-Checking of Modal Mu-Calculus on Acyclic Labeled Transition Systems. Research Report 4430, INRIA Rhône-Alpes, Montbonnot, France, April 2002.

BibTeX

@techreport{inria-4430,
  author =              {Mateescu, Radu},
  title =               {Local Model-Checking of Modal Mu-Calculus on Acyclic
                         Labeled Transition Systems},
  number =              {4430},
  year =                {2002},
  month =               apr,
  institution =         {INRIA Rh\^one-Alpes, Montbonnot, France},
  type =                {Research Report},
}

[Maz02]

René Mazala. Infinite Games. In Erich Grädel, Wolfgang Thomas, and Thomas Wilke (eds.), Automata, Logics, and Infinite Games, Lecture Notes in Computer Science 2500, pages 23-42. Springer-Verlag, 2002.

BibTeX

@incollection{lncs2500-mazala,
  author =              {Mazala, Ren{\'e}},
  title =               {Infinite Games},
  editor =              {Gr{\"a}del, Erich and Thomas, Wolfgang and Wilke,
                         Thomas},
  booktitle =           {Automata, Logics, and Infinite Games},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {2500},
  pages =               {23-42},
  year =                {2002},
}

[McM02]

Kenneth L. McMillan. Applying SAT Methods in Unbounded Symbolic Model Checking. In CAV'02, Lecture Notes in Computer Science 2404, pages 250-264. Springer-Verlag, July 2002.

BibTeX

@inproceedings{cav2002-McM,
  author =              {McMillan, Kenneth L.},
  title =               {Applying {SAT} Methods in Unbounded Symbolic Model
                         Checking},
  editor =              {Brinksma, Ed and Larsen, Kim Guldstrand},
  booktitle =           {{P}roceedings of the 14th {I}nternational
                         {C}onference on {C}omputer {A}ided {V}erification
                         ({CAV}'02)},
  acronym =             {{CAV}'02},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {2404},
  pages =               {250-264},
  year =                {2002},
  month =               jul,
}

[MM02]

Annabelle K. McIver and Carroll C. Morgan. Games, Probability and the Quantitative μ-calculus. In LPAR'02, Lecture Notes in Computer Science 2514, pages 292-310. Springer-Verlag, October 2002.

BibTeX

@inproceedings{lpar2002-MM,
  author =              {McIver, Annabelle K. and Morgan, Carroll C.},
  title =               {Games, Probability and the Quantitative
                         {\(\mu\)}-calculus},
  editor =              {Baaz, Matthias and Voronkov, Andrei},
  booktitle =           {{P}roceedings of the 9th {I}nternational
                         {C}onference {L}ogic {P}rogramming and {A}utomated
                         {R}easoning ({LPAR}'02)},
  acronym =             {{LPAR}'02},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {2514},
  pages =               {292-310},
  year =                {2002},
  month =               oct,
}

[MS02]

Paolo Maggi and Riccardo Sisto. Using SPIN to verify security properties of cryptographic protocols. In SPIN'02, Lecture Notes in Computer Science 2318, pages 187-204. Springer-Verlag, April 2002.

BibTeX

@inproceedings{spin2002-MS,
  author =              {Maggi, Paolo and Sisto, Riccardo},
  title =               {Using SPIN to verify security properties of
                         cryptographic protocols},
  editor =              {Bosnacki, Dragan and Leue, Stefan},
  booktitle =           {{P}roceedings of the 9th {I}nternational {SPIN}
                         {W}orkshop ({SPIN}'02)},
  acronym =             {{SPIN}'02},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {2318},
  pages =               {187-204},
  year =                {2002},
  month =               apr,
}

[Nie02]

Frank Nießner. Non-deterministic tree automata. In Erich Grädel, Wolfgang Thomas, and Thomas Wilke (eds.), Automata, Logics, and Infinite Games, Lecture Notes in Computer Science 2500, pages 227-232. Springer-Verlag, 2002.

BibTeX

@incollection{lncs2500-niessner,
  author =              {Nie{\ss}ner, Frank},
  title =               {Non-deterministic tree automata},
  editor =              {Gr{\"a}del, Erich and Thomas, Wolfgang and Wilke,
                         Thomas},
  booktitle =           {Automata, Logics, and Infinite Games},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {2500},
  pages =               {227-232},
  year =                {2002},
}

[Niw02]

Damian Niwiński. μ-calculus via Games. In CSL'02, Lecture Notes in Computer Science 2471, pages 27-43. Springer-Verlag, September 2002.

BibTeX

@inproceedings{csl2002-Niw,
  author =              {Niwi{\'n}ski, Damian},
  title =               {{\(\mu\)}-calculus via Games},
  booktitle =           {{P}roceedings of the 16th {I}nternational {W}orkshop
                         on {C}omputer {S}cience {L}ogic ({CSL}'02)},
  acronym =             {{CSL}'02},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {2471},
  pages =               {27-43},
  year =                {2002},
  month =               sep,
}

[NU02]

Matti Nykänen and Esko Ukkonen. The Exact Path Length Problem. Journal of Algorithms 42(1):41-53. Elsevier, January 2002.

10.1006/jagm.2001.1201

BibTeX

@article{ja42(1)-NU,
  author =              {Nyk{\"a}nen, Matti and Ukkonen, Esko},
  title =               {The Exact Path Length Problem},
  publisher =           {Elsevier},
  journal =             {Journal of Algorithms},
  volume =              {42},
  number =              {1},
  pages =               {41-53},
  year =                {2002},
  month =               jan,
  doi =                 {10.1006/jagm.2001.1201},
}

[OW02]

Joël Ouaknine and James Worrell. Timed CSP = Closed Timed Safety Automata. In EXPRESS'02, Electronic Notes in Theoretical Computer Science 68(2), pages 145-162. Elsevier, August 2002.

BibTeX

@inproceedings{express2002-OW,
  author =              {Ouaknine, Jo{\"e}l and Worrell, James},
  title =               {Timed {CSP} = Closed Timed Safety Automata},
  editor =              {Nestmann, Uwe and Panangaden, Prakash},
  booktitle =           {{P}roceedings of the 9th {I}nternational {W}orkshop
                         on {E}xpressiveness in {C}oncurrency ({EXPRESS}'02)},
  acronym =             {{EXPRESS}'02},
  publisher =           {Elsevier},
  series =              {Electronic Notes in Theoretical Computer Science},
  volume =              {68},
  number =              {2},
  pages =               {145-162},
  year =                {2002},
  month =               aug,
}

[PBD+02]

Anindya C. Patthak, Indrajit Bhattacharya, Anirban Dasgupta, Pallab Dasgupta, and P. P. Chakrabarti. Quantified Computation Tree Logic. Information Processing Letters 82(3):123-129. Elsevier, 2002.

PDF

BibTeX

@article{ipl82(3)-PBDDC,
  author =              {Patthak, Anindya C. and Bhattacharya, Indrajit and
                         Dasgupta, Anirban and Dasgupta, Pallab and
                         Chakrabarti, P. P.},
  title =               {Quantified Computation Tree Logic},
  publisher =           {Elsevier},
  journal =             {Information Processing Letters},
  volume =              {82},
  number =              {3},
  pages =               {123-129},
  year =                {2002},
}

[Pet02]

Holger Petersen. Expressions with Intersection Is Complete in LOGCFL. In STACS'02, Lecture Notes in Computer Science 2285, pages 513-522. Springer-Verlag, March 2002.

BibTeX

@inproceedings{stacs2002-Pet,
  author =              {Petersen, Holger},
  title =               {Expressions with Intersection Is Complete in
                         {LOGCFL}},
  editor =              {Alt, Helmut and Ferreira, Afonso},
  booktitle =           {{P}roceedings of the 19th {S}ymposium on
                         {T}heoretical {A}spects of {C}omputer {S}cience
                         ({STACS}'02)},
  acronym =             {{STACS}'02},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {2285},
  pages =               {513-522},
  year =                {2002},
  month =               mar,
}

[PK02]

Amir Pnueli and Yonit Kesten. A Deductive Proof System for CTL. In CONCUR'02, Lecture Notes in Computer Science 2421, pages 24-40. Springer-Verlag, August 2002.

BibTeX

@inproceedings{concur2002-PK,
  author =              {Pnueli, Amir and Kesten, Yonit},
  title =               {A~Deductive Proof System for~{CTL}},
  editor =              {Brim, Lubo{\v s} and Jan{\v c}ar, Petr and K{\v
                         r}et{\'\i}nsk{\'y}, Mojm{\'\i}r and Ku{\v c}era,
                         Anton{\'\i}n},
  booktitle =           {{P}roceedings of the 13th {I}nternational
                         {C}onference on {C}oncurrency {T}heory
                         ({CONCUR}'02)},
  acronym =             {{CONCUR}'02},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {2421},
  pages =               {24-40},
  year =                {2002},
  month =               aug,
}

[PXZ02]

Amir Pnueli, Jessie Xu, and Lenore D. Zuck. Liveness with (0,1,infty)-Counter Abstraction. In CAV'02, Lecture Notes in Computer Science 2404, pages 107-122. Springer-Verlag, July 2002.

10.1007/3-540-45657-0_9

PDF

BibTeX

@inproceedings{cav2002-PXZ,
  author =              {Pnueli, Amir and Xu, Jessie and Zuck, Lenore D.},
  title =               {Liveness with {{\((0,1,infty)\)}}-Counter
                         Abstraction},
  editor =              {Brinksma, Ed and Larsen, Kim Guldstrand},
  booktitle =           {{P}roceedings of the 14th {I}nternational
                         {C}onference on {C}omputer {A}ided {V}erification
                         ({CAV}'02)},
  acronym =             {{CAV}'02},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {2404},
  pages =               {107-122},
  year =                {2002},
  month =               jul,
  doi =                 {10.1007/3-540-45657-0_9},
}

[Rab02]

Alexander Rabinovich. Expressive Power of Temporal Logic. In CONCUR'02, Lecture Notes in Computer Science 2421, pages 57-75. Springer-Verlag, August 2002.

BibTeX

@inproceedings{concur2002-Rab,
  author =              {Rabinovich, Alexander},
  title =               {Expressive Power of Temporal Logic},
  editor =              {Brim, Lubo{\v s} and Jan{\v c}ar, Petr and K{\v
                         r}et{\'\i}nsk{\'y}, Mojm{\'\i}r and Ku{\v c}era,
                         Anton{\'\i}n},
  booktitle =           {{P}roceedings of the 13th {I}nternational
                         {C}onference on {C}oncurrency {T}heory
                         ({CONCUR}'02)},
  acronym =             {{CONCUR}'02},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {2421},
  pages =               {57-75},
  year =                {2002},
  month =               aug,
}

[Rot02]

Günter Rote. Crossing the Bridge at Night. EATCS Bulletin 78:241-246. EATCS, October 2002.

BibTeX

@article{eatcs-bull78()-Rot,
  author =              {Rote, G{\"u}nter},
  title =               {Crossing the Bridge at Night},
  publisher =           {EATCS},
  journal =             {EATCS Bulletin},
  volume =              {78},
  pages =               {241-246},
  year =                {2002},
  month =               oct,
}

[RT02]

Tim Roughgarden and Éva Tardos. How bad is selfish routing?. Journal of the ACM 49(2):236-259. ACM Press, March 2002.

10.1145/506147.506153

PDF

BibTeX

@article{jacm49(2)-RT,
  author =              {Roughgarden, Tim and Tardos, {\'E}va},
  title =               {How bad is selfish routing?},
  publisher =           {ACM Press},
  journal =             {Journal of the~ACM},
  volume =              {49},
  number =              {2},
  pages =               {236-259},
  year =                {2002},
  month =               mar,
  doi =                 {10.1145/506147.506153},
}

[SC02]

Michael Soltys and Stephen A. Cook. The Proof Complexity of Linear Algebra. In LICS'02, pages 335-344. IEEE Comp. Soc. Press, July 2002.

BibTeX

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

[Sch02]

Philippe Schnoebelen. Verifying Lossy Channel Systems has Nonprimitive Recursive Complexity. Information Processing Letters 83(5):251-261. Elsevier, September 2002.

BibTeX

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

[Sor02]

Maria Sorea. A Decidable Fixpoint Logic for Time-Outs. In CONCUR'02, Lecture Notes in Computer Science 2421, pages 255-271. Springer-Verlag, August 2002.

BibTeX

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

[Srb02]

Jiří Srba. Undecidability of Weak Bisimulation for Pushdown Processes. In CONCUR'02, Lecture Notes in Computer Science 2421, pages 579-593. Springer-Verlag, August 2002.

BibTeX

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

[SRH02]

Pierre-Yves Schobbens, Jean-François Raskin, and Thomas A. Henzinger. Axioms for Real-Time Logics. Theoretical Computer Science 274(1-2):151-182. Elsevier, March 2002.

BibTeX

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

[SS02]

Vladimiro Sassone and Paweł Sobocoński. Deriving Bisimulationn Congruences: A 2-Categorical Approach. In EXPRESS'02, Electronic Notes in Theoretical Computer Science 68(2), pages 107-126. Elsevier, August 2002.

BibTeX

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

[SU02]

Marcus Schaefer and Christopher Umans. Completeness in the Polynomial-Time hierarchy: A Compendium. SIGACT News 33(3):32-49. ACM Press, September 2002.

BibTeX

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

[SU02]

Marcus Schaefer and Christopher Umans. Completeness in the Polynomial-Time hierarchy: Part II. SIGACT News 33(4):22-36. ACM Press, December 2002.

BibTeX

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

[Tan02]

Till Tantau. Comparing Verboseness for Finite Automata and Turing Machines. In STACS'02, Lecture Notes in Computer Science 2285, pages 465-476. Springer-Verlag, March 2002.

BibTeX

@inproceedings{stacs2002-Tan,
  author =              {Tantau, Till},
  title =               {Comparing Verboseness for Finite Automata and Turing
                         Machines},
  editor =              {Alt, Helmut and Ferreira, Afonso},
  booktitle =           {{P}roceedings of the 19th {S}ymposium on
                         {T}heoretical {A}spects of {C}omputer {S}cience
                         ({STACS}'02)},
  acronym =             {{STACS}'02},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {2285},
  pages =               {465-476},
  year =                {2002},
  month =               mar,
}

[Tho02]

Wolfgang Thomas. Infinite Games and Verification (Extended Abstract of a Tutoral). In CAV'02, Lecture Notes in Computer Science 2404, pages 58-64. Springer-Verlag, July 2002.

BibTeX

@inproceedings{cav2002-Tho,
  author =              {Thomas, Wolfgang},
  title =               {Infinite Games and Verification (Extended Abstract
                         of a Tutoral)},
  editor =              {Brinksma, Ed and Larsen, Kim Guldstrand},
  booktitle =           {{P}roceedings of the 14th {I}nternational
                         {C}onference on {C}omputer {A}ided {V}erification
                         ({CAV}'02)},
  acronym =             {{CAV}'02},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {2404},
  pages =               {58-64},
  year =                {2002},
  month =               jul,
}

[Tri02]

Stavros Tripakis. Description and Schedulability Analysis of the Software Architecture of an Automated Vehicle Control System. In EMSOFT'02, Lecture Notes in Computer Science 2491, pages 123-137. Springer-Verlag, October 2002.

BibTeX

@inproceedings{emsoft2002-Tri,
  author =              {Tripakis, Stavros},
  title =               {Description and Schedulability Analysis of the
                         Software Architecture of an Automated Vehicle
                         Control System},
  editor =              {Sangiovani{-}Vincentelli, Alberto L. and Sifakis,
                         Joseph},
  booktitle =           {{P}roceedings of the 2nd {I}nternational
                         {C}onference on {E}mbedded {S}oftware ({EMSOFT}'02)},
  acronym =             {{EMSOFT}'02},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {2491},
  pages =               {123-137},
  year =                {2002},
  month =               oct,
}

[TW02]

Denis Thérien and Thomas Wilke. Nesting Until and Since in Linear Temporal Logic. In STACS'02, Lecture Notes in Computer Science 2285, pages 455-464. Springer-Verlag, March 2002.

BibTeX

@inproceedings{stacs2002-TW,
  author =              {Th{\'e}rien, Denis and Wilke, Thomas},
  title =               {Nesting Until and Since in Linear Temporal Logic},
  editor =              {Alt, Helmut and Ferreira, Afonso},
  booktitle =           {{P}roceedings of the 19th {S}ymposium on
                         {T}heoretical {A}spects of {C}omputer {S}cience
                         ({STACS}'02)},
  acronym =             {{STACS}'02},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {2285},
  pages =               {455-464},
  year =                {2002},
  month =               mar,
}

[TW02]

P. S. Thiagarajan and Igor Walukiewicz. An Expressively Complete Linear Time Temporal Logic for Mazurkiewicz Traces. Information and Computation 179(2):230-249. Academic Press, December 2002.

BibTeX

@article{icomp179(2)-TW,
  author =              {Thiagarajan, P. S. and Walukiewicz, Igor},
  title =               {An Expressively Complete Linear Time Temporal Logic
                         for {M}azurkiewicz Traces},
  publisher =           {Academic Press},
  journal =             {Information and Computation},
  volume =              {179},
  number =              {2},
  pages =               {230-249},
  year =                {2002},
  month =               dec,
}

[Wal02]

Igor Walukiewicz. Monadic second order logic on tree-like structures. Theoretical Computer Science 275(1-2):311-346. Elsevier, March 2002.

PDF

BibTeX

@article{tcs275(1-2)-Wal,
  author =              {Walukiewicz, Igor},
  title =               {Monadic second order logic on tree-like structures},
  publisher =           {Elsevier},
  journal =             {Theoretical Computer Science},
  volume =              {275},
  number =              {1-2},
  pages =               {311-346},
  year =                {2002},
  month =               mar,
}

Nicolas Markey

My .bib file