Nicolas Markey

2002
[LMS02]	François Laroussinie, Nicolas Markey et Philippe Schnoebelen. On Model Checking Durational Kripke Structures (Extended Abstract). In FoSSaCS'02, Lecture Notes in Computer Science 2303, pages 264-279. Springer-Verlag, avril 2002. 10.1007/3-540-45931-6_19 PDF Abstract + BibTeX Résumé 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 et Philippe Schnoebelen. Temporal Logic with Forgettable Past. In LICS'02, pages 383-392. IEEE Comp. Soc. Press, juillet 2002. 10.1109/LICS.2002.1029846 PDFTest-of-time award Abstract + BibTeX Résumé 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, août 2002. 10.1016/S1571-0661(05)80366-4 PDF Abstract + BibTeX Résumé 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 et 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, avril 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 et 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, avril 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 et 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, avril 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 et Henrik Hulgaard. Boolean Expression Diagrams. Information and Computation 179(2):194-212. Academic Press, décembre 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 et Orna Kupferman. Alternating-time Temporal Logic. Journal of the ACM 49(5):672-713. ACM Press, septembre 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 et François Laroussinie. Is your Model Checker on Time?. Journal of Logic and Algebraic Programming 52-53:3-51. Elsevier, juin 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 et Oded Maler. Preemptive Job-Shop Scheduling using Stopwatch Automata. In TACAS'02, Lecture Notes in Computer Science 2280, pages 113-126. Springer-Verlag, avril 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 et 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, août 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, octobre 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 et Stavros Tripakis. Tools for Controller Synthesis of Timed Systems. In RT-TOOLS'02. Août 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, juillet 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 et Viktor Schuppan. Liveness Checking as Safety Checking. In FMICS'02, Electronic Notes in Theoretical Computer Science 66(2). Elsevier, juillet 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 et Achim Blumensath. The Monadic Theory of Tree-like Structures. In Erich Grädel, Wolfgang Thomas et 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}, chapter = {16}, year = {2002}, }
[BBD+02]	Gerd Behrmann, Johan Bengtsson, Alexandre David, Kim Guldstrand Larsen, Paul Pettersson et Wang Yi. UPPAAL Implementation Secrets. In FTRTFT'02, Lecture Notes in Computer Science 2469, pages 3-22. Springer-Verlag, septembre 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 et Clare Dixon. On the Relationship between ω-Automata and Temporal Logic Normal Forms. Journal of Logic and Computation 12(4):561-581. Oxford University Press, août 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 et Georg Gottlob. Propositional Default Logics made Easier: Computational Complexity of Model Checking. Theoretical Computer Science 289(1):591-627. Elsevier, octobre 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 et Anatol Slissenko. The Probablity Nesting Game. In EXPRESS'02, Electronic Notes in Theoretical Computer Science 68(2), pages 3-13. Elsevier, août 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 et Sergio Yovine. Verification of Asynchronous Circuits using Timed Automata. In TPTS'02, Electronic Notes in Theoretical Computer Science 65(6), pages 47-59. Elsevier, avril 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 et 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 et 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, juillet 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 et Alexander Rabinovich. Monadic Logic of Order over Naturals has no Finite Base. Journal of Logic and Computation 12(2):243-253. Oxford University Press, avril 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 et Franck Pommereau. Petri Nets with Causal Time for System Verification. In MTCS'02, Electronic Notes in Theoretical Computer Science 68(5). Elsevier, août 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 et Elena Calude. The Bridge Crossing Problem. EATCS Bulletin 77:180-190. EATCS, juin 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 et Armando Tacchella. NuSMV2: An OpenSource Tool for Symbolic Model Checking. In CAV'02, Lecture Notes in Computer Science 2404, pages 359-364. Springer-Verlag, juillet 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 et Moshe Y. Vardi. Reasoning about Actions and Planning in LTL Action Theories. In KR'02, pages 593-602. Morgan Kaufmann Publishers, avril 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 et 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, avril 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 et 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, mars 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 et Helmut Veith. Tree-Like Counterexamples in Model Checking. In LICS'02, pages 19-29. IEEE Comp. Soc. Press, juillet 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 et Gerald Lüttgen. A Logical Process Calculi. In EXPRESS'02, Electronic Notes in Theoretical Computer Science 68(2), pages 33-50. Elsevier, août 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 et 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, août 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 et 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, janvier 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 et 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, juillet 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 et 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, mars 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 et Parthasarathy Madhusudan. Timed Control Synthesis for External Specifications. In STACS'02, Lecture Notes in Computer Science 2285, pages 571-582. Springer-Verlag, mars 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 et Philippe Schnoebelen. The Complexity of Propositional Linear Temporal Logics in Simple Cases. Information and Computation 174(1):84-103. Academic Press, avril 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 et 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 et Ferhat Khendek. Timed Wp-Method: Testing Real-Time Systems. IEEE Transactions on Software Engineering 28(11):1023-1038. IEEE Comp. Soc. Press, novembre 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, août 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 et Thomas Wilke. First-Order Logic with Two Variables and Unary Temporal Logic. Information and Computation 179(2):279-295. Academic Press, décembre 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 et 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}, chapter = {1}, year = {2002}, }
[FG02]	Jörg Flum et Martin Grohe. Describing Parameterized Complexity Classes. In STACS'02, Lecture Notes in Computer Science 2285, pages 359-371. Springer-Verlag, mars 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 et Martin Grohe. The Complexity of First-Order and Monadic Second-Order Logic Revisited. In LICS'02, pages 215-224. IEEE Comp. Soc. Press, juillet 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 et Jesper Nyholm Jensen. Modal Logic for Cryptographic Systems. In EXPRESS'02, Electronic Notes in Theoretical Computer Science 68(2), pages 127-144. Elsevier, août 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 et Jérôme Leroux. How to Compose Presburger-Accelerations: Applications to Broadcast Protocols. Research Report, Lab. Spécification & Vérification, ENS Cachan, France, septembre 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 et Aniello Murano. Dense Real-Time Games. In LICS'02, pages 167-176. IEEE Comp. Soc. Press, juillet 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 et Aniello Murano. Automata-Theoretic Decision of Timed Games. In VMCAI'02, Lecture Notes in Computer Science 2294, pages 94-108. Springer-Verlag, janvier 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 et Wang Yi. Timed Automata with Asynchronous Processes: Schedulability and Decidability. In TACAS'02, Lecture Notes in Computer Science 2280, pages 67-82. Springer-Verlag, avril 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 et Henny Sipma. Collecting Statistics over Runtime Executions. In RV'02, Electronic Notes in Theoretical Computer Science 70(4). Elsevier, juillet 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 et 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, novembre 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 et Christoph Koch. Monadic Queries over Tree-Structured Data. In LICS'02, pages 189-202. IEEE Comp. Soc. Press, juillet 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 et 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, novembre 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 et Doron A. Peled. Tracing the Executions of Concurrent Programs. In RV'02, Electronic Notes in Theoretical Computer Science 70(4). Elsevier, juillet 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 et 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 et 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, décembre 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 et Neil Immerman. Complete Problems for Dynamic Complexity Classes. In LICS'02, pages 313-322. IEEE Comp. Soc. Press, juillet 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 et Grégoire Sutre. Lazy abstraction. In POPL'02, ACM SIGPLAN Notices 37(1), pages 58-70. ACM Press, janvier 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 et Tim Roughgarden. On a game in directed graphs. Information Processing Letters 83(1):13-16. Elsevier, juillet 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 et Kim Guldstrand Larsen. Exact Acceleration of real-Time Model Checking. In TPTS'02, Electronic Notes in Theoretical Computer Science 65(6). Elsevier, avril 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 et Grigore Roşu. Synthesizing monitors for safety properties. In TACAS'02, Lecture Notes in Computer Science 2280, pages 342-356. Springer-Verlag, avril 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 et Pierre-Yves Schobbens. Approximating ATL* in ATL (Extended Abstract). In VMCAI'02, Lecture Notes in Computer Science 2294, pages 289-301. Springer-Verlag, janvier 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 et Frits Vaandrager. Linear parametric model checking of timed automata. Journal of Logic and Algebraic Programming 52-53:183-220. Elsevier, juin 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 et Michael Zakharyaschev. Decidable and Undecidable Fragments of First-Order Branching Temporal Logics. In LICS'02, pages 393-402. IEEE Comp. Soc. Press, juillet 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 et Masafumi Yamashita. Local Topological Information and Cover Time. IPSJ SIG Notes 88:27-34. Information Processing Society of Japan, septembre 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 et 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}, chapter = {9}, year = {2002}, }
[KJJ02]	Andrei A. Krokhin, Peter Jeavons et Peter Jonsson. The Complexity of Constraints on Intervals and Lengths. In STACS'02, Lecture Notes in Computer Science 2285, pages 443-454. Springer-Verlag, mars 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, }
[KJJ02]	Andrei A. Krokhin, Peter Jeavons et Peter Jonsson. The Complexity of Constraints on Intervals and Lengths. In STACS'02, Lecture Notes in Computer Science 2285, pages 443-454. Springer-Verlag, mars 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 et Richard Mayr. Why is Simulation Harder than Bisimulation?. In CONCUR'02, Lecture Notes in Computer Science 2421, pages 594-609. Springer-Verlag, août 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 et Jeremy Sproston. Automatic verification of real-time systems with discrete probability distributions. Theoretical Computer Science 282(1):101-150. Elsevier, juin 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 et Amir Pnueli. Complete Proof System for QPTL. Journal of Logic and Computation 12(5):701-745. Oxford University Press, octobre 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 et 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, août 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 et Lenore D. Zuck. Network Invariants in Action. In CONCUR'02, Lecture Notes in Computer Science 2421, pages 101-115. Springer-Verlag, août 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 et 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, juillet 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, août 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, août 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, août 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 et Barbara Morawska. Automatic Decidability. In LICS'02, pages 9-16. IEEE Comp. Soc. Press, juillet 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 et Colin Stirling. Model Checking Fixed Point Logic with Chop. In FoSSaCS'02, Lecture Notes in Computer Science 2303, pages 250-263. Springer-Verlag, avril 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, avril 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 et Thomas Wilke (eds.), Automata, Logics, and Infinite Games, Lecture Notes in Computer Science 2500, pages 23-42. Springer-Verlag, 2002. PDF 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}, chapter = {2}, 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, juillet 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 et Carroll C. Morgan. Games, Probability and the Quantitative μ-calculus. In LPAR'02, Lecture Notes in Computer Science 2514, pages 292-310. Springer-Verlag, octobre 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 et 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, avril 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 et 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}, chapter = {8}, year = {2002}, }
[Niw02]	Damian Niwiński. μ-calculus via Games. In CSL'02, Lecture Notes in Computer Science 2471, pages 27-43. Springer-Verlag, septembre 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 et Esko Ukkonen. The Exact Path Length Problem. Journal of Algorithms 42(1):41-53. Elsevier, janvier 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 et James Worrell. Timed CSP = Closed Timed Safety Automata. In EXPRESS'02, Electronic Notes in Theoretical Computer Science 68(2), pages 145-162. Elsevier, août 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 et 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, mars 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 et Yonit Kesten. A Deductive Proof System for CTL. In CONCUR'02, Lecture Notes in Computer Science 2421, pages 24-40. Springer-Verlag, août 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 et Lenore D. Zuck. Liveness with (0,1,infty)-Counter Abstraction. In CAV'02, Lecture Notes in Computer Science 2404, pages 107-122. Springer-Verlag, juillet 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, août 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, octobre 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 et Éva Tardos. How bad is selfish routing?. Journal of the ACM 49(2):236-259. ACM Press, mars 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 et Stephen A. Cook. The Proof Complexity of Linear Algebra. In LICS'02, pages 335-344. IEEE Comp. Soc. Press, juillet 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, septembre 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, août 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, août 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 et Thomas A. Henzinger. Axioms for Real-Time Logics. Theoretical Computer Science 274(1-2):151-182. Elsevier, mars 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 et 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, août 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 et Christopher Umans. Completeness in the Polynomial-Time hierarchy: A Compendium. SIGACT News 33(3):32-49. ACM Press, septembre 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 et Christopher Umans. Completeness in the Polynomial-Time hierarchy: Part II. SIGACT News 33(4):22-36. ACM Press, décembre 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, mars 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, juillet 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, octobre 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 et Thomas Wilke. Nesting Until and Since in Linear Temporal Logic. In STACS'02, Lecture Notes in Computer Science 2285, pages 455-464. Springer-Verlag, mars 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 et Igor Walukiewicz. An Expressively Complete Linear Time Temporal Logic for Mazurkiewicz Traces. Information and Computation 179(2):230-249. Academic Press, décembre 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, mars 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 et Philippe Schnoebelen. On Model Checking Durational Kripke Structures (Extended Abstract). In FoSSaCS'02, Lecture Notes in Computer Science 2303, pages 264-279. Springer-Verlag, avril 2002.

10.1007/3-540-45931-6_19

PDF

Abstract + BibTeX

Résumé: 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 et Philippe Schnoebelen. Temporal Logic with Forgettable Past. In LICS'02, pages 383-392. IEEE Comp. Soc. Press, juillet 2002.

10.1109/LICS.2002.1029846

PDF

Test-of-time award

Abstract + BibTeX

Résumé: 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, août 2002.

10.1016/S1571-0661(05)80366-4

PDF

Abstract + BibTeX

Résumé: 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 et 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, avril 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 et 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, avril 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 et 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, avril 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 et Henrik Hulgaard. Boolean Expression Diagrams. Information and Computation 179(2):194-212. Academic Press, décembre 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 et Orna Kupferman. Alternating-time Temporal Logic. Journal of the ACM 49(5):672-713. ACM Press, septembre 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 et François Laroussinie. Is your Model Checker on Time?. Journal of Logic and Algebraic Programming 52-53:3-51. Elsevier, juin 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 et Oded Maler. Preemptive Job-Shop Scheduling using Stopwatch Automata. In TACAS'02, Lecture Notes in Computer Science 2280, pages 113-126. Springer-Verlag, avril 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 et 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, août 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, octobre 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 et Stavros Tripakis. Tools for Controller Synthesis of Timed Systems. In RT-TOOLS'02. Août 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, juillet 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 et Viktor Schuppan. Liveness Checking as Safety Checking. In FMICS'02, Electronic Notes in Theoretical Computer Science 66(2). Elsevier, juillet 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 et Achim Blumensath. The Monadic Theory of Tree-like Structures. In Erich Grädel, Wolfgang Thomas et 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},
  chapter =             {16},
  year =                {2002},
}

[BBD+02]

Gerd Behrmann, Johan Bengtsson, Alexandre David, Kim Guldstrand Larsen, Paul Pettersson et Wang Yi. UPPAAL Implementation Secrets. In FTRTFT'02, Lecture Notes in Computer Science 2469, pages 3-22. Springer-Verlag, septembre 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 et Clare Dixon. On the Relationship between ω-Automata and Temporal Logic Normal Forms. Journal of Logic and Computation 12(4):561-581. Oxford University Press, août 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 et Georg Gottlob. Propositional Default Logics made Easier: Computational Complexity of Model Checking. Theoretical Computer Science 289(1):591-627. Elsevier, octobre 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 et Anatol Slissenko. The Probablity Nesting Game. In EXPRESS'02, Electronic Notes in Theoretical Computer Science 68(2), pages 3-13. Elsevier, août 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 et Sergio Yovine. Verification of Asynchronous Circuits using Timed Automata. In TPTS'02, Electronic Notes in Theoretical Computer Science 65(6), pages 47-59. Elsevier, avril 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 et 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 et 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, juillet 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 et Alexander Rabinovich. Monadic Logic of Order over Naturals has no Finite Base. Journal of Logic and Computation 12(2):243-253. Oxford University Press, avril 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 et Franck Pommereau. Petri Nets with Causal Time for System Verification. In MTCS'02, Electronic Notes in Theoretical Computer Science 68(5). Elsevier, août 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 et Elena Calude. The Bridge Crossing Problem. EATCS Bulletin 77:180-190. EATCS, juin 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 et Armando Tacchella. NuSMV2: An OpenSource Tool for Symbolic Model Checking. In CAV'02, Lecture Notes in Computer Science 2404, pages 359-364. Springer-Verlag, juillet 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 et Moshe Y. Vardi. Reasoning about Actions and Planning in LTL Action Theories. In KR'02, pages 593-602. Morgan Kaufmann Publishers, avril 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 et 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, avril 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 et 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, mars 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 et Helmut Veith. Tree-Like Counterexamples in Model Checking. In LICS'02, pages 19-29. IEEE Comp. Soc. Press, juillet 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 et Gerald Lüttgen. A Logical Process Calculi. In EXPRESS'02, Electronic Notes in Theoretical Computer Science 68(2), pages 33-50. Elsevier, août 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 et 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, août 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 et 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, janvier 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 et 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, juillet 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 et 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, mars 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 et Parthasarathy Madhusudan. Timed Control Synthesis for External Specifications. In STACS'02, Lecture Notes in Computer Science 2285, pages 571-582. Springer-Verlag, mars 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 et Philippe Schnoebelen. The Complexity of Propositional Linear Temporal Logics in Simple Cases. Information and Computation 174(1):84-103. Academic Press, avril 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 et 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 et Ferhat Khendek. Timed Wp-Method: Testing Real-Time Systems. IEEE Transactions on Software Engineering 28(11):1023-1038. IEEE Comp. Soc. Press, novembre 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, août 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 et Thomas Wilke. First-Order Logic with Two Variables and Unary Temporal Logic. Information and Computation 179(2):279-295. Academic Press, décembre 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 et 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},
  chapter =             {1},
  year =                {2002},
}

[FG02]

Jörg Flum et Martin Grohe. Describing Parameterized Complexity Classes. In STACS'02, Lecture Notes in Computer Science 2285, pages 359-371. Springer-Verlag, mars 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 et Martin Grohe. The Complexity of First-Order and Monadic Second-Order Logic Revisited. In LICS'02, pages 215-224. IEEE Comp. Soc. Press, juillet 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 et Jesper Nyholm Jensen. Modal Logic for Cryptographic Systems. In EXPRESS'02, Electronic Notes in Theoretical Computer Science 68(2), pages 127-144. Elsevier, août 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 et Jérôme Leroux. How to Compose Presburger-Accelerations: Applications to Broadcast Protocols. Research Report, Lab. Spécification & Vérification, ENS Cachan, France, septembre 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 et Aniello Murano. Dense Real-Time Games. In LICS'02, pages 167-176. IEEE Comp. Soc. Press, juillet 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 et Aniello Murano. Automata-Theoretic Decision of Timed Games. In VMCAI'02, Lecture Notes in Computer Science 2294, pages 94-108. Springer-Verlag, janvier 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 et Wang Yi. Timed Automata with Asynchronous Processes: Schedulability and Decidability. In TACAS'02, Lecture Notes in Computer Science 2280, pages 67-82. Springer-Verlag, avril 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 et Henny Sipma. Collecting Statistics over Runtime Executions. In RV'02, Electronic Notes in Theoretical Computer Science 70(4). Elsevier, juillet 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 et 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, novembre 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 et Christoph Koch. Monadic Queries over Tree-Structured Data. In LICS'02, pages 189-202. IEEE Comp. Soc. Press, juillet 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 et 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, novembre 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 et Doron A. Peled. Tracing the Executions of Concurrent Programs. In RV'02, Electronic Notes in Theoretical Computer Science 70(4). Elsevier, juillet 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 et 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 et 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, décembre 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 et Neil Immerman. Complete Problems for Dynamic Complexity Classes. In LICS'02, pages 313-322. IEEE Comp. Soc. Press, juillet 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 et Grégoire Sutre. Lazy abstraction. In POPL'02, ACM SIGPLAN Notices 37(1), pages 58-70. ACM Press, janvier 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 et Tim Roughgarden. On a game in directed graphs. Information Processing Letters 83(1):13-16. Elsevier, juillet 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 et Kim Guldstrand Larsen. Exact Acceleration of real-Time Model Checking. In TPTS'02, Electronic Notes in Theoretical Computer Science 65(6). Elsevier, avril 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 et Grigore Roşu. Synthesizing monitors for safety properties. In TACAS'02, Lecture Notes in Computer Science 2280, pages 342-356. Springer-Verlag, avril 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 et Pierre-Yves Schobbens. Approximating ATL* in ATL (Extended Abstract). In VMCAI'02, Lecture Notes in Computer Science 2294, pages 289-301. Springer-Verlag, janvier 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 et Frits Vaandrager. Linear parametric model checking of timed automata. Journal of Logic and Algebraic Programming 52-53:183-220. Elsevier, juin 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 et Michael Zakharyaschev. Decidable and Undecidable Fragments of First-Order Branching Temporal Logics. In LICS'02, pages 393-402. IEEE Comp. Soc. Press, juillet 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 et Masafumi Yamashita. Local Topological Information and Cover Time. IPSJ SIG Notes 88:27-34. Information Processing Society of Japan, septembre 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 et 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},
  chapter =             {9},
  year =                {2002},
}

[KJJ02]

Andrei A. Krokhin, Peter Jeavons et Peter Jonsson. The Complexity of Constraints on Intervals and Lengths. In STACS'02, Lecture Notes in Computer Science 2285, pages 443-454. Springer-Verlag, mars 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,
}

[KJJ02]

Andrei A. Krokhin, Peter Jeavons et Peter Jonsson. The Complexity of Constraints on Intervals and Lengths. In STACS'02, Lecture Notes in Computer Science 2285, pages 443-454. Springer-Verlag, mars 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 et Richard Mayr. Why is Simulation Harder than Bisimulation?. In CONCUR'02, Lecture Notes in Computer Science 2421, pages 594-609. Springer-Verlag, août 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 et Jeremy Sproston. Automatic verification of real-time systems with discrete probability distributions. Theoretical Computer Science 282(1):101-150. Elsevier, juin 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 et Amir Pnueli. Complete Proof System for QPTL. Journal of Logic and Computation 12(5):701-745. Oxford University Press, octobre 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 et 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, août 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 et Lenore D. Zuck. Network Invariants in Action. In CONCUR'02, Lecture Notes in Computer Science 2421, pages 101-115. Springer-Verlag, août 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 et 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, juillet 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, août 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, août 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, août 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 et Barbara Morawska. Automatic Decidability. In LICS'02, pages 9-16. IEEE Comp. Soc. Press, juillet 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 et Colin Stirling. Model Checking Fixed Point Logic with Chop. In FoSSaCS'02, Lecture Notes in Computer Science 2303, pages 250-263. Springer-Verlag, avril 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, avril 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 et Thomas Wilke (eds.), Automata, Logics, and Infinite Games, Lecture Notes in Computer Science 2500, pages 23-42. Springer-Verlag, 2002.

PDF

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},
  chapter =             {2},
  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, juillet 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 et Carroll C. Morgan. Games, Probability and the Quantitative μ-calculus. In LPAR'02, Lecture Notes in Computer Science 2514, pages 292-310. Springer-Verlag, octobre 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 et 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, avril 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 et 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},
  chapter =             {8},
  year =                {2002},
}

[Niw02]

Damian Niwiński. μ-calculus via Games. In CSL'02, Lecture Notes in Computer Science 2471, pages 27-43. Springer-Verlag, septembre 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 et Esko Ukkonen. The Exact Path Length Problem. Journal of Algorithms 42(1):41-53. Elsevier, janvier 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 et James Worrell. Timed CSP = Closed Timed Safety Automata. In EXPRESS'02, Electronic Notes in Theoretical Computer Science 68(2), pages 145-162. Elsevier, août 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 et 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, mars 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 et Yonit Kesten. A Deductive Proof System for CTL. In CONCUR'02, Lecture Notes in Computer Science 2421, pages 24-40. Springer-Verlag, août 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 et Lenore D. Zuck. Liveness with (0,1,infty)-Counter Abstraction. In CAV'02, Lecture Notes in Computer Science 2404, pages 107-122. Springer-Verlag, juillet 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, août 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, octobre 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 et Éva Tardos. How bad is selfish routing?. Journal of the ACM 49(2):236-259. ACM Press, mars 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 et Stephen A. Cook. The Proof Complexity of Linear Algebra. In LICS'02, pages 335-344. IEEE Comp. Soc. Press, juillet 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, septembre 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, août 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, août 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 et Thomas A. Henzinger. Axioms for Real-Time Logics. Theoretical Computer Science 274(1-2):151-182. Elsevier, mars 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 et 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, août 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 et Christopher Umans. Completeness in the Polynomial-Time hierarchy: A Compendium. SIGACT News 33(3):32-49. ACM Press, septembre 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 et Christopher Umans. Completeness in the Polynomial-Time hierarchy: Part II. SIGACT News 33(4):22-36. ACM Press, décembre 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, mars 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, juillet 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, octobre 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 et Thomas Wilke. Nesting Until and Since in Linear Temporal Logic. In STACS'02, Lecture Notes in Computer Science 2285, pages 455-464. Springer-Verlag, mars 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 et Igor Walukiewicz. An Expressively Complete Linear Time Temporal Logic for Mazurkiewicz Traces. Information and Computation 179(2):230-249. Academic Press, décembre 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, mars 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

Mon fichier BibTeX