-
Verifying Unboundedness via Amalgamation
Authors:
Ashwani Anand,
Sylvain Schmitz,
Lia Schütze,
Georg Zetzsche
Abstract:
Well-structured transition systems (WSTS) are an abstract family of systems that encompasses a vast landscape of infinite-state systems. By requiring a well-quasi-ordering (wqo) on the set of states, a WSTS enables generic algorithms for classic verification tasks such as coverability and termination. However, even for systems that are WSTS like vector addition systems (VAS), the framework is noto…
▽ More
Well-structured transition systems (WSTS) are an abstract family of systems that encompasses a vast landscape of infinite-state systems. By requiring a well-quasi-ordering (wqo) on the set of states, a WSTS enables generic algorithms for classic verification tasks such as coverability and termination. However, even for systems that are WSTS like vector addition systems (VAS), the framework is notoriously ill-equipped to analyse reachability (as opposed to coverability). Moreover, some important types of infinite-state systems fall out of WSTS' scope entirely, such as pushdown systems (PDS).
Inspired by recent algorithmic techniques on VAS, we propose an abstract notion of systems where the set of runs is equipped with a wqo and supports amalgamation of runs. We show that it subsumes a large class of infinite-state systems, including (reachability languages of) VAS and PDS, and even all systems from the abstract framework of valence systems, except for those already known to be Turing-complete.
Moreover, this abstract setting enables simple and general algorithmic solutions to unboundedness problems, which have received much attention in recent years. We present algorithms for the (i) simultaneous unboundedness problem (which implies computability of downward closures and decidability of separability by piecewise testable languages), (ii) computing priority downward closures, (iii) deciding whether a language is bounded, meaning included in $w_1^*\cdots w_k^*$ for some words $w_1,\ldots,w_k$, and (iv) effective regularity of unary languages. This leads to either drastically simpler proofs or new decidability results for a rich variety of systems.
△ Less
Submitted 20 June, 2024; v1 submitted 16 May, 2024;
originally announced May 2024.
-
HElium: A Language and Compiler for Fully Homomorphic Encryption with Support for Proxy Re-Encryption
Authors:
Mirko Günther,
Lars Schütze,
Kilian Becher,
Thorsten Strufe,
Jeronimo Castrillon
Abstract:
Privacy-preserving analysis of confidential data can increase the value of such data and even improve peoples' lives. Fully homomorphic encryption (FHE) can enable privacy-preserving analysis. However, FHE adds a large amount of computational overhead and its efficient use requires a high level of expertise. Compilers can automate certain aspects such as parameterization and circuit optimizations.…
▽ More
Privacy-preserving analysis of confidential data can increase the value of such data and even improve peoples' lives. Fully homomorphic encryption (FHE) can enable privacy-preserving analysis. However, FHE adds a large amount of computational overhead and its efficient use requires a high level of expertise. Compilers can automate certain aspects such as parameterization and circuit optimizations. This in turn makes FHE accessible to non-cryptographers. Yet, multi-party scenarios remain complicated and exclude many promising use cases such as analyses of large amounts of health records for medical research. Proxy re-encryption (PRE), a technique that allows the conversion of data from multiple sources to a joint encryption key, can enable FHE for multi-party scenarios. Today, there are no optimizing compilers for FHE with PRE capabilities.
We propose HElium, the first optimizing FHE compiler with native support for proxy re-encryption. HElium features HEDSL, a domain-specific language (DSL) specifically designed for multi-party scenarios. By tracking encryption keys and transforming the computation circuit during compilation, HElium minimizes the number of expensive PRE operations. We evaluate the effectiveness of HElium's optimizations based on the real-world use case of the tumor recurrence rate, a well-known subject of medical research. Our empirical evaluation shows that HElium substantially reduces the overhead introduced through complex PRE operations, an effect that increases for larger amounts of input data.
△ Less
Submitted 21 December, 2023;
originally announced December 2023.
-
On the Length of Strongly Monotone Descending Chains over $\mathbb{N}^d$
Authors:
Sylvain Schmitz,
Lia Schütze
Abstract:
A recent breakthrough by Künnemann, Mazowiecki, Schütze, Sinclair-Banks, and Wegrzycki (ICALP, 2023) bounds the running time for the coverability problem in $d$-dimensional vector addition systems under unary encoding to $n^{2^{O(d)}}$, improving on Rackoff's $n^{2^{O(d\lg d)}}$ upper bound (Theor. Comput. Sci., 1978), and provides conditional matching lower bounds.
In this paper, we revisit Laz…
▽ More
A recent breakthrough by Künnemann, Mazowiecki, Schütze, Sinclair-Banks, and Wegrzycki (ICALP, 2023) bounds the running time for the coverability problem in $d$-dimensional vector addition systems under unary encoding to $n^{2^{O(d)}}$, improving on Rackoff's $n^{2^{O(d\lg d)}}$ upper bound (Theor. Comput. Sci., 1978), and provides conditional matching lower bounds.
In this paper, we revisit Lazić and Schmitz' "ideal view" of the backward coverability algorithm (Inform. Comput., 2021) in the light of this breakthrough. We show that the controlled strongly monotone descending chains of downwards-closed sets over $\mathbb{N}^d$ that arise from the dual backward coverability algorithm of Lazić and Schmitz on $d$-dimensional unary vector addition systems also enjoy this tight $n^{2^{O(d)}}$ upper bound on their length, and that this also translates into the same bound on the running time of the backward coverability algorithm.
Furthermore, our analysis takes place in a more general setting than that of Lazić and Schmitz, which allows to show the same results and improve on the 2EXPSPACE upper bound derived by Benedikt, Duff, Sharad, and Worrell (LICS, 2017) for the coverability problem in invertible affine nets.
△ Less
Submitted 20 April, 2024; v1 submitted 4 October, 2023;
originally announced October 2023.
-
Coverability in VASS Revisited: Improving Rackoff's Bound to Obtain Conditional Optimality
Authors:
Marvin Künnemann,
Filip Mazowiecki,
Lia Schütze,
Henry Sinclair-Banks,
Karol Węgrzycki
Abstract:
Seminal results establish that the coverability problem for Vector Addition Systems with States (VASS) is in EXPSPACE (Rackoff, '78) and is EXPSPACE-hard already under unary encodings (Lipton, '76). More precisely, Rosier and Yen later utilise Rackoff's bounding technique to show that if coverability holds then there is a run of length at most $n^{2^{\mathcal{O}(d \log d)}}$, where $d$ is the dime…
▽ More
Seminal results establish that the coverability problem for Vector Addition Systems with States (VASS) is in EXPSPACE (Rackoff, '78) and is EXPSPACE-hard already under unary encodings (Lipton, '76). More precisely, Rosier and Yen later utilise Rackoff's bounding technique to show that if coverability holds then there is a run of length at most $n^{2^{\mathcal{O}(d \log d)}}$, where $d$ is the dimension and $n$ is the size of the given unary VASS. Earlier, Lipton showed that there exist instances of coverability in $d$-dimensional unary VASS that are only witnessed by runs of length at least $n^{2^{Ω(d)}}$. Our first result closes this gap. We improve the upper bound by removing the twice-exponentiated $\log(d)$ factor, thus matching Lipton's lower bound. This closes the corresponding gap for the exact space required to decide coverability. This also yields a deterministic $n^{2^{\mathcal{O}(d)}}$-time algorithm for coverability. Our second result is a matching lower bound, that there does not exist a deterministic $n^{2^{o(d)}}$-time algorithm, conditioned upon the Exponential Time Hypothesis.
When analysing coverability, a standard proof technique is to consider VASS with bounded counters. Bounded VASS make for an interesting and popular model due to strong connections with timed automata. Withal, we study a natural setting where the counter bound is linear in the size of the VASS. Here the trivial exhaustive search algorithm runs in $\mathcal{O}(n^{d+1})$-time. We give evidence to this being near-optimal. We prove that in dimension one this trivial algorithm is conditionally optimal, by showing that $n^{2-o(1)}$-time is required under the $k$-cycle hypothesis. In general fixed dimension $d$, we show that $n^{d-2-o(1)}$-time is required under the 3-uniform hyperclique hypothesis.
△ Less
Submitted 2 May, 2023;
originally announced May 2023.
-
Unboundedness problems for machines with reversal-bounded counters
Authors:
Pascal Baumann,
Flavio D'Alessandro,
Moses Ganardi,
Oscar Ibarra,
Ian McQuillan,
Lia Schütze,
Georg Zetzsche
Abstract:
We consider a general class of decision problems concerning formal languages, called ``(one-dimensional) unboundedness predicates'', for automata that feature reversal-bounded counters (RBCA). We show that each problem in this class reduces -- non-deterministically in polynomial time -- to the same problem for just finite automata. We also show an analogous reduction for automata that have access…
▽ More
We consider a general class of decision problems concerning formal languages, called ``(one-dimensional) unboundedness predicates'', for automata that feature reversal-bounded counters (RBCA). We show that each problem in this class reduces -- non-deterministically in polynomial time -- to the same problem for just finite automata. We also show an analogous reduction for automata that have access to both a pushdown stack and reversal-bounded counters (PRBCA).
This allows us to answer several open questions: For example, we show that it is coNP-complete to decide whether a given (P)RBCA language $L$ is bounded, meaning whether there exist words $w_1,\ldots,w_n$ with $L\subseteq w_1^*\cdots w_n^*$. For PRBCA, even decidability was open. Our methods also show that there is no language of a (P)RBCA of intermediate growth. This means, the number of words of each length grows either polynomially or exponentially. Part of our proof is likely of independent interest: We show that one can translate an RBCA into a machine with $\mathbb{Z}$-counters in logarithmic space, while preserving the accepted language.
△ Less
Submitted 24 January, 2023;
originally announced January 2023.
-
Reachability in Bidirected Pushdown VASS
Authors:
Moses Ganardi,
Rupak Majumdar,
Andreas Pavlogiannis,
Lia Schütze,
Georg Zetzsche
Abstract:
A pushdown vector addition system with states (PVASS) extends the model of vector addition systems with a pushdown store. A PVASS is said to be \emph{bidirected} if every transition (pushing/pop** a symbol or modifying a counter) has an accompanying opposite transition that reverses the effect. Bidirectedness arises naturally in many models; it can also be seen as a overapproximation of reachabi…
▽ More
A pushdown vector addition system with states (PVASS) extends the model of vector addition systems with a pushdown store. A PVASS is said to be \emph{bidirected} if every transition (pushing/pop** a symbol or modifying a counter) has an accompanying opposite transition that reverses the effect. Bidirectedness arises naturally in many models; it can also be seen as a overapproximation of reachability. We show that the reachability problem for \emph{bidirected} PVASS is decidable in Ackermann time and primitive recursive for any fixed dimension. For the special case of one-dimensional bidirected PVASS, we show reachability is in $\mathsf{PSPACE}$, and in fact in polynomial time if the stack is polynomially bounded. Our results are in contrast to the \emph{directed} setting, where decidability of reachability is a long-standing open problem already for one dimensional PVASS, and there is a $\mathsf{PSPACE}$-lower bound already for one-dimensional PVASS with bounded stack.
The reachability relation in the bidirected (stateless) case is a congruence over $\mathbb{N}^d$. Our upper bounds exploit saturation techniques over congruences. In particular, we show novel elementary-time constructions of semilinear representations of congruences generated by finitely many vector pairs. In the case of one-dimensional PVASS, we employ a saturation procedure over bounded-size counters.
We complement our upper bound with a $\mathsf{TOWER}$-hardness result for arbitrary dimension and $k$-$\mathsf{EXPSPACE}$ hardness in dimension $2k+6$ using a technique by Lazić and Totzke to implement iterative exponentiations.
△ Less
Submitted 25 April, 2022;
originally announced April 2022.
