Igor Walukiewicz: publications

Model-Checking Parametric Lock-Sharing Systems Against Regular Constraints
with Corto Mascle, Anca Muscholl, CONCUR'23
DROPS  bibtex

Checking Timed Buchi Automata Emptiness Using the Local-Time Semantics
with Frederic Herbreteau, B. Srivathsan, CONCUR 2022
DROPS  bibtex

Distributed controller synthesis for deadlock avoidance
with Hugo Gimbert, Corto Mascle, Anca Muscholl, ICALP 2022
arxiv, doi  bibtex

Active learning sound negotiations
with Anca Muscholl, LICS 2022
arxiv  bibtex

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

Verifying higher-order concurrency with data automata
with Alex Dixon, Ranko Lazic, Andrzej S. Murawski, LICS 2021
PDF  bibtex

Leafy Automata for Higher-Order Concurrency
with Alex Dixon, Ranko Lazic, Andrzej S. Murawski, FOSSACS 2021
arXiv  bibtex

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

Characterizing consensus in the Heard-Of model
with A. R. Balasubramanian, CONCUR 2020
PDF   bibtex

Revisiting Local Time Semantics for Networks of Timed Automata
with R. Govind, Frederic Herbreteau, and B. Srivathsan, CONCUR 2019
PDF   bibtex

LambdaY-Calculus With Priorities
LICS 2019
PDF   PDF (long version)   bibtex

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

Model-checking linear-time properties of parametrized asynchronous shared-memory pushdown systems
with Marie Fortin and Anca Muscholl, CAV 2017
PDF   bibtex

Static Analysis of Deterministic Negotiations
with Javier Esparza and Anca Muscholl, LICS 2017
PDF   bibtex

Reachability for Dynamic Parametric Processes
with Anca Muscholl and Helmut Seidl, VMCAI 2017
PDF   bibtex

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

Better abstractions for timed automata
with F. Herbreteau, B. Srivathsan, Information and Computation, vol. 251, 2016; long version of LICS 2012.
PDF   bibtex

Soundness in Negotiations
with Javier Esparza, Denis Kuperberg, and Anca Muscholl, LMCS vol 14 (2018) 2016
PDF   bibtex

The Diagonal Problem for Higher-Order Recursion Schemes is Decidable
with Lorenzo Clemente, Pawel Parys, and Sylvain Salvati, LICS 2016
PDF   bibtex

Deciding the topological complexity of Buchi languages
with Michal Skrzypczak, ICALP 2016
PDF   bibtex

Simply typed fixpoint calculus and collapsible pushdown automata
with Sylvain Salvati, Math. Struct. in Comp. Science 2016
PDF   bibtex

Ordered Tree-Pushdown Systems
with Lorenzo Clemente, Pawel Parys, and Sylvain Salvati, FSTTCS 2015
PDF   bibtex

Safety of Parametrized Asynchronous Shared-Memory Systems is Almost Always Decidable
with Salvatore La Torre and Anca Muscholl, CONCUR 2015
PDF   bibtex

A Model for Behavioural Properties of Higher-order Programs
with Sylvain Salvati, CSL 2015
PDF   HAL (long version)   bibtex

A Note on Monitors and Buchi automata
with Volker Diekert and Anca Muscholl, ICTAC 2015
PDF   bibtex

Typing weak MSOL-properties
with Sylvain Salvati, LMCS '17
PDF bibtex

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

Distributed Synthesis for Acyclic Architectures
with Anca Muscholl, FSTTCS 2014
PDF   bibtex

Krivine machines and higher-order schemes
with Sylvain Salvati, Inf. Comput. 239: 340-355 (2014)
PDF   bibtex
journal version of ICALP'11, LNCS 6756, pages 162-173, PDF

Evaluation is MSOL compatible
with Sylvain Salvati, FSTTCS 2013.
PDF   bibtex

Asynchronous Games over Tree Architectures
with B. Genest, H. Gimbert, and A. Muscholl, ICALP, 2013.
PDF   bibtex

Lazy abstractions for timed automata
with F. Herbreteau, B. Srivathsan, CAV, 2013.
arxiv   bibtex

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
Also in proceedings of LICS'09 PDF

Better abstractions for timed automata
with F. Herbreteau, B. Srivathsan, LICS, 2012.
PDF   bibtex

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

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
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
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

Igor Walukiewicz
Last modified: September 2023