Search Results

Documents authored by Meyer, Roland

Document
Track B: Automata, Logic, Semantics, and Theory of Programming
DOI: 10.4230/LIPIcs.ICALP.2024.126
Separability in Büchi VASS and Singly Non-Linear Systems of Inequalities

Authors: Pascal Baumann, Eren Keskin, Roland Meyer, and Georg Zetzsche

Published in: LIPIcs, Volume 297, 51st International Colloquium on Automata, Languages, and Programming (ICALP 2024)

Abstract
The ω-regular separability problem for Büchi VASS coverability languages has recently been shown to be decidable, but with an EXPSPACE lower and a non-primitive recursive upper bound - the exact complexity remained open. We close this gap and show that the problem is EXPSPACE-complete. A careful analysis of our complexity bounds additionally yields a PSPACE procedure in the case of fixed dimension ≥ 1, which matches a pre-established lower bound of PSPACE for one dimensional Büchi VASS. Our algorithm is a non-deterministic search for a witness whose size, as we show, can be suitably bounded. Part of the procedure is to decide the existence of runs in VASS that satisfy certain non-linear properties. Therefore, a key technical ingredient is to analyze a class of systems of inequalities where one variable may occur in non-linear (polynomial) expressions. These so-called singly non-linear systems (SNLS) take the form A(x)⋅ y ≥ b(x), where A(x) and b(x) are a matrix resp. a vector whose entries are polynomials in x, and y ranges over vectors in the rationals. Our main contribution on SNLS is an exponential upper bound on the size of rational solutions to singly non-linear systems. The proof consists of three steps. First, we give a tailor-made quantifier elimination to characterize all real solutions to x. Second, using the root separation theorem about the distance of real roots of polynomials, we show that if a rational solution exists, then there is one with at most polynomially many bits. Third, we insert the solution for x into the SNLS, making it linear and allowing us to invoke standard solution bounds from convex geometry. Finally, we combine the results about SNLS with several techniques from the area of VASS to devise an EXPSPACE decision procedure for ω-regular separability of Büchi VASS.
Cite as

Pascal Baumann, Eren Keskin, Roland Meyer, and Georg Zetzsche. Separability in Büchi VASS and Singly Non-Linear Systems of Inequalities. In 51st International Colloquium on Automata, Languages, and Programming (ICALP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 297, pp. 126:1-126:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{baumann_et_al:LIPIcs.ICALP.2024.126,
  author =	{Baumann, Pascal and Keskin, Eren and Meyer, Roland and Zetzsche, Georg},
  title =	{{Separability in B\"{u}chi VASS and Singly Non-Linear Systems of Inequalities}},
  booktitle =	{51st International Colloquium on Automata, Languages, and Programming (ICALP 2024)},
  pages =	{126:1--126:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-322-5},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{297},
  editor =	{Bringmann, Karl and Grohe, Martin and Puppis, Gabriele and Svensson, Ola},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2024.126},
  URN =		{urn:nbn:de:0030-drops-202695},
  doi =		{10.4230/LIPIcs.ICALP.2024.126},
  annote =	{Keywords: Vector addition systems, infinite words, separability, inequalities, quantifier elimination, rational, polynomials}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2023.8
Separability and Non-Determinizability of WSTS

Authors: Eren Keskin and Roland Meyer

Published in: LIPIcs, Volume 279, 34th International Conference on Concurrency Theory (CONCUR 2023)

Abstract
There is a recent separability result for the languages of well-structured transition systems (WSTS) that is surprisingly general: disjoint WSTS languages are always separated by a regular language. The result assumes that one of the languages is accepted by a deterministic WSTS, and it is not known whether this assumption is needed. There are two ways to get rid of the assumption, none of which has led to conclusions so far: (i) show that WSTS can be determinized or (ii) generalize the separability result to non-deterministic WSTS languages. Our contribution is to show that (i) does not work but (ii) does. As for (i), we give a non-deterministic WSTS language that we prove cannot be accepted by a deterministic WSTS. The proof relies on a novel characterization of the languages accepted by deterministic WSTS. As for (ii), we show how to find finitely represented inductive invariants without having the tool of ideal decompositions at hand. Instead, we work with closures under converging sequences. Our results hold for upward- and downward-compatible WSTS.
Cite as

Eren Keskin and Roland Meyer. Separability and Non-Determinizability of WSTS. In 34th International Conference on Concurrency Theory (CONCUR 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 279, pp. 8:1-8:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@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}
}
Document
DOI: 10.4230/LIPIcs.STACS.2023.9
Regular Separability in Büchi VASS

Authors: Pascal Baumann, Roland Meyer, and Georg Zetzsche

Published in: LIPIcs, Volume 254, 40th International Symposium on Theoretical Aspects of Computer Science (STACS 2023)

Abstract
We study the (ω-)regular separability problem for Büchi VASS languages: Given two Büchi VASS with languages L₁ and L₂, check whether there is a regular language that fully contains L₁ while remaining disjoint from L₂. We show that the problem is decidable in general and PSPACE-complete in the 1-dimensional case, assuming succinct counter updates. The results rely on several arguments. We characterize the set of all regular languages disjoint from L₂. Based on this, we derive a (sound and complete) notion of inseparability witnesses, non-regular subsets of L₁. Finally, we show how to symbolically represent inseparability witnesses and how to check their existence.
Cite as

Pascal Baumann, Roland Meyer, and Georg Zetzsche. Regular Separability in Büchi VASS. In 40th International Symposium on Theoretical Aspects of Computer Science (STACS 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 254, pp. 9:1-9:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{baumann_et_al:LIPIcs.STACS.2023.9,
  author =	{Baumann, Pascal and Meyer, Roland and Zetzsche, Georg},
  title =	{{Regular Separability in B\"{u}chi VASS}},
  booktitle =	{40th International Symposium on Theoretical Aspects of Computer Science (STACS 2023)},
  pages =	{9:1--9:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-266-2},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{254},
  editor =	{Berenbrink, Petra and Bouyer, Patricia and Dawar, Anuj and Kant\'{e}, Mamadou Moustapha},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2023.9},
  URN =		{urn:nbn:de:0030-drops-176617},
  doi =		{10.4230/LIPIcs.STACS.2023.9},
  annote =	{Keywords: Separability problem, Vector addition systems, Infinite words, Decidability}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2020.52
On the Complexity of Multi-Pushdown Games

Authors: Roland Meyer and Sören van der Wall

Published in: LIPIcs, Volume 182, 40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020)

Abstract
We study the influence of parameters like the number of contexts, phases, and stacks on the complexity of solving parity games over concurrent recursive programs. Our first result shows that k-context games are b-EXPTIME-complete, where b = max{k-2, 1}. This means up to three contexts do not increase the complexity over an analysis for the sequential case. Our second result shows that for ordered k-stack as well as k-phase games the complexity jumps to k-EXPTIME-complete.
Cite as

Roland Meyer and Sören van der Wall. On the Complexity of Multi-Pushdown Games. In 40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 182, pp. 52:1-52:35, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{meyer_et_al:LIPIcs.FSTTCS.2020.52,
  author =	{Meyer, Roland and van der Wall, S\"{o}ren},
  title =	{{On the Complexity of Multi-Pushdown Games}},
  booktitle =	{40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020)},
  pages =	{52:1--52:35},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-174-0},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{182},
  editor =	{Saxena, Nitin and Simon, Sunil},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2020.52},
  URN =		{urn:nbn:de:0030-drops-132930},
  doi =		{10.4230/LIPIcs.FSTTCS.2020.52},
  annote =	{Keywords: concurrency, complexity, games, infinite state, multi-pushdown}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2019.37
Complexity of Liveness in Parameterized Systems

Authors: Peter Chini, Roland Meyer, and Prakash Saivasan

Published in: LIPIcs, Volume 150, 39th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2019)

Abstract
We investigate the fine-grained complexity of liveness verification for leader contributor systems. These consist of a designated leader thread and an arbitrary number of identical contributor threads communicating via a shared memory. The liveness verification problem asks whether there is an infinite computation of the system in which the leader reaches a final state infinitely often. Like its reachability counterpart, the problem is known to be NP-complete. Our results show that, even from a fine-grained point of view, the complexities differ only by a polynomial factor. Liveness verification decomposes into reachability and cycle detection. We present a fixed point iteration solving the latter in polynomial time. For reachability, we reconsider the two standard parameterizations. When parameterized by the number of states of the leader L and the size of the data domain D, we show an (L + D)^O(L + D)-time algorithm. It improves on a previous algorithm, thereby settling an open problem. When parameterized by the number of states of the contributor C, we reuse an O^*(2^C)-time algorithm. We show how to connect both algorithms with the cycle detection to obtain algorithms for liveness verification. The running times of the composed algorithms match those of reachability, proving that the fine-grained lower bounds for liveness verification are met.
Cite as

Peter Chini, Roland Meyer, and Prakash Saivasan. Complexity of Liveness in Parameterized Systems. In 39th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 150, pp. 37:1-37:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{chini_et_al:LIPIcs.FSTTCS.2019.37,
  author =	{Chini, Peter and Meyer, Roland and Saivasan, Prakash},
  title =	{{Complexity of Liveness in Parameterized Systems}},
  booktitle =	{39th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2019)},
  pages =	{37:1--37:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-131-3},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{150},
  editor =	{Chattopadhyay, Arkadev and Gastin, Paul},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2019.37},
  URN =		{urn:nbn:de:0030-drops-115993},
  doi =		{10.4230/LIPIcs.FSTTCS.2019.37},
  annote =	{Keywords: Liveness Verification, Fine-Grained Complexity, Parameterized Systems}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2018.12
Bounded Context Switching for Valence Systems

Authors: Roland Meyer, Sebastian Muskalla, and Georg Zetzsche

Published in: LIPIcs, Volume 118, 29th International Conference on Concurrency Theory (CONCUR 2018)

Abstract
We study valence systems, finite-control programs over infinite-state memories modeled in terms of graph monoids. Our contribution is a notion of bounded context switching (BCS). Valence systems generalize pushdowns, concurrent pushdowns, and Petri nets. In these settings, our definition conservatively generalizes existing notions. The main finding is that reachability within a bounded number of context switches is in NPTIME, independent of the memory (the graph monoid). Our proof is genuinely algebraic, and therefore contributes a new way to think about BCS. In addition, we exhibit a class of storage mechanisms for which BCS reachability belongs to PTIME.
Cite as

Roland Meyer, Sebastian Muskalla, and Georg Zetzsche. Bounded Context Switching for Valence Systems. In 29th International Conference on Concurrency Theory (CONCUR 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 118, pp. 12:1-12:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{meyer_et_al:LIPIcs.CONCUR.2018.12,
  author =	{Meyer, Roland and Muskalla, Sebastian and Zetzsche, Georg},
  title =	{{Bounded Context Switching for Valence Systems}},
  booktitle =	{29th International Conference on Concurrency Theory (CONCUR 2018)},
  pages =	{12:1--12:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-087-3},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{118},
  editor =	{Schewe, Sven and Zhang, Lijun},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2018.12},
  URN =		{urn:nbn:de:0030-drops-95500},
  doi =		{10.4230/LIPIcs.CONCUR.2018.12},
  annote =	{Keywords: valence systems, graph monoids, bounded context switching}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2018.35
Regular Separability of Well-Structured Transition Systems

Authors: Wojciech Czerwinski, Slawomir Lasota, Roland Meyer, Sebastian Muskalla, K. Narayan Kumar, and Prakash Saivasan

Published in: LIPIcs, Volume 118, 29th International Conference on Concurrency Theory (CONCUR 2018)

Abstract
We investigate the languages recognized by well-structured transition systems (WSTS) with upward and downward compatibility. Our first result shows that, under very mild assumptions, every two disjoint WSTS languages are regular separable: There is a regular language containing one of them and being disjoint from the other. As a consequence, if a language as well as its complement are both recognized by WSTS, then they are necessarily regular. In particular, no subclass of WSTS languages beyond the regular languages is closed under complement. Our second result shows that for Petri nets, the complexity of the backwards coverability algorithm yields a bound on the size of the regular separator. We complement it by a lower bound construction.
Cite as

Wojciech Czerwinski, Slawomir Lasota, Roland Meyer, Sebastian Muskalla, K. Narayan Kumar, and Prakash Saivasan. Regular Separability of Well-Structured Transition Systems. In 29th International Conference on Concurrency Theory (CONCUR 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 118, pp. 35:1-35:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{czerwinski_et_al:LIPIcs.CONCUR.2018.35,
  author =	{Czerwinski, Wojciech and Lasota, Slawomir and Meyer, Roland and Muskalla, Sebastian and Narayan Kumar, K. and Saivasan, Prakash},
  title =	{{Regular Separability of Well-Structured Transition Systems}},
  booktitle =	{29th International Conference on Concurrency Theory (CONCUR 2018)},
  pages =	{35:1--35:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-087-3},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{118},
  editor =	{Schewe, Sven and Zhang, Lijun},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2018.35},
  URN =		{urn:nbn:de:0030-drops-95733},
  doi =		{10.4230/LIPIcs.CONCUR.2018.35},
  annote =	{Keywords: regular separability, wsts, coverability languages, Petri nets}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2018.57
Parity to Safety in Polynomial Time for Pushdown and Collapsible Pushdown Systems

Authors: Matthew Hague, Roland Meyer, Sebastian Muskalla, and Martin Zimmermann

Published in: LIPIcs, Volume 117, 43rd International Symposium on Mathematical Foundations of Computer Science (MFCS 2018)

Abstract
We give a direct polynomial-time reduction from parity games played over the configuration graphs of collapsible pushdown systems to safety games played over the same class of graphs. That a polynomial-time reduction would exist was known since both problems are complete for the same complexity class. Coming up with a direct reduction, however, has been an open problem. Our solution to the puzzle brings together a number of techniques for pushdown games and adds three new ones. This work contributes to a recent trend of liveness to safety reductions which allow the advanced state-of-the-art in safety checking to be used for more expressive specifications.
Cite as

Matthew Hague, Roland Meyer, Sebastian Muskalla, and Martin Zimmermann. Parity to Safety in Polynomial Time for Pushdown and Collapsible Pushdown Systems. In 43rd International Symposium on Mathematical Foundations of Computer Science (MFCS 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 117, pp. 57:1-57:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{hague_et_al:LIPIcs.MFCS.2018.57,
  author =	{Hague, Matthew and Meyer, Roland and Muskalla, Sebastian and Zimmermann, Martin},
  title =	{{Parity to Safety in Polynomial Time for Pushdown and Collapsible Pushdown Systems}},
  booktitle =	{43rd International Symposium on Mathematical Foundations of Computer Science (MFCS 2018)},
  pages =	{57:1--57:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-086-6},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{117},
  editor =	{Potapov, Igor and Spirakis, Paul and Worrell, James},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2018.57},
  URN =		{urn:nbn:de:0030-drops-96396},
  doi =		{10.4230/LIPIcs.MFCS.2018.57},
  annote =	{Keywords: Parity Games, Safety Games, Pushdown Systems, Collapsible Pushdown Systems, Higher-Order Recursion Schemes, Model Checking}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2017.49
On the Upward/Downward Closures of Petri Nets

Authors: Mohamed Faouzi Atig, Roland Meyer, Sebastian Muskalla, and Prakash Saivasan

Published in: LIPIcs, Volume 83, 42nd International Symposium on Mathematical Foundations of Computer Science (MFCS 2017)

Abstract
We study the size and the complexity of computing finite state automata (FSA) representing and approximating the downward and the upward closure of Petri net languages with coverability as the acceptance condition. We show how to construct an FSA recognizing the upward closure of a Petri net language in doubly-exponential time, and therefore the size is at most doubly exponential. For downward closures, we prove that the size of the minimal automata can be non-primitive recursive. In the case of BPP nets, a well-known subclass of Petri nets, we show that an FSA accepting the downward/upward closure can be constructed in exponential time. Furthermore, we consider the problem of checking whether a simple regular language is included in the downward/upward closure of a Petri net/BPP net language. We show that this problem is EXPSPACE-complete (resp. NP-complete) in the case of Petri nets (resp. BPP nets). Finally, we show that it is decidable whether a Petri net language is upward/downward closed.
Cite as

Mohamed Faouzi Atig, Roland Meyer, Sebastian Muskalla, and Prakash Saivasan. On the Upward/Downward Closures of Petri Nets. In 42nd International Symposium on Mathematical Foundations of Computer Science (MFCS 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 83, pp. 49:1-49:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{atig_et_al:LIPIcs.MFCS.2017.49,
  author =	{Atig, Mohamed Faouzi and Meyer, Roland and Muskalla, Sebastian and Saivasan, Prakash},
  title =	{{On the Upward/Downward Closures of Petri Nets}},
  booktitle =	{42nd International Symposium on Mathematical Foundations of Computer Science (MFCS 2017)},
  pages =	{49:1--49:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-046-0},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{83},
  editor =	{Larsen, Kim G. and Bodlaender, Hans L. and Raskin, Jean-Francois},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2017.49},
  URN =		{urn:nbn:de:0030-drops-81278},
  doi =		{10.4230/LIPIcs.MFCS.2017.49},
  annote =	{Keywords: Petri nets, BPP nets, downward closure, upward closure}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2017.59
Domains for Higher-Order Games

Authors: Matthew Hague, Roland Meyer, and Sebastian Muskalla

Published in: LIPIcs, Volume 83, 42nd International Symposium on Mathematical Foundations of Computer Science (MFCS 2017)

Abstract
We study two-player inclusion games played over word-generating higher-order recursion schemes. While inclusion checks are known to capture verification problems, two-player games generalize this relationship to program synthesis. In such games, non-terminals of the grammar are controlled by opposing players. The goal of the existential player is to avoid producing a word that lies outside of a regular language of safe words. We contribute a new domain that provides a representation of the winning region of such games. Our domain is based on (functions over) potentially infinite Boolean formulas with words as atomic propositions. We develop an abstract interpretation framework that we instantiate to abstract this domain into a domain where the propositions are replaced by states of a finite automaton. This second domain is therefore finite and we obtain, via standard fixed-point techniques, a direct algorithm for the analysis of two-player inclusion games. We show, via a second instantiation of the framework, that our finite domain can be optimized, leading to a (k+1)EXP algorithm for order-k recursion schemes. We give a matching lower bound, showing that our approach is optimal. Since our approach is based on standard Kleene iteration, existing techniques and tools for fixed-point computations can be applied.
Cite as

Matthew Hague, Roland Meyer, and Sebastian Muskalla. Domains for Higher-Order Games. In 42nd International Symposium on Mathematical Foundations of Computer Science (MFCS 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 83, pp. 59:1-59:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{hague_et_al:LIPIcs.MFCS.2017.59,
  author =	{Hague, Matthew and Meyer, Roland and Muskalla, Sebastian},
  title =	{{Domains for Higher-Order Games}},
  booktitle =	{42nd International Symposium on Mathematical Foundations of Computer Science (MFCS 2017)},
  pages =	{59:1--59:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-046-0},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{83},
  editor =	{Larsen, Kim G. and Bodlaender, Hans L. and Raskin, Jean-Francois},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2017.59},
  URN =		{urn:nbn:de:0030-drops-81409},
  doi =		{10.4230/LIPIcs.MFCS.2017.59},
  annote =	{Keywords: higher-order recursion schemes, games, semantics, abstract interpretation, fixed points}
}
Document
Complete Volume
DOI: 10.4230/LIPIcs.CONCUR.2017
LIPIcs, Volume 85, CONCUR'17, Complete Volume

Authors: Roland Meyer and Uwe Nestmann

Published in: LIPIcs, Volume 85, 28th International Conference on Concurrency Theory (CONCUR 2017)

Abstract
LIPIcs, Volume 85, CONCUR'17, Complete Volume
Cite as

28th International Conference on Concurrency Theory (CONCUR 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 85, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@Proceedings{meyer_et_al:LIPIcs.CONCUR.2017,
  title =	{{LIPIcs, Volume 85, CONCUR'17, Complete Volume}},
  booktitle =	{28th International Conference on Concurrency Theory (CONCUR 2017)},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-048-4},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{85},
  editor =	{Meyer, Roland and Nestmann, Uwe},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2017},
  URN =		{urn:nbn:de:0030-drops-79070},
  doi =		{10.4230/LIPIcs.CONCUR.2017},
  annote =	{Keywords: Software, Data, Theory of Computation}
}
Document
Front Matter
DOI: 10.4230/LIPIcs.CONCUR.2017.0
Front Matter, Table of Contents, Preface, Conference Organization

Authors: Roland Meyer and Uwe Nestmann

Published in: LIPIcs, Volume 85, 28th International Conference on Concurrency Theory (CONCUR 2017)

Abstract
Front Matter, Table of Contents, Preface, Conference Organization
Cite as

28th International Conference on Concurrency Theory (CONCUR 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 85, pp. 0:i-0:xx, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{meyer_et_al:LIPIcs.CONCUR.2017.0,
  author =	{Meyer, Roland and Nestmann, Uwe},
  title =	{{Front Matter, Table of Contents, Preface, Conference Organization}},
  booktitle =	{28th International Conference on Concurrency Theory (CONCUR 2017)},
  pages =	{0:i--0:xx},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-048-4},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{85},
  editor =	{Meyer, Roland and Nestmann, Uwe},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2017.0},
  URN =		{urn:nbn:de:0030-drops-77693},
  doi =		{10.4230/LIPIcs.CONCUR.2017.0},
  annote =	{Keywords: Front Matter, Table of Contents, Preface, Conference Organization}
}
Document
DOI: 10.4230/LIPIcs.ESA.2017.27
On the Complexity of Bounded Context Switching

Authors: Peter Chini, Jonathan Kolberg, Andreas Krebs, Roland Meyer, and Prakash Saivasan

Published in: LIPIcs, Volume 87, 25th Annual European Symposium on Algorithms (ESA 2017)

Abstract
Bounded context switching (BCS) is an under-approximate method for finding violations to safety properties in shared-memory concurrent programs. Technically, BCS is a reachability problem that is known to be NP-complete. Our contribution is a parameterized analysis of BCS. The first result is an algorithm that solves BCS when parameterized by the number of context switches (cs) and the size of the memory (m) in O*(m^(cs)2^(cs)). This is achieved by creating instances of the easier problem Shuff which we solve via fast subset convolution. We also present a lower bound for BCS of the form m^o(cs / log(cs)), based on the exponential time hypothesis. Interestingly, the gap is closely related to a conjecture that has been open since FOCS'07. Further, we prove that BCS admits no polynomial kernel. Next, we introduce a measure, called scheduling dimension, that captures the complexity of schedules. We study BCS parameterized by the scheduling dimension (sdim) and show that it can be solved in O*((2m)^(4sdim)4^t), where t is the number of threads. We consider variants of the problem for which we obtain (matching) upper and lower bounds.
Cite as

Peter Chini, Jonathan Kolberg, Andreas Krebs, Roland Meyer, and Prakash Saivasan. On the Complexity of Bounded Context Switching. In 25th Annual European Symposium on Algorithms (ESA 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 87, pp. 27:1-27:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{chini_et_al:LIPIcs.ESA.2017.27,
  author =	{Chini, Peter and Kolberg, Jonathan and Krebs, Andreas and Meyer, Roland and Saivasan, Prakash},
  title =	{{On the Complexity of Bounded Context Switching}},
  booktitle =	{25th Annual European Symposium on Algorithms (ESA 2017)},
  pages =	{27:1--27:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-049-1},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{87},
  editor =	{Pruhs, Kirk and Sohler, Christian},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ESA.2017.27},
  URN =		{urn:nbn:de:0030-drops-78730},
  doi =		{10.4230/LIPIcs.ESA.2017.27},
  annote =	{Keywords: Shared memory concurrency, safety verification, fixed-parameter tractability, exponential time hypothesis, bounded context switching}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2016.41
Summaries for Context-Free Games

Authors: Lukás Holík, Roland Meyer, and Sebastian Muskalla

Published in: LIPIcs, Volume 65, 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016)

Abstract
We study two-player games played on the infinite graph of sentential forms induced by a context-free grammar (that comes with an ownership partitioning of the non-terminals). The winning condition is inclusion of the derived terminal word in the language of a finite automaton. Our contribution is a new algorithm to decide the winning player and to compute her strategy. It is based on a novel representation of all plays starting in a non-terminal. The representation uses the domain of Boolean formulas over the transition monoid of the target automaton. The elements of the monoid are essentially procedure summaries, and our approach can be seen as the first summary-based algorithm for the synthesis of recursive programs. We show that our algorithm has optimal (doubly exponential) time complexity, that it is compatible with recent antichain optimizations, and that it admits a lazy evaluation strategy. Our preliminary experiments indeed show encouraging results, indicating a speed up of three orders of magnitude over a competitor.
Cite as

Lukás Holík, Roland Meyer, and Sebastian Muskalla. Summaries for Context-Free Games. In 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 65, pp. 41:1-41:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{holik_et_al:LIPIcs.FSTTCS.2016.41,
  author =	{Hol{\'\i}k, Luk\'{a}s and Meyer, Roland and Muskalla, Sebastian},
  title =	{{Summaries for Context-Free Games}},
  booktitle =	{36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016)},
  pages =	{41:1--41:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-027-9},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{65},
  editor =	{Lal, Akash and Akshay, S. and Saurabh, Saket and Sen, Sandeep},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2016.41},
  URN =		{urn:nbn:de:0030-drops-68763},
  doi =		{10.4230/LIPIcs.FSTTCS.2016.41},
  annote =	{Keywords: summaries, context-free games, Kleene iteration, transition monoid, strategy synthesis}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2015.192
What's Decidable about Availability Languages?

Authors: Parosh Aziz Abdulla, Mohamed Faouzi Atig, Roland Meyer, and Mehdi Seyed Salehi

Published in: LIPIcs, Volume 45, 35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015)

Abstract
We study here the algorithmic analysis of systems modeled in terms of availability languages. Our first main result is a positive answer to the emptiness problem: it is decidable whether a given availability language contains a word. The key idea is an inductive construction that replaces availability languages with Parikh-equivalent regular languages. As a second contribution, we solve the intersection problem modulo bounded languages: given availability languages and a bounded language, it is decidable whether the intersection of the former contains a word from the bounded language. We show that the problem is NP-complete. The idea is to reduce to satisfiability of existential Presburger arithmetic. Since the (general) intersection problem for availability languages is known to be undecidable, our results characterize the decidability border for this model. Our last contribution is a study of the containment problem between regular and availability languages. We show that safety verification, i.e., checking containment of an availability language in a regular language, is decidable. The containment problem of regular languages in availability languages is proven undecidable.
Cite as

Parosh Aziz Abdulla, Mohamed Faouzi Atig, Roland Meyer, and Mehdi Seyed Salehi. What's Decidable about Availability Languages?. In 35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 45, pp. 192-205, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{abdulla_et_al:LIPIcs.FSTTCS.2015.192,
  author =	{Abdulla, Parosh Aziz and Atig, Mohamed Faouzi and Meyer, Roland and Seyed Salehi, Mehdi},
  title =	{{What's Decidable about Availability Languages?}},
  booktitle =	{35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015)},
  pages =	{192--205},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-97-2},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{45},
  editor =	{Harsha, Prahladh and Ramalingam, G.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2015.192},
  URN =		{urn:nbn:de:0030-drops-56602},
  doi =		{10.4230/LIPIcs.FSTTCS.2015.192},
  annote =	{Keywords: Availability, formal languages, emptiness, decidability}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2013.127
A Theory of Partitioned Global Address Spaces

Authors: Georgel Calin, Egor Derevenetc, Rupak Majumdar, and Roland Meyer

Published in: LIPIcs, Volume 24, IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2013)

Abstract
Partitioned global address space (PGAS) is a parallel programming model for the development of high-performance applications on clusters. It provides a global address space partitioned among the cluster nodes, and is supported in programming languages like C, C++, and Fortran by means of APIs. Our first contribution is a formal model for the semantics of single program, multiple data programs that use PGAS APIs. Our model reflects the main features of popular real-world APIs such as SHMEM, ARMCI, GASNet, GPI, and GASPI. A key feature of PGAS is the support for one-sided communication: a node may directly read and write the memory located at a remote node, without explicit synchronization with the processes running on the remote side. One-sided communication increases performance by decoupling process synchronization from data transfer, but requires the programmer to reason about appropriate synchronizations between reads and writes. As a second contribution, we propose and investigate robustness, a criterion for correct synchronization of PGAS programs. Robustness corresponds to acyclicity of a suitable happens-before relation defined on PGAS computations. The requirement is finer than classical data race freedom and rules out most false error reports. Our main technical result is an algorithm for checking robustness of PGAS programs. The algorithm makes use of two insights. We first show that, if a PGAS program is not robust, then there are computations in a certain normal form that violate happens-before acyclicity. Intuitively, normal-form computations delay remote accesses in an ordered way. We then devise an algorithm that checks for cyclic normal-form computations. Essentially, the algorithm is an emptiness check for a novel automaton model that accepts normal-form computations in streaming fashion. Altogether, we prove that the robustness problem is PSPACE complete.
Cite as

Georgel Calin, Egor Derevenetc, Rupak Majumdar, and Roland Meyer. A Theory of Partitioned Global Address Spaces. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 24, pp. 127-139, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)

Copy BibTex To Clipboard

@InProceedings{calin_et_al:LIPIcs.FSTTCS.2013.127,
  author =	{Calin, Georgel and Derevenetc, Egor and Majumdar, Rupak and Meyer, Roland},
  title =	{{A Theory of Partitioned Global Address Spaces}},
  booktitle =	{IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2013)},
  pages =	{127--139},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-64-4},
  ISSN =	{1868-8969},
  year =	{2013},
  volume =	{24},
  editor =	{Seth, Anil and Vishnoi, Nisheeth K.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2013.127},
  URN =		{urn:nbn:de:0030-drops-43665},
  doi =		{10.4230/LIPIcs.FSTTCS.2013.127},
  annote =	{Keywords: PGAS, SC preservation, Robustness, Semantics, Formal languages}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2011.140
Petri Net Reachability Graphs: Decidability Status of FO Properties

Authors: Philippe Darondeau, Stéphane Demri, Roland Meyer, and Christophe Morvan

Published in: LIPIcs, Volume 13, IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2011)

Abstract
We investigate the decidability and complexity status of model-checking problems on unlabelled reachability graphs of Petri nets by considering first-order, modal and pattern-based languages without labels on transitions or atomic propositions on markings. We consider several parameters to separate decidable problems from undecidable ones. Not only are we able to provide precise borders and a systematic analysis, but we also demonstrate the robustness of our proof techniques.
Cite as

Philippe Darondeau, Stéphane Demri, Roland Meyer, and Christophe Morvan. Petri Net Reachability Graphs: Decidability Status of FO Properties. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2011). Leibniz International Proceedings in Informatics (LIPIcs), Volume 13, pp. 140-151, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)

Copy BibTex To Clipboard

@InProceedings{darondeau_et_al:LIPIcs.FSTTCS.2011.140,
  author =	{Darondeau, Philippe and Demri, St\'{e}phane and Meyer, Roland and Morvan, Christophe},
  title =	{{Petri Net Reachability Graphs: Decidability Status of FO Properties}},
  booktitle =	{IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2011)},
  pages =	{140--151},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-34-7},
  ISSN =	{1868-8969},
  year =	{2011},
  volume =	{13},
  editor =	{Chakraborty, Supratik and Kumar, Amit},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2011.140},
  URN =		{urn:nbn:de:0030-drops-33563},
  doi =		{10.4230/LIPIcs.FSTTCS.2011.140},
  annote =	{Keywords: Petri nets, First order logic, Reachability graph}
}
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact