Stefan Göller

SODA Conference 2023 Conference Paper

Weak Bisimulation Finiteness of Pushdown Systems With Deterministic ε-Transitions Is 2-EXPTIME-Complete

• Stefan Göller
• Pawel Parys

CSL Conference 2016 Conference Paper

On the Parallel Complexity of Bisimulation on Finite Systems

• Moses Ganardi
• Stefan Göller
• Markus Lohrey

In this paper the computational complexity of the (bi)simulation problem over restricted graph classes is studied. For trees given as pointer structures or terms the (bi)simulation problem is complete for logarithmic space or NC^1, respectively. This solves an open problem from Balcázar, Gabarró, and Sántha. We also show that the simulation problem is P-complete even for graphs of bounded path-width.

Highlights Conference 2013 Conference Abstract

Bisimilarity of pushdown automata is nonelementary

• Michael Benedikt
• Stefan Göller
• Stefan Kiefer
• Andrzej Murawski

Given two pushdown systems, the bisimilarity problem asks whether they are bisimilar. While this problem is known to be decidable our main result states that it is nonelementary, improving EXPTIME-hardness, which was the previously best known lower bound for this problem. Our lower bound result holds for normed pushdown systems as well.

Highlights Conference 2013 Conference Abstract

Equivalence of deterministic one-counter automata is NL-complete

• Stanislav Böhm
• Stefan Göller
• Petr Jančar

We prove that language equivalence of deterministic one- counter automata is NL-complete. This improves the super- polynomial time complexity upper bound shown by Valiant and Paterson in 1975. Our main contribution is to prove that two deterministic one-counter automata are inequivalent if and only if they can be distinguished by a word of length polynomial in the size of the two input automata.

STOC Conference 2013 Conference Paper

Equivalence of deterministic one-counter automata is NL-complete

• Stanislav Böhm
• Stefan Göller
• Petr Jancar

MFCS Conference 2013 Conference Paper

Reachability in Register Machines with Polynomial Updates

• Alain Finkel
• Stefan Göller
• Christoph Haase

Abstract This paper introduces a class of register machines whose registers can be updated by polynomial functions when a transition is taken, and the domain of the registers can be constrained by linear constraints. This model strictly generalises a variety of known formalisms such as various classes of Vector Addition Systems with States. Our main result is that reachability in our class is PSPACE -complete when restricted to one register. We moreover give a classification of the complexity of reachability according to the type of polynomials allowed and the geometry induced by the range-constraining formula.

CSL Conference 2013 Conference Paper

The Fixed-Parameter Tractability of Model Checking Concurrent Systems

• Stefan Göller

We study the fixed-parameter complexity of model checking temporal logics on concurrent systems that are modeled as the product of finite systems and where the size of the formula is the parameter. We distinguish between asynchronous product and synchronous product. Sometimes it is possible to show that there is an algorithm for this with running time (\sum_i T_i|)O(1) * f(|\phi|), where the T_i are the component systems and \phi is the formula and f is computable function, thus model checking is fixed-parameter tractable when the size of the formula is the parameter. In this paper we concern ourselves with the question, provided fixed-parameter tractability is known, whether it holds for an elementary function f. Negative answers to this question are provided for modal logic and EF logic: Depending on the mode of synchronization we show the non-existence of such an elementary function f under different assumptions from (parameterized) complexity theory.

MFCS Conference 2011 Conference Paper

Language Equivalence of Deterministic Real-Time One-Counter Automata Is NL-Complete

• Stanislav Böhm
• Stefan Göller

Abstract We prove that deciding language equivalence of deterministic real-time one-counter automata is NL -complete, in stark contrast to the inclusion problem which is known to be undecidable. This yields a subclass of deterministic pushdown automata for which the precise complexity of the equivalence problem can be determined. Moreover, we show that deciding regularity is NL -complete as well.

CSL Conference 2007 Conference Paper

On the Complexity of Reasoning About Dynamic Policies

• Stefan Göller

Abstract We study the complexity of satisfiability for DLP \(_{\mathrm{dyn}}^+\), an expressive logic introduced by Demri that allows to reason about dynamic policies. DLP \(_{\mathrm{dyn}}^+\) extends the logic DLP dyn of Pucella and Weissman, which in turn extends van der Meyden’s Dynamic Logic of Permission (DLP). DLP \(_{\mathrm{dyn}}^+\) generously enhances DLP and DLP dyn by allowing to update the policy set by adding or removing policy transitions, which are defined as a direct product of two sets, each specified by a formula of the logic itself. It is proven that satisfiability for DLP \(_{\mathrm{dyn}}^+\) is complete for deterministic exponential time. Our results close the complexity gap of satisfiability for DLP \(_{\mathrm{dyn}}^+\) from 2 EXP, and for DLP dyn from NEXP, to EXP respectively, matching the EXP lower bound both inherit from Propositional Dynamic Logic (PDL). To prove the EXP upper bound for DLP \(_{\mathrm{dyn}}^+\), we first proceed by accurately identifying a suitable generalization of PDL, which allows to use compressed programs and then find a satisfiability preserving translation from DLP \(_{\mathrm{dyn}}^+\) to this extension of PDL. To finally show the EXP upper bound for DLP \(_{\mathrm{dyn}}^+\), we prove that satisfiability of our extension of PDL lies in EXP! .

CSL Conference 2006 Conference Paper

Infinite State Model-Checking of Propositional Dynamic Logics

• Stefan Göller
• Markus Lohrey

Abstract Model-checking problems for PDL (propositional dynamic logic) and its extension PDL ∩ (which includes the intersection operator on programs) over various classes of infinite state systems (BPP, BPA, pushdown systems, prefix-recognizable systems) are studied. Precise upper and lower bounds are shown for the data/expression/combined complexity of these model-checking problems.