# Selected Publications

## Energy, parity and related games

- W. Czerwinski, L. Daviaud, N. Fijalkow, M. Jurdzinski, R. Lazic and P. Parys

*Universal trees grow inside separating automata: Quasi-polynomial lower bounds for parity games*

30th Annual ACM-SIAM Symposium on Discrete Algorithms (SODA)

2333-2349, January 2019 - L. Daviaud, M. Jurdzinski, R. Lazic

*A pseudo-quasi-polynomial algorithm for mean-payoff parity games*

33rd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)

July 2018 - M. Jurdzinski and R. Lazic

*Succinct progress measures for solving parity games*

32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)

June 2017 - Th. Colcombet, M. Jurzinski, R. Lazic and S. Schmitz

*Perfect half space games*

32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)

June 2017 - M. Jurdzinski, R. Lazic and S. Schmitz

*Fixed-Dimensional Energy Games are in Pseudo-Polynomial Time*

42nd International Colloquium on Automata, Languages, and Programming (ICALP), Part II

Lecture Notes in Computer Science 9135: 260-272, Springer, July 2015 Talk

## Petri nets and related models

- W. Czerwinski, S. Lasota, R. Lazic, J. Leroux and F. Mazowiecki

*The reachability problem for Petri nets is not elementary*

51st Annual ACM SIGACT Symposium on Theory of Computing (STOC)

24-33, June 2019 - D. Figueira, R. Lazic, J. Leroux, F. Mazowiecki and G. Sutre

*Polynomial-space completeness of reachability for succinct branching VASS in dimension one*

44th International Colloquium on Automata, Languages, and Programming (ICALP)

LIPIcs 80, 119:1-119:14, Schloss Dagstuhl, July 2017 - R. Lazic and P. Totzke

*What Makes Petri Nets Harder to Verify: Stack or Data?*

Concurrency, Security, and Puzzles - Essays Dedicated to Andrew William Roscoe on the Occasion of His 60th Birthday

Lecture Notes in Computer Science 10160: 144-161, Springer, January 2017 - S. Göller, C. Haase, R. Lazic and P. Totzke

*A Polynomial-Time Algorithm for Reachability in Branching VASS in Dimension One*

43rd International Colloquium on Automata, Languages, and Programming (ICALP)

LIPIcs 55, 105: 1-13, Schloss Dagstuhl, July 2016 - M. Englert, R. Lazic and P. Totzke

*Reachability in Two-Dimensional Unary Vector Addition Systems with States is NL-Complete*

31st Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)

477-484, July 2016 - R. Lazic and S. Schmitz

*The Complexity of Coverability in ν-Petri Nets*

31st Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)

467-476, July 2016 - P. Hofman, S. Lasota, R. Lazic, J. Leroux, S. Schmitz and P. Totzke

*Coverability Trees for Petri Nets with Unordered Data*

19th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS)

Lecture Notes in Computer Science 9634: 445-461, Springer, April 2016 - R. Lazic and S. Schmitz

*The Ideal View on Rackoff's Coverability Technique*

9th International Workshop on Reachability Problems (RP)

Lecture Notes in Computer Science 9328: 76-88, Springer, September 2015 - R. Lazic and S. Schmitz

*Non-Elementary Complexities for Branching VASS, MELL, and Extensions*

Transactions on Computational Logic 16(3), 30 pages, ACM, 2015 - R. Lazic and S. Schmitz

*Non-Elementary Complexities for Branching VASS, MELL, and Extensions*

23rd EACSL Annual Conference on Computer Science Logic (CSL) and 29th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)

July 2014 Talk - R. Lazic

*The reachability problem for vector addition systems with a stack is not elementary*

6th International Workshop on Reachability Problems (RP)

Informal presentation, September 2012: 4-page abstract, talk - R. Lazic

*The reachability problem for branching vector addition systems requires doubly-exponential space*

Information Processing Letters 110(17): 740-745, Elsevier, 2010 - S. Demri, M. Jurdzinski, O. Lachish and R. Lazic

*The covering and boundedness problems for branching vector addition systems*

Journal of Computer and System Sciences 79(1): 23-38, Elsevier, 2013 - S. Demri, M. Jurdzinski, O. Lachish and R. Lazic

*The covering and boundedness problems for branching vector addition systems*

29th Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS)

LIPIcs 4: 181-192, Schloss Dagstuhl, December 2009 - R. Lazic, T. Newcomb, J. Ouaknine, A.W. Roscoe and J. Worrell

*Nets with tokens which carry data*

Fundamenta Informaticae 88(3): 251-274, 2008 - R. Lazic, T. Newcomb, J. Ouaknine, A.W. Roscoe and J. Worrell

*Nets with tokens which carry data*

28th International Conference on Application and Theory of Petri Nets and Other Models of Concurrency (ICATPN)

Lecture Notes in Computer Science 4546: 301-320, Springer, June 2007

## Data logics and automata

- S. Demri, R. Lazic and A. Sangnier

*Model checking memoryful linear-time logics over one-counter automata*

Theoretical Computer Science 411(22-24): 2298-2316, 2010 - S. Demri, R. Lazic and A. Sangnier

*Model checking freeze LTL over one-counter automata*

11th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS)

Lecture Notes in Computer Science 4962: 490-504, Springer, March 2008 - M. Jurdzinski and R. Lazic

*Alternating automata on data trees and XPath satisfiability*

Transactions on Computational Logic 12(3), 23 pages, ACM, 2011 - M. Jurdzinski and R. Lazic

*Alternation-free modal mu-calculus for data trees*

22nd Annual Symposium on Logic in Computer Science (LICS): 131-140

IEEE, July 2007 - R. Lazic

*Safety alternating automata on data words*

Transactions on Computational Logic 12(2), 23 pages, ACM, 2011 - R. Lazic

*Safely Freezing LTL*

26th Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS)

Lecture Notes in Computer Science 4337: 381-392, Springer, December 2006 - S. Demri and R. Lazic

*LTL with the Freeze Quantifier and Register Automata*

Transactions on Computational Logic 10(3), 30 pages, ACM, 2009 - S. Demri and R. Lazic

*LTL with the Freeze Quantifier and Register Automata*

21st Annual Symposium on Logic in Computer Science (LICS): 17-26 Talk

IEEE, August 2006 - S. Demri, R. Lazic and D. Nowak

*On the freeze quantifier in constraint LTL: decidability and complexity*

Information and Computation 205(1): 2-24, Elsevier, 2007 - S. Demri, R. Lazic and D. Nowak

*On the freeze quantifier in constraint LTL: decidability and complexity*

12th International Symposium on Temporal Representation and Reasoning (time): 113-121

IEEE, June 2005

## Verification and game semantics

- R. Lazic and A.S. Murawski

*Contextual approximation and higher-order procedures*

19th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS)

Lecture Notes in Computer Science 9634: 162-179, Springer, April 2016 - A.S. Dimovski and R. Lazic

*Assume-Guarantee Software Verification Based on Game Semantics*

8th International Conference on Formal Engineering Methods (ICFEM)

Lecture Notes in Computer Science 4260: 529-548, Springer, November 2006

Overview talk given at GaLoP '06 - A. Bakewell, A. Dimovski, D.R. Ghica and R. Lazic

*Data-Abstraction Refinement: A Game Semantic Approach*

International Journal on Software Tools for Technology Transfer (STTT) 12(5): 373-389, Springer, 2010

*Supercedes the SAS '05 and SPIN '06 papers* - A.S. Dimovski, D.R. Ghica and R. Lazic

*A Counterexample-Guided Refinement Tool for Open Procedural Programs*

13th International SPIN Workshop on Model Checking of Software (SPIN)

Lecture Notes in Computer Science 3925: 288-292, Springer, March 2006 - A.S. Dimovski, D.R. Ghica and R. Lazic

*Data-Abstraction Refinement: A Game Semantic Approach*

12th International Static Analysis Symposium (SAS)

Lecture Notes in Computer Science 3672: 102-117, Springer, September 2005 - A.S. Dimovski and R. Lazic

*Compositional Software Verification Based on Game Semantics and Process Algebra*

International Journal on Software Tools for Technology Transfer (STTT) 9(1): 37-51, Springer, 2007

*Supercedes the AVoCS '04 and ICFEM '04 papers* - A.S. Dimovski and R. Lazic

*Software Model Checking Based on Game Semantics and CSP*

4th International Workshop on Automated Verification of Critical Systems (AVoCS '04)

Electronic Notes in Theoretical Computer Science 128(6): 105-125, Elsevier, May 2005 - A.S. Dimovski and R. Lazic

*CSP Representation of Game Semantics for Second-order Idealized Algol*

6th International Conference on Formal Engineering Methods (ICFEM)

Lecture Notes in Computer Science 3308: 146-161, Springer, November 2004

## Probabilistic, timed and hybrid systems

- L. Clemente, S. Lasota, R. Lazic and F. Mazowiecki

*Binary reachability of timed-register pushdown automata and branching vector addition systems*

Transactions on Computational Logic 20(3): 31 pages, ACM, 2019 - L. Daviaud, M. Jurdzinski, R. Lazic, F. Mazowiecki, G.A. Perez, J. Worrell

*When is Containment Decidable for Probabilistic Automata?*

45th International Colloquium on Automata, Languages, and Programming (ICALP)

LIPIcs 107, 121:1-121:14, Schloss Dagstuhl, July 2018 - L. Clemente, S. Lasota, R. Lazic and F. Mazowiecki

*Timed pushdown automata and branching vector addition systems*

32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)

June 2017 - R. Lazic, J. Ouaknine and J. Worrell

*Zeno, Hercules, and the Hydra: Safety Metric Temporal Logic is ACKERMANN-Complete*

Transactions on Computational Logic 17(3): 27 pages, ACM, 2016 - R. Lazic, J. Ouaknine and J. Worrell

*Zeno, Hercules and the Hydra: Downward Rational Termination Is Ackermannian*

38th International Symposium on Mathematical Foundations of Computer Science (MFCS)

Lecture Notes in Computer Science 8087: 643-654, Springer, August 2013 - M. Rutkowski, R. Lazic and M. Jurdzinski

*Average-Price-per-Reward Games on Hybrid Automata with Strong Resets*

International Journal on Software Tools for Technology Transfer (STTT) 13(6): 553-569, Springer, 2011 - M. Jurdzinski, R. Lazic and M. Rutkowski

*Average-Price-per-Reward Games on Hybrid Automata with Strong Resets*

10th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI)

Lecture Notes in Computer Science 5403: 167-181, Springer, January 2009 - P. Bouyer, T. Brihaye, M. Jurdzinski, R. Lazic and M. Rutkowski

*Average-price and reachability-price games on hybrid automata with strong resets*

6th International Conference on Formal Modelling and Analysis of Timed Systems (FORMATS)

Lecture Notes in Computer Science 5215: 63-77, Springer, September 2008

## Polymorphic systems with arrays

- R. Lazic

*Decidability of Reachability for Polymorphic Systems with Arrays: A Complete Classification*

6th International Workshop on Verification of Infinite-State Systems (Infinity '04)

Electronic Notes in Theoretical Computer Science 138(3): 3-19, Elsevier, December 2005 - R. Lazic, T. Newcomb and A.W. Roscoe

*Polymorphic Systems with Arrays, 2-Counter Machines and Multiset Rewriting*

6th International Workshop on Verification of Infinite-State Systems (Infinity '04)

Electronic Notes in Theoretical Computer Science 138(3): 61-86, Elsevier, December 2005

Research report version: CS-RR-399 Talk - R. Lazic, T. Newcomb and A.W. Roscoe

*On model checking data-independent systems with arrays with whole-array operations*

Communicating Sequential Processes: The First 25 Years

Lecture Notes in Computer Science 3525: 275-291, Springer, July 2004

Research report version: CS-RR-395 - R.S. Lazic, T.C. Newcomb and A.W. Roscoe

*On model checking data-independent systems with arrays without reset*

Theory and Practice of Logic Programming (TPLP) 4 (5 & 6): 659-693, Cambridge University Press, 2004

Research report version: RR-02-02 - A.W. Roscoe and R.S. Lazic

*What can you decide about resetable arrays?*

2nd International Workshop on Verification and Computational Logic (VCL)

Technical Report DSSE-TR-2001-3: 5-23, September 2001 - R. Lazic and A.W. Roscoe

*Verifying determinism of concurrent systems which use unbounded arrays*

3rd International Workshop on Verification of Infinite State Systems (INFINITY '98)

Report TUM-I9825: 2-8, Technical University of Munich, July 1998

Research report version: PRG-TR-2-98

## Verification and process algebra

- X. Wang, A.W. Roscoe and R.S. Lazic

*Relating Data Independent Trace Checks in CSP with UNITY Reachability under a Normality Assumption*

4th International Conference on Integrated Formal Methods (IFM)

Lecture Notes in Computer Science 2999: 247-266, Springer, April 2004

Research report version: RR-03-08 - R. Lazic and D. Nowak

*On a Semantic Definition of Data Independence*

6th International Conference on Typed Lambda Calculi and Applications (TLCA)

Lecture Notes in Computer Science 2701: 226-240, Springer, June 2003

Research report version: CS-RR-392 - R. Lazic and D. Nowak

*A unifying approach to data-independence*

11th International Conference on Concurrency Theory (CONCUR)

Lecture Notes in Computer Science 1877: 581-595, Springer, August 2000

Research report version: PRG-TR-4-00 - R. Lazic and A.W. Roscoe

*Data independence with generalised predicate symbols*

International Conference on Parallel and Distributed Processing Techniques and Applications (PDPTA)

Volume I: 319-325, CSREA Press, June 1999 - R.S. Lazic

*A Semantic Study of Data Independence with Applications to Model Checking*

DPhil thesis, Oxford University Computing Laboratory, April 1999

## Set theory

- R.S. Lazic and A.W. Roscoe

*On transition systems and non-well-founded sets*

Papers on General Topology and Applications: 11th Summer Conference at the University of Southern Maine (August 1995)

Annals of the New York Academy of Sciences 806: 238-264, December 1996

**Copyright note:** The documents contained in these directories are included by the contributing authors as a means to ensure timely dissemination of scholarly and technical work on a non-commercial basis. Copyright and all rights therein are maintained by the authors or by other copyright holders, notwithstanding that they have offered their works here electronically. It is understood that all persons copying this information will adhere to the terms and constraints invoked by each author's copyright. These works may not be reposted without the explicit written permission of the copyright holder.