@Proceedings{perez_et_al:LIPIcs.CONCUR.2023, title = {{LIPIcs, Volume 279, CONCUR 2023, Complete Volume}}, booktitle = {34th International Conference on Concurrency Theory (CONCUR 2023)}, pages = {1--666}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-299-0}, ISSN = {1868-8969}, year = {2023}, volume = {279}, editor = {P\'{e}rez, Guillermo A. and Raskin, Jean-Fran\c{c}ois}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2023}, URN = {urn:nbn:de:0030-drops-189936}, doi = {10.4230/LIPIcs.CONCUR.2023}, annote = {Keywords: LIPIcs, Volume 279, CONCUR 2023, Complete Volume} } @InProceedings{perez_et_al:LIPIcs.CONCUR.2023.0, author = {P\'{e}rez, Guillermo A. and Raskin, Jean-Fran\c{c}ois}, title = {{Front Matter, Table of Contents, Preface, Conference Organization}}, booktitle = {34th International Conference on Concurrency Theory (CONCUR 2023)}, pages = {0:i--0:x}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-299-0}, ISSN = {1868-8969}, year = {2023}, volume = {279}, editor = {P\'{e}rez, Guillermo A. and Raskin, Jean-Fran\c{c}ois}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2023.0}, URN = {urn:nbn:de:0030-drops-189942}, doi = {10.4230/LIPIcs.CONCUR.2023.0}, annote = {Keywords: Front Matter, Table of Contents, Preface, Conference Organization} } @InProceedings{jonsson_et_al:LIPIcs.CONCUR.2023.1, author = {Jonsson, Bengt and Kwiatkowska, Marta and Walukiewicz, Igor}, title = {{CONCUR Test-Of-Time Award 2023}}, booktitle = {34th International Conference on Concurrency Theory (CONCUR 2023)}, pages = {1:1--1:2}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-299-0}, ISSN = {1868-8969}, year = {2023}, volume = {279}, editor = {P\'{e}rez, Guillermo A. and Raskin, Jean-Fran\c{c}ois}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2023.1}, URN = {urn:nbn:de:0030-drops-189953}, doi = {10.4230/LIPIcs.CONCUR.2023.1}, annote = {Keywords: CONCUR Test-of-Time Award} } @InProceedings{bouajjani:LIPIcs.CONCUR.2023.2, author = {Bouajjani, Ahmed}, title = {{On Verifying Concurrent Programs Under Weakly Consistent Models}}, booktitle = {34th International Conference on Concurrency Theory (CONCUR 2023)}, pages = {2:1--2:1}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-299-0}, ISSN = {1868-8969}, year = {2023}, volume = {279}, editor = {P\'{e}rez, Guillermo A. and Raskin, Jean-Fran\c{c}ois}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2023.2}, URN = {urn:nbn:de:0030-drops-189961}, doi = {10.4230/LIPIcs.CONCUR.2023.2}, annote = {Keywords: Concurrent programs, weakly consistent models} } @InProceedings{michaliszyn_et_al:LIPIcs.CONCUR.2023.3, author = {Michaliszyn, Jakub and Otop, Jan and Wieczorek, Piotr}, title = {{Reachability and Bounded Emptiness Problems of Constraint Automata with Prefix, Suffix and Infix}}, booktitle = {34th International Conference on Concurrency Theory (CONCUR 2023)}, pages = {3:1--3:16}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-299-0}, ISSN = {1868-8969}, year = {2023}, volume = {279}, editor = {P\'{e}rez, Guillermo A. and Raskin, Jean-Fran\c{c}ois}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2023.3}, URN = {urn:nbn:de:0030-drops-189971}, doi = {10.4230/LIPIcs.CONCUR.2023.3}, annote = {Keywords: constraint automata, emptiness problem} } @InProceedings{vanspaendonck_et_al:LIPIcs.CONCUR.2023.4, author = {van Spaendonck, P. H. M. and Willemse, Tim A. C.}, title = {{The Best of Both Worlds: Model-Driven Engineering Meets Model-Based Testing}}, booktitle = {34th International Conference on Concurrency Theory (CONCUR 2023)}, pages = {4:1--4:16}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-299-0}, ISSN = {1868-8969}, year = {2023}, volume = {279}, editor = {P\'{e}rez, Guillermo A. and Raskin, Jean-Fran\c{c}ois}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2023.4}, URN = {urn:nbn:de:0030-drops-189988}, doi = {10.4230/LIPIcs.CONCUR.2023.4}, annote = {Keywords: stable-failures refinement, Model-Driven Engineering, input output conformance, Input Output Labelled Transition Systems, internal choice} } @InProceedings{spronck_et_al:LIPIcs.CONCUR.2023.5, author = {Spronck, Myrthe S. C. and Luttik, Bas}, title = {{Process-Algebraic Models of Multi-Writer Multi-Reader Non-Atomic Registers}}, booktitle = {34th International Conference on Concurrency Theory (CONCUR 2023)}, pages = {5:1--5:17}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-299-0}, ISSN = {1868-8969}, year = {2023}, volume = {279}, editor = {P\'{e}rez, Guillermo A. and Raskin, Jean-Fran\c{c}ois}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2023.5}, URN = {urn:nbn:de:0030-drops-189995}, doi = {10.4230/LIPIcs.CONCUR.2023.5}, annote = {Keywords: mutual exclusion, model checking, non-atomic reads and writes, regular register} } @InProceedings{guttenberg_et_al:LIPIcs.CONCUR.2023.6, author = {Guttenberg, Roland and Raskin, Mikhail and Esparza, Javier}, title = {{Geometry of Reachability Sets of Vector Addition Systems}}, booktitle = {34th International Conference on Concurrency Theory (CONCUR 2023)}, pages = {6:1--6:16}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-299-0}, ISSN = {1868-8969}, year = {2023}, volume = {279}, editor = {P\'{e}rez, Guillermo A. and Raskin, Jean-Fran\c{c}ois}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2023.6}, URN = {urn:nbn:de:0030-drops-190005}, doi = {10.4230/LIPIcs.CONCUR.2023.6}, annote = {Keywords: Vector Addition System, Petri net, Reachability Set, Almost hybridlinear, Partition, Geometry} } @InProceedings{guillou_et_al:LIPIcs.CONCUR.2023.7, author = {Guillou, Lucie and Sangnier, Arnaud and Sznajder, Nathalie}, title = {{Safety Analysis of Parameterised Networks with Non-Blocking Rendez-Vous}}, booktitle = {34th International Conference on Concurrency Theory (CONCUR 2023)}, pages = {7:1--7:17}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-299-0}, ISSN = {1868-8969}, year = {2023}, volume = {279}, editor = {P\'{e}rez, Guillermo A. and Raskin, Jean-Fran\c{c}ois}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2023.7}, URN = {urn:nbn:de:0030-drops-190015}, doi = {10.4230/LIPIcs.CONCUR.2023.7}, annote = {Keywords: Parameterised verification, Coverability, Counter machines} } @InProceedings{keskin_et_al:LIPIcs.CONCUR.2023.8, author = {Keskin, Eren and Meyer, Roland}, title = {{Separability and Non-Determinizability of WSTS}}, booktitle = {34th International Conference on Concurrency Theory (CONCUR 2023)}, pages = {8:1--8:17}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-299-0}, ISSN = {1868-8969}, year = {2023}, volume = {279}, editor = {P\'{e}rez, Guillermo A. and Raskin, Jean-Fran\c{c}ois}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2023.8}, URN = {urn:nbn:de:0030-drops-190025}, doi = {10.4230/LIPIcs.CONCUR.2023.8}, annote = {Keywords: WSTS, regular separability, determinization} } @InProceedings{klvstad_et_al:LIPIcs.CONCUR.2023.9, author = {Kl{\o}vstad, \r{A}smund Aqissiaq Arild and Kamburjan, Eduard and Johnsen, Einar Broch}, title = {{Compositional Correctness and Completeness for Symbolic Partial Order Reduction}}, booktitle = {34th International Conference on Concurrency Theory (CONCUR 2023)}, pages = {9:1--9:16}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-299-0}, ISSN = {1868-8969}, year = {2023}, volume = {279}, editor = {P\'{e}rez, Guillermo A. and Raskin, Jean-Fran\c{c}ois}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2023.9}, URN = {urn:nbn:de:0030-drops-190035}, doi = {10.4230/LIPIcs.CONCUR.2023.9}, annote = {Keywords: Symbolic Execution, Coq, Trace Semantics, Partial Order Reduction} } @InProceedings{baumann_et_al:LIPIcs.CONCUR.2023.10, author = {Baumann, Pascal and Madnani, Khushraj and Mazowiecki, Filip and Zetzsche, Georg}, title = {{Monus Semantics in Vector Addition Systems with States}}, booktitle = {34th International Conference on Concurrency Theory (CONCUR 2023)}, pages = {10:1--10:18}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-299-0}, ISSN = {1868-8969}, year = {2023}, volume = {279}, editor = {P\'{e}rez, Guillermo A. and Raskin, Jean-Fran\c{c}ois}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2023.10}, URN = {urn:nbn:de:0030-drops-190047}, doi = {10.4230/LIPIcs.CONCUR.2023.10}, annote = {Keywords: Vector addition systems, Overapproximation, Reachability, Coverability} } @InProceedings{silva_et_al:LIPIcs.CONCUR.2023.11, author = {Silva, Gil and Mordido, Andreia and Vasconcelos, Vasco T.}, title = {{Subtyping Context-Free Session Types}}, booktitle = {34th International Conference on Concurrency Theory (CONCUR 2023)}, pages = {11:1--11:19}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-299-0}, ISSN = {1868-8969}, year = {2023}, volume = {279}, editor = {P\'{e}rez, Guillermo A. and Raskin, Jean-Fran\c{c}ois}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2023.11}, URN = {urn:nbn:de:0030-drops-190055}, doi = {10.4230/LIPIcs.CONCUR.2023.11}, annote = {Keywords: Session types, Subtyping, Simulation, Simple grammars, Non-regular recursion} } @InProceedings{ajdarow_et_al:LIPIcs.CONCUR.2023.12, author = {Ajdar\'{o}w, Michal and Ku\v{c}era, Anton{\'\i}n}, title = {{Asymptotic Complexity Estimates for Probabilistic Programs and Their VASS Abstractions}}, booktitle = {34th International Conference on Concurrency Theory (CONCUR 2023)}, pages = {12:1--12:16}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-299-0}, ISSN = {1868-8969}, year = {2023}, volume = {279}, editor = {P\'{e}rez, Guillermo A. and Raskin, Jean-Fran\c{c}ois}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2023.12}, URN = {urn:nbn:de:0030-drops-190065}, doi = {10.4230/LIPIcs.CONCUR.2023.12}, annote = {Keywords: Probabilistic programs, asymptotic complexity, vector addition systems} } @InProceedings{haase_et_al:LIPIcs.CONCUR.2023.13, author = {Haase, Christoph and Pi\'{o}rkowski, Rados{\l}aw}, title = {{Universal Quantification Makes Automatic Structures Hard to Decide}}, booktitle = {34th International Conference on Concurrency Theory (CONCUR 2023)}, pages = {13:1--13:17}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-299-0}, ISSN = {1868-8969}, year = {2023}, volume = {279}, editor = {P\'{e}rez, Guillermo A. and Raskin, Jean-Fran\c{c}ois}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2023.13}, URN = {urn:nbn:de:0030-drops-190075}, doi = {10.4230/LIPIcs.CONCUR.2023.13}, annote = {Keywords: automatic structures, universal projection, state complexity, tiling problems} } @InProceedings{finkel_et_al:LIPIcs.CONCUR.2023.14, author = {Finkel, Alain and Haddad, Serge and Ye, Lina}, title = {{About Decisiveness of Dynamic Probabilistic Models}}, booktitle = {34th International Conference on Concurrency Theory (CONCUR 2023)}, pages = {14:1--14:17}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-299-0}, ISSN = {1868-8969}, year = {2023}, volume = {279}, editor = {P\'{e}rez, Guillermo A. and Raskin, Jean-Fran\c{c}ois}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2023.14}, URN = {urn:nbn:de:0030-drops-190089}, doi = {10.4230/LIPIcs.CONCUR.2023.14}, annote = {Keywords: infinite Markov chain, reachability probability, decisiveness} } @InProceedings{schmitt_et_al:LIPIcs.CONCUR.2023.15, author = {Schmitt, Anna and Peters, Kirstin}, title = {{Probabilistic Operational Correspondence}}, booktitle = {34th International Conference on Concurrency Theory (CONCUR 2023)}, pages = {15:1--15:17}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-299-0}, ISSN = {1868-8969}, year = {2023}, volume = {279}, editor = {P\'{e}rez, Guillermo A. and Raskin, Jean-Fran\c{c}ois}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2023.15}, URN = {urn:nbn:de:0030-drops-190090}, doi = {10.4230/LIPIcs.CONCUR.2023.15}, annote = {Keywords: Probabilistic Process Calculi, Encodings, Operational Correspondence} } @InProceedings{avni_et_al:LIPIcs.CONCUR.2023.16, author = {Avni, Guy and Ghorpade, Pranav and Guha, Shibashis}, title = {{A Game of Pawns}}, booktitle = {34th International Conference on Concurrency Theory (CONCUR 2023)}, pages = {16:1--16:17}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-299-0}, ISSN = {1868-8969}, year = {2023}, volume = {279}, editor = {P\'{e}rez, Guillermo A. and Raskin, Jean-Fran\c{c}ois}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2023.16}, URN = {urn:nbn:de:0030-drops-190100}, doi = {10.4230/LIPIcs.CONCUR.2023.16}, annote = {Keywords: Graph games, Reachability games, Pawn games, Dynamic vertex control} } @InProceedings{boker_et_al:LIPIcs.CONCUR.2023.17, author = {Boker, Udi and Henzinger, Thomas A. and Mazzocchi, Nicolas and Sara\c{c}, N. Ege}, title = {{Safety and Liveness of Quantitative Automata}}, booktitle = {34th International Conference on Concurrency Theory (CONCUR 2023)}, pages = {17:1--17:18}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-299-0}, ISSN = {1868-8969}, year = {2023}, volume = {279}, editor = {P\'{e}rez, Guillermo A. and Raskin, Jean-Fran\c{c}ois}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2023.17}, URN = {urn:nbn:de:0030-drops-190118}, doi = {10.4230/LIPIcs.CONCUR.2023.17}, annote = {Keywords: quantitative safety, quantitative liveness, quantitative automata} } @InProceedings{bose_et_al:LIPIcs.CONCUR.2023.18, author = {Bose, Sougata and Purser, David and Totzke, Patrick}, title = {{History-Deterministic Vector Addition Systems}}, booktitle = {34th International Conference on Concurrency Theory (CONCUR 2023)}, pages = {18:1--18:17}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-299-0}, ISSN = {1868-8969}, year = {2023}, volume = {279}, editor = {P\'{e}rez, Guillermo A. and Raskin, Jean-Fran\c{c}ois}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2023.18}, URN = {urn:nbn:de:0030-drops-190120}, doi = {10.4230/LIPIcs.CONCUR.2023.18}, annote = {Keywords: Vector Addition Systems, History-determinism, Good-for Games} } @InProceedings{kupferman_et_al:LIPIcs.CONCUR.2023.19, author = {Kupferman, Orna and Shenwald, Noam}, title = {{Games with Trading of Control}}, booktitle = {34th International Conference on Concurrency Theory (CONCUR 2023)}, pages = {19:1--19:17}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-299-0}, ISSN = {1868-8969}, year = {2023}, volume = {279}, editor = {P\'{e}rez, Guillermo A. and Raskin, Jean-Fran\c{c}ois}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2023.19}, URN = {urn:nbn:de:0030-drops-190137}, doi = {10.4230/LIPIcs.CONCUR.2023.19}, annote = {Keywords: Parity Games, Rational Synthesis, Game Theory, Auctions} } @InProceedings{iosif_et_al:LIPIcs.CONCUR.2023.20, author = {Iosif, Radu and Zuleger, Florian}, title = {{Expressiveness Results for an Inductive Logic of Separated Relations}}, booktitle = {34th International Conference on Concurrency Theory (CONCUR 2023)}, pages = {20:1--20:20}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-299-0}, ISSN = {1868-8969}, year = {2023}, volume = {279}, editor = {P\'{e}rez, Guillermo A. and Raskin, Jean-Fran\c{c}ois}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2023.20}, URN = {urn:nbn:de:0030-drops-190146}, doi = {10.4230/LIPIcs.CONCUR.2023.20}, annote = {Keywords: Separation Logic, Model Theory, Monadic Second Order Logic, Treewidth} } @InProceedings{bartocci_et_al:LIPIcs.CONCUR.2023.21, author = {Bartocci, Ezio and Henzinger, Thomas A. and Nickovic, Dejan and Oliveira da Costa, Ana}, title = {{Hypernode Automata}}, booktitle = {34th International Conference on Concurrency Theory (CONCUR 2023)}, pages = {21:1--21:16}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-299-0}, ISSN = {1868-8969}, year = {2023}, volume = {279}, editor = {P\'{e}rez, Guillermo A. and Raskin, Jean-Fran\c{c}ois}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2023.21}, URN = {urn:nbn:de:0030-drops-190153}, doi = {10.4230/LIPIcs.CONCUR.2023.21}, annote = {Keywords: Hyperproperties, Asynchronous, Automata, Logic} } @InProceedings{abate_et_al:LIPIcs.CONCUR.2023.22, author = {Abate, Alessandro and Edwards, Alec and Giacobbe, Mirco and Punchihewa, Hashan and Roy, Diptarko}, title = {{Quantitative Verification with Neural Networks}}, booktitle = {34th International Conference on Concurrency Theory (CONCUR 2023)}, pages = {22:1--22:18}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-299-0}, ISSN = {1868-8969}, year = {2023}, volume = {279}, editor = {P\'{e}rez, Guillermo A. and Raskin, Jean-Fran\c{c}ois}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2023.22}, URN = {urn:nbn:de:0030-drops-190162}, doi = {10.4230/LIPIcs.CONCUR.2023.22}, annote = {Keywords: Data-driven Verification, Quantitative Verification, Probabilistic Programs, Stochastic Dynamical Models, Counterexample-guided Inductive Synthesis, Neural Networks} } @InProceedings{krishna_et_al:LIPIcs.CONCUR.2023.23, author = {Krishna, Shankara Narayanan and Madnani, Khushraj Nanik and Majumdar, Rupak and Pandya, Paritosh}, title = {{Satisfiability Checking of Multi-Variable TPTL with Unilateral Intervals Is PSPACE-Complete}}, booktitle = {34th International Conference on Concurrency Theory (CONCUR 2023)}, pages = {23:1--23:18}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-299-0}, ISSN = {1868-8969}, year = {2023}, volume = {279}, editor = {P\'{e}rez, Guillermo A. and Raskin, Jean-Fran\c{c}ois}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2023.23}, URN = {urn:nbn:de:0030-drops-190171}, doi = {10.4230/LIPIcs.CONCUR.2023.23}, annote = {Keywords: TPTL, Satisfiability, Non-Punctuality, Decidability, Expressiveness, ATA} } @InProceedings{mascle_et_al:LIPIcs.CONCUR.2023.24, 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 = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-299-0}, ISSN = {1868-8969}, year = {2023}, volume = {279}, editor = {P\'{e}rez, Guillermo A. and Raskin, Jean-Fran\c{c}ois}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2023.24}, URN = {urn:nbn:de:0030-drops-190184}, doi = {10.4230/LIPIcs.CONCUR.2023.24}, annote = {Keywords: Parametric systems, Locks, Model-checking} } @InProceedings{raad_et_al:LIPIcs.CONCUR.2023.25, author = {Raad, Azalea and Vanegue, Julien and Berdine, Josh and O'Hearn, Peter}, title = {{A General Approach to Under-Approximate Reasoning About Concurrent Programs}}, booktitle = {34th International Conference on Concurrency Theory (CONCUR 2023)}, pages = {25:1--25:17}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-299-0}, ISSN = {1868-8969}, year = {2023}, volume = {279}, editor = {P\'{e}rez, Guillermo A. and Raskin, Jean-Fran\c{c}ois}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2023.25}, URN = {urn:nbn:de:0030-drops-190195}, doi = {10.4230/LIPIcs.CONCUR.2023.25}, annote = {Keywords: Under-approximate reasoning, incorrectness logic, bug detection, software exploits, separation logic} } @InProceedings{isac_et_al:LIPIcs.CONCUR.2023.26, author = {Isac, Omri and Zohar, Yoni and Barrett, Clark and Katz, Guy}, title = {{DNN Verification, Reachability, and the Exponential Function Problem}}, booktitle = {34th International Conference on Concurrency Theory (CONCUR 2023)}, pages = {26:1--26:18}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-299-0}, ISSN = {1868-8969}, year = {2023}, volume = {279}, editor = {P\'{e}rez, Guillermo A. and Raskin, Jean-Fran\c{c}ois}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2023.26}, URN = {urn:nbn:de:0030-drops-190205}, doi = {10.4230/LIPIcs.CONCUR.2023.26}, annote = {Keywords: Formal Verification, Computability Theory, Deep Neural Networks} } @InProceedings{attiya_et_al:LIPIcs.CONCUR.2023.27, author = {Attiya, Hagit and Enea, Constantin and Nassar, Shafik}, title = {{Faithful Simulation of Randomized BFT Protocols on Block DAGs}}, booktitle = {34th International Conference on Concurrency Theory (CONCUR 2023)}, pages = {27:1--27:17}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-299-0}, ISSN = {1868-8969}, year = {2023}, volume = {279}, editor = {P\'{e}rez, Guillermo A. and Raskin, Jean-Fran\c{c}ois}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2023.27}, URN = {urn:nbn:de:0030-drops-190210}, doi = {10.4230/LIPIcs.CONCUR.2023.27}, annote = {Keywords: Byzantine failures, Hyperproperties, Forward Simulation} } @InProceedings{groote_et_al:LIPIcs.CONCUR.2023.28, author = {Groote, Jan Friso and Willemse, Tim A. C.}, title = {{Real Equation Systems with Alternating Fixed-Points}}, booktitle = {34th International Conference on Concurrency Theory (CONCUR 2023)}, pages = {28:1--28:17}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-299-0}, ISSN = {1868-8969}, year = {2023}, volume = {279}, editor = {P\'{e}rez, Guillermo A. and Raskin, Jean-Fran\c{c}ois}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2023.28}, URN = {urn:nbn:de:0030-drops-190225}, doi = {10.4230/LIPIcs.CONCUR.2023.28}, annote = {Keywords: Real Equation System, Solution method, Gau{\ss}-elimination, Model checking, Quantitative modal mu-calculus} } @InProceedings{demri_et_al:LIPIcs.CONCUR.2023.29, author = {Demri, St\'{e}phane and Quaas, Karin}, title = {{Constraint Automata on Infinite Data Trees: from CTL(\mathbb{Z})/CTL^*(\mathbb{Z}) to Decision Procedures}}, booktitle = {34th International Conference on Concurrency Theory (CONCUR 2023)}, pages = {29:1--29:18}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-299-0}, ISSN = {1868-8969}, year = {2023}, volume = {279}, editor = {P\'{e}rez, Guillermo A. and Raskin, Jean-Fran\c{c}ois}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2023.29}, URN = {urn:nbn:de:0030-drops-190238}, doi = {10.4230/LIPIcs.CONCUR.2023.29}, annote = {Keywords: Constraints, Constraint Automata, Temporal Logics, Infinite Data Trees} } @InProceedings{dominguez_et_al:LIPIcs.CONCUR.2023.30, author = {Dom{\'\i}nguez, Jes\'{u}s and Nanevski, Aleksandar}, title = {{Visibility and Separability for a Declarative Linearizability Proof of the Timestamped Stack}}, booktitle = {34th International Conference on Concurrency Theory (CONCUR 2023)}, pages = {30:1--30:16}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-299-0}, ISSN = {1868-8969}, year = {2023}, volume = {279}, editor = {P\'{e}rez, Guillermo A. and Raskin, Jean-Fran\c{c}ois}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2023.30}, URN = {urn:nbn:de:0030-drops-190245}, doi = {10.4230/LIPIcs.CONCUR.2023.30}, annote = {Keywords: Linearizability, Visibility Relations, Timestamped Stack} } @InProceedings{erlich_et_al:LIPIcs.CONCUR.2023.31, author = {Erlich, Enzo and Guha, Shibashis and Jecker, Isma\"{e}l and Lehtinen, Karoliina and Zimmermann, Martin}, title = {{History-Deterministic Parikh Automata}}, booktitle = {34th International Conference on Concurrency Theory (CONCUR 2023)}, pages = {31:1--31:16}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-299-0}, ISSN = {1868-8969}, year = {2023}, volume = {279}, editor = {P\'{e}rez, Guillermo A. and Raskin, Jean-Fran\c{c}ois}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2023.31}, URN = {urn:nbn:de:0030-drops-190250}, doi = {10.4230/LIPIcs.CONCUR.2023.31}, annote = {Keywords: Parikh automata, History-determinism, Reversal-bounded Counter Machines} } @InProceedings{martens_et_al:LIPIcs.CONCUR.2023.32, author = {Martens, Jan and Groote, Jan Friso}, title = {{Computing Minimal Distinguishing Hennessy-Milner Formulas is NP-Hard, but Variants are Tractable}}, booktitle = {34th International Conference on Concurrency Theory (CONCUR 2023)}, pages = {32:1--32:17}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-299-0}, ISSN = {1868-8969}, year = {2023}, volume = {279}, editor = {P\'{e}rez, Guillermo A. and Raskin, Jean-Fran\c{c}ois}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2023.32}, URN = {urn:nbn:de:0030-drops-190268}, doi = {10.4230/LIPIcs.CONCUR.2023.32}, annote = {Keywords: Distinguishing behaviour, Hennessy-Milner logic, NP-hardness} } @InProceedings{bertrand_et_al:LIPIcs.CONCUR.2023.33, author = {Bertrand, Cl\'{e}ment and Di Giusto, Cinzia and Klaudel, Hanna and Regnault, Damien}, title = {{Complexity of Membership and Non-Emptiness Problems in Unbounded Memory Automata}}, booktitle = {34th International Conference on Concurrency Theory (CONCUR 2023)}, pages = {33:1--33:17}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-299-0}, ISSN = {1868-8969}, year = {2023}, volume = {279}, editor = {P\'{e}rez, Guillermo A. and Raskin, Jean-Fran\c{c}ois}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2023.33}, URN = {urn:nbn:de:0030-drops-190277}, doi = {10.4230/LIPIcs.CONCUR.2023.33}, annote = {Keywords: memory automata, \nu-automata, LaMA, HRA, complexity, non-emptiness, membership} } @InProceedings{liu_et_al:LIPIcs.CONCUR.2023.34, author = {Liu, Tiange and Tiu, Alwen and de Groot, Jim}, title = {{Modal Logics for Mobile Processes Revisited}}, booktitle = {34th International Conference on Concurrency Theory (CONCUR 2023)}, pages = {34:1--34:17}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-299-0}, ISSN = {1868-8969}, year = {2023}, volume = {279}, editor = {P\'{e}rez, Guillermo A. and Raskin, Jean-Fran\c{c}ois}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2023.34}, URN = {urn:nbn:de:0030-drops-190289}, doi = {10.4230/LIPIcs.CONCUR.2023.34}, annote = {Keywords: pi-calculus, modal logic, intuitionistic logic, bisimilarity} } @InProceedings{schewe_et_al:LIPIcs.CONCUR.2023.35, author = {Schewe, Sven and Tang, Qiyi and Zhanabekova, Tansholpan}, title = {{Deciding What Is Good-For-MDPs}}, booktitle = {34th International Conference on Concurrency Theory (CONCUR 2023)}, pages = {35:1--35:16}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-299-0}, ISSN = {1868-8969}, year = {2023}, volume = {279}, editor = {P\'{e}rez, Guillermo A. and Raskin, Jean-Fran\c{c}ois}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2023.35}, URN = {urn:nbn:de:0030-drops-190290}, doi = {10.4230/LIPIcs.CONCUR.2023.35}, annote = {Keywords: B\"{u}chi automata, Markov Decision Processes, Omega-regular objectives, Reinforcement learning} } @InProceedings{jancar_et_al:LIPIcs.CONCUR.2023.36, author = {Jan\v{c}ar, Petr and Leroux, J\'{e}r\^{o}me}, title = {{The Semilinear Home-Space Problem Is Ackermann-Complete for Petri Nets}}, booktitle = {34th International Conference on Concurrency Theory (CONCUR 2023)}, pages = {36:1--36:17}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-299-0}, ISSN = {1868-8969}, year = {2023}, volume = {279}, editor = {P\'{e}rez, Guillermo A. and Raskin, Jean-Fran\c{c}ois}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2023.36}, URN = {urn:nbn:de:0030-drops-190300}, doi = {10.4230/LIPIcs.CONCUR.2023.36}, annote = {Keywords: Petri nets, home-space property, semilinear sets, Ackermannian complexity} } @InProceedings{li_et_al:LIPIcs.CONCUR.2023.37, author = {Li, Yong and Schewe, Sven and Vardi, Moshe Y.}, title = {{Singly Exponential Translation of Alternating Weak B\"{u}chi Automata to Unambiguous B\"{u}chi Automata}}, booktitle = {34th International Conference on Concurrency Theory (CONCUR 2023)}, pages = {37:1--37:17}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-299-0}, ISSN = {1868-8969}, year = {2023}, volume = {279}, editor = {P\'{e}rez, Guillermo A. and Raskin, Jean-Fran\c{c}ois}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2023.37}, URN = {urn:nbn:de:0030-drops-190313}, doi = {10.4230/LIPIcs.CONCUR.2023.37}, annote = {Keywords: B\"{u}chi automata, unambiguous automata, alternation, weak, disambiguation} } @InProceedings{dallago_et_al:LIPIcs.CONCUR.2023.38, author = {Dal Lago, Ugo and Murgia, Maurizio}, title = {{Contextual Behavioural Metrics}}, booktitle = {34th International Conference on Concurrency Theory (CONCUR 2023)}, pages = {38:1--38:17}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-299-0}, ISSN = {1868-8969}, year = {2023}, volume = {279}, editor = {P\'{e}rez, Guillermo A. and Raskin, Jean-Fran\c{c}ois}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2023.38}, URN = {urn:nbn:de:0030-drops-190320}, doi = {10.4230/LIPIcs.CONCUR.2023.38}, annote = {Keywords: Behavioural metrics, Labelled Transition Systems, Differential Semantics} } @InProceedings{anand_et_al:LIPIcs.CONCUR.2023.39, author = {Anand, Ashwani and Zetzsche, Georg}, title = {{Priority Downward Closures}}, booktitle = {34th International Conference on Concurrency Theory (CONCUR 2023)}, pages = {39:1--39:18}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-299-0}, ISSN = {1868-8969}, year = {2023}, volume = {279}, editor = {P\'{e}rez, Guillermo A. and Raskin, Jean-Fran\c{c}ois}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2023.39}, URN = {urn:nbn:de:0030-drops-190339}, doi = {10.4230/LIPIcs.CONCUR.2023.39}, annote = {Keywords: downward closure, priority order, pushdown automata, non-deterministic finite automata, abstraction, computability} }