 Distributed controller synthesis for deadlock avoidance
 with Hugo Gimbert, Corto Mascle, Anca Muscholl, ICALP 2022
arxiv
bibtex
@inproceedings{igwicalp22,
author = {Hugo Gimbert and Corto Mascle and Anca Muscholl and Igor Walukiewicz},
title = {Distributed controller synthesis for deadlock avoidance},
booktitle = {ICALP},
pages = {114},
year = {2022},
}
 Active learning sound negotiations
 with Anca Muscholl, LICS 2022
arxiv
bibtex
@inproceedings{igwnegolics22,
author = {Anca Muscholl and
Igor Walukiewicz},
title = {Active learning sound negotiations},
booktitle = {LICS},
pages = {114},
year = {2022},
}
 Abstractions for the localtime semantics of timed automata: a
foundation for partialorder methods
 with R. Govind, Frederic Herbreteau, B. Srivathsan, LICS 2022
PDF
bibtex
@inproceedings{igwtimedlics22,
author = {R. Govind and Frédéric Herbreteau and B. Srivathsan and Igor Walukiewicz},
title = {Abstractions for the localtime semantics of timed automata: a
foundation for partialorder methods},
booktitle = {LICS},
pages = {114},
year = {2022},
}
 Verifying higherorder concurrency with data automata
 with Alex Dixon, Ranko Lazic, Andrzej S. Murawski, LICS 2021
PDF
bibtex
@inproceedings{igwlics21,
author = {Alex Dixon and
Ranko Lazic and
Andrzej S. Murawski and
Igor Walukiewicz},
title = {Verifying higherorder concurrency with data automata},
booktitle = {LICS},
pages = {113},
year = {2021},
}
 Leafy Automata for HigherOrder Concurrency
 with Alex Dixon, Ranko Lazic, Andrzej S. Murawski, FOSSACS 2021
arXiv
bibtex
@inproceedings{igwfossacs21,
author = {Alex Dixon and
Ranko Lazic and
Andrzej S. Murawski and
Igor Walukiewicz},
title = {Leafy automata for higherorder concurrency},
booktitle = {FOSSACS},
series = {LNCS},
volume = {12650},
pages = {184204},
publisher = {Springer},
year = {2021},
url = {https://doi.org/10.1007/9783030719951\_10},
doi = {10.1007/9783030719951\_10},
}
 Why Liveness for Timed Automata Is Hard, and What We
Can Do About It
 with
F. Herbreteau, B. Srivathsan, ThanhTung Tran, ACM Trans. Comput. Log. 21 (3) pp
17:117:28
PDF
bibtex
@article{HerSriTra20,
author = {Fr{\'{e}}d{\'{e}}ric Herbreteau and B. Srivathsan and Thanh{}Tung Tran and Igor Walukiewicz},
doi = {10.1145/3372310},
journal = {{ACM} Trans. Comput. Log.},
number = {3},
pages = {17:117:28},
title = {Why Liveness for Timed Automata Is Hard, and What We Can Do About It},
url = {https://doi.org/10.1145/3372310},
volume = {21},
year = {2020}
}
 Characterizing consensus in the HeardOf model
 with A. R. Balasubramanian, CONCUR 2020
PDF
bibtex
@inproceedings{igwheardof20,
author = {A. R. Balasubramanian and Igor Walukiewicz},
title = {Characterizing consensus in the HeardOf model},
booktitle = {{CONCUR}},
series = {LIPIcs},
volume = {171},
pages = {9:19:18},
publisher = {Schloss Dagstuhl  LeibnizZentrum f{\"{u}}r Informatik},
year = {2020}
}
 Revisiting Local Time Semantics for Networks of Timed Automata
 with R. Govind,
Frederic Herbreteau, and
B. Srivathsan, CONCUR 2019
PDF
bibtex
@inproceedings{igwconcur19,
author = {R. Govind and
Fr{\'{e}}d{\'{e}}ric Herbreteau and
B. Srivathsan and
Igor Walukiewicz},
title = {Revisiting Local Time Semantics for Networks of Timed Automata},
booktitle = {{CONCUR}},
series = {LIPIcs},
volume = {140},
pages = {16:116:15},
publisher = {Schloss Dagstuhl  LeibnizZentrum f{\"{u}}r Informatik},
year = {2019}
}
 LambdaYCalculus With Priorities
 LICS 2019
PDF
PDF (long version)
bibtex
@inproceedings{igwlics19,
author = {Igor Walukiewicz},
title = {LambdaYCalculus With Priorities},
booktitle = {lics17},
pages = {113},
publisher = {IEEE},
year = {2019}
}
 The mucalculus and Model Checking
 with Julian Bradfield, in Handbook of Model Checking 2018, E.M. Clarke, T. A. Henzinger, H. Veith, R. Bloem, eds
PDF
bibtex
@inproceedings{igwmu18,
author = {Julian C. Bradfield and Igor Walukiewicz},
title = {The mucalculus and Model Checking},
booktitle = {Handbook of Model Checking},
editor = {Edmund M. Clarke and
Thomas A. Henzinger and
Helmut Veith and
Roderick Bloem},
publisher = {Springer},
pages = {871919},
year = {2018}
}
 Modelchecking lineartime properties of parametrized asynchronous sharedmemory pushdown systems
 with Marie Fortin and Anca Muscholl, CAV 2017
PDF
bibtex
@inproceedings{igwCAV17,
author = {Marie Fortin and
Anca Muscholl and
Igor Walukiewicz},
title = {Modelchecking lineartime properties of parametrized asynchronous sharedmemory pushdown systems},
booktitle = {CAV},
pages = {155175},
series = {LNCS},
volume = {10427},
publisher = {Springer},
year = {2017},
note = {to appear}
 Static Analysis of Deterministic Negotiations
 with
Javier Esparza and Anca Muscholl, LICS 2017
PDF
bibtex
@inproceedings{igwLICS17,
author = {Javier Esparza and
Anca Muscholl and
Igor Walukiewicz},
title = {Static Analysis of Deterministic Negotiations},
booktitle = {LICS},
publisher = {IEEE},
year = {2017},
note = {to appear}
 Reachability for Dynamic Parametric Processes
 with Anca Muscholl and Helmut Seidl, VMCAI 2017
PDF
bibtex
@inproceedings{igwMSW17,
author = {Anca Muscholl and
Helmut Seidl and
Igor Walukiewicz},
title = {Reachability for Dynamic Parametric Processes},
booktitle = {VMCAI},
series = {LNCS},
volume = {10145},
publisher = {Springer},
pages = {424441},
year = {2017},
url = {http://dx.doi.org/10.1007/9783319522340_23},
doi = {10.1007/9783319522340_23}}
 Synthesis with finite automata
 A chapter to appear in a handbook
PDF

Automata theory and higherorder modelchecking
 SIGLOG News 4/2016 pp. 1331
PDF
bibtex
@article{Walsiglog16,
Author = {Igor Walukiewicz},
Biburl = {http://dblp.unitrier.de/rec/bib/journals/siglog/Walukiewicz16},
Journal = {{SIGLOG} News},
Number = {4},
Pages = {1331},
Title = {Automata theory and higherorder modelchecking},
Url = {http://dl.acm.org/citation.cfm?id=3026745},
Volume = {3},
Year = {2016}}
 Better abstractions for timed automata
 with
F. Herbreteau, B. Srivathsan, Information and Computation, vol. 251,
2016; long version of LICS 2012.
PDF
bibtex
@article{HerSriWal16,
Author = {Fr{\'{e}}d{\'{e}}ric Herbreteau and {S}rivathsan, {B}. and Igor Walukiewicz},
DateAdded = {20161114 17:47:11 +0000},
DateModified = {20161114 17:49:32 +0000},
Journal = {Inform. and Comput.},
Pages = {6790},
Title = {Better Abstractions for Timed Automata},
Volume = {251},
Year = {2016}}
 Soundness in Negotiations
 with Javier Esparza, Denis Kuperberg, and Anca Muscholl, LMCS vol
14 (2018)
2016
PDF
bibtex
@article{EKMW18,
Author = {Esparza, Javier and Kuperberg, Denis and Muscholl, Anca and Walukiewicz, Igor},
Journal = {Logical Methods in Computer Science},
Title = {Soundness in negotiations},
Volume = {14},
Year = {2018}}
 The Diagonal Problem for HigherOrder Recursion Schemes is
Decidable
 with Lorenzo Clemente, Pawel Parys, and Sylvain Salvati, LICS
2016
PDF
bibtex
@inproceedings{CleParSalWal16,
Author = {Lorenzo Clemente and Pawel Parys and Sylvain Salvati and Igor Walukiewicz},
Booktitle = {LICS'16},
Title = {The Diagonal Problem for HigherOrder Recursion Schemes is Decidable},
pages = {96105},
Year = {2016}}
 Deciding the topological complexity of Buchi languages
 with Michal Skrzypczak, ICALP 2016
PDF
bibtex
@inproceedings{SkrWal16,
Author = {Michal Skrzypczak and Igor Walukiewicz},
Booktitle = {ICALP'16},
pages = {99:199:13},
Series = {LIPIcs},
Title = {Deciding the topological complexity of B\"uchi languages},
series = {LIPIcs},
volume = {55},
Year = {2016}
}
 Simply typed fixpoint calculus and collapsible pushdown automata
 with Sylvain Salvati, Math. Struct. in Comp. Science 2016
PDF
bibtex
@article{SalWal16,
author = {Sylvain Salvati and
Igor Walukiewicz},
title = {Simply typed fixpoint calculus and collapsible pushdown automata},
journal = {Mathematical Structures in Computer Science},
volume = {26},
number = {7},
pages = {13041350},
year = {2016},
keywords = {ours},
url = {https://doi.org/10.1017/S0960129514000590},
doi = {10.1017/S0960129514000590},
biburl = {http://dblp.org/rec/bib/journals/mscs/SalvatiW16},
bibsource = {dblp computer science bibliography, http://dblp.org}
}
 Ordered TreePushdown Systems
 with Lorenzo Clemente, Pawel Parys, and Sylvain Salvati, FSTTCS
2015
PDF
bibtex
@inproceedings{CleParSal15,
Author = {Lorenzo Clemente and Pawel Parys and Sylvain Salvati and Igor Walukiewicz},
Booktitle = {FSTTCS'15},
Doi = {10.4230/LIPIcs.FSTTCS.2015.163},
Pages = {163177},
Series = {LIPIcs},
Title = {Ordered TreePushdown Systems},
Url = {http://dx.doi.org/10.4230/LIPIcs.FSTTCS.2015.163},
Volume = {45},
Year = {2015}}
 Safety of Parametrized Asynchronous SharedMemory Systems is Almost
Always Decidable
 with Salvatore
La Torre and
Anca Muscholl, CONCUR 2015
PDF
bibtex
@inproceedings{TorreMWCONCUR15,
author = {Salvatore {La Torre} and
Anca Muscholl and
Igor Walukiewicz},
title = {Safety of Parametrized Asynchronous SharedMemory Systems is Almost
Always Decidable},
booktitle = {26th International Conference on Concurrency Theory, {CONCUR} 2015},
pages = {7284},
year = {2015},
series = {LIPIcs},
volume = {42},
publisher = {Schloss Dagstuhl  LeibnizZentrum fuer Informatik}
url = {http://dx.doi.org/10.4230/LIPIcs.CONCUR.2015.72},
doi = {10.4230/LIPIcs.CONCUR.2015.72},
biburl = {http://dblp.unitrier.de/rec/bib/conf/concur/TorreMW15},
bibsource = {dblp computer science bibliography, http://dblp.org}
}
 A Model for Behavioural Properties of Higherorder Programs
 with Sylvain Salvati, CSL 2015
PDF
HAL (long version)
bibtex
@InProceedings{SalWalcsl2015,
author = {Sylvain Salvati and Igor Walukiewicz},
title = {{A Model for Behavioural Properties of Higherorder Programs}},
booktitle = {24th EACSL Annual Conference on Computer Science Logic (CSL 2015)},
pages = {229243},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {9783939897903},
ISSN = {18688969},
year = {2015},
volume = {41},
editor = {Stephan Kreutzer},
publisher = {Schloss DagstuhlLeibnizZentrum fuer Informatik},
address = {Dagstuhl, Germany},
URL = {http://drops.dagstuhl.de/opus/volltexte/2015/5417},
URN = {urn:nbn:de:0030drops54173},
doi = {http://dx.doi.org/10.4230/LIPIcs.CSL.2015.229},
annote = {Keywords: Simply typed lambdaYcalculus, Monadic second order logic, semantic models}
}
 A Note on Monitors and Buchi automata
 with Volker Diekert and
Anca Muscholl, ICTAC 2015
PDF
bibtex
@inproceedings{DieMusWal15,
Author = {Volker Diekert and Anca Muscholl and Igor Walukiewicz},
Booktitle = {{ICTAC} 2015},
Doi = {10.1007/9783319251509_3},
Pages = {3957},
Series = {LNCS},
Title = {A Note on Monitors and Buchi Automata},
Url = {http://dx.doi.org/10.1007/9783319251509_3},
Volume = {9399},
Year = {2015}}
 Typing weak MSOLproperties
 with Sylvain Salvati, LMCS '17
PDF
bibtex
@article{igwlmcs17,
author = {Sylvain Salvati and
Igor Walukiewicz},
title = {Typing weak {MSOL} properties},
journal = {Logical Methods in Computer Science},
volume = {13},
number = {1},
year = {2017}
}
 Using models to modelcheck recursive schemes
 with S. Salvati, Logical Methods in Computer Science 11(2), 2015
journal version of, TLCA 2013.
PDF
arxiv
bibtex
@article{SalWal15,
Author = {Sylvain Salvati and Igor Walukiewicz},
Doi = {10.2168/LMCS11(2:7)2015},
Journal = {Logical Methods in Computer Science},
Number = {2},
Title = {Using models to modelcheck recursive schemes},
Url = {http://dx.doi.org/10.2168/LMCS11(2:7)2015},
Volume = {11},
Year = {2015}}
}
 Distributed Synthesis for Acyclic Architectures
 with Anca Muscholl, FSTTCS 2014
PDF
bibtex
@inproceedings{MusWal14,
Author = {Anca Muscholl and Igor Walukiewicz},
Title = {Distributed Synthesis for Acyclic Architectures},
Booktitle = {FSTTCS},
Doi = {10.4230/LIPIcs.FSTTCS.2014.639},
Pages = {639651},
Publisher = {Schloss Dagstuhl  LeibnizZentrum fuer Informatik},
Series = {LIPIcs},
Volume = {29},
Year = {2014},
Url = {http://dx.doi.org/10.4230/LIPIcs.FSTTCS.2014.639}}
 Krivine machines and higherorder schemes
 with Sylvain Salvati, Inf. Comput. 239: 340355 (2014)
PDF
bibtex
@article{SalWal14Krivine,
Author = {Sylvain Salvati and Igor Walukiewicz},
Title = {Krivine machines and higherorder schemes},
Journal = {Inf. Comput.},
Pages = {340355},
Volume = {239},
Year = {2014},
Url = {http://dx.doi.org/10.1016/j.ic.2014.07.012},
Doi = {10.1016/j.ic.2014.07.012}}
 journal version of ICALP'11, LNCS 6756, pages 162173,
PDF
 Evaluation is MSOL compatible
 with Sylvain Salvati, FSTTCS 2013.
PDF
bibtex
@inproceedings{salwal13,
author = {Sylvain Salvati and Igor Walukiewicz},
title = {Evaluation is MSOLcompatible},
booktitle = {FSTTCS 2013},
series = {LIPIcs},
volume = {24},
publisher = {Schloss Dagstuhl  LeibnizZentrum fuer Informatik},
pages = {103114},
year = {2013},
url = {http://dx.doi.org/10.4230/LIPIcs.FSTTCS.2013.103},
doi = {10.4230/LIPIcs.FSTTCS.2013.103}}
 Asynchronous Games over Tree Architectures
 with
B. Genest, H. Gimbert, and A. Muscholl, ICALP,
2013.
PDF
bibtex
@inproceedings{GGMW13,
author = {Blaise Genest and Hugo Gimbert and
Anca Muscholl and Igor Walukiewicz},
title = {Asynchronous Games over Tree Architectures},
booktitle = {ICALP 2013},
pages = {275286},
year = {2013},
series = {Lecture Notes in Computer Science},
volume = {7966},
publisher = {Springer},
url = {http://dx.doi.org/10.1007/9783642392122_26},
doi = {10.1007/9783642392122_26}}
 Lazy abstractions for timed automata
 with
F. Herbreteau, B. Srivathsan, CAV, 2013.
arxiv
bibtex
@inproceedings{HerSriWal13,
Author = {Fr{\'{e}}d{\'{e}}ric Herbreteau and B. Srivathsan and Igor Walukiewicz},
Title = {Lazy Abstractions for Timed Automata},
Booktitle = {CAV},
Doi = {10.1007/9783642397998_71},
Pages = {9901005},
Publisher = {Springer},
Series = {LNCS},
Url = {http://dx.doi.org/10.1007/9783642397998_71},
Volume = {8044},
Year = {2013}}
 Wreath Products of Forest Algebras, with Applications to
Tree Logics
 with Mikolaj Bojanczyk and Howard Straubing.
Logical Methods in Computer Science, 8(3), 2012
PDF
bibtex
@article{BojStrWal12,
Author = {Mikolaj Bojanczyk and Howard Straubing and Igor Walukiewicz},
Title = {Wreath Products of Forest Algebras, with Applications to Tree Logics},
Ee = {http://dx.doi.org/10.2168/LMCS8(3:19)2012},
Journal = {Logical Methods in Computer Science},
Number = {3},
Volume = {8},
Year = {2012}}
 Also in proceedings of LICS'09
PDF
 Better abstractions for timed automata
 with
F. Herbreteau, B. Srivathsan, LICS, 2012.
PDF
bibtex
@inproceedings{HerSriWal12,
Author = {Fr{\'{e}}d{\'{e}}ric Herbreteau and B. Srivathsan and Igor Walukiewicz},
Title = {Better Abstractions for Timed Automata},
Booktitle = {LICS},
Doi = {10.1109/LICS.2012.48},
Pages = {375384},
Publisher = {{IEEE} Computer Society},
Url = {http://dx.doi.org/10.1109/LICS.2012.48},
Year = {2012}}
 An alternate proof of Statman's finite completeness
theorem
 with B. Srivathsan, Information Processing
Letters, Volume 112, Issues 1415 pp.612616, 2012
PDF
bibtex
@article{SriWal12,
Author = {B. Srivathsan and Igor Walukiewicz},
Title = {An alternate proof of Statman's finite completeness theorem},
Doi = {10.1016/j.ipl.2012.04.014},
Journal = {Inf. Process. Lett.},
Number = {1415},
Pages = {612616},
Url = {http://dx.doi.org/10.1016/j.ipl.2012.04.014},
Volume = {112},
Year = {2012}}
 Efficient Emptiness Check for Timed Buchi
Automata
 with Frederic Herbreteau and B. Srivathsan.
Formal Methods in System Design: Volume 40, Issue 2 (2012), Pages
122146
PDF
bibtex
@article{HerSriWal12Buchi,
Author = {Fr{\'{e}}d{\'{e}}ric Herbreteau and B. Srivathsan and Igor Walukiewicz},
Title = {Efficient emptiness check for timed B{\"{u}}chi automata},
Doi = {10.1007/s1070301101331},
Journal = {Formal Methods in System Design},
Number = {2},
Pages = {122146},
Url = {http://dx.doi.org/10.1007/s1070301101331},
Volume = {40},
Year = {2012}}

Also in Proceedings of CAV'10,
LNCS 6174, pages
148161 PDF
 Weak Alternating Timed Automata
 with Pawel
Parys. Logical Methods in Computer Science 8(3), 2012
PDF
bibtex
@article{ParWal12,
Author = {Pawel Parys and Igor Walukiewicz},
Title = {Weak Alternating Timed Automata},
Doi = {10.2168/LMCS8(3:18)2012},
Journal = {Logical Methods in Computer Science},
Number = {3},
Url = {http://dx.doi.org/10.2168/LMCS8(3:18)2012},
Volume = {8},
Year = {2012}}

Also in proceedings of ICALP'09, LNCS 5556,
pp. 273284 PDF
 Using nonconvex approximations for efficient analysis of timed automata
 with F. Herbreteau and D. Kini and B. Srivathsan, FSTTCS'11,
LIPIcs 13, pages 162173,
Proceedings
 Choice Functions and WellOrderings over the Infinite
Binary Tree
 with Arnaud Carayol, Christof L�ding, Damian Niwinski.
Central European Journal of Mathematics 8(4), 2010, pp 662682
PDF
 Optimal ZielonkaType Construction of Deterministic
Asynchronous Automata
 with Blaise Genest, Hugo Gimbert, Anca Muscholl. Proceedings of
ICALP'10, LNCS 6199, pages
5263 PDF
 A look at the control of asynchronous automata
 with Anca Muscholl and Marc Zeitoun, in Perspectives in
Concurrency Theory, K. Lodaya, M. Mukund, R. Ramanujam (Ed.) (2008)
356371 PDF
 Nondeterministic controllers of nondeterministic
processes
 with Andre Arnold, in
J. Flum, E. Graedel, T. Wilke eds. "Logic and Automata", Texts in Logic and
Games, Amsterdam University Press,
2007 PDF
 Forest Algebras
 with Mikolaj Bojanczyk, in
J. Flum, E. Graedel, T. Wilke eds. "Logic and Automata", Texts in Logic and
Games, Amsterdam University Press,
2007 PDF
 Minimizing variants of visibly pushdown
automata
 with Pat Chervet, in Proceedings of MFCS'07, LNCS 4708, pp. 135146, PDF
 The Complexity of Games on Higher Order Pushdown
Automata
 with Thierry Cachat. A short
note. PDF at
HAL
 A lower bound on web services composition
 with Anca Muscholl, Logical Methods in Computer
Science (FOSSACS, Special
Issue) CORR
(conference version FOSSACS
2007, PDF )
 Positional determinacy of games with infinitely many
priorities
 with Erich Grädel,
Logical Methods in Computer Science
Vol. 2 2006, pp. 122
PDF,
arXiv
 Idealized Algol with ground recursion, and PDA
equivalence
 with Andrzej Murawski and Luke Ong, Proceedings of
ICALP'05, LNCS 3580, pp 917929 PDF
 Unsafe grammars and panic automata

with Teodor Knapik, Damian Niwinski and Pawel Urzyczyn, Proceedings of
ICALP'05, LNCS 3580, pp 14501461
PostScript, PDF.
Long version: PostScript, PDF
 ThirdOrder Idealized Algol with Iteration is
Decidable
 with Andrzej Murawski,
Theor. Comput. Sci. 390(23): 214229 (2008) (Conference version,
FOSSACS'05, LNCS 3441, pp. 202218
PostScript, PDF)
 Alternating Timed Automata
 with Slawomir
Lasota, ACM Trans. Comput. Log. 9(2),
(2008) PDF (conference
version, FOSSACS'05 LNCS 3441, PDF)
 An NPcomplete fragment of LTL

with Anca Muschol, Proceedings of DLT'04, PostScript, PDF
 Characterizing EF and EX tree logics

with Mikolaj Bojanczyk, TCS 358 (23) pp. 255272 (2006) PostScript, PDF)
 Deciding Nondeterministic Hierarchy of Deterministic Tree
Automata

with Damian Niwinski, ENTCS 123 pp. 195208, PostScript, PDF
 A landscape with games in the background

Invited talk at LICS'04, Proceedings of LICS'04, pp. 356366, PostScript, PDF
 Distributed Games
 with Swarup Mohalik,
Proceedings of FSTTCS'03, LNCS 2914, pp. 338351, PostScript, PDF
(Full version PostScript, PDF)
 Pushdown games with unboundedness and regular
conditions
 with Alexis Bouquet, Olivier Serre,
Proceedings of FSTTCS'03, LNCS 2914, pp. 8899, PostScript, PDF (Full version PostScript, PDF)
 Games for synthesis of controlers with partial
observation,
 with Andre Arnold and Aymeric Vincent. Theoretical Computer Science vol. 303(1)
(2003) pp. 734, PostScript,
PDF
 A gap property of deterministic tree languages,
 with Damian Niwinski. Theoretical Computer Science vol. 303(1)
(2003) pp. 215231
PostScript, PDF
 Complexity of weak acceptance conditions in tree automata,
 with Jakub Neumann and Andrzej Szepietowski. IPL vol. 84 (2002)
pp. 181187, PostScript, PDF
 Deciding low levels of treeautomata hierarchy
 Proceedings of WoLLIC'02, ENTCS vol 67, PostScript, PDF
 Permissive strategies: from parity games to safety
games,
 with Julien Bernet and David Janin. Theoretical
Informatics and Applications (RAIRO) 36(2002) pp. 251275,
PostScript, PDF
 Model checking CTL properties of pushdown systems,
 FSTTCS'00, LNCS 1974, pp. 127138,
PostScript,
PDF
 Local logics for traces,
 Journal of Automata, Languages and Combinatorics 7(2002)
pp. 259290, PostScript,
PDF
 Guarded fixed point logic,
 with Erich Grädel, LICS 99, PostScript, PDF
 Difficult configurations  On the complexity of
LTrL,
 ICALP '98, LNCS 1443 PostScript, (Full version to
appear in Formal Methods in System Design
PostScript,
PDF)
 The Horn Mucalculus,
 with Witold Charatonik,
David McAllester Damian Niwinski, Andreas Podelski, LICS '98, PostScript,
PDF
 Relating hierachies of word and tree automata,
 with Damian Niwinski, STACS'98, LNCS 1373, PDF
 How much memory is needed to win infinite games,
 with Stefan Dziembowski and Marcin Jurdzinski, IEEE LICS'97,
PDF
 An expressively complete linear time temporal
logic,
 with P. S. Thiagarajan, IEEE LICS'97, PostScript. Full version in
Information and Computation 179(2002) pp. 230249, PDF
 On the expressive completeness of the propositional
mucalculus with respect to the monadic second order logic,
 with David Janin, CONCUR'96, LNCS 1119, pp. 263277
PDF
 Pushdown processes: games and model checking,
 CAV'96, LNCS 1102 pp. 6275 PDF. Full version
in Information and Computation 164(2001) pp. 234263, PDF
 Monadic second order logic on treelike
structures,
 STACS'96, LNCS 1046, pp. 401414 PostScript. Full version
Theoretical Computer Science 275 (2002), no. 12, pp 311346.
PDF.
 Monadic SecondOrder Logic, Graph Coverings and Unfoldings
of Transition Systems
 with Bruno Courcelle, CSL'95, Full
version in Annals of Pure and Applied Logic, 92 (1998) pp. 3562, PDF.
 Automata for the mucalculus and related results,
 with David Janin, MFCS'95, LNCS 969, pp. 552562,
PDF
 Completeness of Kozen's axiomatisation of the
propositional Mucalculus,
 LICS'95, pp. 1424. Full
version in Information and Computation 157 (2000), pp.142182 (PDF ,
PDF of a full of version)
 A Complete Deductive System for the muCalculus,
 IEEE LICS'93 proceedings, pp. 136147, also BRICS
Report Series RS956 (University of Aarhus) PDF (full version)
 A Complete Deductive System for the muCalculus,
 PhDthesis, Warsaw University, 1994, PostScript, PDF
 Games for the mucalculus,
 with Damian Niwinski,
TCS 163, 1997, pp. 99116 PDF
 Gentzen Type Axiomatization for Propositional Algorithmic
Logic,
 MFCS'90 B.Rovan (ed.) LNCS 452, pp. 499508. Full version in
TCS 118
(1993) 6779