- Model-Checking Parametric Lock-Sharing Systems Against Regular Constraints
- with Corto Mascle, Anca Muscholl, CONCUR'23
DROPS
bibtex
@InProceedings{igw-concur23,
author = {Mascle, Corto and Muscholl, Anca and Walukiewicz, Igor},
title = {{Model-Checking Parametric Lock-Sharing Systems Against Regular Constraints}},
booktitle = {34th International Conference on Concurrency Theory (CONCUR 2023)},
pages = {24:1--24:17},
series = {LIPIcs},
ISBN = {978-3-95977-299-0},
ISSN = {1868-8969},
year = {2023},
volume = {279},
URL = {https://drops.dagstuhl.de/opus/volltexte/2023/19018},
URN = {urn:nbn:de:0030-drops-190184},
doi = {10.4230/LIPIcs.CONCUR.2023.24},
annote = {Keywords: Parametric systems, Locks, Model-checking}
}
- Checking Timed Buchi Automata Emptiness Using the Local-Time Semantics
- with Frederic Herbreteau, B. Srivathsan, CONCUR 2022
DROPS
bibtex
@inproceedings{concur22,
author = {Frédéric Herbreteau and B. Srivathsan and Igor Walukiewicz},
title = {Checking Timed Büchi Automata Emptiness Using the Local-Time Semantic},
booktitle = {CONCUR},
pages = {12:1--12:24,
year = {2022},
}
- Distributed controller synthesis for deadlock avoidance
- with Hugo Gimbert, Corto Mascle, Anca Muscholl, ICALP 2022
arxiv,
doi
bibtex
@inproceedings{igw-icalp22,
author = {Hugo Gimbert and Corto Mascle and Anca Muscholl and Igor Walukiewicz},
title = {Distributed controller synthesis for deadlock avoidance},
booktitle = {ICALP},
pages = {1--14},
year = {2022},
}
- Active learning sound negotiations
- with Anca Muscholl, LICS 2022
arxiv
bibtex
@inproceedings{igw-nego-lics22,
author = {Anca Muscholl and
Igor Walukiewicz},
title = {Active learning sound negotiations},
booktitle = {LICS},
pages = {1--14},
year = {2022},
}
- Abstractions for the local-time semantics of timed automata: a
foundation for partial-order methods
- with R. Govind, Frederic Herbreteau, B. Srivathsan, LICS 2022
PDF
bibtex
@inproceedings{igw-timed-lics22,
author = {R. Govind and Frédéric Herbreteau and B. Srivathsan and Igor Walukiewicz},
title = {Abstractions for the local-time semantics of timed automata: a
foundation for partial-order methods},
booktitle = {LICS},
pages = {1--14},
year = {2022},
}
- Verifying higher-order concurrency with data automata
- with Alex Dixon, Ranko Lazic, Andrzej S. Murawski, LICS 2021
PDF
bibtex
@inproceedings{igw-lics21,
author = {Alex Dixon and
Ranko Lazic and
Andrzej S. Murawski and
Igor Walukiewicz},
title = {Verifying higher-order concurrency with data automata},
booktitle = {LICS},
pages = {1--13},
year = {2021},
}
- Leafy Automata for Higher-Order Concurrency
- with Alex Dixon, Ranko Lazic, Andrzej S. Murawski, FOSSACS 2021
arXiv
bibtex
@inproceedings{igw-fossacs21,
author = {Alex Dixon and
Ranko Lazic and
Andrzej S. Murawski and
Igor Walukiewicz},
title = {Leafy automata for higher-order concurrency},
booktitle = {FOSSACS},
series = {LNCS},
volume = {12650},
pages = {184--204},
publisher = {Springer},
year = {2021},
url = {https://doi.org/10.1007/978-3-030-71995-1\_10},
doi = {10.1007/978-3-030-71995-1\_10},
}
- Why Liveness for Timed Automata Is Hard, and What We
Can Do About It
- with
F. Herbreteau, B. Srivathsan, Thanh-Tung Tran, ACM Trans. Comput. Log. 21 (3) pp
17:1--17: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:1--17: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 Heard-Of model
- with A. R. Balasubramanian, CONCUR 2020
PDF
 
bibtex
@inproceedings{igw-heard-of20,
author = {A. R. Balasubramanian and Igor Walukiewicz},
title = {Characterizing consensus in the Heard-Of model},
booktitle = {{CONCUR}},
series = {LIPIcs},
volume = {171},
pages = {9:1--9:18},
publisher = {Schloss Dagstuhl - Leibniz-Zentrum 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{igw-concur19,
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:1--16:15},
publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
year = {2019}
}
- LambdaY-Calculus With Priorities
- LICS 2019
PDF
 
PDF (long version)
 
bibtex
@inproceedings{igw-lics19,
author = {Igor Walukiewicz},
title = {LambdaY-Calculus With Priorities},
booktitle = {lics17},
pages = {1--13},
publisher = {IEEE},
year = {2019}
}
- The mu-calculus 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{igw-mu18,
author = {Julian C. Bradfield and Igor Walukiewicz},
title = {The mu-calculus 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 = {871--919},
year = {2018}
}
- Model-checking linear-time properties of parametrized asynchronous shared-memory pushdown systems
- with Marie Fortin and Anca Muscholl, CAV 2017
PDF
 
bibtex
@inproceedings{igw-CAV17,
author = {Marie Fortin and
Anca Muscholl and
Igor Walukiewicz},
title = {Model-checking linear-time properties of parametrized asynchronous shared-memory pushdown systems},
booktitle = {CAV},
pages = {155--175},
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{igw-LICS17,
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{igw-MSW17,
author = {Anca Muscholl and
Helmut Seidl and
Igor Walukiewicz},
title = {Reachability for Dynamic Parametric Processes},
booktitle = {VMCAI},
series = {LNCS},
volume = {10145},
publisher = {Springer},
pages = {424--441},
year = {2017},
url = {http://dx.doi.org/10.1007/978-3-319-52234-0_23},
doi = {10.1007/978-3-319-52234-0_23}}
- Synthesis with finite automata
- A chapter to appear in a handbook
PDF
-
Automata theory and higher-order model-checking
- SIGLOG News 4/2016 pp. 13-31
PDF
 
bibtex
@article{Wal-siglog16,
Author = {Igor Walukiewicz},
Biburl = {http://dblp.uni-trier.de/rec/bib/journals/siglog/Walukiewicz16},
Journal = {{SIGLOG} News},
Number = {4},
Pages = {13--31},
Title = {Automata theory and higher-order model-checking},
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},
Date-Added = {2016-11-14 17:47:11 +0000},
Date-Modified = {2016-11-14 17:49:32 +0000},
Journal = {Inform. and Comput.},
Pages = {67--90},
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 Higher-Order 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 Higher-Order Recursion Schemes is Decidable},
pages = {96--105},
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:1--99: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 = {1304--1350},
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 Tree-Pushdown 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 = {163--177},
Series = {LIPIcs},
Title = {Ordered Tree-Pushdown Systems},
Url = {http://dx.doi.org/10.4230/LIPIcs.FSTTCS.2015.163},
Volume = {45},
Year = {2015}}
- Safety of Parametrized Asynchronous Shared-Memory Systems is Almost
Always Decidable
- with Salvatore
La Torre and
Anca Muscholl, CONCUR 2015
PDF
 
bibtex
@inproceedings{TorreMW-CONCUR15,
author = {Salvatore {La Torre} and
Anca Muscholl and
Igor Walukiewicz},
title = {Safety of Parametrized Asynchronous Shared-Memory Systems is Almost
Always Decidable},
booktitle = {26th International Conference on Concurrency Theory, {CONCUR} 2015},
pages = {72--84},
year = {2015},
series = {LIPIcs},
volume = {42},
publisher = {Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik}
url = {http://dx.doi.org/10.4230/LIPIcs.CONCUR.2015.72},
doi = {10.4230/LIPIcs.CONCUR.2015.72},
biburl = {http://dblp.uni-trier.de/rec/bib/conf/concur/TorreMW15},
bibsource = {dblp computer science bibliography, http://dblp.org}
}
- A Model for Behavioural Properties of Higher-order Programs
- with Sylvain Salvati, CSL 2015
PDF
 
HAL (long version)
 
bibtex
@InProceedings{SalWal-csl2015,
author = {Sylvain Salvati and Igor Walukiewicz},
title = {{A Model for Behavioural Properties of Higher-order Programs}},
booktitle = {24th EACSL Annual Conference on Computer Science Logic (CSL 2015)},
pages = {229--243},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-90-3},
ISSN = {1868-8969},
year = {2015},
volume = {41},
editor = {Stephan Kreutzer},
publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
address = {Dagstuhl, Germany},
URL = {http://drops.dagstuhl.de/opus/volltexte/2015/5417},
URN = {urn:nbn:de:0030-drops-54173},
doi = {http://dx.doi.org/10.4230/LIPIcs.CSL.2015.229},
annote = {Keywords: Simply typed lambda-Y-calculus, 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/978-3-319-25150-9_3},
Pages = {39--57},
Series = {LNCS},
Title = {A Note on Monitors and Buchi Automata},
Url = {http://dx.doi.org/10.1007/978-3-319-25150-9_3},
Volume = {9399},
Year = {2015}}
- Typing weak MSOL-properties
- with Sylvain Salvati, LMCS '17
PDF
bibtex
@article{igw-lmcs17,
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 model-check 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/LMCS-11(2:7)2015},
Journal = {Logical Methods in Computer Science},
Number = {2},
Title = {Using models to model-check recursive schemes},
Url = {http://dx.doi.org/10.2168/LMCS-11(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 = {639--651},
Publisher = {Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik},
Series = {LIPIcs},
Volume = {29},
Year = {2014},
Url = {http://dx.doi.org/10.4230/LIPIcs.FSTTCS.2014.639}}
- Krivine machines and higher-order schemes
- with Sylvain Salvati, Inf. Comput. 239: 340-355 (2014)
PDF
 
bibtex
@article{SalWal14Krivine,
Author = {Sylvain Salvati and Igor Walukiewicz},
Title = {Krivine machines and higher-order schemes},
Journal = {Inf. Comput.},
Pages = {340--355},
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 162-173,
PDF
- Evaluation is MSOL compatible
- with Sylvain Salvati, FSTTCS 2013.
PDF
 
bibtex
@inproceedings{salwal13,
author = {Sylvain Salvati and Igor Walukiewicz},
title = {Evaluation is MSOL-compatible},
booktitle = {FSTTCS 2013},
series = {LIPIcs},
volume = {24},
publisher = {Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik},
pages = {103--114},
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 = {275--286},
year = {2013},
series = {Lecture Notes in Computer Science},
volume = {7966},
publisher = {Springer},
url = {http://dx.doi.org/10.1007/978-3-642-39212-2_26},
doi = {10.1007/978-3-642-39212-2_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/978-3-642-39799-8_71},
Pages = {990--1005},
Publisher = {Springer},
Series = {LNCS},
Url = {http://dx.doi.org/10.1007/978-3-642-39799-8_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/LMCS-8(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 = {375--384},
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 14-15 pp.612-616, 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 = {14-15},
Pages = {612--616},
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
122-146
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/s10703-011-0133-1},
Journal = {Formal Methods in System Design},
Number = {2},
Pages = {122--146},
Url = {http://dx.doi.org/10.1007/s10703-011-0133-1},
Volume = {40},
Year = {2012}}
-
Also in Proceedings of CAV'10,
LNCS 6174, pages
148-161 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/LMCS-8(3:18)2012},
Journal = {Logical Methods in Computer Science},
Number = {3},
Url = {http://dx.doi.org/10.2168/LMCS-8(3:18)2012},
Volume = {8},
Year = {2012}}
-
Also in proceedings of ICALP'09, LNCS 5556,
pp. 273--284 PDF
- Using non-convex approximations for efficient analysis of timed automata
- with F. Herbreteau and D. Kini and B. Srivathsan, FSTTCS'11,
LIPIcs 13, pages 162-173,
Proceedings
- Choice Functions and Well-Orderings over the Infinite
Binary Tree
- with Arnaud Carayol, Christof L�ding, Damian Niwinski.
Central European Journal of Mathematics 8(4), 2010, pp 662-682
PDF
- Optimal Zielonka-Type Construction of Deterministic
Asynchronous Automata
- with Blaise Genest, Hugo Gimbert, Anca Muscholl. Proceedings of
ICALP'10, LNCS 6199, pages
52-63 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)
356--371 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. 135-146,  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. 1-22
PDF,
arXiv
- Idealized Algol with ground recursion, and PDA
equivalence
- with Andrzej Murawski and Luke Ong, Proceedings of
ICALP'05, LNCS 3580, pp 917-929 PDF
- Unsafe grammars and panic automata
-
with Teodor Knapik, Damian Niwinski and Pawel Urzyczyn, Proceedings of
ICALP'05, LNCS 3580, pp 1450-1461
PostScript, PDF.
Long version: PostScript, PDF
- Third-Order Idealized Algol with Iteration is
Decidable
- with Andrzej Murawski,
Theor. Comput. Sci. 390(2-3): 214-229 (2008) (Conference version,
FOSSACS'05, LNCS 3441, pp. 202-218
PostScript, PDF)
- Alternating Timed Automata
- with Slawomir
Lasota, ACM Trans. Comput. Log. 9(2),
(2008) PDF (conference
version, FOSSACS'05 LNCS 3441, PDF)
- An NP-complete fragment of LTL
-
with Anca Muschol, Proceedings of DLT'04, PostScript, PDF
- Characterizing EF and EX tree logics
-
with Mikolaj Bojanczyk, TCS 358 (2-3) pp. 255-272 (2006) PostScript, PDF)
- Deciding Nondeterministic Hierarchy of Deterministic Tree
Automata
-
with Damian Niwinski, ENTCS 123 pp. 195-208, PostScript, PDF
- A landscape with games in the background
-
Invited talk at LICS'04, Proceedings of LICS'04, pp. 356-366, PostScript, PDF
- Distributed Games
- with Swarup Mohalik,
Proceedings of FSTTCS'03, LNCS 2914, pp. 338-351, 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. 88-99, 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. 7-34, PostScript,
PDF
- A gap property of deterministic tree languages,
- with Damian Niwinski. Theoretical Computer Science vol. 303(1)
(2003) pp. 215-231
PostScript, PDF
- Complexity of weak acceptance conditions in tree automata,
- with Jakub Neumann and Andrzej Szepietowski. IPL vol. 84 (2002)
pp. 181-187, PostScript, PDF
- Deciding low levels of tree-automata 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. 251-275,
PostScript, PDF
- Model checking CTL properties of pushdown systems,
- FSTTCS'00, LNCS 1974, pp. 127-138,
PostScript,
PDF
- Local logics for traces,
- Journal of Automata, Languages and Combinatorics 7(2002)
pp. 259-290, 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 Mu--calculus,
- 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. 230--249, PDF
- On the expressive completeness of the propositional
mu-calculus with respect to the monadic second order logic,
- with David Janin, CONCUR'96, LNCS 1119, pp. 263-277
PDF
- Pushdown processes: games and model checking,
- CAV'96, LNCS 1102 pp. 62-75 PDF. Full version
in Information and Computation 164(2001) pp. 234-263, PDF
- Monadic second order logic on tree-like
structures,
- STACS'96, LNCS 1046, pp. 401-414 PostScript. Full version
Theoretical Computer Science 275 (2002), no. 1-2, pp 311-346.
PDF.
- Monadic Second-Order 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. 35-62, PDF.
- Automata for the mu-calculus and related results,
- with David Janin, MFCS'95, LNCS 969, pp. 552-562,
PDF
- Completeness of Kozen's axiomatisation of the
propositional Mu-calculus,
- LICS'95, pp. 14-24. Full
version in Information and Computation 157 (2000), pp.142--182 (PDF ,
PDF of a full of version)
- A Complete Deductive System for the mu-Calculus,
- IEEE LICS'93 proceedings, pp. 136--147, also BRICS
Report Series RS-95-6 (University of Aarhus) PDF (full version)
- A Complete Deductive System for the mu-Calculus,
- PhD-thesis, Warsaw University, 1994, PostScript, PDF
- Games for the mu-calculus,
- with Damian Niwinski,
TCS 163, 1997, pp. 99--116 PDF
- Gentzen Type Axiomatization for Propositional Algorithmic
Logic,
- MFCS'90 B.Rovan (ed.) LNCS 452, pp. 499-508. Full version in
TCS 118
(1993) 67-79