Recent zbMATH articles in MSC 68Qhttps://zbmath.org/atom/cc/68Q2023-09-22T14:21:46.120933ZUnknown authorWerkzeugComplexity of the infinitary Lambek calculus with Kleene starhttps://zbmath.org/1517.030422023-09-22T14:21:46.120933Z"Kuznetsov, Stepan"https://zbmath.org/authors/?q=ai:kuznetsov.s-lSummary: We consider the Lambek calculus, or noncommutative multiplicative intuitionistic linear logic, extended with iteration, or Kleene star, axiomatised by means of an \(\omega\)-rule, and prove that the derivability problem in this calculus is \(\Pi_1^0\)-hard. This solves a problem left open by \textit{W. Buszkowski} [J. Log. Comput. 17, No. 1, 199--217 (2007; Zbl 1118.03013)], who obtained the same complexity bound for infinitary action logic, which additionally includes additive conjunction and disjunction. As a by-product, we prove that any context-free language without the empty word can be generated by a Lambek grammar with unique type assignment, without Lambek's nonemptiness restriction imposed (cf. [\textit{A. N. Safiullin}, Vestn. Mosk. Univ., Ser. I 2007, No. 4, 72--76 (2007; Zbl 1164.03003)]).Distance problems within Helly graphs and \(k\)-Helly graphshttps://zbmath.org/1517.050452023-09-22T14:21:46.120933Z"Ducoffe, Guillaume"https://zbmath.org/authors/?q=ai:ducoffe.guillaumeSummary: The ball hypergraph of a graph \(G\) is the family of balls of all possible centers and radii in \(G\). Balls in a subfamily are \(k\)-wise intersecting if the intersection of any \(k\) balls in the subfamily is always nonempty. The Helly number of a ball hypergraph is the least integer \(k\) greater than one such that every subfamily of \(k\)-wise intersecting balls has a nonempty common intersection. A graph is \(k\)-Helly (or Helly, if \(k = 2\)) if its ball hypergraph has a Helly number at most \(k\). We prove that a central vertex and all the medians in an \(n\)-vertex \(m\)-edge Helly graph can be computed w.h.p. in \(\widetilde{\mathcal{O}}(m \sqrt{ n})\) time. Both results extend to a broader setting where we assign a nonnegative cost to the vertices. For any fixed \(k\), we also present an \(\widetilde{\mathcal{O}}(m \sqrt{ k n})\)-time randomized algorithm for radius computation within \(k\)-Helly graphs. If we relax the definition of Helly number (for what is sometimes called an ``almost Helly-type'' property in the literature), then our approach leads to an approximation algorithm for computing the radius with an additive one-sided error of at most some constant.Algorithms for the rainbow vertex coloring problem on graph classeshttps://zbmath.org/1517.050572023-09-22T14:21:46.120933Z"Lima, Paloma T."https://zbmath.org/authors/?q=ai:lima.paloma-t"van Leeuwen, Erik Jan"https://zbmath.org/authors/?q=ai:van-leeuwen.erik-jan"van der Wegen, Marieke"https://zbmath.org/authors/?q=ai:van-der-wegen.mariekeSummary: Given a vertex-colored graph, we say a path is a rainbow vertex path if all its internal vertices have distinct colors. The graph is rainbow vertex-connected if there is a rainbow vertex path between every pair of its vertices. In the \textsc{Rainbow Vertex Coloring (RVC)} problem we want to decide whether the vertices of a given graph can be colored with at most \(k\) colors so that the graph becomes rainbow vertex-connected. This problem is known to be NP-complete even in very restricted scenarios, and very few efficient algorithms are known for it. In this work, we give polynomial-time algorithms for RVC on permutation graphs, powers of trees and split strongly chordal graphs. The algorithm for the latter class also works for the strong variant of the problem, where the rainbow vertex paths between each vertex pair must be shortest paths. We complement the polynomial-time solvability results for split strongly chordal graphs by showing that, for any fixed \(p \geq 3\) both variants of the problem become NP-complete when restricted to split \(( S_3, \ldots, S_p)\)-free graphs, where \(S_q\) denotes the \(q\)-sun graph.Role colouring graphs in hereditary classeshttps://zbmath.org/1517.050582023-09-22T14:21:46.120933Z"Purcell, Christopher"https://zbmath.org/authors/?q=ai:purcell.christopher-j"Rombach, Puck"https://zbmath.org/authors/?q=ai:rombach.puckSummary: A locally surjective homomorphism from a graph \(G\) to a graph \(H\) is called an \(H\)-role colouring of \(G\). Deciding the existence of such a colouring with \(| H | = k\) is known to be NP-hard even under substantial restrictions on the input graph \(G\). We study the family of hereditary classes for which the problem can be solved efficiently. Our main result is the first boundary class for this problem; that is, a minimal obstruction to solving the problem efficiently in a finitely defined hereditary class. We also give the first boundary class for the related \(k\)-coupon colouring problem, in which \(H\) is a complete graph with each vertex incident to a loop, when \(k\) is a prime power. As additional results, we show that 2-role colouring \(2 K_2\)-free graphs and 2-coupon colouring cographs can be done in linear time.On the proper orientation number of chordal graphshttps://zbmath.org/1517.050632023-09-22T14:21:46.120933Z"Araujo, J."https://zbmath.org/authors/?q=ai:araujo.julio-cesar-silva"Cezar, A."https://zbmath.org/authors/?q=ai:cezar.alexandre"Lima, C. V. G. C."https://zbmath.org/authors/?q=ai:lima.carlos-vinicius-gomes-costa"dos Santos, V. F."https://zbmath.org/authors/?q=ai:dos-santos.vinicius-fernandes"Silva, A."https://zbmath.org/authors/?q=ai:silva.ana-r-s|silva.andre-luis-ferreira-da|silva.ariosto-s|silva.alexandru|silva.a-de-a-e|silva.a-pedro-duarte|silva.ana-carolina|silva.ana-maria-f|silva.anderson-t|silva.adriano-w|silva.anibal|silva.alexandre-m-f|silva.arlenes-s|silva.adilson|silva.analia|silva.arlaine-a|silva.alberto|silva.alessandro|silva.anne|silva.andres|silva.ana-t-c|silva.ana-l|silva.antonio-m-p|silva.a-i|silva.a-christian|silva.augusto|silva.adriano-da|silva.adriana-r|silva.alexandra|silva.alonso|silva.andre-c|silva.antonio-m-m|silva.aline-p|silva.alisson-r|silva.andrea-r-d|silva.a-f-c|silva.aristofanes-correa|silva.aldy-f|silva.allyson|silva.antonio-kelson|silva.arlindo|silva.allessandro|silva.adao|silva.apollo-v|silva.antonio-n-jun|silva.andreia-f|silva.anabela-sousaSummary: An orientation \(D\) of a graph \(G = (V, E)\) is a digraph obtained from \(G\) by replacing each edge by exactly one of the two possible arcs with the same end vertices. For each \(v \in V(G)\), the indegree of \(v\) in \(D\), denoted by \(d_D^-(v)\), is the number of arcs with head \(v\) in \(D\). An orientation \(D\) of \(G\) is proper if \(d_D^-(u) \neq d_D^-(v)\), for all \(u v \in E(G)\). An orientation with maximum indegree at most \(k\) is called a \(k\)-orientation. The proper orientation number of \(G\), denoted by \(\overrightarrow{\chi}(G)\), is the minimum integer \(k\) such that \(G\) admits a proper \(k\)-orientation. We prove that determining whether \(\overrightarrow{\chi}(G) \leq k\) is \(\mathsf{NP}\)-complete for chordal graphs of bounded diameter, but can be solved in linear-time in the subclass of quasi-threshold graphs. When parameterizing by \(k\), we argue that this problem is \textsf{FPT} for chordal graphs and argue that no polynomial kernel exists, unless \(\mathsf{NP} \subseteq \mathsf{coNP} / \mathsf{poly} \). We present a better kernel to the subclass of split graphs and a linear kernel to the class of cobipartite graphs.
Concerning bounds, we first prove that if \(G\) is split, then \(\overrightarrow{\chi}(G) \leq 2 \omega(G) - 2\) and that if \(G\) is a \(k\)-uniform block graph, then \(\overrightarrow{\chi}(G) \leq 3 k - 2\). These bounds are tight. We also present new families of trees having proper orientation number at most 2 and at most 3. Actually, we prove a general bound stating that any graph \(G\) having no adjacent vertices of degree at least \(c + 1\) has proper orientation number at most \(c\). This implies new classes of (outer)planar graphs with bounded proper orientation number. We also prove that maximal outerplanar graphs \(G\) whose weak-dual is a path satisfy \(\overrightarrow{\chi}(G) \leq 13\). Finally, we present simple bounds to the classes of chordal claw-free graphs and cographs.The complexity of 2-vertex-connected orientation in mixed graphshttps://zbmath.org/1517.050902023-09-22T14:21:46.120933Z"Hörsch, Florian"https://zbmath.org/authors/?q=ai:horsch.florian"Szigeti, Zoltán"https://zbmath.org/authors/?q=ai:szigeti.zoltanSummary: We consider two possible extensions of a theorem of \textit{C. Thomassen} [in: Combinatorial mathematics: Proceedings of the third international conference, held in New York, USA, June 10--14, 1985. New York: New York Academy of Sciences. 402--412 (1989; Zbl 0709.05030)] characterizing the graphs admitting a 2-vertex-connected orientation. First, we show that the problem of deciding whether a mixed graph has a 2-vertex-connected orientation is NP-hard. This answers a question of \textit{J. Bang-Jensen} et al. [J. Graph Theory 87, No. 3, 285--304 (2018; Zbl 1386.05121)]. For the second part, we call a directed graph \(D=(V,A)2T\)-connected for some \(T\subseteq V\) if \(D\) is 2-arc-connected and \(D-v\) is strongly connected for all \(v\in T\). We deduce a characterization of the graphs admitting a \(2T\)-connected orientation from the theorem of Thomassen [loc. cit.].\(k\)-efficient domination: algorithmic perspectivehttps://zbmath.org/1517.051342023-09-22T14:21:46.120933Z"Meybodi, Mohsen Alambardar"https://zbmath.org/authors/?q=ai:meybodi.mohsen-alambardarSummary: A set \(D\subseteq V\) of a graph \(G=(V,E)\) is called an efficient dominating set of \(G\) if every vertex \(v\) has exactly one neighbor in \(D\), in other words, the vertex set \(V\) is partitioned to some circles with radius one such that the vertices in \(D\) are the centers of partitions. A generalization of this concept, introduced by \textit{M. Chellali} et al. [Commun. Comb. Optim. 4, No. 2, 109--122 (2019; Zbl 1438.05190)], is called \(k\)-efficient dominating set that briefly partitions the vertices of graph with different radiuses. It leads to a partition set \(\{U_1, U_2,\dots, U_t\}\) such that each \(U_i\) consists a center vertex \(u_i\) and all the vertices in distance \(d_i\), where \(d_i\in\{0,1,\dots,k\}\). In other words, there exist the dominators with various dominating powers. The problem of finding minimum set \(\{ u_1, u_2,\dots, u_t\}\) is called the minimum \(k\)-efficient domination problem. Given a positive integer \(S\) and a graph \(G=(V,E)\), the \(k\)-efficient Domination Decision problem is to decide whether \(G\) has a \(k\)-efficient dominating set of cardinality at most \(S\). The \(k\)-efficient Domination Decision problem is known to be NP-complete even for bipartite graphs [loc. cit.]. Clearly, every graph has a \(k\)-efficient dominating set but it is not correct for efficient dominating set. In this paper, we study the following:
\begin{itemize}
\item[\(\bullet\)] \(k\)-efficient domination problem set is NP-complete even in chordal graphs.
\item[\(\bullet\)] A polynomial-time algorithm for \(k\)-efficient domination in trees.
\item[\(\bullet\)] \(k\)-efficient domination on sparse graphs from the parametrized complexity perspective. In particular, we show that it is \(W[1]\)-hard on \(d\)-degenerate graphs while the original dominating set has Fixed Parameter Tractable (FPT) algorithm on \(d\)-degenerate graphs.
\item[\(\bullet\)] \(k\)-efficient domination on nowhere-dense graphs is FPT.
\end{itemize}Dominating induced matching in some subclasses of bipartite graphshttps://zbmath.org/1517.051362023-09-22T14:21:46.120933Z"Panda, B. S."https://zbmath.org/authors/?q=ai:panda.bhawani-sankar"Chaudhary, Juhi"https://zbmath.org/authors/?q=ai:chaudhary.juhiSummary: A subset \(M \subseteq E\) of edges of a graph \(G = (V, E)\) is called a matching if no two edges of \(M\) share a common vertex. An edge \(e \in E\) is said to dominate itself and all other edges adjacent to it. A matching \(M\) in a graph \(G = (V, E)\) is called a dominating induced matching (d.i.m.) if every edge of \(G\) is dominated by edges of \(M\) exactly once. The dominating induced matching decide (\textsc{DIM-Decide}) problem asks whether a graph \(G\) contains a dominating induced matching. The dominating induced matching (\textsc{DIM}) problem asks to compute a dominating induced matching (d.i.m.) in a graph \(G\) that admits a dominating induced matching. The \textsc{DIM-Decide} problem is known to be NP-complete for general graphs as well as for bipartite graphs. In this paper, we strengthen the NP-completeness result of the \textsc{DIM-Decide} problem by showing that this problem remains NP-complete for perfect elimination bipartite graphs, a proper subclass of bipartite graphs. On the positive side, we characterize the class of star-convex bipartite graphs admitting a d.i.m. This characterization leads to a linear time algorithm to test whether a star-convex bipartite graph admits a d.i.m. and, if so, constructs a d.i.m. in such a star-convex bipartite graph in linear time. We also propose polynomial time algorithms to construct a d.i.m. in long-\(k\)-star-convex bipartite graphs as well as in circular-convex bipartite graphs if the input graph admits a d.i.m.Algorithms for the rainbow vertex coloring problem on graph classeshttps://zbmath.org/1517.051682023-09-22T14:21:46.120933Z"Lima, Paloma T."https://zbmath.org/authors/?q=ai:lima.paloma-t"van Leeuwen, Erik Jan"https://zbmath.org/authors/?q=ai:van-leeuwen.erik-jan"van der Wegen, Marieke"https://zbmath.org/authors/?q=ai:van-der-wegen.mariekeSummary: Given a vertex-colored graph, we say a path is a rainbow vertex path if all its internal vertices have distinct colors. The graph is rainbow vertex-connected if there is a rainbow vertex path between every pair of its vertices. In the Rainbow Vertex Coloring (RVC) problem we want to decide whether the vertices of a given graph can be colored with at most \(k\) colors so that the graph becomes rainbow vertex-connected. This problem is known to be NP-complete even in very restricted scenarios, and very few efficient algorithms are known for it. In this work, we give polynomial-time algorithms for RVC on permutation graphs, powers of trees and split strongly chordal graphs. The algorithm for the latter class also works for the strong variant of the problem, where the rainbow vertex paths between each vertex pair must be shortest paths. We complement the polynomial-time solvability results for split strongly chordal graphs by showing that, for any fixed \(p\geq 3\) both variants of the problem become NP-complete when restricted to split \((S_3,\dots,S_p)\)-free graphs, where \(S_q\) denotes the \(q\)-sun graph.
For the entire collection see [Zbl 1445.68013].On the complexity of the planar edge-disjoint paths problem with terminals on the outer boundaryhttps://zbmath.org/1517.051692023-09-22T14:21:46.120933Z"Schwärzler, Werner"https://zbmath.org/authors/?q=ai:schwarzler.wernerSummary: It is shown that both the undirected and the directed edge-disjoint paths problem are NP-complete, if the supply graph is planar and all edges of the demand graph are incident with vertices lying on the outer boundary of the supply graph. In the directed case, the problem remains NP-complete, if in addition the supply graph is acyclic. The undirected case solves open problem no. 56 of \textit{A. Schrijver}'s book [Combinatorial optimization. Polyhedra and efficiency (3 volumes). Berlin: Springer (2003; Zbl 1041.90001)].Lamplighter groups and automatahttps://zbmath.org/1517.200552023-09-22T14:21:46.120933Z"Jain, Sanjay"https://zbmath.org/authors/?q=ai:jain.sanjay"Moldagaliyev, Birzhan"https://zbmath.org/authors/?q=ai:moldagaliyev.birzhan"Stephan, Frank"https://zbmath.org/authors/?q=ai:stephan.frank"Tien Dat Tran"https://zbmath.org/authors/?q=ai:tien-dat-tran.\noindent A \textit{transducer} \(M=(Q,\Sigma,\delta,s_0,F)\) is a non-deterministic finite automaton, where~\(Q\) is a finite set of states, \(\Sigma\) is a finite alphabet, \(s_0\) is the starting state, \(F\) is a set of accepting states and \(\delta\) is a function from \(Q\times\big(\Sigma^*\big)^k\) to the powerset of \(Q\) (here, \(\Sigma^*\) is the set of words on the alphabet \(\Sigma\)).
The \(k\)-tuple \((w_1,\dots,w_k)\in\Sigma^*\) is \textit{accepted} by \(M\) if there are \(q_0,q_1,\dots,q_r\in Q\), and \(w_{i,j}\in\Sigma^*\) (with \(i=1,\dots,k\) and \(j=0,1,\dots,r-1\)) such that:
\begin{itemize}
\item[(1)] \(q_{j+1}\in\delta(q_j,w_{1,j},\dots,w_{k,j})\) for \(j<r\);
\item[(2)] \(q_0=s_0\) and \(q_r\in F\);
\item[(3)]\(w_i=w_{i,0}\dots w_{i,r-1}\) for \(i=1,\dots,k\).
\end{itemize}
A relation is \textit{transducer recognisable} if there is a transducer accepting every element of the relation. A function is \textit{transducer recognisable} if its graph is transducer recognisable.
A group \((G,\circ)\) is said to be \textit{transducer one-to-one presented} if it admits a \textit{transducer presentation}, that is, a bijective map \(\phi:D\rightarrow G\) such that
\begin{itemize}
\item \(D\) is a transducer recognisable language;
\item The relation \(\{(x,y)\in D\times D\,:\, \phi(x)=\phi(y)\}\) is transducer recognisable;
\item Some transducer recognisable function computes for inputs \(x,y\in D\), a \(z\in D\) such that \(\phi(x)\circ\phi(y)=\phi(z)\).
\end{itemize}
The main aim of the paper under review is to show that given a transducer one-to-one presented group \(G\), then also the wreath product \(G\wr\mathbb{Z}\) is transducer one-to-one presented (see Theorem 14). The paper contains other results on the argument. For example, it is shown that the Baumslag-Solitar group \(BS(1,n)\) is also transducer one-to-one presented (see Theorem 16). Other types of presentations (that is, Cayley transducer presentations and tree automata presentations) for certain types of wreath products are also dealt with.
Reviewer: Marco Trombetti (Napoli)An explicit algorithm for normal forms in small overlap monoidshttps://zbmath.org/1517.200822023-09-22T14:21:46.120933Z"Mitchell, James D."https://zbmath.org/authors/?q=ai:mitchell.james-d"Tsalakou, Maria"https://zbmath.org/authors/?q=ai:tsalakou.mariaSummary: We describe a practical algorithm for computing normal forms for semigroups and monoids with finite presentations satisfying so-called small overlap conditions. Small overlap conditions are natural conditions on the relations in a presentation, which were introduced by J. H. Remmers and subsequently studied extensively by M. Kambites. Presentations satisfying these conditions are ubiquitous; Kambites showed that a randomly chosen finite presentation satisfies the \(C(4)\) condition with probability tending to 1 as the sum of the lengths of relation words tends to infinity. Kambites also showed that several key problems for finitely presented semigroups and monoids are tractable in \(C(4)\) monoids: the word problem is solvable in \(O(\min \{| u |, | v | \})\) time in the size of the input words \(u\) and \(v\); the uniform word problem for \(\langle A \mid R \rangle\) is solvable in \(O( N^2 \min \{| u |, | v | \})\) where \(N\) is the sum of the lengths of the words in \(R\); and a normal form for any given word \(u\) can be found in \(O(| u |)\) time. Although Kambites' algorithm for solving the word problem in \(C(4)\) monoids is highly practical, it appears that the coefficients in the linear time algorithm for computing normal forms are too large in practice. In this paper, we present an algorithm for computing normal forms in \(C(4)\) monoids that has time complexity \(O(| u |^2)\) for input word \(u\), but where the coefficients are sufficiently small to allow for practical computation. Additionally, we show that the uniform word problem for small overlap monoids can be solved in \(O(N \min \{| u |, | v | \})\) time.On the word problem for free products of semigroups and monoidshttps://zbmath.org/1517.200832023-09-22T14:21:46.120933Z"Nyberg-Brodda, Carl-Fredrik"https://zbmath.org/authors/?q=ai:nyberg-brodda.carl-fredrikSummary: We study the language-theoretic aspects of the word problem, in the sense of \textit{A. Duncan} and \textit{R. H. Gilman} [Math. Proc. Camb. Philos. Soc. 136, No. 3, 513--524 (2004; Zbl 1064.20055)], of free products of semigroups and monoids. First, we provide algebraic tools for studying classes of languages known as super-AFLs, which generalise e.g. the context-free or the indexed languages. When \(\mathcal{C}\) is a super-AFL closed under reversal, we prove that the semigroup (monoid) free product of two semigroups (resp. monoids) with word problem in \(\mathcal{C}\) also has word problem in \(\mathcal{C}\). This recovers and generalises a recent result by \textit{T. Brough} et al. [Lect. Notes Comput. Sci. 11647, 292--305 (2019; Zbl 07117554)] that the class of context-free semigroups (monoids) is closed under taking free products. As a group-theoretic corollary, we deduce that the word problem of the (group) free product of two groups with word problem in \(\mathcal{C}\) is also in \(\mathcal{C}\). As a particular case, we find that the free product of two groups with indexed word problem has indexed word problem.Groups, languages and dendric shiftshttps://zbmath.org/1517.370032023-09-22T14:21:46.120933Z"Perrin, Dominique"https://zbmath.org/authors/?q=ai:perrin.dominiqueSummary: We present a survey of results obtained on symbolic dynamical systems called dendric shifts. We state and sketch the proofs (sometimes new ones) of the main results obtained on these shifts. This includes the return theorem and the finite index basis theorem which both put in evidence the central role played by free groups in these systems. We also present a series of applications of these results, including some on profinite semigroups and some on dimension groups.
For the entire collection see [Zbl 1398.68030].Rapid left expansivity, a commonality between Wolfram's rule 30 and powers of \(p/q\)https://zbmath.org/1517.370212023-09-22T14:21:46.120933Z"Kopra, Johan"https://zbmath.org/authors/?q=ai:kopra.johanSummary: We define the class of rapidly left expansive cellular automata, which contains Wolfram's Rule 30, fractional multiplication automata, and many others. Previous results on aperiodicity of columns in space-time diagrams of certain cellular automata generalize to this new class. We also present conditions that imply periodic behavior in cellular automata and use these to prove new results on rapidly left expansive cellular automata that originate from the theory of distribution modulo 1.Attractor separation and signed cycles in asynchronous Boolean networkshttps://zbmath.org/1517.370502023-09-22T14:21:46.120933Z"Richard, Adrien"https://zbmath.org/authors/?q=ai:richard.adrien"Tonello, Elisa"https://zbmath.org/authors/?q=ai:tonello.elisaSummary: The structure of the graph defined by the interactions in a Boolean network can determine properties of the asymptotic dynamics. For instance, considering the asynchronous dynamics, the absence of positive cycles guarantees the existence of a unique attractor, and the absence of negative cycles ensures that all attractors are fixed points. In presence of multiple attractors, one might be interested in properties that ensure that attractors are sufficiently ``isolated'', that is, they can be found in separate subspaces or even trap spaces, subspaces that are closed with respect to the dynamics. Here we introduce notions of separability for attractors and identify corresponding necessary conditions on the interaction graph. In particular, we show that if the interaction graph has at most one positive cycle, or at most one negative cycle, or if no positive cycle intersects a negative cycle, then the attractors can be separated by subspaces. If the interaction graph has no path from a negative to a positive cycle, then the attractors can be separated by trap spaces. Furthermore, we study networks with interaction graphs admitting two vertices that intersect all cycles, and show that if their attractors cannot be separated by subspaces, then their interaction graph must contain a copy of the complete signed digraph on two vertices, deprived of a negative loop. We thus establish a connection between a dynamical property and a complex network motif. The topic is far from exhausted and we conclude by stating some open questions.Approximate integrals over the volume of the ballhttps://zbmath.org/1517.650162023-09-22T14:21:46.120933Z"Reeger, Jonah A."https://zbmath.org/authors/?q=ai:reeger.jonah-aSummary: A radial basis function generated finite-differences (RBF-FD) inspired technique for evaluating definite integrals over the volume of the ball in three dimensions is described. Such methods are necessary in many areas of applied mathematics, mathematical physics and myriad other application areas. Previous approaches needed restrictive uniformity in the node set, which the algorithm presented here does not require. By using RBF-FD approach, the proposed algorithm computes quadrature weights for \(N\) arbitrarily scattered nodes in only \(O(N\log N)\) operations with high orders of accuracy.Descriptional complexity of formal systems. 25th IFIP WG 1.02 international conference, DCFS 2023, Potsdam, Germany, July 4--6, 2023. Proceedingshttps://zbmath.org/1517.680052023-09-22T14:21:46.120933ZThe articles of this volume will be reviewed individually. For the preceding conference see [Zbl 1503.68015].
Indexed articles:
\textit{Caron, Pascal; Luque, Jean-Gabriel; Patrou, Bruno}, Operational state complexity revisited: the contribution of monsters and modifiers, 1-20 [Zbl 07729454]
\textit{Anselmo, Marcella; Castiglione, Giuseppa; Flores, Manuela; Giammarresi, Dora; Madonia, Maria; Mantaci, Sabrina}, Hypercubes and isometric words based on swap and mismatch distance, 21-35 [Zbl 07729455]
\textit{Chavrimootoo, Michael C.}, Defying gravity and gadget numerosity: the complexity of the Hanano puzzle, 36-50 [Zbl 07729456]
\textit{Han, Yo-Sub; Kim, Sungmin; Ko, Sang-Ki; Salomaa, Kai}, Existential and universal width of alternating finite automata, 51-64 [Zbl 07729457]
\textit{Holzer, Markus; Rauch, Christian}, On Jaffe's pumping lemma, revisited, 65-78 [Zbl 07729458]
\textit{Hospodár, Michal; Jirásek, Jozef; Jirásková, Galina; Šebej, Juraj}, Operational complexity: NFA-to-DFA trade-off, 79-93 [Zbl 07729459]
\textit{Kotowsky, Maximilian; Wächter, Jan Philipp}, The word problem for finitary automaton groups, 94-108 [Zbl 07729460]
\textit{Kuntewar, Neha; Anoop, S. K. M.; Sarma, Jayalal}, Separating words problem over groups, 109-120 [Zbl 07729461]
\textit{Kutrib, Martin; Malcher, Andreas; Wendlandt, Matthias}, Complexity of exclusive nondeterministic finite automata, 121-133 [Zbl 07729462]
\textit{Martynova, Olga; Okhotin, Alexander}, Shortest accepted strings for two-way finite automata: approaching the \(2^n\) lower bound, 134-145 [Zbl 07729463]
\textit{Pighizzini, Giovanni; Prigioniero, Luca}, Pushdown and one-counter automata: constant and non-constant memory usage, 146-157 [Zbl 07729464]
\textit{Rukavicka, Josef}, Construction of a bi-infinite power free word with a given factor and a non-recurrent letter, 158-168 [Zbl 07729465]
\textit{Truthe, Bianca}, Merging two hierarchies of external contextual grammars with subregular selection, 169-180 [Zbl 07729466]
\textit{Weight, Jean; Grobler, Trienko; van Zijl, Lynette; Stewart, Carlyle}, A tight upper bound on the length of maximal bordered box repetition-free words, 181-196 [Zbl 07729467]Mathematical foundations of programming semantics. 7th international conference, Pittsburgh, PA, USA, March 25--28, 1991. Proceedingshttps://zbmath.org/1517.680062023-09-22T14:21:46.120933ZThe articles of this volume will be reviewed individually. For the 5th conference see [Zbl 0751.68005].
Indexed articles:
\textit{Ma, QingMing; Reynolds, John C.}, Types, abstraction, and parametric polymorphism. II, 1-40 [Zbl 07727392]
\textit{Gateley, John; Duba, Bruce F.}, Call-by-value combinatory logic and the lambda-value calculus, 41-53 [Zbl 07727393]
\textit{Smith, Scott F.}, From operational to denotational semantics, 54-76 [Zbl 07727394]
\textit{Mislove, Michael W.; Oles, Prank J.}, A simple language supporting angelic nondeterminism and parallel composition, 77-101 [Zbl 07727395]
\textit{Bruce, Kim B.}, The equivalence of two semantic definitions for inheritance in object-oriented languages, 102-124 [Zbl 07727396]
\textit{Nelson, Neal}, Primitive recursive functional with dependent types, 125-143 [Zbl 07727397]
\textit{Leavens, Gary T.; Pigozzi, Don}, Typed homomorphic relations extended with subtypes, 144-167 [Zbl 07727398]
\textit{Barwise, Jon}, Information links in domain theory, 168-192 [Zbl 07727399]
\textit{Rutten, J. J. M. M.}, Nonwellfounded sets and programming language semantics, 193-206 [Zbl 07727400]
\textit{Gray, John W.}, Simultaneous substitution in the typed lambda calculus, 207-220 [Zbl 07727401]
\textit{Barr, Michael}, HSP type theorems in the category of posets, 221-234 [Zbl 07727402]
\textit{Jung, Achim; Libkin, Leonid; Puhlmann, Hermann}, Decomposition of domains, 235-258 [Zbl 07727403]
\textit{Huth, Michael}, Cartesian closed categories of domains and the space \(\operatorname{Proj}(D)\), 259-271 [Zbl 07727404]
\textit{Heckmann, Reinhold}, An upper power domain construction in terms of strongly compact sets, 272-293 [Zbl 07727405]
\textit{Wand, Mitchell}, Correctness of procedure representations in higher-order assembly language, 294-311 [Zbl 07727406]
\textit{Mercouroff, N.}, An algorithm for analyzing communicating processes, 312-325 [Zbl 07727407]
\textit{Brookes, Stephen; Geva, Shai}, Continuous functions and parallel algorithms on concrete data structures, 326-349 [Zbl 07727408]
\textit{Bloom, Bard; Kwiatkowska, Marta}, Trade-offs in true concurrency: pomsets and Mazurkiewicz traces, 350-375 [Zbl 07727409]
\textit{Aceto, Luca}, On relating concurrency and nondeterminism, 376-402 [Zbl 07727410]
\textit{Kasangian, S.; Labella, A.}, On continuous time agents, 403-425 [Zbl 07727411]
\textit{Zhang, Guo-Qiang}, A monoidal closed category of event structures, 426-435 [Zbl 07727412]
\textit{Rosolini, G.}, An exper model for Quest, 436-445 [Zbl 07727413]
\textit{Manes, Ernest G.}, Equations for if-then-else, 446-456 [Zbl 07727414]
\textit{Bloom, Stephen L.; Ésik, Zoltán}, Program correctness and matricial iteration theories, 457-476 [Zbl 07727415]
\textit{Klarlund, Nils}, Liminf progress measures, 477-491 [Zbl 07727416]
\textit{Melton, Austin; Schröder, Bernd S. W.; Strecker, George E.}, Connections, 492-506 [Zbl 07727417]Formal methods. 25th international symposium, FM 2023, Lübeck, Germany, March 6--10, 2023. Proceedingshttps://zbmath.org/1517.680072023-09-22T14:21:46.120933ZThe articles of mathematical interest will be reviewed individually. For the preceding symposium see [Zbl 1509.68013].Preface: Special issue: 15th international conference on automata and formal languageshttps://zbmath.org/1517.680082023-09-22T14:21:46.120933ZFrom the text: AFL 2017, the 15th International Conference on Automata and Formal Languages was held in Debrecen, Hungary, September 4--6, 2017. It was organized by the Faculty of Informatics of the University of Debrecen, and by the Faculty of Informatics of the Eötvös Loránd University, Budapest.
This collection contains revised and extended versions of ten selected papers presented at the conference.Algorithmic learning theory 2022. Proceedings of the 33rd international conference (ALT 2022), Paris, March 29 -- April 1, 2022https://zbmath.org/1517.680092023-09-22T14:21:46.120933ZThe articles of this volume will be reviewed individually. For the preceding conference see [Zbl 1517.68012].Verification, model checking, and abstract interpretation. 24th international conference, VMCAI 2023, Boston, MA, USA, January 16--17, 2023. Proceedingshttps://zbmath.org/1517.680102023-09-22T14:21:46.120933ZThe articles of mathematical interest will be reviewed individually. For the preceding conference see [Zbl 1490.68015].Algorithmic learning theory 2021. Proceedings of the 32nd international conference (ALT 2021), virtual, March 16--19, 2021https://zbmath.org/1517.680122023-09-22T14:21:46.120933ZThe articles of this volume will be reviewed individually. For the preceding conference see [Zbl 1517.68020].Algorithmic learning theory 2019. Proceedings of the 30th international conference (ALT 2019), Chicago, IL, USA, March 22--24, 2019https://zbmath.org/1517.680132023-09-22T14:21:46.120933ZThe articles of this volume will be reviewed individually. For the preceding conference see [Zbl 1405.68011].SOFSEM 2023: theory and practice of computer science. 48th international conference on current trends in theory and practice of computer science, SOFSEM 2023, Nový Smokovec, Slovakia, January 15--18, 2023. Proceedingshttps://zbmath.org/1517.680142023-09-22T14:21:46.120933ZThe articles of mathematical interest will be reviewed individually. For the preceding conference see [Zbl 1482.68014].Relational and algebraic methods in computer science. 20th international conference, RAMiCS 2023, Augsburg, Germany, April 3--6, 2023. Proceedingshttps://zbmath.org/1517.680162023-09-22T14:21:46.120933ZThe articles of this volume will be reviewed individually. For the preceding conference see [Zbl 1507.68032].
Indexed articles:
\textit{Aguzzoli, Stefano; Bianchi, Matteo}, Amalgamation property for some varieties of BL-algebras generated by one finite set of BL-chains with finitely many components, 1-16 [Zbl 07728629]
\textit{Alm, Jeremy F.; Andrews, David; Levet, Michael}, Comer schemes, relation algebras, and the flexible atom conjecture, 17-33 [Zbl 07728630]
\textit{Berghammer, Rudolf; Winter, Michael}, A general method for representing sets of relations by vectors, 34-51 [Zbl 07728631]
\textit{Evangelou-Oost, Nasos; Bannister, Callum; Hayes, Ian J.}, Contextuality in distributed systems, 52-68 [Zbl 07728632]
\textit{Gil-Férez, José; Jipsen, Peter; Lodhia, Siddhartha}, The structure of locally integral involutive po-monoids and semirings, 69-86 [Zbl 07728633]
\textit{Glück, Roland}, Compatibility of refining and controlling plant automata with bisimulation quotients, 87-104 [Zbl 07728634]
\textit{Guttmann, Walter}, Dependences between domain constructions in heterogeneous relation algebras, 105-121 [Zbl 07728635]
\textit{Hopkins, Mark; Leiß, Hans}, Normal forms for elements of the *-continuous Kleene algebras \(K{\otimes_\mathcal{R}}C_2'\), 122-139 [Zbl 07728636]
\textit{Jipsen, Peter; Šemrl, Jaš}, Representable and diagonally representable weakening relation algebras, 140-157 [Zbl 07728637]
\textit{Kappé, Tobias}, Completeness and the finite model property for Kleene algebra, reconsidered, 158-175 [Zbl 07728638]
\textit{Kovács, Laura; Varonka, Anton}, What else is undecidable about loops?, 176-193 [Zbl 07728639]
\textit{Lewis-Smith, Andrew; Šemrl, Jaš}, Implication algebras and implication semigroups of binary relations, 194-207 [Zbl 07728640]
\textit{Sedlár, Igor}, On the complexity of Kleene algebra with domain, 208-223 [Zbl 07728641]
\textit{Shamsgovara, Arman}, Enumerating, cataloguing and classifying all quantales on up to nine elements, 224-240 [Zbl 07728642]
\textit{Heunen, Chris; Sigal, Jesse}, Duoidally enriched Freyd categories, 241-257 [Zbl 07728643]
\textit{Trancón y. Widemann, Baltasar; Lepper, Markus}, Towards a theory of conversion relations for prefixed units of measure, 258-273 [Zbl 07728644]
\textit{Winter, Michael}, Relational algebraic approach to the real numbers the additive group, 274-292 [Zbl 07728645]Prefacehttps://zbmath.org/1517.680172023-09-22T14:21:46.120933ZFrom the text: This special issue is dedicated to Professor Nelma Moreira and Professor Rogério Reis on the occasion of their special birthdays. The volume contains articles on recent research in the theory of automata, formal languages, and related topics.Prefacehttps://zbmath.org/1517.680182023-09-22T14:21:46.120933ZFrom the text: This special issue of the International Journal of Foundations of Computer Science contains eight revised and extended versions of the papers selected from those accepted at the 24th International Conference on Developments in Language Theory (DLT-2020).Algorithmic learning theory 2020. Proceedings of the 31st international conference (ALT 2020), San Diego, CA USA, February 8--11, 2020https://zbmath.org/1517.680202023-09-22T14:21:46.120933ZThe articles of this volume will be reviewed individually. For the preceding conference see [Zbl 1517.68013].Analysis, verification and transformation for declarative programming and intelligent systems. Essays dedicated to Manuel Hermenegildo on the occasion of his 60th birthdayhttps://zbmath.org/1517.680222023-09-22T14:21:46.120933ZThe articles of mathematical interest will be reviewed individually.26th international conference on theory and applications of satisfiability testing, SAT 2023, Alghero, Italy, July 4--8, 2023https://zbmath.org/1517.680232023-09-22T14:21:46.120933ZThe articles of this volume will be reviewed individually. For the preceding conference see [Zbl 1494.68012].Preface: Special issue: 25th international conference on developments in language theory (DLT 2021)https://zbmath.org/1517.680252023-09-22T14:21:46.120933ZFrom the text: This special issue of the International Journal of Foundations of Computer Science contains nine papers, which are revised and extended versions of the papers selected from the 25th International Conference on Developments in Language Theory (DLT 2021).Word equations and related topics. 1st international workshop, IWWERT '90, Tübingen, Germany, October 1--3, 1990. Proceedingshttps://zbmath.org/1517.680272023-09-22T14:21:46.120933ZThe articles of this volume will be reviewed individually.
Indexed articles:
\textit{Makanin, G. S.}, Investigations on equations in a free group, 1-11 [Zbl 07726630]
\textit{Kościelski, Antoni}, An analysis of Makanin's algorithm deciding solvability of equations in free groups, 12-60 [Zbl 07726631]
\textit{Abdulrab, Habib}, Implementation of Makanin's algorithm, 61-84 [Zbl 07726632]
\textit{Schulz, Klaus U.}, Makanin's algorithm for word equations -- two improvements and a generalization, 85-150 [Zbl 07726633]
\textit{Baader, Franz}, Unification theory, 151-170 [Zbl 07726634]
\textit{Bockmayr, Alexander}, Algebraic and logical aspects of unification, 171-180 [Zbl 07726635]
\textit{Bockmayr, Alexander}, Model-theoretic aspects of unification, 181-196 [Zbl 07726636]
\textit{Ohsuga, Akihiko; Sakai, Kô}, Complete equational unification based on an extension of the Knuth-Bendix completion procedure, 197-209 [Zbl 07726637]
\textit{Baader, Franz}, Unification in varieties of completely regular semigroups, 210-230 [Zbl 07726638]
\textit{Book, Ronald V.}, A note on confluent Thue systems, 231-236 [Zbl 07726639]
\textit{Wrathall, C.}, Confluence of one-rule Thue systems, 237-246 [Zbl 07726640]
\textit{Karhumäki, Juhani}, Systems of equations over a finite set of words and automata theory (extended abstract), 247-249 [Zbl 07726641]
\textit{Makanina, A. G.}, New systems of defining relations of the braid group, 250-256 [Zbl 07726642]Space lower bounds for the signal detection problemhttps://zbmath.org/1517.680442023-09-22T14:21:46.120933Z"Ellen, Faith"https://zbmath.org/authors/?q=ai:ellen.faith"Gelashvili, Rati"https://zbmath.org/authors/?q=ai:gelashvili.rati"Woelfel, Philipp"https://zbmath.org/authors/?q=ai:woelfel.philipp"Zhu, Leqi"https://zbmath.org/authors/?q=ai:zhu.leqiSummary: Many shared memory algorithms have to deal with the problem of determining whether the value of a shared object has changed in between two successive accesses of that object by a process when the responses from both are the same. Motivated by this problem, we define the \textit{signal detection problem}, which can be studied on a purely combinatorial level. Consider a system with \(n+1\) processes consisting of \(n\) readers and one signaller. The processes communicate through a shared \textit{blackboard} that can store a value from a domain of size \(m\). Processes are scheduled by an adversary. When scheduled, a process reads the blackboard, modifies its contents arbitrarily, and, provided it is a reader, returns a Boolean value. A reader must return \textit{true} if the signaller has taken a step since the reader's preceding step; otherwise it must return \textit{false}. Intuitively, in a system with \(n\) processes, signal detection should require at least \(n\) bits of shared information, i.e., \(m\geq 2^n\). But a proof of this conjecture remains elusive. For the general case, we prove a lower bound of \(m\geq n^2\). For restricted versions of the problem, where the processes are oblivious or where the signaller must write a fixed sequence of values, we prove a tight lower bound of \(m\geq 2^n\). We also consider a version of the problem where each reader takes at most two steps. In this case, we prove that \(m=n+1\) blackboard values are necessary and sufficient.Space lower bounds for the signal detection problemhttps://zbmath.org/1517.680452023-09-22T14:21:46.120933Z"Ellen, Faith"https://zbmath.org/authors/?q=ai:ellen.faith"Gelashvili, Rati"https://zbmath.org/authors/?q=ai:gelashvili.rati"Woelfel, Philipp"https://zbmath.org/authors/?q=ai:woelfel.philipp"Zhu, Leqi"https://zbmath.org/authors/?q=ai:zhu.leqiSummary: Many shared memory algorithms have to deal with the problem of determining whether the value of a shared object has changed in between two successive accesses of that object by a process when the responses from both are the same. Motivated by this problem, we define the signal detection problem, which can be studied on a purely combinatorial level. Consider a system with \(n+1\) processes consisting of \(n\) readers and one signaller. The processes communicate through a shared blackboard that can store a value from a domain of size \(m\). Processes are scheduled by an adversary. When scheduled, a process reads the blackboard, modifies its contents arbitrarily, and, provided it is a reader, returns a Boolean value. A reader must return true if the signaller has taken a step since the reader's preceding step; otherwise it must return false.\par Intuitively, in a system with \(n\) processes, signal detection should require at least \(n\) bits of shared information, i.e., \(m\ge 2^n\). But a proof of this conjecture remains elusive. We prove a lower bound of \(m\ge n^2\), as well as a tight lower bound of \(m\ge 2^n\) for two restricted versions of the problem, where the processes are oblivious or where the signaller always resets the blackboard to the same fixed value. We also consider a one-shot version of the problem, where each reader takes at most two steps. In this case, we prove that it is necessary and sufficient that the blackboard can store \(m=n+1\) values.
For the entire collection see [Zbl 1411.68018].Affine tasks for \(k\)-test-and-sethttps://zbmath.org/1517.680472023-09-22T14:21:46.120933Z"Kuznetsov, Petr"https://zbmath.org/authors/?q=ai:kuznetsov.petr"Rieutord, Thibault"https://zbmath.org/authors/?q=ai:rieutord.thibaultSummary: The paper proposes a surprisingly simple characterization of task computability of the wait-free shared-memory model in which processes, in addition to read-write registers, have access to \(k\)\textit{-test-and-set} objects. Our characterization is expressed in the form of an \textit{affine task}: a subcomplex of some iteration of the standard chromatic subdivision. This appears to be the first topological characterization of a model in which processes communicate via long-lived objects beyond read-write registers.
For the entire collection see [Zbl 1507.68029].A combinatorial characterization of self-stabilizing population protocolshttps://zbmath.org/1517.680482023-09-22T14:21:46.120933Z"Mathur, Shaan"https://zbmath.org/authors/?q=ai:mathur.shaan"Ostrovsky, Rafail"https://zbmath.org/authors/?q=ai:ostrovsky.rafail|ostrovsky.rafail-mSummary: We characterize self-stabilizing functions in population protocols for complete interaction graphs. In particular, we investigate self-stabilization in systems of \(n\) finite state agents in which a malicious scheduler selects an arbitrary sequence of pairwise interactions under a global fairness condition. We show a necessary and sufficient condition for self-stabilization. Specifically we show that functions without certain set-theoretic conditions are impossible to compute in a self-stabilizing manner. Our main contribution is in the converse, where we construct a self-stabilizing protocol for all other functions that meet this characterization. Our positive construction uses Dickson's Lemma to develop the notion of the root set, a concept that turns out to fundamentally characterize self-stabilization in this model. We believe it may lend to characterizing self-stabilization in more general models as well.
For the entire collection see [Zbl 1507.68029].On knowledge and communication complexity in distributed systemshttps://zbmath.org/1517.680542023-09-22T14:21:46.120933Z"Pfleger, Daniel"https://zbmath.org/authors/?q=ai:pfleger.daniel"Schmid, Ulrich"https://zbmath.org/authors/?q=ai:schmid.ulrichSummary: This paper contributes to exploring the connection between epistemic knowledge and communication complexity in distributed systems. We focus on Action Models, a well-known variant of dynamic epistemic logic, which allows to cleanly separate the state of knowledge of the processes and its update due to communication actions: exactly like the set of possible global states, the possible actions are described by means of a Kripke model that specifies which communication actions are indistinguishable for which process. We first show that the number of connected components in the action model results in a lower bound for communication complexity. We then apply this result, in the restricted setting of a two processor system, for determining communication complexity lower bounds for solving a distributed computing problem \(\mathcal{P}\): We first determine some properties of the action model corresponding to any given protocol that solves \(\mathcal{P}\), and then use our action model communication complexity lower bounds. Finally, we demonstrate our approach by applying it to synchronous distributed function computation and to a simple instance of consensus in directed dynamic networks.
For the entire collection see [Zbl 1400.68027].Time-optimal self-stabilizing leader election on rings in population protocolshttps://zbmath.org/1517.680622023-09-22T14:21:46.120933Z"Yokota, Daisuke"https://zbmath.org/authors/?q=ai:yokota.daisuke"Sudo, Yuichi"https://zbmath.org/authors/?q=ai:sudo.yuichi"Masuzawa, Toshimitsu"https://zbmath.org/authors/?q=ai:masuzawa.toshimitsuSummary: We propose a self-stabilizing leader election protocol on directed rings in the model of population protocols. Given an upper bound \(N\) on the population size \(n\), the proposed protocol elects a unique leader within \(O(nN)\) expected steps starting from any configuration and uses \(O(N)\) states. This convergence time is optimal if a given upper bound \(N\) is asymptotically tight, i.e., \(N=O(n)\).
For the entire collection see [Zbl 1507.68029].\textit{D\_PSNI}: delimited persistent stochastic non-interferencehttps://zbmath.org/1517.680662023-09-22T14:21:46.120933Z"Marin, Andrea"https://zbmath.org/authors/?q=ai:marin.andrea"Piazza, Carla"https://zbmath.org/authors/?q=ai:piazza.carla"Rossi, Sabina"https://zbmath.org/authors/?q=ai:rossi.sabinaSummary: Non-Interference is an information flow security property which aims to protect confidential data by ensuring the complete absence of any information flow from high level entities to low level ones. However, this requirement is too demanding when dealing with real applications: indeed, no real policy ever guarantees a total absence of information flow. In order to deal with real applications, it is often necessary to allow mechanisms for downgrading or declassifying information such as information filters and channel control. In this paper we introduce the notion of \textit{Delimited Persistent Stochastic Non-Interference} (\textit{D\_PSNI}) that allows information to flow from a higher to a lower security level through a downgrader. We provide two algebraic characterizations of \textit{D\_PSNI} and prove some compositionality properties. Finally, we present a decision algorithm and discuss its time complexity.The Scott model of PCF in univalent type theoryhttps://zbmath.org/1517.680692023-09-22T14:21:46.120933Z"de Jong, Tom"https://zbmath.org/authors/?q=ai:de-jong.tom-jSummary: We develop the Scott model of the programming language PCF in univalent type theory. Moreover, we work constructively and predicatively. To account for the non-termination in PCF, we use the lifting monad (also known as the partial map classifier monad) from topos theory, which has been extended to univalent type theory by Escardó and Knapp. Our results show that lifting is a viable approach to partiality in univalent type theory. Moreover, we show that the Scott model can be constructed in a predicative and constructive setting. Other approaches to partiality either require some form of choice or quotient inductive-inductive types. We show that one can do without these extensions.Type-based analysis of logarithmic amortised complexityhttps://zbmath.org/1517.680702023-09-22T14:21:46.120933Z"Hofmann, Martin"https://zbmath.org/authors/?q=ai:hofmann.martin.1"Leutgeb, Lorenz"https://zbmath.org/authors/?q=ai:leutgeb.lorenz"Obwaller, David"https://zbmath.org/authors/?q=ai:obwaller.david"Moser, Georg"https://zbmath.org/authors/?q=ai:moser.georg"Zuleger, Florian"https://zbmath.org/authors/?q=ai:zuleger.florianSummary: We introduce a novel amortised resource analysis couched in a type-and-effect system. Our analysis is formulated in terms of the physicist's method of amortised analysis and is potentialbased. The type system makes use of logarithmic potential functions and is the first such system to exhibit \textit{logarithmic amortised complexity}. With our approach, we target the automated analysis of self-adjusting data structures, like splay trees, which so far have only manually been analysed in the literature. In particular, we have implemented a semi-automated prototype, which successfully analyses the zig-zig case of \textit{splaying}, once the type annotations are fixed.A mathematical model of parallel programs and an approach based on it to verification of MPI programshttps://zbmath.org/1517.680732023-09-22T14:21:46.120933Z"Mironov, A. M."https://zbmath.org/authors/?q=ai:mironov.andrew-m(no abstract)A decision procedure for path feasibility of string manipulating programs with integer data typehttps://zbmath.org/1517.680742023-09-22T14:21:46.120933Z"Chen, Taolue"https://zbmath.org/authors/?q=ai:chen.taolue"Hague, Matthew"https://zbmath.org/authors/?q=ai:hague.matthew"He, Jinlong"https://zbmath.org/authors/?q=ai:he.jinlong"Hu, Denghang"https://zbmath.org/authors/?q=ai:hu.denghang"Lin, Anthony Widjaja"https://zbmath.org/authors/?q=ai:lin.anthony-widjaja"Rümmer, Philipp"https://zbmath.org/authors/?q=ai:rummer.philipp"Wu, Zhilin"https://zbmath.org/authors/?q=ai:wu.zhilinSummary: In this paper, we propose a decision procedure for a class of string-manipulating programs which includes not only a wide range of string operations such as concatenation, replaceAll, reverse, and finite transducers, but also those involving the integer data-type such as length, indexof, and substring. To the best of our knowledge, this represents one of the most expressive string constraint languages that is currently known to be decidable. Our decision procedure is based on a variant of cost register automata. We implement the decision procedure, giving rise to a new solver OSTRICH+. We evaluate the performance of OSTRICH+ on a wide range of existing and new benchmarks. The experimental results show that OSTRICH+ is the first string decision procedure capable of tackling finite transducers and integer constraints, whilst its overall performance is comparable with the state-of-the-art string constraint solvers.
For the entire collection see [Zbl 1502.68030].Implicit computation complexity in higher-order programming languages. A survey in memory of Martin Hofmannhttps://zbmath.org/1517.680752023-09-22T14:21:46.120933Z"Dal Lago, U."https://zbmath.org/authors/?q=ai:dal-lago.ugoSummary: This paper is meant to be a survey about implicit characterizations of complexity classes by fragments of higher-order programming languages, with a special focus on type systems and subsystems of linear logic. Particular emphasis will be put on Martin Hofmann's contributions to the subject, which very much helped in shaping the field.A metalanguage for guarded iterationhttps://zbmath.org/1517.680762023-09-22T14:21:46.120933Z"Goncharov, Sergey"https://zbmath.org/authors/?q=ai:goncharov.sergei-savostyanovich"Rauch, Christoph"https://zbmath.org/authors/?q=ai:rauch.christoph"Schröder, Lutz"https://zbmath.org/authors/?q=ai:schroder.lutzSummary: Notions of guardedness serve to delineate admissible recursive definitions in various settings in a compositional manner. In recent work, we have introduced an axiomatic notion of guardedness in symmetric monoidal categories, which serves as a unifying framework for various examples from program semantics, process algebra, and beyond. In the present paper, we propose a generic metalanguage for guarded iteration based on combining this notion with the fine-grain call-by-value paradigm, which we intend as a unifying programming language for guarded and unguarded iteration in the presence of computational effects. We give a generic (categorical) semantics of this language over a suitable class of strong monads supporting guarded iteration, and show it to be in touch with the standard operational behaviour of iteration by giving a concrete big-step operational semantics for a certain specific instance of the metalanguage and establishing adequacy for this case.
For the entire collection see [Zbl 1398.68027].A metalanguage for guarded iterationhttps://zbmath.org/1517.680772023-09-22T14:21:46.120933Z"Goncharov, Sergey"https://zbmath.org/authors/?q=ai:goncharov.sergei-savostyanovich"Rauch, Christoph"https://zbmath.org/authors/?q=ai:rauch.christoph"Schröder, Lutz"https://zbmath.org/authors/?q=ai:schroder.lutzSummary: Notions of guardedness serve to delineate admissible recursive definitions in various settings in a compositional manner. In recent work, we have introduced an axiomatic notion of guardedness in symmetric monoidal categories, which serves as a unifying framework for various examples from program semantics, process algebra, and beyond. In the present paper, we propose a generic \textit{metalanguage for guarded iteration} based on combining this notion with the fine-grain call-by-value paradigm, which we intend as a unifying programming language for guarded and unguarded iteration in the presence of computational effects. We give a generic (categorical) semantics of this language over a suitable class of strong monads supporting guarded iteration, and show it to be in touch with the standard operational behaviour of iteration by giving a concrete big-step operational semantics for a certain specific instance of the metalanguage and establishing soundness and (computational) adequacy for this case.Active objects with deterministic behaviourhttps://zbmath.org/1517.680782023-09-22T14:21:46.120933Z"Henrio, Ludovic"https://zbmath.org/authors/?q=ai:henrio.ludovic"Johnsen, Einar Broch"https://zbmath.org/authors/?q=ai:johnsen.einar-broch"Pun, Violet Ka I."https://zbmath.org/authors/?q=ai:pun.violet-ka-iSummary: Active objects extend the Actor paradigm with structured communication using method calls and futures. Active objects are, like actors, known to be data race free. Both are inherently concurrent, as they share a fundamental decoupling of communication and synchronisation. Both encapsulate their state, restricting access to one process at a time. Clearly, this rules out low-level races between two processes accessing a shared variable. However, is that sufficient to guarantee deterministic results from the execution of an active object program?
In this paper we are interested in so-called high-level races caused by the fact that the arrival order of messages between active objects can be non-deterministic, resulting in non-deterministic overall behaviour. We study this problem in the setting of a core calculus and identify restrictions on active object programs which are sufficient to guarantee deterministic behaviour for active object programs. We formalise these restrictions as a simple extension to the type system of the calculus and prove that well-typed programs exhibit deterministic behaviour .
For the entire collection see [Zbl 1507.68030].Ranking and repulsing supermartingales for reachability in probabilistic programshttps://zbmath.org/1517.680842023-09-22T14:21:46.120933Z"Takisaka, Toru"https://zbmath.org/authors/?q=ai:takisaka.toru"Oyabu, Yuichiro"https://zbmath.org/authors/?q=ai:oyabu.yuichiro"Urabe, Natsuki"https://zbmath.org/authors/?q=ai:urabe.natsuki"Hasuo, Ichiro"https://zbmath.org/authors/?q=ai:hasuo.ichiroSummary: Computing reachability probabilities is a fundamental problem in the analysis of probabilistic programs. This paper aims at a comprehensive and comparative account of various \textit{martingale-based methods} for over- and underapproximating reachability probabilities. Based on the existing works that stretch across different communities (formal verification, control theory, etc.), we offer a unifying account. In particular, we emphasize the role of order-theoretic fixed points -- a classic topic in computer science -- in the analysis of probabilistic programs. This leads us to two new martingale-based techniques, too. We also make an experimental comparison using our implementation of template-based synthesis algorithms for those martingales.
For the entire collection see [Zbl 1396.68018].On Tseitin formulas, read-once branching programs and treewidthhttps://zbmath.org/1517.680912023-09-22T14:21:46.120933Z"Glinskih, Ludmila"https://zbmath.org/authors/?q=ai:glinskih.ludmila"Itsykson, Dmitry"https://zbmath.org/authors/?q=ai:itsykson.dmitry-mSummary: We show that any nondeterministic read-once branching program that decides a satisfiable Tseitin formula based on an \(n\times n\) grid graph has size at least \(2^{\varOmega (n)}\). Then using the Excluded Grid theorem by Robertson and Seymour we show that for arbitrary graph \(G(V, E)\) any nondeterministic read-once branching program that computes a satisfiable Tseitin formula based on \(G\) has size at least \(2^{\varOmega (\operatorname{tw}(G)^\delta )}\) for all \(\delta <1/36\), where \(\operatorname{tw}(G)\) is the treewidth of \(G\) (for planar graphs and some other classes of graphs the statement holds for \(\delta =1)\). We also show an upper bound of \(O(|E| 2^{\operatorname{pw}(G)})\), where \(\operatorname{pw}(G)\) is the pathwidth of \(G\).
We apply the mentioned results to the analysis of the complexity of derivations in the proof system \(\mathrm{OBDD}(\land, \mathrm{reordering})\) and show that any \(\mathrm{OBDD}(\land, \mathrm{reordering})\)-refutation of an unsatisfiable Tseitin formula based on a graph \(G\) has size at least \(2^{\varOmega (\operatorname{tw}(G)^\delta )}\).
For the entire collection see [Zbl 1416.68013].On Tseitin formulas, read-once branching programs and treewidthhttps://zbmath.org/1517.680922023-09-22T14:21:46.120933Z"Glinskih, Ludmila"https://zbmath.org/authors/?q=ai:glinskih.ludmila"Itsykson, Dmitry"https://zbmath.org/authors/?q=ai:itsykson.dmitry-mSummary: We show that any nondeterministic read-once branching program that decides a satisfiable Tseitin formula based on an \(n\times n\) grid graph has size at least \(2^{ \Omega (n)}\). Then using the Excluded Grid Theorem by Robertson and Seymour we show that for an arbitrary graph \(G(V,E)\) any nondeterministic read-once branching program that computes a satisfiable Tseitin formula based on \(G\) has size at least \(2^{\Omega (\operatorname{tw}(G)^{\delta})}\) for all \(\delta<1/36\), where \(\operatorname{tw}(G)\) is the treewidth of \(G\) (for planar graphs and some other classes of graphs the statement holds for \(\delta = 1)\). We apply the mentioned results to the analysis of the complexity of derivations in the proof system \(\mathrm{OBDD}(\land, \mathrm{reordering})\) and show that any \(\mathrm{OBDD}(\land, \mathrm{reordering})\)-refutation of an unsatisfiable Tseitin formula based on a graph \(G\) has size at least \(2^{\Omega(\operatorname{tw}(G)^{\delta})}\). We also show an upper bound \(O(|E|2^{\operatorname{pw}(G)} )\) on the size of OBDD representations of a satisfiable Tseitin formula based on \(G\) and an upper bound \(O(|E||V| 2^{\operatorname{pw}(G)}+|\mathrm{TS}_{G,c}|^2)\) on the size of \(\mathrm{OBDD}(\land)\)-refutation of an unsatisifable Tseitin formula \(\mathrm{TS}_{G,c}\), where \(\operatorname{pw}(G)\) is the pathwidth of \(G\).Compressed range minimum querieshttps://zbmath.org/1517.680932023-09-22T14:21:46.120933Z"Jo, Seungbum"https://zbmath.org/authors/?q=ai:jo.seungbum"Mozes, Shay"https://zbmath.org/authors/?q=ai:mozes.shay"Weimann, Oren"https://zbmath.org/authors/?q=ai:weimann.orenSummary: Given a string \(S\) of \(n\) integers in \([0,\sigma )\), a range minimum query \({\mathsf{RMQ}}(i, j)\) asks for the index of the smallest integer in \(S[i \dots j]\). It is well known that the problem can be solved with a succinct data structure of size \(2n + o(n)\) and constant query-time. In this paper we show how to preprocess \(S\) into a \textit{compressed representation} that allows fast range minimum queries. This allows for \textit{sublinear} size data structures with logarithmic query time. The most natural approach is to use string compression and construct a data structure for answering range minimum queries directly on the compressed string. We investigate this approach using grammar compression. We then consider an alternative approach. Even if \(S\) is not compressible, its Cartesian tree necessarily is. Therefore, instead of compressing \(S\) using string compression, we compress the Cartesian tree of \(S\) using tree compression. We show that this approach can be exponentially better than the former, and is never worse by more than an \(O(\sigma )\) factor (i.e. for constant alphabets it is never asymptotically worse).
For the entire collection see [Zbl 1398.68028].A generic approach to the verification of the permutation property of sequential and parallel swap-based sorting algorithmshttps://zbmath.org/1517.680972023-09-22T14:21:46.120933Z"Safari, Mohsen"https://zbmath.org/authors/?q=ai:safari.mohsen"Huisman, Marieke"https://zbmath.org/authors/?q=ai:huisman.mariekeSummary: Sorting is one of the fundamental operations in computer science, and many sequential and parallel algorithms have been proposed in the literature. Swap-based sorting algorithms are one category of sorting algorithms where elements are swapped repeatedly to achieve the desired order. Since these algorithms are widely used in practice, their (functional) correctness, i.e., proving sortedness and permutation properties, is of utmost importance. However, proving the permutation property using automated program verifiers is much more challenging as the formal definition of this property involves existential quantifiers. In this paper, we propose a generic pattern to verify the permutation property for any sequential and parallel swap-based sorting algorithm automatically. To demonstrate our approach, we use VerCors, a verification tool based on separation logic for concurrent and parallel programs, to verify the permutation property of bubble sort, selection sort, insertion sort, parallel odd-even transposition sort, quick sort, two in-place merge sorts and TimSort for any arbitrary size of input.
For the entire collection see [Zbl 1507.68030].Characterizing tractability of simple well-designed pattern trees with projectionhttps://zbmath.org/1517.681022023-09-22T14:21:46.120933Z"Mengel, Stefan"https://zbmath.org/authors/?q=ai:mengel.stefan"Skritek, Sebastian"https://zbmath.org/authors/?q=ai:skritek.sebastianSummary: We study the complexity of evaluating well-designed pattern trees, a query language extending conjunctive queries with the possibility to define parts of the query to be optional. This possibility of optional parts is important for obtaining meaningful results over incomplete data sources as it is common in semantic web settings. Recently, a structural characterization of the classes of well-designed pattern trees that can be evaluated in polynomial time was shown. However, projection -- a central feature of many query languages -- was not considered in this study. We work towards closing this gap by giving a characterization of all tractable classes of simple well-designed pattern trees with projection (under some common complexity theoretic assumptions). Since well-designed pattern trees correspond to the fragment of well-designed \(\{\textsf{AND}, \textsf{OPTIONAL}\}\)-SPARQL queries this gives a complete description of the tractable classes of queries with projections in this fragment that can be characterized by the underlying graph structures of the queries. For non-simple pattern trees the tractability criteria for simple pattern trees do not capture all tractable classes. We thus extend the characterization for the non-simple case in order to capture some additional tractable cases.An adaptation-complete proof system for local reasoning about cloud storage systemshttps://zbmath.org/1517.681032023-09-22T14:21:46.120933Z"Jin, Zhao"https://zbmath.org/authors/?q=ai:jin.zhao"Zhang, Bowen"https://zbmath.org/authors/?q=ai:zhang.bowen"Zhang, Lei"https://zbmath.org/authors/?q=ai:zhang.lei.186"Cao, Yongzhi"https://zbmath.org/authors/?q=ai:cao.yongzhi"Wang, Hanpin"https://zbmath.org/authors/?q=ai:wang.hanpinSummary: The rapid growth of data presents a significant challenge to the capability of traditional storage technologies to collect and manage data. Cloud storage systems (CSSs) have been proposed as a method to improve storage capacity. To safely and effectively manage cloud storage data and improve data service quality, it is necessary to verify the correctness of CSS management programs. However, the complexity of these systems renders program verification difficult. In this paper, we propose a Hoare-style proof system, in conjunction with two languages, to analyze and verify CSS management programs. The first is a modeling language that describes the program execution. The second is an assertion language based on Separation Logic (SL), used to describe the properties of the CSS file-block-location storage structure. The proof system supports modular local reasoning for CSS programs by a set of adaptation rules, which enable the condition of specifications to be applied to broader contexts. A key question that arises is whether the proof system can meet adaptation completeness. If so, arbitrary satisfiable specifications can be adjusted using the adaptation rules. To this end, we developed local predicate transformers and used their domain to interpret all types of commands. By finding the smallest local predicate transformer, we established adaptation completeness. In summary, this work provides a formalization of automatic modular reasoning patterns and lays a theoretical foundation for the compositional program verification of CSSs.Bisimilarity distances for approximate differential privacyhttps://zbmath.org/1517.681082023-09-22T14:21:46.120933Z"Chistikov, Dmitry"https://zbmath.org/authors/?q=ai:chistikov.dmitry-v"Murawski, Andrzej S."https://zbmath.org/authors/?q=ai:murawski.andrzej-s"Purser, David"https://zbmath.org/authors/?q=ai:purser.davidSummary: Differential privacy is a widely studied notion of privacy for various models of computation. Technically, it is based on measuring differences between probability distributions. We study \(\epsilon ,\delta \)-differential privacy in the setting of labelled Markov chains. While the exact differences relevant to \(\epsilon ,\delta \)-differential privacy are not computable in this framework, we propose a computable bisimilarity distance that yields a sound technique for measuring \(\delta \), the parameter that quantifies deviation from pure differential privacy. We show this bisimilarity distance is always rational, the associated threshold problem is in \textbf{NP}, and the distance can be computed exactly with polynomially many calls to an \textbf{NP} oracle.
For the entire collection see [Zbl 1396.68018].Constructing reversible Turing machines in a reversible and conservative elementary triangular cellular automatonhttps://zbmath.org/1517.681132023-09-22T14:21:46.120933Z"Morita, Kenichi"https://zbmath.org/authors/?q=ai:morita.kenichiSummary: We study the problem of how we can construct reversible Turing machines (RTMs) compactly in a two-dimensional reversible cellular automaton (CA). The CA model used here is an elementary triangular partitioned CA (ETPCA) having an extremely simple local transition function. It has been shown that any RTM is realized in a reversible and non-conservative ETPCA No. 0347, where 0347 is an identification number in the class of 256 ETPCAs. In this paper, we show that it is also possible to construct RTMs in a reversible and conservative ETPCA 0137, which has very different features from ETPCA 0347, by a systematic and hierarchical manner. Here, a reversible logic element with memory (RLEM), rather than a reversible logic gate, is used in the basic level of the construction. In particular, a special type of an RLEM No. 4-31 is implemented in ETPCA 0137. Then RTMs are constructed using the RLEM pattern. By this, the construction of configurations that simulates RTMs is greatly simplified.Transactions and contracts based on reaction systemshttps://zbmath.org/1517.681142023-09-22T14:21:46.120933Z"Bottoni, Paolo"https://zbmath.org/authors/?q=ai:bottoni.paolo"Labella, Anna"https://zbmath.org/authors/?q=ai:labella.annaSummary: Smart contracts are currently \textit{en vogue}, thanks to the infrastructure provided by the blockchain technology. However, their effective use requires that the textual (legalese) specification of the contract be accompanied by a precise computational definition of the actions leading to its satisfaction or breach, as well as of their admissible sequences. Insofar as contracts can be viewed as prescribing transactional exchanges of well-specified resources among well-specified actors, contract execution can be modelled as following some protocol in a closed world. This suggests a modelling of such executions as interactive processes in reaction systems, where the entities in the background set represent possible allocations of resources to actors and reactions describe changes in such allocations. We use this type of reaction systems and interactive processes as a basis for the modelling of transactions and contracts and explore properties of such processes, highlighting their peculiarities with respect to the original notion of interactive processes in reaction systems. We also discuss several constructions for composition and decomposition of processes, which guarantee equivalence of effects: two interactive processes are equivalent if, starting from the same initial set of allocations, they produce the same final set of allocations.A process algebraic approach to reaction systemshttps://zbmath.org/1517.681152023-09-22T14:21:46.120933Z"Brodo, Linda"https://zbmath.org/authors/?q=ai:brodo.linda"Bruni, Roberto"https://zbmath.org/authors/?q=ai:bruni.roberto"Falaschi, Moreno"https://zbmath.org/authors/?q=ai:falaschi.morenoSummary: In the area of Natural Computing, Reaction Systems (RSs) are a qualitative abstraction inspired by the functioning of living cells, suitable to model the main mechanisms of biochemical reactions. RSs interact with a context, and pose challenges for modularity, compositionality, extendibility and behavioural equivalence. In this paper we define a modular encoding of RSs as processes in the chained Core Network Algebra (cCNA), which is a new variant of the \texttt{link}-calculus. The encoding represents the behaviour of each entity separately and preserves faithfully their features, and we prove its correctness and completeness. Our encoding provides a Labelled Transition System (LTS) semantics for RSs. Based on the LTS semantics, we adapt the classical notion of bisimulation to define a novel equivalence, called bio-similarity, for studying properties of RSs. In particular, we define a new assertion language based on regular expressions, which allows us to specify the properties of interest, and use it to extend Hennessy-Milner logic to our setting. We prove that our bio-similarity relation and the logical equivalence, that are defined parametrically on some assertion of interest, coincide. Finally, we claim that our encoding contributes to increase the expressiveness of RSs, by exploiting the interaction among different RSs.Freezing simulates non-freezing tile automatahttps://zbmath.org/1517.681162023-09-22T14:21:46.120933Z"Chalk, Cameron"https://zbmath.org/authors/?q=ai:chalk.cameron-t"Luchsinger, Austin"https://zbmath.org/authors/?q=ai:luchsinger.austin"Martinez, Eric"https://zbmath.org/authors/?q=ai:martinez.eric"Schweller, Robert"https://zbmath.org/authors/?q=ai:schweller.robert-t"Winslow, Andrew"https://zbmath.org/authors/?q=ai:winslow.andrew"Wylie, Tim"https://zbmath.org/authors/?q=ai:wylie.timSummary: Self-assembly is the process by which a system of particles randomly agitate and combine, through local interactions, to form larger complex structures. In this work, we fuse a particular well-studied generalization of tile assembly (the 2-handed or hierarchical tile assembly model) with concepts from cellular automata such as states and state transitions characterized by neighboring states. This allows for a simplification of the concepts from active self-assembly, and gives us machinery to relate the disparate existing models. We show that this model, coined tile automata, is invariant with respect to freezing and non-freezing transition rules via a simulation theorem showing that any non-freezing tile automata system can be simulated by a freezing one. Freezing tile automata systems restrict state transitions such that each tile may visit a state only once, i.e., a tile may undergo only a finite number of transitions. We conjecture that this result can be used to show that the signal-passing tile assembly model is also invariant to this constraint via a series of simulation results between that model and the tile automata model. Further, we conjecture that this model can be used to consolidate the several oft-studied models of self-assembly wherein assemblies may break apart, such as the signal-passing tile assembly model, the negative-glue 2-handed tile assembly model, and the size-dependent tile assembly model. Lastly, the tile automata model may prove useful in combining results in cellular automata with self-assembly.
For the entire collection see [Zbl 1396.68011].Know when to fold 'em: self-assembly of shapes by folding in oritatamihttps://zbmath.org/1517.681172023-09-22T14:21:46.120933Z"Demaine, Erik D."https://zbmath.org/authors/?q=ai:demaine.erik-d"Hendricks, Jacob"https://zbmath.org/authors/?q=ai:hendricks.jacob"Olsen, Meagan"https://zbmath.org/authors/?q=ai:olsen.meagan"Patitz, Matthew J."https://zbmath.org/authors/?q=ai:patitz.matthew-j"Rogers, Trent A."https://zbmath.org/authors/?q=ai:rogers.trent-a"Schabanel, Nicolas"https://zbmath.org/authors/?q=ai:schabanel.nicolas"Seki, Shinnosuke"https://zbmath.org/authors/?q=ai:seki.shinnosuke"Thomas, Hadley"https://zbmath.org/authors/?q=ai:thomas.hadleySummary: An oritatami system (OS) is a theoretical model of self-assembly via co-transcriptional folding. It consists of a growing chain of beads which can form bonds with each other as they are transcribed. During the transcription process, the \(\delta\) most recently produced beads dynamically fold so as to maximize the number of bonds formed, self-assemblying into a shape incrementally. The parameter \(\delta\) is called the delay and is related to the transcription rate in nature.
This article initiates the study of shape self-assembly using oritatami. A shape is a connected set of points in the triangular lattice. We first show that oritatami systems differ fundamentally from tile-assembly systems by exhibiting a family of infinite shapes that can be tile-assembled but cannot be folded by any OS. As it is NP-hard in general to determine whether there is an OS that folds into (self-assembles) a given finite shape, we explore the folding of upscaled versions of finite shapes. We show that any shape can be folded from a constant size seed, at any scale \(n\geqslant 3\), by an OS with delay 1. We also show that any shape can be folded at the smaller scale 2 by an OS with unbounded delay. This leads us to investigate the influence of delay and to prove that, for all \(\delta>2\), there are shapes that can be folded (at scale~1) with delay \(\delta\) but not with delay \(\delta'<\delta\).
These results serve as a foundation for the study of shape-building in this new model of self-assembly, and have the potential to provide better understanding of cotranscriptional folding in biology, as well as improved abilities of experimentalists to design artificial systems that self-assemble via this complex dynamical process.
For the entire collection see [Zbl 1396.68011].Self-assembly of 3-D structures using 2-D folding tileshttps://zbmath.org/1517.681182023-09-22T14:21:46.120933Z"Durand-Lose, Jérôme"https://zbmath.org/authors/?q=ai:durand-lose.jerome-olivier"Hendricks, Jacob"https://zbmath.org/authors/?q=ai:hendricks.jacob"Patitz, Matthew J."https://zbmath.org/authors/?q=ai:patitz.matthew-j"Perkins, Ian"https://zbmath.org/authors/?q=ai:perkins.ian"Sharp, Michael"https://zbmath.org/authors/?q=ai:sharp.michaelSummary: Self-assembly is a process which is ubiquitous in natural, especially biological systems. It occurs when groups of relatively simple components spontaneously combine to form more complex structures. While such systems have inspired a large amount of research into designing theoretical models of self-assembling systems, and even laboratory-based implementations of them, these artificial models and systems often tend to be lacking in one of the powerful features of natural systems (e.g. the assembly and folding of proteins), namely the dynamic reconfigurability of structures. In this paper, we present a new mathematical model of self-assembly, based on the abstract tile assembly model (aTAM), called the flexible tile assembly model (FTAM). In the FTAM, the individual components are 2-dimensional square tiles as in the aTAM, but in the FTAM, bonds between the edges of tiles can be flexible, allowing bonds to flex and entire structures to reconfigure, thus allowing 2-dimensional components to form 3-dimensional structures. We analyze the powers and limitations of FTAM systems by (1) demonstrating how flexibility can be controlled to carefully build desired structures, and (2) showing how flexibility can be beneficially harnessed to form structures which can ``efficiently'' reconfigure into many different configurations and/or greatly varying configurations. We also show that with such power comes a heavy burden in terms of computational complexity of simulation and prediction by proving that, for important properties of FTAM systems, determining their existence is intractable, even for properties which are easily computed for systems in less dynamic models.
For the entire collection see [Zbl 1396.68011].Optimizing tile set size while preserving proofreading with a DNA self-assembly compilerhttps://zbmath.org/1517.681192023-09-22T14:21:46.120933Z"Evans, Constantine G."https://zbmath.org/authors/?q=ai:evans.constantine-g"Winfree, Erik"https://zbmath.org/authors/?q=ai:winfree.erikSummary: Algorithmic DNA tile systems have the potential to allow the construction by self-assembly of large structures with complex nanometer-scale details out of relatively few monomer types, but are constrained by errors in growth and the limited sequence space of orthogonal DNA sticky ends that program tile interactions. We present a tile set optimization technique that, through analysis of algorithmic growth equivalence, potentially sensitive error pathways, and potential lattice defects, can significantly reduce the size of tile systems while preserving proofreading behavior that is essential for obtaining low error rates. Applied to systems implementing multiple algorithms that are far beyond the size of currently feasible implementations, the optimization technique results in systems that are comparable in size to already-implemented experimental systems.
For the entire collection see [Zbl 1396.68011].Linear bounds on the size of conformations in greedy deterministic oritatamihttps://zbmath.org/1517.681202023-09-22T14:21:46.120933Z"Fazekas, Szilárd Zsolt"https://zbmath.org/authors/?q=ai:fazekas.szilard-zsolt"Kim, Hwee"https://zbmath.org/authors/?q=ai:kim.hwee"Matsuoka, Ryuichi"https://zbmath.org/authors/?q=ai:matsuoka.ryuichi"Morita, Reoto"https://zbmath.org/authors/?q=ai:morita.reoto"Seki, Shinnosuke"https://zbmath.org/authors/?q=ai:seki.shinnosukeSummary: Oritatami is a computational model of RNA cotranscriptional folding, in which an RNA transcript is folding upon itself while being synthesized from its template DNA. This model is known to be Turing universal. Under the restriction on its parameters delay and arity both being 1, however, any deterministically foldable conformation is known to be at most ten times as large as its initial conformation (seed), and hence, the model becomes weaker. In this paper, we shall improve the size upper bound from \(10n\) down to \(4n+5\) and also provide a system that can fold into a conformation of size \(3n-20\). These tighter bounds result from a novel graph representation of deterministic oritatami folding pathways. We shall also study the case in which a transcript is trapped in a region closed by a seed and show that under this confinement, the upper bound is further improved to \(\frac{11}{3}n-5\).Comparing reactions in reaction systemshttps://zbmath.org/1517.681212023-09-22T14:21:46.120933Z"Genova, Daniela"https://zbmath.org/authors/?q=ai:genova.daniela"Hoogeboom, Hendrik Jan"https://zbmath.org/authors/?q=ai:hoogeboom.hendrik-jan"Kleijn, Jetty"https://zbmath.org/authors/?q=ai:kleijn.jettySummary: Originally, reaction systems were introduced to describe in a formal way the interactions between biochemical reactions taking place in living cells. They are also investigated as an abstract model of interactive computation. A reaction system is determined by a finite background set of entities and a finite set of reactions. Each reaction specifies the entities that it needs to be able to occur, the entities which block its execution, and the entities that it produces if it occurs. Based on the entities available in a state of the system, all reactions of the system that are enabled take place and together produce the entities that form the next state. In this paper we compare reactions in terms of their enabledness and results. We investigate three partial orders on reactions that build on two definitions of equivalence of (sets of) reactions. It is demonstrated how each partial order defines a lattice (with greatest lower bounds and least upper bounds) for all nontrivial reactions. Together, these orders provide an insight in possible redundancies and (re)combinations of the reactions of a reaction system.Forming tile shapes with simple robotshttps://zbmath.org/1517.681222023-09-22T14:21:46.120933Z"Gmyr, Robert"https://zbmath.org/authors/?q=ai:gmyr.robert"Hinnenthal, Kristian"https://zbmath.org/authors/?q=ai:hinnenthal.kristian"Kostitsyna, Irina"https://zbmath.org/authors/?q=ai:kostitsyna.irina"Kuhn, Fabian"https://zbmath.org/authors/?q=ai:kuhn.fabian"Rudolph, Dorian"https://zbmath.org/authors/?q=ai:rudolph.dorian"Scheideler, Christian"https://zbmath.org/authors/?q=ai:scheideler.christian"Strothmann, Thim"https://zbmath.org/authors/?q=ai:strothmann.thimSummary: Motivated by the problem of manipulating nanoscale materials, we investigate the problem of reconfiguring a set of tiles into certain shapes by robots with limited computational capabilities. As a first step towards developing a general framework for these problems, we consider the problem of rearranging a connected set of hexagonal tiles by a single deterministic finite automaton. After investigating some limitations of a single-robot system, we show that a feasible approach to build a particular shape is to first rearrange the tiles into an intermediate structure by performing very simple tile movements. We introduce three types of such intermediate structures, each having certain advantages and disadvantages. Each of these structures can be built in asymptotically optimal \(O(n^2)\) rounds, where \(n\) is the number of tiles. As a proof of concept, we give an algorithm for reconfiguring a set of tiles into an equilateral triangle through one of the intermediate structures. Finally, we experimentally show that the algorithm for building the simplest of the three intermediate structures can be modified to be executed by multiple robots in a distributed manner, achieving an almost linear speedup in the case where the number of robots is reasonably small.
For the entire collection see [Zbl 1396.68011].Construction of geometric structure by oritatami systemhttps://zbmath.org/1517.681232023-09-22T14:21:46.120933Z"Han, Yo-Sub"https://zbmath.org/authors/?q=ai:han.yo-sub"Kim, Hwee"https://zbmath.org/authors/?q=ai:kim.hweeSummary: Self-assembly is the process where smaller components autonomously assemble to form a larger and more complex structure. One of the application areas of self-assembly is engineering and production of complicated nanostructures. Recently, researchers proposed a new folding model called the oritatami model (OM) that simulates the cotranscriptional self-assembly, based on the kinetics on the final shape of folded molecules. Nanostructures in oritatami system (OS) are represented by a sequence of beads and interactions on the lattice. We propose a method to design a general OS, which we call GEOS, that constructs a given geometric structure. The main idea is to design small modular OSs, which we call hinges, for every possible pair of adjacent points in the target structure. Once a shape filling curve for the target structure is ready, we construct an appropriate primary structure that follows the curve by a sequence of hinges. We establish generalized guidelines on designing a GEOS, and propose two GEOSs.
For the entire collection see [Zbl 1396.68011].Transcript design problem of oritatami systemshttps://zbmath.org/1517.681242023-09-22T14:21:46.120933Z"Han, Yo-Sub"https://zbmath.org/authors/?q=ai:han.yo-sub"Kim, Hwee"https://zbmath.org/authors/?q=ai:kim.hwee"Seki, Shinnosuke"https://zbmath.org/authors/?q=ai:seki.shinnosukeSummary: RNA cotranscriptional folding refers to the phenomenon in which an RNA transcript folds upon itself while being synthesized out of a gene. Oritatami model is a computation model of this phenomenon, which lets its sequence (transcript) of beads (abstract molecules) fold cotranscriptionally by the interactions between beads according to its ruleset. We study the problem of designing a transcript that folds into the given conformation using the given ruleset, which is called the transcript design problem. We prove that the problem is computationally difficult to solve (NP-hard). Then we design efficient poly-time algorithms with additional restrictions on the oritatami system.
For the entire collection see [Zbl 1396.68011].Hierarchical growth is necessary and (sometimes) sufficient to self-assemble discrete self-similar fractalshttps://zbmath.org/1517.681252023-09-22T14:21:46.120933Z"Hendricks, Jacob"https://zbmath.org/authors/?q=ai:hendricks.jacob"Opseth, Joseph"https://zbmath.org/authors/?q=ai:opseth.joseph"Patitz, Matthew J."https://zbmath.org/authors/?q=ai:patitz.matthew-j"Summers, Scott M."https://zbmath.org/authors/?q=ai:summers.scott-mSummary: In this paper, we prove that in the abstract tile assembly model (aTAM), an accretion-based model which only allows for a single tile to attach to a growing assembly at each step, there are no tile assembly systems capable of self-assembling the discrete self-similar fractals known as the ``H'' and ``U'' fractals. We then show that in a related model which allows for hierarchical self-assembly, the 2-handed assembly model (2HAM), there does exist a tile assembly systems which self-assembles the ``U'' fractal and conjecture that the same holds for the ``H'' fractal. This is the first example of discrete self similar fractals which self-assemble in the 2HAM but not in the aTAM, providing a direct comparison of the models and greater understanding of the power of hierarchical assembly.
For the entire collection see [Zbl 1396.68011].Asynchrony and persistence in reaction systemshttps://zbmath.org/1517.681262023-09-22T14:21:46.120933Z"Koutny, Maciej"https://zbmath.org/authors/?q=ai:koutny.maciej"Pietkiewicz-Koutny, Marta"https://zbmath.org/authors/?q=ai:pietkiewicz-koutny.marta"Yakovlev, Alex"https://zbmath.org/authors/?q=ai:yakovlev.alexandre-vSummary: Reaction systems are a model of interactive computation, where the interaction between a system -- itself built up of a number of reactions -- and its environment is modelled through context sequences provided by the environment. The standard execution semantics of reaction systems is synchronous, i.e., at each computational step all the enabled reactions are executed. In this paper, we `de-synchronise' such an execution model by allowing only a subset of enabled reactions to be executed. We then study the resulting asynchronous model assuming two fundamental execution policies. The first one allows any subset of reactions to be executed, and the second one draws each subset from a pre-defined pool. We also introduce and discuss the notion of persistence of reactions and sets of reactions in the resulting models of asynchronous reaction systems. In particular, we demonstrate that reaction persistence can be implemented.Non-preserving accepting splicing systemshttps://zbmath.org/1517.681272023-09-22T14:21:46.120933Z"Mitrana, Victor"https://zbmath.org/authors/?q=ai:mitrana.victor"Păun, Andrei"https://zbmath.org/authors/?q=ai:paun.andrei"Păun, Mihaela"https://zbmath.org/authors/?q=ai:paun.mihaela"Sánchez Martín, José Ángel"https://zbmath.org/authors/?q=ai:martin.jose-angel-sanchezSummary: We define a variant of accepting splicing system such that the history preserving property is dropped, namely every new generation of strings is obtained by applying splicing to the set of strings of the previous generation altogether with a predefined finite set of axioms. The condition for halting the computation is defined by a finite set of strings. The computation halts, and the input string is accepted, as soon as a string in the halting set is obtained. We present here simulations of two computationally complete models: 2-tag systems and Turing machines, both deterministic and nondeterministic. Although all these models are computationally complete and can be simulated by each other, we are interested to investigate the computational as well as descriptional complexity of our direct simulations.Temporal DNA barcodes: a time-based approach for single-molecule imaginghttps://zbmath.org/1517.681282023-09-22T14:21:46.120933Z"Shah, Shalin"https://zbmath.org/authors/?q=ai:shah.shalin"Reif, John"https://zbmath.org/authors/?q=ai:reif.john-hSummary: In the past decade, single-molecule imaging has opened new opportunities to understand reaction kinetics of molecular systems. DNA-PAINT uses transient binding of DNA strands to perform super-resolution fluorescence imaging. An interesting challenge in DNA nanoscience and related fields is the unique identification of single-molecules. While wavelength multiplexing (using fluorescent dyes of different colors) can be used to increase the number of distinguishable targets, the resultant total number of targets is still limited by the number of dyes with non-overlapping spectra. In this work, we introduce the use of time-domain to develop a DNA-based reporting framework for unique identification of single-molecules. These fluorescent DNA devices undergo a series of conformational transformations that result in (unique) time-changing intensity signals. We define this stochastic temporal intensity trace as the device's temporal barcode since it can uniquely identify the corresponding DNA device if the collection time is long enough. Our barcodes work with as few as one dye making them easy to design, extremely low-cost, and greatly simplifying the hardware setup. In addition, by adding multiple dyes, we can create a much larger family of uniquely identifiable reporter molecules. Finally, our devices are designed to follow the principle of transient binding and can be imaged using total internal reflection fluorescence (TIRF) microscopes so they are not susceptible to photo-bleaching, allowing us to monitor their activity for extended time periods. We model our devices using continuous-time Markov chains (CTMCs) and simulate their behavior using a stochastic simulation algorithm (SSA). These temporal barcodes are later analyzed and classified in their parameter space. The results obtained from our simulation experiments can provide crucial insights for collecting experimental data.
For the entire collection see [Zbl 1396.68011].A content-addressable DNA database with learned sequence encodingshttps://zbmath.org/1517.681292023-09-22T14:21:46.120933Z"Stewart, Kendall"https://zbmath.org/authors/?q=ai:stewart.kendall"Chen, Yuan-Jyue"https://zbmath.org/authors/?q=ai:chen.yuan-jyue"Ward, David"https://zbmath.org/authors/?q=ai:ward.david-d|ward.david-g|ward.david-j"Liu, Xiaomeng"https://zbmath.org/authors/?q=ai:liu.xiaomeng"Seelig, Georg"https://zbmath.org/authors/?q=ai:seelig.georg"Strauss, Karin"https://zbmath.org/authors/?q=ai:strauss.karin"Ceze, Luis"https://zbmath.org/authors/?q=ai:ceze.luisSummary: We present strand and codeword design schemes for a DNA database capable of approximate similarity search over a multidimensional dataset of content-rich media. Our strand designs address cross-talk in associative DNA databases, and we demonstrate a novel method for learning DNA sequence encodings from data, applying it to a dataset of tens of thousands of images. We test our design in the wetlab using one hundred target images and ten query images, and show that our database is capable of performing similarity-based enrichment: on average, visually similar images account for 30\% of the sequencing reads for each query, despite making up only 10\% of the database.
For the entire collection see [Zbl 1396.68011].CRN++: molecular programming languagehttps://zbmath.org/1517.681302023-09-22T14:21:46.120933Z"Vasic, Marko"https://zbmath.org/authors/?q=ai:vasic.marko"Soloveichik, David"https://zbmath.org/authors/?q=ai:soloveichik.david"Khurshid, Sarfraz"https://zbmath.org/authors/?q=ai:khurshid.sarfrazSummary: Synthetic biology is a rapidly emerging research area, with expected wide-ranging impact in biology, nanofabrication, and medicine. A key technical challenge lies in embedding computation in molecular contexts where electronic micro-controllers cannot be inserted. This necessitates effective representation of computation using molecular components. While previous work established the Turing-completeness of chemical reactions, defining representations that are faithful, efficient, and practical remains challenging. This paper introduces CRN++, a new language for programming deterministic (mass-action) chemical kinetics to perform computation. We present its syntax and semantics, and build a compiler translating CRN++ programs into chemical reactions, thereby laying the foundation of a comprehensive framework for molecular programming. Our language addresses the key challenge of embedding familiar imperative constructs into a set of chemical reactions happening simultaneously and manipulating real-valued concentrations. Although some deviation from ideal output value cannot be avoided, we develop methods to minimize the error, and implement error analysis tools. We demonstrate the feasibility of using CRN++ on a suite of well-known algorithms for discrete and real-valued computation. CRN++ can be easily extended to support new commands or chemical reaction implementations, and thus provides a foundation for developing more robust and practical molecular programs.
For the entire collection see [Zbl 1396.68011].A reaction network scheme which implements the EM algorithmhttps://zbmath.org/1517.681312023-09-22T14:21:46.120933Z"Viswa Virinchi, Muppirala"https://zbmath.org/authors/?q=ai:virinchi.muppirala-viswa"Behera, Abhishek"https://zbmath.org/authors/?q=ai:behera.abhishek"Gopalkrishnan, Manoj"https://zbmath.org/authors/?q=ai:gopalkrishnan.manojSummary: A detailed algorithmic explanation is required for how a network of chemical reactions can generate the sophisticated behavior displayed by living cells. Though several previous works have shown that reaction networks are computationally universal and can in principle implement any algorithm, there is scope for constructions that map well onto biological reality, make efficient use of the computational potential of the native dynamics of reaction networks, and make contact with statistical mechanics. We describe a new reaction network scheme for solving a large class of statistical problems. Specifically we show how reaction networks can implement information projection, and consequently a generalized expectation-maximization algorithm, to solve maximum likelihood estimation problems in partially-observed exponential families on categorical data. Our scheme can be thought of as an algorithmic interpretation of E. T. Jaynes's vision of statistical mechanics as statistical inference [Zbl 0084.43701].
For the entire collection see [Zbl 1396.68011].Multiparty cardinality testing for threshold private intersectionhttps://zbmath.org/1517.681322023-09-22T14:21:46.120933Z"Branco, Pedro"https://zbmath.org/authors/?q=ai:branco.pedro"Döttling, Nico"https://zbmath.org/authors/?q=ai:dottling.nico"Pu, Sihang"https://zbmath.org/authors/?q=ai:pu.sihangSummary: Threshold Private Set Intersection (PSI) allows multiple parties to compute the intersection of their input sets if and only if the intersection is larger than \(n-t\), where \(n\) is the size of each set and \(t\) is some threshold. The main appeal of this primitive is that, in contrast to standard PSI, known upper-bounds on the communication complexity only depend on the threshold \(t\) and not on the sizes of the input sets. Current threshold PSI protocols split themselves into two components: A Cardinality Testing phase, where parties decide if the intersection is larger than some threshold; and a PSI phase, where the intersection is computed. The main source of inefficiency of threshold PSI is the former part.
In this work, we present a new Cardinality Testing protocol that allows \(N\) parties to check if the intersection of their input sets is larger than \(n-t\). The protocol incurs in \(\tilde{ \mathcal{O}} (Nt^2)\) communication complexity. We thus obtain a Threshold PSI scheme for \(N\) parties with communication complexity \(\tilde{\mathcal{O}}(Nt^2)\).
For the entire collection see [Zbl 1476.94004].Computational irrelevancy: bridging the gap between pseudo- and real randomness in MPC protocolshttps://zbmath.org/1517.681332023-09-22T14:21:46.120933Z"Heseri, Nariyasu"https://zbmath.org/authors/?q=ai:heseri.nariyasu"Nuida, Koji"https://zbmath.org/authors/?q=ai:nuida.kojiSummary: Due to the fact that classical computers cannot efficiently obtain random numbers, it is common practice to design cryptosystems in terms of real random numbers and then replace them with cryptographically secure pseudorandom ones for concrete implementations. However, as pointed out by the previous work [the second author, Lect. Notes Comput. Sci. 12711, 441--468 (2021; Zbl 1517.68135)], this technique may lead to compromise of security in secure multiparty computation (MPC) protocols, due to the property that a seed for a pseudorandom generator (PRG) is visible by an adversary in the context of MPC. Although this work suggested to use information-theoretically secure protocols (together with PRGs with high min-entropy) to alleviate the problem, yet it is preferable to base the security on computational assumptions rather than the stronger information-theoretic ones. By observing that the contrived constructions in the aforementioned work use MPC protocols and PRGs that are closely related to each other, we notice that it may help to alleviate the problem by using protocols and PRGs that are ``unrelated'' to each other. In this paper, we propose a notion called ``computational irrelevancy'' to formalise the term ``unrelated'' and under this condition provide a security guarantee under computational assumptions.
For the entire collection see [Zbl 1503.68013].The power of distributed verifiers in interactive proofshttps://zbmath.org/1517.681342023-09-22T14:21:46.120933Z"Naor, Moni"https://zbmath.org/authors/?q=ai:naor.moni"Parter, Merav"https://zbmath.org/authors/?q=ai:parter.merav"Yogev, Eylon"https://zbmath.org/authors/?q=ai:yogev.eylonCryptographic pseudorandom generators can make cryptosystems problematichttps://zbmath.org/1517.681352023-09-22T14:21:46.120933Z"Nuida, Koji"https://zbmath.org/authors/?q=ai:nuida.kojiSummary: Randomness is an essential resource for cryptography. For practical randomness generation, the security notion of pseudorandom generators (PRGs) intends to automatically preserve (computational) security of cryptosystems when used in implementation. Nevertheless, some opposite case such as in computational randomness extractors [\textit{B. Barak} et al., Lect. Notes Comput. Sci. 6841, 1--20 (2011; Zbl 1287.94047)] is known (but not yet systematically studied so far) where the security can be lost even by applying secure PRGs. The present paper aims at pushing ahead the observation and understanding about such a phenomenon; we reveal such situations at layers of primitives and protocols as well, not just of building blocks like randomness extractors. We present three typical types of such cases: (1) adversaries can legally see the seed of the PRGs (including the case of randomness extractors); (2) the set of ``bad'' randomness may be not efficiently recognizable; (3) the formulation of a desired property implicitly involves non-uniform distinguishers for PRGs. We point out that the semi-honest security of multiparty computation also belongs to Type 1, while the correctness with negligible decryption error probability for public key encryption belongs to Types 2 and 3. We construct examples for each type where a secure PRG (against uniform distinguishers only, for Type 3) does not preserve the security/correctness of the original scheme; and discuss some countermeasures to avoid such an issue.
For the entire collection see [Zbl 1476.94004].Compressed communication complexity of longest common prefixeshttps://zbmath.org/1517.681362023-09-22T14:21:46.120933Z"Bille, Philip"https://zbmath.org/authors/?q=ai:bille.philip"Berggreen Ettienne, Mikko"https://zbmath.org/authors/?q=ai:berggreen-ettienne.mikko"Grossi, Roberto"https://zbmath.org/authors/?q=ai:grossi.roberto"Gørtz, Inge Li"https://zbmath.org/authors/?q=ai:gortz.inge-li"Rotenberg, Eva"https://zbmath.org/authors/?q=ai:rotenberg.evaSummary: We consider the communication complexity of fundamental longest common prefix (\textsc{Lcp}) problems. In the simplest version, two parties, Alice and Bob, each hold a string, \(A\) and \(B\), and we want to determine the length of their longest common prefix \(\ell =\textsc{Lcp}(A,B)\) using as few rounds and bits of communication as possible. We show that if the longest common prefix of \(A\) and \(B\) is compressible, then we can significantly reduce the number of rounds compared to the optimal uncompressed protocol, while achieving the same (or fewer) bits of communication. Namely, if the longest common prefix has an LZ77 parse of \(z\) phrases, only \(O(\lg z)\) rounds and \(O(\lg \ell )\) total communication is necessary. We extend the result to the natural case when Bob holds a set of strings \(B_1, \ldots , B_k\), and the goal is to find the length of the maximal longest prefix shared by \(A\) and any of \(B_1, \ldots , B_k\). Here, we give a protocol with \(O(\log z)\) rounds and \(O(\lg z \lg k + \lg \ell )\) total communication. We present our result in the public-coin model of computation but by a standard technique our results generalize to the private-coin model. Furthermore, if we view the input strings as integers the problems are the greater-than problem and the predecessor problem.
For the entire collection see [Zbl 1398.68028].Communication complexity in vertex partition whiteboard modelhttps://zbmath.org/1517.681372023-09-22T14:21:46.120933Z"Jurdzinski, Tomasz"https://zbmath.org/authors/?q=ai:jurdzinski.tomasz"Lorys, Krzysztof"https://zbmath.org/authors/?q=ai:lorys.krzysztof"Nowicki, Krzysztof"https://zbmath.org/authors/?q=ai:nowicki.krzysztofSummary: We study the multi-party communication model, where players correspond to the nodes of a graph and each player knows its neighbors in the input graph. The players can send messages on a whiteboard which are immediately available to each player. Eventually, the referee which knows only messages on the whiteboard is supposed to give a solution to the considered (graph) problem. We distinguish between oblivious and adaptive variant of the model. The former model is related to simultaneous multi-party communication complexity, while the latter is closely related to so-called broadcast congested clique.
Communication complexity is the maximum over all nodes of the sizes of messages put on the whiteboard by a node. Our goal is to study the impact of adaptivity on communication complexity of graph problems. We show that there exists an infinite hierarchy of problems with respect to the number of rounds for constant size messages. Moreover, motivated by unsuccessful attempts to establish non-adaptive communication complexity of graph connectivity in recent years, we study the connectivity problem in the severely restricted class of two-regular graphs. We determine an asymptotically tight bound on communication complexity in the oblivious model and provide \(\omega(1)\) lower bound on the number of rounds in the adaptive model for some message size \(b(n)=\omega(1)\).
For the entire collection see [Zbl 1400.68027].Approximating any logic program by a CS-programhttps://zbmath.org/1517.681382023-09-22T14:21:46.120933Z"Boichut, Yohan"https://zbmath.org/authors/?q=ai:boichut.yohan"Pelletier, Vivien"https://zbmath.org/authors/?q=ai:pelletier.vivien"Réty, Pierre"https://zbmath.org/authors/?q=ai:rety.pierreSummary: In this paper, we propose an extension of a technique transforming logic programs into a particular class of logic programs called CS-programs. Up to now, this technique is a semi-algorithm preserving the least Herbrand model. We integrate in this technique a process of generalization. Thanks to it, we are able to make the computation (the transformation) terminate and if we force the computation to terminate then we obtain a CS-program whose least Herbrand model contains the initial one. In this way, we can tackle successfully reachability problems that are out of the scope of techniques using regular approximations and also of the initial transformation technique (for which computations do not terminate).
For the entire collection see [Zbl 1398.68038].Physical zero-knowledge proof for Suguru puzzlehttps://zbmath.org/1517.681392023-09-22T14:21:46.120933Z"Robert, Léo"https://zbmath.org/authors/?q=ai:robert.leo"Miyahara, Daiki"https://zbmath.org/authors/?q=ai:miyahara.daiki"Lafourcade, Pascal"https://zbmath.org/authors/?q=ai:lafourcade.pascal"Mizuki, Takaaki"https://zbmath.org/authors/?q=ai:mizuki.takaakiSummary: Suguru is a paper and pencil puzzle invented by Naoki Inaba. The goal of the game is to fulfil a grid with numbers between 1 and 5 and to respect three simple constraints. In this paper we design a physical Zero-Knowledge Proof (ZKP) protocol for Suguru. A ZKP protocol allows a prover (P) to prove that he knows a solution of a Suguru grid to a verifier (V) without leaking any information on the solution. For constructing such a physical ZKP protocol, we only rely on a small number of physical cards and an adapted encoding. For a grid of Suguru with \(n\) cells, we only use \(5n+5\) cards. Moreover, we prove the three classical security properties of a ZKP: completeness, extractability, and zero-knowledge.
For the entire collection see [Zbl 1507.68029].Descriptive complexity of deterministic polylogarithmic time and spacehttps://zbmath.org/1517.681402023-09-22T14:21:46.120933Z"Ferrarotti, Flavio"https://zbmath.org/authors/?q=ai:ferrarotti.flavio-antonio"González, Senén"https://zbmath.org/authors/?q=ai:gonzalez.senen"Turull Torres, José María"https://zbmath.org/authors/?q=ai:turull-torres.jose-maria"Van den Bussche, Jan"https://zbmath.org/authors/?q=ai:van-den-bussche.jan"Virtema, Jonni"https://zbmath.org/authors/?q=ai:virtema.jonniThis paper presents model-theoretic representations of POLYLOGTIME and POLYLOGSPACE and, to this end, presents a variant of the Random Access Machine, called the ``Direct Access Machine'', and an associated logic, called ``Index Logic''. Given a finite ordered structure \(\mathbf A = (A, R_1^{\mathbf A}, \ldots, R_p^{\mathbf A}, c_1^{\mathbf A}, \ldots, c_q^{\mathbf A}, f_1^{\mathbf A}, \ldots, f_s^{\mathbf A})\) of binary encoding \(\operatorname{bin}(\mathbf A)\), where \(A\) has \(n\) elements and \(\operatorname{bin}(\mathbf A)\) has \(\hat{n}\), a direct access machine has \(r_i\) ``address'' work tapes for each \(r_i\)-ary relation \(R_i\), \(k_j\) ``address'' work tapes for each \(k_j\)-argument function \(f_j\) (along with a read-only ``value tape'' for each function), \(q + 1\) tapes for the \(q\) constants, plus several other work tapes, and the mechanism is designed to (passively) enforce logarithmic space bounds on the tapes.
If the binary code of an \(r_i\)-tuple \(\mathbf x\) is entered on the address work tape for \(R_i\), the machine produces the value \(0\) or \(1\), depending on whether or not \(\mathbf A, \mathbf x \models R_i\) and the state transition function for that tape uses that value in computing the next state and determining head movement on that tape. Similarly, if the binary code of a \(k_j\)-tuple \(\mathbf y\) is entered on the address work tape for \(f_j\), the binary code for \(f_j(\mathbf y)\) spontaneously appears on the \(j\)th value tape, which can then be used in the computation. The operation for constants is similar.
Index Logic has two sorts of variables, those that range over the domain of the input structure and those that range over \(\operatorname{Num}(\mathbf A) = \{ 0, 1, \ldots, \lceil \log n \rceil - 1 \}\) (where \(n\) is the cardinality of the domain of the input structure). The syntax is typical for a fixed-point logic, except for terms for accessing \(A\)-valued elements of given binary representations (and vice versa) and that fixed points are derived for \(\operatorname{Num}(\mathbf A)\)-valued variables.
Once these constructions are completed, the article presents proofs that Index Logic + Inflationary Fixed Point captures POLYLOGTIME (using direct access machines) and that Index Logic + Partial Fixed Point captures POLYLOGSPACE (random access machines may be used here).
Reviewer: Gregory Loren McColm (Tampa)On matching generalised repetitive patternshttps://zbmath.org/1517.681412023-09-22T14:21:46.120933Z"Day, Joel D."https://zbmath.org/authors/?q=ai:day.joel-d"Fleischmann, Pamela"https://zbmath.org/authors/?q=ai:fleischmann.pamela"Manea, Florin"https://zbmath.org/authors/?q=ai:manea.florin"Nowotka, Dirk"https://zbmath.org/authors/?q=ai:nowotka.dirk"Schmid, Markus L."https://zbmath.org/authors/?q=ai:schmid.markus-lSummary: A pattern is a string with terminals and variables (which can be uniformly replaced by terminal words). Given a class \(\mathcal{C}\) of patterns (with variables), we say a pattern \(\alpha\) is a \(\mathcal{C}\)-(pseudo-)repetition if its skeleton -- the result of removing all terminal symbols to leave only the variables -- is a (pseudo-)repetition of a pattern from \(\mathcal{C}\). We introduce a large class of patterns which generalises several known classes such as the \(k\)-local and bounded scope coincidence degree patterns, and show that for this class, \( \mathcal{C}\)-(pseudo-)repetitions can be matched in polynomial time. We also show that for most classes \(\mathcal{C}\), the class of \(\mathcal{C}\)-(pseudo-)repetitions does not have bounded treewidth. Finally, we show that if the notion of repetition is relaxed, so that in each occurrence the variables may occur in a different order, the matching problem is NP-complete, even in severely restricted cases.
For the entire collection see [Zbl 1398.68030].Synchronizing words and monoid factorization: a parameterized perspectivehttps://zbmath.org/1517.681422023-09-22T14:21:46.120933Z"Bruchertseifer, Jens"https://zbmath.org/authors/?q=ai:bruchertseifer.jens"Fernau, Henning"https://zbmath.org/authors/?q=ai:fernau.henningSummary: The concept of a synchronizing word is a very important notion in the theory of finite automata. We consider the associated decision problem to decide if a given DFA possesses a synchronizing word of length at most \(k\), where \(k\) is the standard parameter. We show that this problem DFA-SW is equivalent to the problem \textsc{Monoid Factorization} introduced by Cai, Chen, Downey and Fellows. Apart from the known \textsf{W}[2]-hardness results, we show that these problems belong to \textsf{A}[2], \textsf{W}[P] and \textsf{WNL}. This indicates that DFA-SW is not complete for any of these classes and hence, we suggest a new parameterized complexity class \textsf{W}[\textsf{Sync}] as a proper home for these (and more) problems.
For the entire collection see [Zbl 1502.68022].Balanced stable marriage: how close is close enough?https://zbmath.org/1517.681432023-09-22T14:21:46.120933Z"Gupta, Sushmita"https://zbmath.org/authors/?q=ai:gupta.sushmita"Roy, Sanjukta"https://zbmath.org/authors/?q=ai:roy.sanjukta"Saurabh, Saket"https://zbmath.org/authors/?q=ai:saurabh.saket"Zehavi, Meirav"https://zbmath.org/authors/?q=ai:zehavi.meiravSummary: Balanced Stable Marriage (BSM) is a central optimization version of the classic Stable Marriage (SM) problem. We study BSM from the viewpoint of Parameterized Complexity. Informally, the input of BSM consists of \(n\) men, \(n\) women, and an integer \(k\). Each person \(a\) has a (sub)set of acceptable partners, \(\mathcal{A}(a)\), who \(a\) ranks strictly; we use \(p_a(b)\) to denote the position of \(b\in\mathcal{A}(a)\) in \(a\)'s preference list. The objective is to decide whether there exists a stable matching \(\mu\) such that \(\mathsf{balance}(\mu)\triangleq\max\{\sum_{(m,w)\in\mu}p_m(w), \sum_{(m,w)\in\mu}p_w(m)\}\le k\). In SM, all stable matchings match the same set of agents, \(A^\star\) which can be computed in polynomial time. As \(\mathsf{balance}(\mu)\ge\frac{|A^\star |}{2}\) for any stable matching \(\mu\), BSM is trivially fixed-parameter tractable (FPT) with respect to \(k\). Thus, a natural question is whether BSM is FPT with respect to \(k-\frac{|A^\star|}{2}\). With this viewpoint in mind, we draw a line between tractability and intractability in relation to the target value. This line separates additional natural parameterizations higher/lower than ours (e.g., we automatically resolve the parameterization \(k-\frac{|A^\star|}{2})\). The two extreme stable matchings are the man-optimal \(\mu_M\) and the woman-optimal \(\mu_W\). Let \(O_M=\sum_{(m,w)\in\mu_M}p_m(w)\), and \(O_W=\sum_{(m,w)\in \mu_W}p_w(m)\). In this work, we prove that
\begin{itemize}
\item [--] BSM parameterized by \(t=k-\min\{O_M,O_W\}\) admits (1) a kernel where the number of people is linear in \(t\), and (2) a parameterized algorithm whose running time is single exponential in \(t\).
\item [--]BSM parameterized by \(t=k-\max\{O_M,O_W\}\) is W[1]-hard.
\end{itemize}
For the entire collection see [Zbl 1419.68009].Balanced stable marriage: how close is close enough?https://zbmath.org/1517.681442023-09-22T14:21:46.120933Z"Gupta, Sushmita"https://zbmath.org/authors/?q=ai:gupta.sushmita"Roy, Sanjukta"https://zbmath.org/authors/?q=ai:roy.sanjukta"Saurabh, Saket"https://zbmath.org/authors/?q=ai:saurabh.saket"Zehavi, Meirav"https://zbmath.org/authors/?q=ai:zehavi.meiravSummary: \textsc{Balanced Stable Marriage (BSM)} is a central optimization version of the classic \textsc{Stable Marriage (SM)} problem. We study \textsc{BSM} from the viewpoint of Parameterized Complexity. Informally, the input of \textsc{BSM} consists of \(n\) men, \(n\) women, and an integer \(k\). Each person \(a\) has a (sub)set of acceptable partners, \( \mathcal{A}(a)\), whom \(a\) ranks strictly; we use \(p_a(b)\) to denote the position of \(b \in \mathcal{A}(a)\) in \(a\)'s preference list. The objective is to decide whether there exists a stable matching \(\mu\) such that \(\mathsf{balance}(\mu) \triangleq \max \{ \sum_{( m , w ) \in \mu} p_m(w), \sum_{( m , w ) \in \mu} p_w(m) \} \leq k\). In \textsc{SM}, all stable matchings match the same set of agents, \( A^\star\) which can be computed in polynomial time. \(As \mathsf{balance}(\mu) \geq \frac{ | A^\star |}{ 2}\) for any stable matching \(\mu \), \textsc{BSM} is trivially fixed-parameter tractable (FPT) with respect to \(k\). Thus, a natural question is whether \textsc{BSM} is FPT with respect to \(k - \frac{ | A^\star |}{ 2} \). With this viewpoint in mind, we draw a line between tractability and intractability in relation to the target value. This line separates additional natural parameterizations higher/lower than ours (e.g., we automatically resolve the parameterization \(k - \frac{ | A^\star |}{ 2} )\). The two extreme stable matchings are the man-optimal \(\mu_M\) and the woman-optimal \(\mu_W\). Let \(O_M = \sum_{( m , w ) \in \mu_M} p_m(w)\), and \(O_W = \sum_{( m , w ) \in \mu_W} p_w(m)\). In this work, we prove that
\begin{itemize}
\item[\(\bullet\)] \textsc{BSM} parameterized by \(t = k - \min \{ O_M, O_W \}\) admits (1) a kernel where the number of people is linear in \(t\), and (2) a parameterized algorithm whose running time is single exponential in \(t\).
\item[\(\bullet\)] \textsc{BSM} parameterized by \(t = k - \max \{ O_M, O_W \}\) is W[1]-hard.
\end{itemize}Parameterized complexity of conflict-free set coverhttps://zbmath.org/1517.681452023-09-22T14:21:46.120933Z"Jacob, Ashwin"https://zbmath.org/authors/?q=ai:jacob.ashwin"Majumdar, Diptapriyo"https://zbmath.org/authors/?q=ai:majumdar.diptapriyo"Raman, Venkatesh"https://zbmath.org/authors/?q=ai:raman.venkateshSummary: Set Cover is one of the well-known classical NP-hard problems. Following some recent trends, we study the conflict-free version of the Set Cover problem. Here we have a universe \({\mathcal U}\), a family \({\mathcal F}\) of subsets of \({\mathcal U}\) and a graph \(G_{{\mathcal F}}\) on the vertex set \({\mathcal F}\) and we look for a subfamily \({\mathcal F}' \subseteq{\mathcal F}\) of minimum size that covers \({\mathcal U}\) and also forms an independent set in \(G_{{\mathcal F}}\). Here we initiate a systematic study of the problem in parameterized complexity by restricting the focus to the variants where Set Cover is fixed-parameter tractable (FPT). We give upper bounds and lower bounds for conflict-free version of the Set Cover with and without duplicate sets along with restrictions to the graph classes of \(G_{{\mathcal F}}\).
For the entire collection see [Zbl 1416.68013].Parameterized complexity of conflict-free set coverhttps://zbmath.org/1517.681462023-09-22T14:21:46.120933Z"Jacob, Ashwin"https://zbmath.org/authors/?q=ai:jacob.ashwin"Majumdar, Diptapriyo"https://zbmath.org/authors/?q=ai:majumdar.diptapriyo"Raman, Venkatesh"https://zbmath.org/authors/?q=ai:raman.venkateshSummary: \textsc{Set Cover} is one of the well-known classical NP-hard problems. We study the \textit{conflict-free} version of the \textsc{Set Cover} problem. Here we have a universe \(\mathcal{U}\), a family \(\mathcal{F}\) of subsets of \(\mathcal{U}\) and a graph \(G_{\mathcal{F}}\) on the vertex set \(\mathcal{F}\) and we look for a subfamily \(\mathcal{F}'\subseteq\mathcal{F}\) of minimum size that covers \(\mathcal{U}\) and also forms an independent set in \(G_{\mathcal{F}}\). We study conflict-free \textsc{Set Cover} in parameterized complexity by restricting the focus to the variants where \textsc{Set Cover} is fixed parameter tractable (FPT). We give upper bounds and lower bounds for the running time of conflict-free version of \textsc{Set Cover} with and without duplicate sets along with restrictions to the graph classes of \(G_{\mathcal{F}}\). For example, when pairs of sets in \(\mathcal{F}\) intersect in at most one element, for a solution of size \(k\), we give
\begin{itemize}
\item an \(f(k)|\mathcal{F}|^{o(k)}\) lower bound for any computable function \(f\) assuming ETH even if \(G_{\mathcal{F}}\) is bipartite, but
\item an \(O^*(3^{k^2})\) FPT algorithm \((\mathcal{O}^*\) notation ignores polynomial factors of input) when \(G_{\mathcal{F}}\) is chordal.
\end{itemize}On the parametrized complexity of read-once refutations in UTVPI+ constraint systemshttps://zbmath.org/1517.681472023-09-22T14:21:46.120933Z"Subramani, K."https://zbmath.org/authors/?q=ai:subramani.karthick|subramani.kandasamy|subramani.krishnan"Wojciechowski, P."https://zbmath.org/authors/?q=ai:wojciechowski.piotr-j|wojciechowski.pawel-tSummary: In this paper, we study the problem of finding read-once refutations (ROR) of linear feasibility in a specialized class of constraint systems called UTVPI+ constraint systems \(( \text{UCS}^+)\). The refutations in this paper are analyzed using the ADD inference rule. Recall that a Unit Two Variable Per Inequality (UTVPI) constraint is a constraint of the form \(a_i \cdot x_i + a_j \cdot x_j \leq b\), where \(b \in \mathbb{Z} \), and \(a_i, a_j \in \{0, 1, - 1 \} \). A conjunction of such constraints is called a UTVPI constraint system (UCS). UCSs find applications in a number of domains such as abstract interpretation and scheduling. We examine a more general form of UCSs that allows for a limited number of non-UTVPI constraints to be added to a UCS. We refer to these more general UCSs as UTVPI+ constraint systems or \(\text{UCS}^+ \text{s} \). If a \(\text{UCS}^+\) has only \(k\) non-UTVPI constraints, then we refer to it as a \(\text{UCS}_k^+\). Our focus in this paper is on refutations, i.e., proofs of infeasibility in \(\text{UCS}^+ \text{s} \). In particular, we study read-once refutations of linear feasibility in \(\text{UCS}^+ \text{s} \). Although the problem of finding read-once refutations of UCSs is polynomial time solvable, the presence of non-UTVPI constraints makes the problem \textbf{NP-hard}. However, if the number of non-UTVPI constraints is fixed, then read-once refutations can be found in polynomial time. In fact, in this paper, we show that the ROR problem is fixed-parameter tractable (\textbf{FPT}) for \(\text{UCS}_k^+ \text{s} \), with respect to \(k\), the number of non-UTVPI constraints in the system. We also provide a lower bound on the efficiency of a class of parameterized algorithms for this problem, based on the Strong Exponential Time Hypothesis.Randomness and intractability in Kolmogorov complexityhttps://zbmath.org/1517.681482023-09-22T14:21:46.120933Z"Oliveira, Igor Carboni"https://zbmath.org/authors/?q=ai:oliveira.igor-carboniSummary: We introduce randomized time-bounded Kolmogorov complexity (rKt), a natural extension of \textit{L. A. Levin}'s notion [Inf. Control 61, 15--37 (1984; Zbl 0592.03035)] of Kolmogorov complexity. A string \(w\) of low rKt complexity can be decompressed from a short representation via a time-bounded algorithm that outputs \(w\) with high probability.\par This complexity measure gives rise to a decision problem over strings: MrKtP (The Minimum rKt Problem). We explore ideas from pseudorandomness to prove that MrKtP and its variants cannot be solved in randomized quasi-polynomial time. This exhibits a natural string compression problem that is provably intractable, even for randomized computations. Our techniques also imply that there is no \(n^{1-\varepsilon}\)-approximate algorithm for MrKtP running in randomized quasi-polynomial time.\par Complementing this lower bound, we observe connections between rKt, the power of randomness in computing, and circuit complexity. In particular, we present the first hardness magnification theorem for a natural problem that is unconditionally hard against a strong model of computation.
For the entire collection see [Zbl 1414.68003].Computable randomness is about more than probabilitieshttps://zbmath.org/1517.681492023-09-22T14:21:46.120933Z"Persiau, Floris"https://zbmath.org/authors/?q=ai:persiau.floris"De Bock, Jasper"https://zbmath.org/authors/?q=ai:de-bock.jasper"de Cooman, Gert"https://zbmath.org/authors/?q=ai:de-cooman.gertSummary: We introduce a notion of computable randomness for infinite sequences that generalises the classical version in two important ways. First, our definition of computable randomness is associated with imprecise probability models, in the sense that we consider lower expectations -- or sets of probabilities -- instead of classical `precise' probabilities. Secondly, instead of binary sequences, we consider sequences whose elements take values in some finite sample space. Interestingly, we find that every sequence is computably random with respect to at least one lower expectation, and that lower expectations that are more informative have fewer computably random sequences. This leads to the intriguing question whether every sequence is computably random with respect to a unique most informative lower expectation. We study this question in some detail and provide a partial answer.
For the entire collection see [Zbl 1502.68025].Sharp bounds on the price of bandit feedback for several models of mistake-bounded online learninghttps://zbmath.org/1517.681502023-09-22T14:21:46.120933Z"Feng, Raymond"https://zbmath.org/authors/?q=ai:feng.raymond"Geneson, Jesse"https://zbmath.org/authors/?q=ai:geneson.jesse-t"Lee, Andrew"https://zbmath.org/authors/?q=ai:lee.andrew-chung-yeung|lee.andrew-t|lee.andrew-ray"Slettnes, Espen"https://zbmath.org/authors/?q=ai:slettnes.espenSummary: We determine sharp bounds on the price of bandit feedback for several variants of the mistake-bound model. The first part of the paper presents bounds on the \(r\)-input weak reinforcement model and the \(r\)-input delayed, ambiguous reinforcement model. In both models, the adversary gives \(r\) inputs in each round and only indicates a correct answer if all \(r\) guesses are correct. The only difference between the two models is that in the delayed, ambiguous model, the learner must answer each input before receiving the next input of the round, while the learner receives all \(r\) inputs at once in the weak reinforcement model. In the second part of the paper, we investigate models for online learning with permutation patterns, in which a learner attempts to learn a permutation from a set of permutations by guessing statistics related to sub-permutations. For these permutation models, we prove sharp bounds on the price of bandit feedback. One of our lower bounds for online learning of permutations improves on a lower bound of
\textit{S. A. Goldman} et al. [SIAM J. Comput. 22, No. 5, 1006--1034 (1993; Zbl 0788.68115)]
and matches an upper bound from the same paper.Grey-box learning of register automatahttps://zbmath.org/1517.681512023-09-22T14:21:46.120933Z"Garhewal, Bharat"https://zbmath.org/authors/?q=ai:garhewal.bharat"Vaandrager, Frits"https://zbmath.org/authors/?q=ai:vaandrager.frits-w"Howar, Falk"https://zbmath.org/authors/?q=ai:howar.falk"Schrijvers, Timo"https://zbmath.org/authors/?q=ai:schrijvers.timo"Lenaerts, Toon"https://zbmath.org/authors/?q=ai:lenaerts.toon"Smits, Rob"https://zbmath.org/authors/?q=ai:smits.robSummary: Model learning (a.k.a. active automata learning) is a highly effective technique for obtaining black-box finite state models of software components. We show how one can boost the performance of model learning techniques for register automata by extracting the constraints on input and output parameters from a run, and making this grey-box information available to the learner. More specifically, we provide new implementations of the tree oracle and equivalence oracle from the RALib tool, which use the derived constraints. We extract the constraints from runs of Python programs using an existing tainting library for Python, and compare our grey-box version of RALib with the existing black-box version on several benchmarks, including some data structures from Python's standard library. Our proof-of-principle implementation results in almost two orders of magnitude improvement in terms of numbers of inputs sent to the software system. Our approach, which can be generalized to richer model classes, also enables RALib to learn models that are out of reach of black-box techniques, such as combination locks.
For the entire collection see [Zbl 1507.68030].Preserving consistency in geometric modeling with graph transformationshttps://zbmath.org/1517.681522023-09-22T14:21:46.120933Z"Arnould, Agnès"https://zbmath.org/authors/?q=ai:arnould.agnes"Belhaouari, Hakim"https://zbmath.org/authors/?q=ai:belhaouari.hakim"Bellet, Thomas"https://zbmath.org/authors/?q=ai:bellet.thomas"Le Gall, Pascale"https://zbmath.org/authors/?q=ai:le-gall.pascale"Pascual, Romain"https://zbmath.org/authors/?q=ai:pascual.romainSummary: Labeled graphs are particularly well adapted to represent objects in the context of topology-based geometric modeling. Thus, graph transformation theory is used to implement modeling operations and check their consistency. This article defines a class of graph transformation rules dedicated to embedding computations. Objects are here defined as a particular subclass of labeled graphs in which arc labels encode their topological structure (i.e., cell subdivision: vertex, edge, face) and node labels encode their embedding (i.e., relevant data: vertex positions, face colors, volume density). Object consistency is defined by labeling constraints which must be preserved by modeling operations that modify topology and/or embedding. Dedicated graph transformation variables allow us to access the existing embedding from the underlying topological structure (e.g., collecting all the points of a face) in order to compute the new embedding using user-provided functions (e.g., compute the barycenter of several points). To ensure the safety of the defined operations, we provide syntactic conditions on rules that preserve the object consistency constraints.Rewriting theory for the life sciences: a unifying theory of CTMC semanticshttps://zbmath.org/1517.681532023-09-22T14:21:46.120933Z"Behr, Nicolas"https://zbmath.org/authors/?q=ai:behr.nicolas"Krivine, Jean"https://zbmath.org/authors/?q=ai:krivine.jean"Andersen, Jakob L."https://zbmath.org/authors/?q=ai:andersen.jakob-lykke"Merkle, Daniel"https://zbmath.org/authors/?q=ai:merkle.danielSummary: The \textsc{Kappa} biochemistry and the MØD organic chemistry frameworks are amongst the most intensely developed applications of rewriting-based methods in the life sciences to date. A typical feature of these types of rewriting theories is the necessity to implement certain structural constraints on the objects to be rewritten (a protein is empirically found to have a certain signature of sites, a carbon atom can form at most four bonds,\dots). In this paper, we contribute a number of original developments that permit to implement a universal theory of continuous-time Markov chains (CTMCs) for stochastic rewriting systems. Our core mathematical concepts are a novel rule algebra construction for the relevant setting of rewriting rules with conditions, both in Double- and in Sesqui-Pushout semantics, augmented by a suitable stochastic mechanics formalism extension that permits to derive dynamical evolution equations for pattern-counting statistics. A second main contribution of our paper is a novel framework of restricted rewriting theories, which comprises a rule-algebra calculus under the restriction to so-called constraint-preserving completions of application conditions (for rules considered to act only upon objects of the underlying category satisfying a globally fixed set of structural constraints). This novel framework in turn renders a faithful encoding of bio- and organo-chemical rewriting in the sense of \textsc{Kappa} and MØD possible, which allows us to derive a rewriting-based formulation of reaction systems including a full-fledged CTMC semantics as instances of our universal CTMC framework. While offering an interesting new perspective and conceptual simplification of this semantics in the setting of \textsc{Kappa}, both the formal encoding and the CTMC semantics of organo-chemical reaction systems as motivated by the MØD framework are the first such results of their kind.Combining parallel graph rewriting and quotient graphshttps://zbmath.org/1517.681542023-09-22T14:21:46.120933Z"Boy de la Tour, Thierry"https://zbmath.org/authors/?q=ai:boy-de-la-tour.thierry"Echahed, Rachid"https://zbmath.org/authors/?q=ai:echahed.rachidSummary: We define two graph transformations, one by parallelizing graph rewrite rules, the other by taking quotients of graphs. The former consists in the exhaustive application of local transformations defined by graph rewrite rules expressed in a set-theoretic framework. Compared with other approaches to parallel rewriting, we allow a substantial amount of overlapping only restricted by a condition called the \textit{effective deletion property}. This transformation can be reduced by factoring out possibly many equivalent matchings by the automorphism groups of the rules. The second transformation is based on the use of equivalence relations over graph items and offers a new way of performing simultaneous merging operations. The relevance of combining the two transformations is illustrated on a running example.
For the entire collection see [Zbl 1502.68028].Abstract strategies and coherencehttps://zbmath.org/1517.681552023-09-22T14:21:46.120933Z"Calk, Cameron"https://zbmath.org/authors/?q=ai:calk.cameron"Goubault, Eric"https://zbmath.org/authors/?q=ai:goubault.eric"Malbos, Philippe"https://zbmath.org/authors/?q=ai:malbos.philippeSummary: Normalisation strategies give a categorical interpretation of the notion of contracting homotopy via confluent and terminating rewriting. This approach relates standardisation to coherence results in the context of higher-dimensional rewriting systems. On the other hand, globular 2-Kleene algebras provide a formal setting for reasoning about coherence proofs in abstract rewriting systems. In this setting, we formalise the notion of normalisation strategy and we prove a formal coherence theorem for convergent abstract rewriting systems.
For the entire collection see [Zbl 1507.68032].Confluence up to garbage in graph transformationhttps://zbmath.org/1517.681562023-09-22T14:21:46.120933Z"Campbell, Graham"https://zbmath.org/authors/?q=ai:campbell.graham-h"Plump, Detlef"https://zbmath.org/authors/?q=ai:plump.detlefSummary: The transformation of graphs and graph-like structures is ubiquitous in computer science. When a system is described by graph-transformation rules, it is often desirable that the rules are both terminating and confluent so that rule applications in an arbitrary order produce unique resulting graphs. However, there are application scenarios where the rules are not globally confluent but confluent on a subclass of graphs that are of interest. In other words, non-resolvable conflicts can only occur on graphs that are considered as ``garbage''. In this paper, we introduce the notion of confluence up to garbage and generalise Plump's critical pair lemma for double-pushout graph transformation, providing a sufficient condition for confluence up to garbage by non-garbage critical pair analysis. We apply our results in two case studies about efficient language recognition: we present backtracking-free graph reduction systems which recognise a class of flow diagrams and a class of labelled series-parallel graphs, respectively. Both systems are non-confluent but confluent up to garbage. We also give a critical pair condition for subcommutativity up to garbage which, together with closedness, implies confluence up to garbage even in non-terminating systems.Connecting constrained constructor patterns and matching logichttps://zbmath.org/1517.681572023-09-22T14:21:46.120933Z"Chen, Xiaohong"https://zbmath.org/authors/?q=ai:chen.xiaohong|chen.xiaohong.1|chen.xiaohong.2|chen.xiaohong.3"Lucanu, Dorel"https://zbmath.org/authors/?q=ai:lucanu.dorel"Roşu, Grigore"https://zbmath.org/authors/?q=ai:rosu.grigoreSummary: Constrained constructor patterns are pairs of a constructor term pattern and a quantifier-free first-order logic constraint, built from conjunction and disjunction. They are used to express state predicates for reachability logic defined over rewrite theories. Matching logic has been recently proposed as a unifying foundation for programming languages, specification and verification. It has been shown to capture several logical systems and/or models that are important for programming languages, including first-order logic with fixpoints and order-sorted algebra. In this paper, we investigate the relationship between constrained constructor patterns and matching logic. The comparison result brings us a mutual benefit for the two approaches. Matching logic can borrow computationally efficient proofs for some equivalences, and the language of the constrained constructor patterns can get a more logical flavor and more expressiveness.
For the entire collection see [Zbl 1502.68028].Associative unification and symbolic reasoning modulo associativity in Maudehttps://zbmath.org/1517.681582023-09-22T14:21:46.120933Z"Durán, Francisco"https://zbmath.org/authors/?q=ai:duran.francisco"Eker, Steven"https://zbmath.org/authors/?q=ai:eker.steven"Escobar, Santiago"https://zbmath.org/authors/?q=ai:escobar.santiago"Martí-Oliet, Narciso"https://zbmath.org/authors/?q=ai:marti-oliet.narciso"Meseguer, José"https://zbmath.org/authors/?q=ai:meseguer.jose"Talcott, Carolyn"https://zbmath.org/authors/?q=ai:talcott.carolyn-lSummary: We have added support for associative unification to Maude 2.7.1. Associative unification is infinitary, i.e., there are unification problems \(u =^? v\) such that there is an infinite minimal set of unifiers, whereas associative-commutative unification is finitary. A unique feature of the associative unification algorithm implemented in Maude is that it is guaranteed to terminate with a \textit{finite} and \textit{complete} set of associative unifiers for a fairly large class of unification problems occurring in practice. For any problems outside this class, the algorithm returns a finite set of unifiers together with a \textit{warning} that such set may be incomplete. This paper describes this associative unification algorithm implemented in Maude and also how other symbolic reasoning Maude features such as (i) variant generation; (ii) variant unification; and (iii) narrowing based symbolic reachability analysis have been extended to deal with associativity.
For the entire collection see [Zbl 1398.68038].Proving ground confluence of equational specifications modulo axiomshttps://zbmath.org/1517.681592023-09-22T14:21:46.120933Z"Durán, Francisco"https://zbmath.org/authors/?q=ai:duran.francisco"Meseguer, José"https://zbmath.org/authors/?q=ai:meseguer.jose"Rocha, Camilo"https://zbmath.org/authors/?q=ai:rocha.camiloSummary: Terminating functional programs should be \textit{deterministic}, i.e., should evaluate to a \textit{unique} result, regardless of the evaluation order. For equational functional programs such determinism is exactly captured by the \textit{ground confluence} property. For terminating equations this is equivalent to \textit{ground local confluence}, which follows from \textit{local confluence}. Checking local confluence by computing critical pairs is the \textit{standard} way to check ground confluence. The problem is that some perfectly reasonable equational programs are \textit{not} locally confluent and it can be very hard or even impossible to make them so by adding more equations. We propose a three-step strategy to prove that an equational program \textit{as is} is ground confluent: \textit{First}: apply the strategy proposed in [\textit{F. Durán} and \textit{J. Meseguer}, J. Log. Algebr. Program. 81, No. 7--8, 816--850 (2012; Zbl 1272.03139)] to use non-joinable critical pairs as \textit{completion hints} to either achieve local confluence or reduce the number of critical pairs. \textit{Second}: use the \textit{inductive inference system} proposed in this paper to prove the remaining critical pairs ground joinable. \textit{Third}: to show ground confluence of the original specification, prove also ground joinable the equations added. These methods apply to order-sorted and possibly conditional equational programs modulo axioms such as, e.g., Maude functional modules.
For the entire collection see [Zbl 1398.68038].Complexity of decision problems on totally rigid acyclic tree grammarshttps://zbmath.org/1517.681602023-09-22T14:21:46.120933Z"Eberhard, Sebastian"https://zbmath.org/authors/?q=ai:eberhard.sebastian"Ebner, Gabriel"https://zbmath.org/authors/?q=ai:ebner.gabriel"Hetzl, Stefan"https://zbmath.org/authors/?q=ai:hetzl.stefanSummary: Totally rigid acyclic tree grammars (TRATGs) are an emerging grammatical formalism with numerous applications in proof theory and automated reasoning. We determine the computational complexity of several decision problems on TRATGs: membership, containment, disjointness, equivalence, minimization, and the complexity of minimal cover with a fixed number of nonterminals. We relate non-parametric minimal cover to a problem on regular word grammars of unknown complexity.
For the entire collection see [Zbl 1398.68030].Ogden's lemma for subclasses of random context gallerieshttps://zbmath.org/1517.681612023-09-22T14:21:46.120933Z"Ewert, Sigrid"https://zbmath.org/authors/?q=ai:ewert.sigrid"Idahosa, Joy"https://zbmath.org/authors/?q=ai:idahosa.joySummary: Random context picture grammars are used to generate pictures through successive refinement. There exist several subclasses of these grammars, e. g., context-free picture grammars, random permitting context picture grammars, random forbidding context picture grammars and table-driven context-free picture grammars. These classes generate context-free galleries (cfpls), random permitting context galleries (rPcpls), random forbidding context galleries (rFcpls) and table-driven context-free galleries (Tcfpls), respectively. For all these classes of galleries, necessary conditions have been proven. In particular, for cfpls, there exists a pumping-shrinking lemma, for rPcpls, a pumping lemma and for rFcpls, a shrinking lemma. For Tcfpls, two necessary conditions have been proven. Recently, a new necessary condition related to the size of a subpicture
was proven for each of the abovementioned classes of galleries. We now prove theorems that are an alternative to the existing necessary conditions. This is done by adapting Ogden's idea of marking parts of a word for the picture case. We illustrate the new conditions with examples. For rPcpls and Tcfpls, we also give examples of galleries for which the marking is necessary.Rewriting in Gray categories with applications to coherencehttps://zbmath.org/1517.681622023-09-22T14:21:46.120933Z"Forest, Simon"https://zbmath.org/authors/?q=ai:forest.simon"Mimram, Samuel"https://zbmath.org/authors/?q=ai:mimram.samuelSummary: Over the recent years, the theory of rewriting has been used and extended in order to provide systematic techniques to show coherence results for strict higher categories. Here, we investigate a further generalization to Gray categories, which are known to be equivalent to tricategories. This requires us to develop the theory of rewriting in the setting of precategories, which are adapted to mechanized computations and include Gray categories as particular cases. We show that a finite rewriting system in precategories admits a finite number of critical pairs, which can be efficiently computed. We also extend Squier's theorem to our context, showing that a convergent rewriting system is coherent, which means that any two parallel 3-cells are necessarily equal. This allows us to prove coherence results for several well-known structures in the context of Gray categories: monoids, adjunctions, and Frobenius monoids.Transformation rules with nested application conditions: critical pairs, initial conflicts \& minimalityhttps://zbmath.org/1517.681632023-09-22T14:21:46.120933Z"Lambers, Leen"https://zbmath.org/authors/?q=ai:lambers.leen"Orejas, Fernando"https://zbmath.org/authors/?q=ai:orejas.fernandoSummary: Recently, initial conflicts were introduced in the framework of \(\mathcal{M} \)-adhesive categories as an important optimization of critical pairs. In particular, they represent a proper subset such that each conflict is represented in a minimal context by a unique initial one. The theory of critical pairs has been extended in the framework of \(\mathcal{M} \)-adhesive categories to rules with nested application conditions (ACs), restricting the applicability of a rule and generalizing the well-known negative application conditions. A notion of initial conflicts for rules with ACs does not exist yet.
In this paper, on the one hand, we extend the theory of initial conflicts in the framework of \(\mathcal{M} \)-adhesive categories to transformation rules with ACs. They represent a proper subset again of critical pairs for rules with ACs, and represent each conflict in a minimal context uniquely. They are moreover symbolic because we can show that in general no finite and complete set of conflicts for rules with ACs exists. On the other hand, we show that critical pairs are minimally \(\mathcal{M} \)-complete, whereas initial conflicts are minimally complete. Finally, we introduce important special cases of rules with ACs for which we can obtain finite, minimally \(( \mathcal{M} \)-)complete sets of conflicts.Variants in the infinitary unification wonderlandhttps://zbmath.org/1517.681642023-09-22T14:21:46.120933Z"Meseguer, José"https://zbmath.org/authors/?q=ai:meseguer.jose|meseguer.jose.1Summary: So far, results about variants, the finite variant property (FVP), and variant unification have been developed for equational theories \(E \cup B\) where \(B\) is a set of axioms having a finitary unification algorithm, and the equations \(E\), oriented as rewrite rules \(\vec{E} \), are convergent modulo \(B\). The extension to the case when \(B\) has an infinitary unification algorithm, for example because of non-commutative symbols having associative axioms, seems undeveloped. This paper takes a first step in developing such an extension. In particular, the relationships between the FVP and the boundedness properties, the identification of conditions on \(E \cup B\) ensuring FVP, and the effective computation of variants and variant unifiers are explored in detail. The extension from the finitary to the infinitary case includes both surprises and opportunities.
For the entire collection see [Zbl 1502.68028].Variant satisfiability of parameterized stringshttps://zbmath.org/1517.681652023-09-22T14:21:46.120933Z"Meseguer, José"https://zbmath.org/authors/?q=ai:meseguer.jose|meseguer.jose.1Summary: Two ``knowingly incomplete,'' yet useful, variant-based satisfiability procedures for QF formulas in the instantiations of two, increasingly more expressive, parameterized data types of strings are proposed. The first has four selector functions decomposing a list concatenation into its parts. The second adds a list membership predicate. The meaning of ``parametric'' here is much more general than is the case for decision procedures for strings in current SMT solvers, which are parametric on a finite alphabet. The parameterized data types presented here are parametric on a (typically infinite) algebraic data type of string elements. The main result is that if an algebraic data type has a variant satisfiability algorithm, then the data type of strings over such elements has a ``knowingly incomplete,'' yet practical, variant satisfiability algorithm, with no need for a Nelson-Oppen combination algorithm relating satisfiability in strings and in the given data type.
For the entire collection see [Zbl 1502.68028].Generalized rewrite theories and coherence completionhttps://zbmath.org/1517.681662023-09-22T14:21:46.120933Z"Meseguer, José"https://zbmath.org/authors/?q=ai:meseguer.jose|meseguer.jose.1Summary: A new notion of generalized rewrite theory suitable for symbolic reasoning and generalizing the standard notion in [\textit{R. Bruni} and the author, Theor. Comput. Sci. 360, No. 1--3, 386--414 (2006; Zbl 1097.68051)] is motivated and defined. Also, new requirements for \textit{symbolic executability} of generalized rewrite theories that extend those in [\textit{F. Durán} and the author, J. Log. Algebr. Program. 81, No. 7--8, 816--850 (2012; Zbl 1272.03139)] for standard rewrite theories, including a generalized notion of \textit{coherence}, are given. Finally, symbolic executability, including coherence, is both ensured and made available for a wide class of such theories by automatable \textit{theory transformations}.
For the entire collection see [Zbl 1398.68038].Inductive reasoning with equality predicates, contextual rewriting and variant-based simplificationhttps://zbmath.org/1517.681672023-09-22T14:21:46.120933Z"Meseguer, José"https://zbmath.org/authors/?q=ai:meseguer.jose"Skeirik, Stephen"https://zbmath.org/authors/?q=ai:skeirik.stephenSummary: We present an inductive inference system for proving validity of formulas in the initial algebra \(T_{\mathcal{E}}\) of an order-sorted equational theory \(\mathcal{E}\) with 17 inference rules, where only 6 of them require user interaction, while the remaining 11 can be automated as \textit{simplification rules} and can be combined together as a limited, yet practical, automated inductive theorem prover. The 11 simplification rules are based on powerful equational reasoning techniques, including: equationally defined equality predicates, constructor variant unification, variant satisfiability, order-sorted congruence closure, contextual rewriting and recursive path orderings. For \(\mathcal{E} = (\varSigma , E \uplus B)\), these techniques work modulo \(B\), with \(B\) a combination of associativity and/or commutativity and/or identity axioms.
For the entire collection see [Zbl 1502.68028].A simplified application of Howard's vector notation system to termination proofs for typed lambda-calculus systemshttps://zbmath.org/1517.681682023-09-22T14:21:46.120933Z"Okada, Mitsuhiro"https://zbmath.org/authors/?q=ai:okada.mitsuhiro"Takahashi, Yuta"https://zbmath.org/authors/?q=ai:takahashi.yutaSummary: There have been some important methods of combining a recursive path ordering and Tait-Girard's computability argument to provide an ordering for termination proofs of higher-order rewrite systems. The higher-order recursive path ordering HORPO by Jouannaud and Rubio and the computability path ordering CPO by Blanqui, Jouannaud and Rubio are examples of such an ordering. In this paper, we give a case study of yet another direction of such extension of recursive path ordering, avoiding Tait-Girard's computability method plugged in the above mentioned works. This motivation comes from Lévy's question in the RTA open problem 19, which asks for a reasonably straightforward interpretation of simply typed \(\lambda \)-calculus \(\lambda_{\rightarrow }\) in a certain well founded ordering. As in the cases of HORPO and CPO, the addition of \(\lambda \)-abstraction and application into path orderings might be considered as one solution, but the following question still remains; can the termination of \(\lambda_{\rightarrow }\) be proved by an interpretation in a first-order well founded ordering in the sense that \(\lambda \)-abstraction/application are not directly built in the ordering? Reconsidering one of Howard's works on proof-theoretic studies, we introduce the path ordering with Howard algebra as a case study towards further studies on Lévy's question.
For the entire collection see [Zbl 1502.68028].A tale of conjunctive grammarshttps://zbmath.org/1517.681692023-09-22T14:21:46.120933Z"Okhotin, Alexander"https://zbmath.org/authors/?q=ai:okhotin.alexanderSummary: Conjunctive grammars are an extension of ordinary (''context-free'') grammars with a conjunction operator, which can be used in any rules to specify a substring that satisfies several syntactic conditions simultaneously. This family has been systematically studied since the turn of the century, and is a subject of current studies. This paper gives an overview of the current state of the art in the research on conjunctive grammars.
For the entire collection see [Zbl 1398.68030].Strategies, model checking and branching-time properties in Maudehttps://zbmath.org/1517.681702023-09-22T14:21:46.120933Z"Rubio, Rubén"https://zbmath.org/authors/?q=ai:rubio.ruben"Martí-Oliet, Narciso"https://zbmath.org/authors/?q=ai:marti-oliet.narciso"Pita, Isabel"https://zbmath.org/authors/?q=ai:pita.isabel"Verdejo, Alberto"https://zbmath.org/authors/?q=ai:verdejo.albertoSummary: Maude 3 includes as a new feature an object-level strategy language. Rewriting strategies can now be used to easily control how rules are applied, restricting the rewriting systems behavior. This new specification layer would not be useful if there were no tools to execute, analyze and verify its creatures. For that reason, we extended the Maude LTL model checker to systems controlled by strategies, after studying their model-checking problem. Now, we widen the range of properties that can be checked in Maude models, both strategy-aware and strategy-free, by implementing a module for the language-independent model checker LTSmin that supports logics like CTL* and \(\mu \)-calculus.
For the entire collection see [Zbl 1502.68028].Single pushout rewriting in comprehensive systems of graph-like structureshttps://zbmath.org/1517.681712023-09-22T14:21:46.120933Z"Stünkel, Patrick"https://zbmath.org/authors/?q=ai:stunkel.patrick"König, Harald"https://zbmath.org/authors/?q=ai:konig.haraldSummary: The elegance of the \textit{single-pushout} (SPO) approach to graph transformations arises from substituting total morphisms by partial ones in the underlying category. SPO's applicability depends on the durability of pushouts after this transition. There is a wide range of work on the question when pushouts exist in categories with partial morphisms starting with the pioneering work of Löwe and Kennaway and ending with an essential characterisation in terms of an exactness property (for the interplay between pullbacks and pushouts) and an adjointness condition (w.r.t. inverse image functions) by Hayman and Heindel. Triple graphs and graph diagrams are frameworks to synchronise two or more updatable data sources by means of internal mappings, which identify common sub-structures. \textit{Comprehensive systems} generalise these frameworks, treating the network of data sources and their structural inter-relations as a homogeneous comprehensive artefact, in which partial maps identify commonalities. Although this inherent partiality produces amplified complexity, we can show that Heindel's characterisation still yields existence of pushouts in the category of comprehensive systems and reflective partial morphisms and thus enables computing by typed SPO graph transformation.Decidability of right one-way jumping finite automatahttps://zbmath.org/1517.681722023-09-22T14:21:46.120933Z"Beier, Simon"https://zbmath.org/authors/?q=ai:beier.simon"Holzer, Markus"https://zbmath.org/authors/?q=ai:holzer.markusSummary: We continue our investigation [Lect. Notes Comput. Sci. 10952, 11--23 (2018; Zbl 1435.68142)] on (right) one-way jumping finite automata (ROWJFA), a variant of jumping automata, which is an automaton model for discontinuous information processing. Here we focus on decision problems for ROWJFAs. It turns out that most problems such as, e.g., emptiness, finiteness, universality, the word problem and variants thereof, closure under permutation, etc., are decidable. Moreover, we show that the containment of a language within the strict hierarchy of ROWJFA permutation closed languages induced by the number of accepting states as well as whether permutation closed regular or jumping finite automata languages can be accepted by ROWJFAs is decidable, too. On the other hand, we prove that for (linear) context-free languages the corresponding ROWJFA acceptance problem becomes undecidable. Moreover, we also discuss some complexity results for the considered decision problems.
For the entire collection see [Zbl 1398.68030].Minimisation of automatahttps://zbmath.org/1517.681732023-09-22T14:21:46.120933Z"Berstel, Jean"https://zbmath.org/authors/?q=ai:berstel.jean"Boasson, Luc"https://zbmath.org/authors/?q=ai:boasson.luc"Carton, Olivier"https://zbmath.org/authors/?q=ai:carton.olivier"Fagnot, Isabelle"https://zbmath.org/authors/?q=ai:fagnot.isabelleThis chapter of the Handbook gives a survey of the most important minimisation algorithms for deterministic finite automata on finite words.
After a brief mention of Brzozowski's algorithm [\textit{J. A. Brzozowski}, in: Proceedings of the symposium on mathematical theory of automata, New York 1962. Polytechnic Press of the Polytechnic Institutes of Brooklyn; New York-London: John Wiley and Sons, Inc. 529--561 (1963; Zbl 0116.33605)], the authors focus in detail on minimisation techniques based on partition refinement, namely Moore's algorithm [\textit{E. F. Moore}, ``Gedanken-experiments on sequential machines'', in: C. E. Shannon (ed.) and J. McCarthy (ed.), Automata studies. Princeton, NJ: Princeton University Press. 129--153 (1956), contained in Zbl 0074.11204] and Hopcroft's algorithm [\textit{J. Hopcroft}, in: Z. Kohavi (ed.) and A. Paz (ed.), Theory of machines and computations. New York-London: Academic Press. 189--196 (1971; Zbl 0293.94022), contained in Zbl 0266.94019]. They summarise the results known about their performance and also present some original observations about the relation of the two latter algorithms. More precisely, the authors give an example showing that these algorithms are fundamentally different, as there exist an automaton and a partition of its set of states that can be obtained during the execution of Moore's algorithm but cannot be obtained during any execution of Hopcroft's algorithm. Moreover, the authors consider what they call \textit{slow automata} for Moore's and Hopcroft's algorithms -- i.e., automata upon which the algorithm under consideration performs the maximum possible number of steps among all automata of the same size -- and they show that the classes of slow automata for both algorithms coincide.
Next, the authors survey minimisation algorithms based on state fusion, which can only be applied to some very special automata. Namely, they discuss Revuz's linear-time minimisation algorithm for automata without cycles [\textit{D. Revuz}, Theor. Comput. Sci. 92, No. 1, 181--189 (1992; Zbl 0759.68066)] and its extension by \textit{J. Almeida} and \textit{M. Zeitoun} [Inf. Process. Lett. 107, No. 2, 52--59 (2008; Zbl 1186.68242)] to automata whose nontrivial, strongly connected components all take the form of cycles (a trim automaton thus satisfies this property if and only if the growth function of the language it recognises is bounded from above by a polynomial function).
Finally, the authors touch upon the problem of dynamic minimisation, relations between minimisation of automata and string matching, and the minimisation of nondeterministic finite automata.
For the entire collection see [Zbl 1470.68001].
Reviewer: Peter Kostolányi (Bratislava)Tree-to-graph transductions with scopehttps://zbmath.org/1517.681742023-09-22T14:21:46.120933Z"Björklund, Johanna"https://zbmath.org/authors/?q=ai:bjorklund.johannaSummary: High-level natural language processing requires formal languages to represent semantic information. A recent addition of this kind is abstract meaning representations. These are graphs in which nodes encode concepts and edges relations. Node-sharing is common, and cycles occur. We show that the required structures can be generated through the combination of (i) a regular tree grammar, (ii) a sequence of linear top-down tree transducers, and (iii) a fold operator that merges selected nodes. Delimiting the application of the fold operator to connected subgraphs gains expressive power, while keeping the complexity of the associated membership problem in polynomial time.
For the entire collection see [Zbl 1398.68030].A characterization of completely reachable automatahttps://zbmath.org/1517.681752023-09-22T14:21:46.120933Z"Bondar, E. A."https://zbmath.org/authors/?q=ai:bondar.eugenija-a"Volkov, M. V."https://zbmath.org/authors/?q=ai:volkov.mikhail-vSummary: A complete deterministic finite automaton in which every non-empty subset of the state set occurs as the image of the whole state set under the action of a suitable input word is called completely reachable. We characterize completely reachable automata in terms of certain directed graphs.
For the entire collection see [Zbl 1398.68030].The prefix automatonhttps://zbmath.org/1517.681762023-09-22T14:21:46.120933Z"Broda, Sabine"https://zbmath.org/authors/?q=ai:broda.sabine"Maia, Eva"https://zbmath.org/authors/?q=ai:maia.eva"Moreira, Nelma"https://zbmath.org/authors/?q=ai:moreira.nelma"Reis, Rogério"https://zbmath.org/authors/?q=ai:reis.rogerioSummary: There are many different constructions when converting regular expressions to finite automata. In this paper we focus on the prefix automaton, \(\mathcal{A}_{\mathrm{Pre}}\), introduced by Yamamoto in 2014. We present two different methods for the construction of \(\mathcal{A}_{\mathrm{Pre}}\). First, an inductive one, based on a system of expression equations. A second one using an iterative function for computing the states and transitions. We establish relationships between \(\mathcal{A}_{\mathrm{Pre}}\) and other constructions, such as the position automaton, partial derivative automaton and their double reversal (dual) counterparts. We study the average size of these constructions, both experimentally and from an analytic combinatorics point of view. Finally, we extend the construction of the prefix automaton to regular expressions with intersection and show that the relationships with the other automaton constructions also hold for these expressions.On the commutative equivalence of context-free languageshttps://zbmath.org/1517.681772023-09-22T14:21:46.120933Z"Carpi, Arturo"https://zbmath.org/authors/?q=ai:carpi.arturo"D'Alessandro, Flavio"https://zbmath.org/authors/?q=ai:dalessandro.flavioSummary: The problem of the commutative equivalence of context-free and regular languages is studied. In particular conditions ensuring that a context-free language of exponential growth is commutatively equivalent with a regular language are investigated.
For the entire collection see [Zbl 1398.68030].Recognizability for automatahttps://zbmath.org/1517.681782023-09-22T14:21:46.120933Z"Caucal, Didier"https://zbmath.org/authors/?q=ai:caucal.didier"Rispal, Chloé"https://zbmath.org/authors/?q=ai:rispal.chloeSummary: We present a new approach to define Boolean algebras of various language families: given a family \(\mathcal{F}\) of infinite automata, an automaton \(H\) recognizes the set of languages accepted by all automata of \(\mathcal{F}\) that can be mapped by morphism into \(H\). Considering appropriate automata families, we get Boolean algebras of context-free languages, indexed languages, Petri net languages, higher order indexed languages and context-sensitive languages.
For the entire collection see [Zbl 1398.68030].Minimal automaton for multiplying and translating the Thue-Morse sethttps://zbmath.org/1517.681792023-09-22T14:21:46.120933Z"Charlier, Émilie"https://zbmath.org/authors/?q=ai:charlier.emilie"Cisternino, Célia"https://zbmath.org/authors/?q=ai:cisternino.celia"Massuir, Adeline"https://zbmath.org/authors/?q=ai:massuir.adelineSummary: The Thue-Morse set \(\mathcal{T}\) is the set of those non-negative integers whose binary expansions have an even number of \(1\)'s. The name of this set comes from the fact that its characteristic sequence is given by the famous Thue-Morse word \[\mathtt{0110100110010110}\cdots,\] which is the fixed point starting with \(0\) of the word morphism \(\mathtt{0\mapsto 01}\), \(\mathtt{1\mapsto 10}\). The numbers in \(\mathcal{T}\) are commonly called the evil numbers. We obtain an exact formula for the state complexity of the set \(m\mathcal{T}+r\) (i.e. the number of states of its minimal automaton) with respect to any base \(b\) which is a power of \(2\). Our proof is constructive and we are able to explicitly provide the minimal automaton of the language of all \(2^p\)-expansions of the set of integers \(m\mathcal{T}+r\) for any positive integers \(p\) and \(m\) and any remainder \(r\in\{0,\ldots,m{-}1\} \). The proposed method is general for any \(b\)-recognizable set of integers.Site-directed deletionhttps://zbmath.org/1517.681802023-09-22T14:21:46.120933Z"Cho, Da-Jung"https://zbmath.org/authors/?q=ai:cho.da-jung"Han, Yo-Sub"https://zbmath.org/authors/?q=ai:han.yo-sub"Kim, Hwee"https://zbmath.org/authors/?q=ai:kim.hwee"Salomaa, Kai"https://zbmath.org/authors/?q=ai:salomaa.kai-tSummary: We introduce a new bio-inspired operation called a site-directed deletion motivated from site-directed mutagenesis performed by enzymatic activity of DNA polymerase: Given two strings \(x\) and \(y\), a site-directed deletion partially deletes a substring of \(x\) guided by the string \(y\) that specifies which part of a substring can be deleted. We study a few decision problems with respect to the new operation and examine the closure properties of the (iterated) site-directed deletion operations. We, then, define a site-directed deletion-closed (and -free) language \(L\) and investigate its decidability properties when \(L\) is regular or context-free.
For the entire collection see [Zbl 1398.68030].Deque languages, automata and planar graphshttps://zbmath.org/1517.681812023-09-22T14:21:46.120933Z"Crespi Reghizzi, Stefano"https://zbmath.org/authors/?q=ai:crespi-reghizzi.stefano"San Pietro, Pierluigi"https://zbmath.org/authors/?q=ai:san-pietro.pierluigi-lSummary: The memory of a deque automaton is more general than a queue or two stacks; to avoid overgeneralization, we consider quasi-real-time operation. Normal forms of such automata are given. Deque languages form an AFL but not a full one. We define the characteristic deque language, CDL, which combines Dyck and AntiDyck (or FIFO) languages, and homomorphically characterizes the deque languages. The notion of deque graph, from graph theory, well represents deque computation by means of a planar Hamiltonian graph on a cylinder, with edges visualizing producer-consumer relations for deque symbols. We give equivalent definitions of CDL by labelled deque graphs, by cancellation rules, and by means of shuffle and intersection of simpler languages. The labeled deque graph of a sentence generalizes traditional syntax trees. The layout of deque computations on a cylinder is remindful of 3D models used in theoretical (bio)chemistry.
For the entire collection see [Zbl 1398.68030].A general approach to state complexity of operations: formalization and limitationshttps://zbmath.org/1517.681822023-09-22T14:21:46.120933Z"Davies, Sylvie"https://zbmath.org/authors/?q=ai:davies.sylvieSummary: The state complexity of the result of a regular operation is often positively correlated with the number of distinct transformations induced by letters in the minimal deterministic finite automaton of the input languages. That is, more transformations in the inputs means higher state complexity in the output. When this correlation holds, the state complexity of a unary operation can be maximized using languages in which there is one letter corresponding to each possible transformation; for operations of higher arity, we can use \(k\)-tuples of languages in which there is one letter corresponding to each possible \(k\)-tuple of transformations. In this way, a small set of languages can be used as witnesses for many common regular operations, eliminating the need to search for witnesses - though at the expense of using very large alphabets. We formalize this approach and examine its limitations, focusing on the special case of unary operations. We define a class of ``uniform'' unary operations for which this approach works; the class is closed under composition and includes common operations such as star, reversal, and complement. Our main result is that the worst-case state complexity of a uniform unary operation can be determined by considering just \(2n\) witnesses for each \(n\), where \(n\) is the state complexity of the input language.
For the entire collection see [Zbl 1398.68030].Intersection non-emptiness and hardness within polynomial timehttps://zbmath.org/1517.681832023-09-22T14:21:46.120933Z"de Oliveira Oliveira, Mateus"https://zbmath.org/authors/?q=ai:de-oliveira-oliveira.mateus"Wehar, Michael"https://zbmath.org/authors/?q=ai:wehar.michaelSummary: We establish strong connections between the Non-Emptiness of Intersection problem for two and three DFA's over a binary alphabet and the Triangle Finding and 3SUM problems. In particular, we introduce efficient reductions from triangle finding to non-emptiness of intersection for two DFA's over a binary alphabet and from 3SUM to non-emptiness of intersection for three DFA's over a binary alphabet. Additionally, in our main result, we show that for every \(\alpha\geq 2\), non-emptiness of intersection for three DFA's over a unary alphabet can be solved in \(O(n^{\frac{\alpha}{2}})\) time if and only if triangle finding can be solved in \(O(n^{\alpha})\) time.
For the entire collection see [Zbl 1398.68030].On decidability of regular languages theorieshttps://zbmath.org/1517.681842023-09-22T14:21:46.120933Z"Dudakov, Sergey"https://zbmath.org/authors/?q=ai:dudakov.sergey-m"Karlov, Boris"https://zbmath.org/authors/?q=ai:karlov.borisSummary: This paper is dedicated to studying decidability properties of some regular languages theories. We prove that the regular languages theory with the Kleene star only is decidable. If we use union and concatenation simultaneously then the theory becomes both \(\varSigma _1\)- and \(\varPi _1\)-hard over the one-symbol alphabet. Finally, we prove that the regular languages theory over one-symbol alphabet with union and the Kleene star is equivalent to arithmetic. The Kleene star is definable with union and concatenation, hence, the previous theory is equivalent to arithmetic also.
For the entire collection see [Zbl 1416.68013].On decidability of theories of regular languageshttps://zbmath.org/1517.681852023-09-22T14:21:46.120933Z"Dudakov, Sergey"https://zbmath.org/authors/?q=ai:dudakov.sergey-m"Karlov, Boris"https://zbmath.org/authors/?q=ai:karlov.borisSummary: This paper is dedicated to studying decidability properties of theories of regular languages with classical operations: union, concatenation, and the Kleene star. The theory with union only is a theory of some Boolean algebra, so it is decidable. We prove that the theory of regular languages with the Kleene star only is decidable. If we use union and concatenation simultaneously, then the theory becomes both \(\Sigma_1\)- and \(\Pi_1\)-hard over the one-symbol alphabet. Using methods from the proof of this theorem we establish that the theory of regular languages over one-symbol alphabet with union and the Kleene star is as hard as arithmetic. Then we establish that the theory with all three operations is reducible to arithmetic also, hence, it is equivalent to arithmetic. Finally, we prove that the theory of regular languages over any alphabet with concatenation only is equivalent to arithmetic also. The last result is based on our previous work where an analogous theorem was proved for one-symbol languages.On (\(I/O\))-aware good-for-games automatahttps://zbmath.org/1517.681862023-09-22T14:21:46.120933Z"Faran, Rachel"https://zbmath.org/authors/?q=ai:faran.rachel"Kupferman, Orna"https://zbmath.org/authors/?q=ai:kupferman.ornaSummary: Good-For-Games (GFG) automata are nondeterministic automata that can resolve their nondeterministic choices based on the past. The fact that the synthesis problem can be reduced to solving a game on top of a GFG automaton for the specification (that is, no determinization is needed) has made them the subject of extensive research in the last years. GFG automata are defined for general alphabets, whereas in the synthesis problem, the specification is over an alphabet \(2^{I \cup O}\), for sets \(I\) and \(O\) of input and output signals, respectively. We introduce and study (\(I/O\))-\textit{aware GFG automata}, which distinguish between nondeterminism due to \(I\) and \(O\): both should be resolved in a way that depends only on the past; but while nondeterminism in \(I\) is hostile, and all \(I\)-futures should be accepted, nondeterminism in \(O\) is cooperative, and a single \(O\)-future may be accepted. We show that (\(I/O\))-aware GFG automata can be used for synthesis, study their properties, special cases and variants, and argue for their usefulness. In particular, (\(I/O\))-aware GFG automata are unboundedly more succinct than deterministic and even GFG automata, using them circumvents determinization, and their study leads to new and interesting insights about hostile vs. collaborative nondeterminism, as well as the theoretical bound for realizing systems.
For the entire collection see [Zbl 1502.68030].Automata, palindromes, and reversed subwordshttps://zbmath.org/1517.681872023-09-22T14:21:46.120933Z"Fleischer, Lukas"https://zbmath.org/authors/?q=ai:fleischer.lukas"Shallit, Jeffrey"https://zbmath.org/authors/?q=ai:shallit.jeffrey-oSummary: In [Theor. Comput. Sci. 481, 1--8 (2013; Zbl 1291.68307)], \textit{G. Fici} and \textit{L. Q. Zamboni} proved a number of theorems about finite and infinite words having only a small number of factors that are palindromes. Earlier, in [J. Comb. Math. Comb. Comput. 54, 157--164 (2005; Zbl 1081.68076)], \textit{N. Rampersad} and the second author had proved a number of theorems about infinite words \(\mathbf{x}\) with the property that if \(w\) is any sufficiently long finite factor of \(\mathbf{x}\), then its reversal \(w^R\) is \textit{not} a factor of \(\mathbf{x}\). In both cases, the arguments used were typically case-based and somewhat involved.
In this note we rederive most of these results, and obtain many new ones, by a different method based on finite automata. Two variations of the method are presented. One advantage to our method is that it replaces complicated case-based proofs with (relatively simple) machine computations. Another advantage is that our method can provide detailed enumeration results about the number of words satisfying the various conditions. We explore these ideas in detail.On completely reachable automata and subset reachabilityhttps://zbmath.org/1517.681882023-09-22T14:21:46.120933Z"Gonze, François"https://zbmath.org/authors/?q=ai:gonze.francois"Jungers, Raphaël M."https://zbmath.org/authors/?q=ai:jungers.raphael-mSummary: This article focuses on subset reachability in synchronizing automata. First, we provide families of synchronizing automata with subsets which cannot be reached with short words. These families do not fulfil Don's Conjecture about subset reachability. Moreover, they show that some subsets need exponentially long words to be reached, and that the restriction of the conjecture to included subsets also does not hold. Second, we analyze completely reachable automata and provide a counterexample to the conjecture of Bondar and Volkov about the so-called \(\varGamma_1\)-graph. We finally prove an alternative version of this conjecture.
For the entire collection see [Zbl 1398.68030].On minimal grammar problems for finite languageshttps://zbmath.org/1517.681892023-09-22T14:21:46.120933Z"Gruber, Hermann"https://zbmath.org/authors/?q=ai:gruber.hermann"Holzer, Markus"https://zbmath.org/authors/?q=ai:holzer.markus"Wolfsteiner, Simon"https://zbmath.org/authors/?q=ai:wolfsteiner.simonSummary: We investigate the grammatical complexity of finite languages w.r.t. context-free grammars and variants thereof. For fixed alphabets, it is shown that both the minimal number of productions and the minimal size of a context-free grammar generating a finite language cannot be approximated within a factor of \(o(p^{1/6})\) and \(o(s^{1/7})\), respectively, unless \(\mathrm{P}=\mathrm{NP}\). Here, \(p\) is the number of productions and \(s\) the size of the given grammar. Similar inapproximability results also hold for linear context-free and right-linear (or regular) grammars. As a byproduct, we show that the language of all cubes of a given length requires an exponential number of context-free productions and we also investigate upper and lower bounds on the complexity of the operations union and concatenation for finite languages.
For the entire collection see [Zbl 1398.68030].Enumerating regular expressions and their languageshttps://zbmath.org/1517.681902023-09-22T14:21:46.120933Z"Gruber, Hermann"https://zbmath.org/authors/?q=ai:gruber.hermann"Lee, Jonathan"https://zbmath.org/authors/?q=ai:lee.jonathan-k|lee.jonathan-d|lee.jonathan-t|lee.jonathan-w"Shallit, Jeffrey"https://zbmath.org/authors/?q=ai:shallit.jeffrey-oThis chapter of the Handbook guides the reader through the process of enumerating rational expressions of a given length and, subsequently, obtaining lower and upper bounds for the number of rational languages determined by rational expressions of given length. The authors consider three different notions of length in this context and summarise the basic relations among them.
The enumeration of rational expressions of given length can be performed using the standard methodology of \textit{analytic combinatorics} -- see, e.g., [\textit{P. Flajolet} and \textit{R. Sedgewick}, Analytic combinatorics. Cambridge: Cambridge University Press (2009; Zbl 1165.05001)]. The key is to observe that the language of all rational expressions can be generated by an unambiguous context-free grammar. This grammar may differ depending on precisely which rational expressions one considers to be valid (for instance, it is debatable whether one should allow the empty expression or expressions containing superfluous parentheses). The authors explicitly describe an unambiguous context-free grammar that they use as a specification of valid rational expressions in their considerations.
Given an unambiguous context-free grammar generating some subset \(S\) of all rational expressions, it follows by the Chomsky-Schützenberger enumeration theorem that if \(a_n\) denotes the number of rational expressions of (ordinary) length \(n\) in \(S\), then the generating function of the sequence of all such \(a_n\) is algebraic. In fact, the grammar can be directly transformed to an \(\mathbb{N}\)-algebraic system of equations such that the said generating function is the first component of its unique solution. Using Gröbner bases, one can further transform this system to a single algebraic equation satisfied by the generating function. This process is informally explained by the authors.
An exact asymptotic estimate for \(a_n\) as \(n\) tends to infinity can be obtained from such an algebraic equation via singularity analysis. Nevertheless, this is not strictly necessary for the enumeration of rational languages as presented by the authors, so the reader is only referred to [loc. cit.] regarding these matters. Instead, the authors describe in detail how to obtain simple lower and upper bounds for \(a_n\) by making use of Pringsheim's theorem.
Lower bounds for the number of rational languages determined by rational expressions of given length are then obtained by applying these observations to unambiguous grammars for certain particular families of rational expressions such that any two distinct expressions in this family determine different rational languages. Any lower bound for the number of such expressions thus also gives a lower bound for the number of rational languages. On the other hand, upper bounds are obtained by considering certain normal forms of rational expressions, i.e., families of expressions that still can be used to determine every rational language. Any upper bound for the number of such expressions yields an upper bound for the number of rational languages.
For the entire collection see [Zbl 1470.68001].
Reviewer: Peter Kostolányi (Bratislava)Reversible pushdown transducershttps://zbmath.org/1517.681912023-09-22T14:21:46.120933Z"Guillon, Bruno"https://zbmath.org/authors/?q=ai:guillon.bruno"Kutrib, Martin"https://zbmath.org/authors/?q=ai:kutrib.martin"Malcher, Andreas"https://zbmath.org/authors/?q=ai:malcher.andreas"Prigioniero, Luca"https://zbmath.org/authors/?q=ai:prigioniero.lucaSummary: Deterministic pushdown transducers are studied with respect to their ability to compute reversible transductions, that is, to transform inputs into outputs in a reversible way. This means that the transducers are also backward deterministic and thus are able to uniquely step the computation back and forth. The families of transductions computed are classified with regard to four types of length-preserving transductions as well as to the property of working reversibly. It turns out that accurate to one case separating witness transductions can be provided. For the remaining case it is possible to establish the equivalence of both families by proving that stationary moves can always be removed in length-preserving reversible pushdown transductions.
For the entire collection see [Zbl 1398.68030].Two-way automata and one-tape machines. Read only versus linear timehttps://zbmath.org/1517.681922023-09-22T14:21:46.120933Z"Guillon, Bruno"https://zbmath.org/authors/?q=ai:guillon.bruno"Pighizzini, Giovanni"https://zbmath.org/authors/?q=ai:pighizzini.giovanni"Prigioniero, Luca"https://zbmath.org/authors/?q=ai:prigioniero.luca"Průša, Daniel"https://zbmath.org/authors/?q=ai:prusa.danielSummary: It is well-known that one-tape Turing machines working in linear time are no more powerful than finite automata, namely they recognize exactly the class of regular languages. We study the costs, in terms of description sizes, of the conversion of nondeterministic finite automata into equivalent linear-time one-tape deterministic machines. We prove a polynomial blowup from two-way nondeterministic finite automata into equivalent weight-reducing one-tape deterministic machines that work in linear time. The blowup remains polynomial if the tape in the resulting machines is restricted to the portion which initially contains the input. However, in this case the machines resulting from our construction are not weight reducing, unless the input alphabet is unary.
For the entire collection see [Zbl 1398.68030].Dynamics of the independence number and automata synchronizationhttps://zbmath.org/1517.681932023-09-22T14:21:46.120933Z"Gusev, Vladimir V."https://zbmath.org/authors/?q=ai:gusev.vladimir-v"Jungers, Raphaël M."https://zbmath.org/authors/?q=ai:jungers.raphael-m"Průša, Daniel"https://zbmath.org/authors/?q=ai:prusa.danielSummary: We study the lengths of synchronizing words produced by the classical greedy compression algorithm. We associate a sequence of graphs with every synchronizing automaton and rely on evolution of the independence number to bound the lengths of produced words. By leveraging graph theoretical results we show that in many cases automata with good extension properties have good compression properties as well. More precisely, we show that the compression algorithm will produce a synchronizing word of length \(\mathcal{O}(n^2\log (n))\) on cyclic, regular and strongly-transitive automata with \(n\) states, which is not far from the best possible bound of \((n-1)^2\). Furthermore, we provide a relatively simple proof that every \(n\)-state automaton has a synchronizing word of length at most \(\frac{n^3}{4}+\mathcal{O}(n^2)\).
For the entire collection see [Zbl 1398.68030].Properties of hash functions based on Gluškov product of automatahttps://zbmath.org/1517.681942023-09-22T14:21:46.120933Z"Hannusch, Carolin"https://zbmath.org/authors/?q=ai:hannusch.carolin"Horváth, Géza"https://zbmath.org/authors/?q=ai:horvath.gezaSummary: We investigate the properties of hash functions introduced on Gluškov product of automata. Further, we give some important conditions for the transition matrix of the Gluškov product which make the introduced hash functions secure.Finite transducers and rational transductionshttps://zbmath.org/1517.681952023-09-22T14:21:46.120933Z"Harju, Tero"https://zbmath.org/authors/?q=ai:harju.tero"Karhumäki, Juhani"https://zbmath.org/authors/?q=ai:karhumaki.juhaniThis contribution provides an excellent introduction to finite-state transducers and the rational transductions they compute. It first introduces finite transducers as essentially finite-state automata with outputs (in a free monoid). It recalls the main syntactic properties and provides several examples of transducers together with their properties as well as computed relations. It then proceeds to the closure properties of the rational relations, which are the relations computable by finite transducers. The classical definition of the rational relations as the least set containing the empty set and singletons that is closed under union, product, and iteration, is also presented. The rational functions (i.e., those rational relations that are actually functions) are identified and their representation by unambiguous finite transducers is recalled. Finally, the matrix representations of transductions are presented, which are sometimes also called extended transducers, in which each transition carries a regular output language instead of just a single output word.
Section 3 presents the representation of finite transducers by means of homomorphisms culminating in the seminal result of Nivat stating that every rational relation can be presented as a composition of an inverse homomorphism, a regular intersection, and a homomorphism. Particular emphasis is placed on this representation, and several subclasses are also identified by means of their representation in a similar manner. A Hasse diagram in Figure 4 summarizes these homomorphic compositions. Section 4 showcases two major applications of finite transducers. The classical nonperiodic tiling problem, introduced by Wang, is mentioned first, and the best solutions utilizing the least number of tiles are derived using finite transducers. The isomorphism problem for F-semigroups is also introduced and its solution relies on decidability results for rational relations and Ehrenfeucht's conjecture. Finally, the last main section deals with an abundance of undecidability results, as unfortunately most basic problems for rational relations are undecidable. The reduction from the Post correspondence problem is presented in full detail. In several instances restrictions are mentioned which make the corresponding problem decidable (e.g., equivalence of rational functions).
Overall, the contribution is an excellent introduction to the theory of rational transductions. Its focus on homomorphic representations provides additional insight not commonly available in classical textbooks, but all the main results any researcher or practicioner will need are presented as well. The contribution is self-contained in the context of the Handbook and provides ample examples and illustrations for the basic notions. Proofs are provided for most of the major results, but not all results are provided with full proof details. This is not a drawback, but rather allows major progress and exposition of more results. Surprisingly absent are the characterization results for subsequential functions and the related twins property, but these are probably covered in another chapter of the Handbook. The text is written to be understandable by any graduate with some mathematical maturity and can serve as an excellent introduction as well as a reference.
For the entire collection see [Zbl 1470.68001].
Reviewer: Andreas Maletti (Leipzig)Simulation algorithms for symbolic automatahttps://zbmath.org/1517.681962023-09-22T14:21:46.120933Z"Holík, Lukáš"https://zbmath.org/authors/?q=ai:holik.lukas"Lengál, Ondřej"https://zbmath.org/authors/?q=ai:lengal.ondrej"Síč, Juraj"https://zbmath.org/authors/?q=ai:sic.juraj"Veanes, Margus"https://zbmath.org/authors/?q=ai:veanes.margus"Vojnar, Tomáš"https://zbmath.org/authors/?q=ai:vojnar.tomasSummary: We investigate means of efficient computation of the simulation relation over symbolic finite automata (SFAs), i.e., finite automata with transitions labeled by predicates over alphabet symbols. In one approach, we build on the algorithm by Ilie, Navaro, and Yu proposed originally for classical finite automata, modifying it using the so-called mintermisation of the transition predicates. This solution, however, generates all Boolean combinations of the predicates, which easily causes an exponential blowup in the number of transitions. Therefore, we propose two more advanced solutions. The first one still applies mintermisation but in a local way, mitigating the size of the exponential blowup. The other one focuses on a novel symbolic way of dealing with transitions, for which we need to sacrifice the counting technique of the original algorithm (counting is used to decrease the dependency of the running time on the number of transitions from quadratic to linear). We perform a thorough experimental evaluation of all the algorithms, together with several further alternatives, showing that all of them have their merits in practice, but with the clear indication that in most of the cases, efficient treatment of symbolic transitions is more beneficial than counting.
For the entire collection see [Zbl 1396.68018].Computational complexity of decision problems on self-verifying finite automatahttps://zbmath.org/1517.681972023-09-22T14:21:46.120933Z"Holzer, Markus"https://zbmath.org/authors/?q=ai:holzer.markus"Jakobi, Sebastian"https://zbmath.org/authors/?q=ai:jakobi.sebastian"Jirásek, Jozef jun."https://zbmath.org/authors/?q=ai:jirasek.jozef-junSummary: A self-verifying finite automaton (SVFA) is a nondeterministic automaton whose computation can accept, reject, or give no answer. Every word is guaranteed to be either accepted or rejected, and the automaton can not give contradictory answers. This paper examines the computational complexity of several decision problems for SVFAs. First, determining whether a given automaton is an SVFA is PSPACE-complete. All other problems are therefore stated as promise problems. The complexity of (non-)emptiness, universality, and equivalence is comparable to that for deterministic automata. On the other hand, SVFA membership and minimization problems, as well as several counting problems, behave more like their nondeterministic variants.
For the entire collection see [Zbl 1398.68030].Generalizations of checking stack automata: characterizations and hierarchieshttps://zbmath.org/1517.681982023-09-22T14:21:46.120933Z"Ibarra, Oscar H."https://zbmath.org/authors/?q=ai:ibarra.oscar-h"McQuillan, Ian"https://zbmath.org/authors/?q=ai:mcquillan.ianSummary: We examine different generalizations of checking stack automata (e.g., allowing multiple input heads and multiple stacks) and characterize their computing power in terms of two-way multi-head finite automata and space-bounded Turing machines. For various models, we obtain hierarchies in terms of their computing power. Our characterizations and hierarchies expand or tighten some previously known results.
For the entire collection see [Zbl 1398.68030].On counting functions of languageshttps://zbmath.org/1517.681992023-09-22T14:21:46.120933Z"Ibarra, Oscar H."https://zbmath.org/authors/?q=ai:ibarra.oscar-h"McQuillan, Ian"https://zbmath.org/authors/?q=ai:mcquillan.ian"Ravikumar, Bala"https://zbmath.org/authors/?q=ai:ravikumar.balaSummary: We study counting-regular languages -- these are languages \(L\) for which there is a regular language \(L'\) such that the number of strings of length \(n\) in \(L\) and \(L'\) are the same for all \(n\). Our main result is that the languages accepted by the class of one-way unambiguous, reversal-bounded pushdown automata (PDA's) are counting-regular. This generalizes an old result of Baron and Kuich that such languages have rational generating functions. We show that this result is the best possible in the sense that the claim does not hold for either 2-ambiguous PDA's, unambiguous PDA's with no reversal-bound, and other generalizations. We provide a number of examples of languages that are (and are not) counting-regular. We study closure properties of the class of context-free languages that are counting-regular. We also show the undecidability of counting-regularity of PDA's. The undecidability is shown to hold for even the subclass of 2-ambiguous PDA's which make only one reversal on the stack.
For the entire collection see [Zbl 1398.68030].Minimal witnesses for probabilistic timed automatahttps://zbmath.org/1517.682002023-09-22T14:21:46.120933Z"Jantsch, Simon"https://zbmath.org/authors/?q=ai:jantsch.simon"Funke, Florian"https://zbmath.org/authors/?q=ai:funke.florian"Baier, Christel"https://zbmath.org/authors/?q=ai:baier.christelSummary: Witnessing subsystems have proven to be a useful concept in the analysis of probabilistic systems, for example as diagnostic information on why a given property holds or as input to refinement algorithms. This paper introduces witnessing subsystems for reachability problems in probabilistic timed automata (PTA). Using a new operation on difference bounds matrices, it is shown how Farkas certificates of finite-state bisimulation quotients of a PTA can be translated into witnessing subsystems. We present algorithms for the computation of minimal witnessing subsystems under three notions of minimality, which capture the timed behavior from different perspectives, and discuss their complexity.
For the entire collection see [Zbl 1502.68030].Towards exact state complexity bounds for input-driven pushdown automatahttps://zbmath.org/1517.682012023-09-22T14:21:46.120933Z"Jirásková, Galina"https://zbmath.org/authors/?q=ai:jiraskova.galina"Okhotin, Alexander"https://zbmath.org/authors/?q=ai:okhotin.alexanderSummary: The paper improves several state complexity bounds for input-driven pushdown automata (IDPDA), also known as visibly pushdown automata. For deterministic IDPDA it is proved that the number of states sufficient and in the worst case necessary to represent the reversal of an \(n\)-state automaton is exactly \(n^n\) if all inputs are assumed to be well-nested, and between \(n^n\) and \(n(n^n-(n-1)^n)+1\) without this restriction, cf. \(2^{\varTheta(n\log n)}\) in the literature. For the concatenation of an \(m\)-state and an \(n\)-state IDPDA, the new lower bound is \(mn^n\), which is asymptotically tight for well-nested inputs. Without this restriction, the state complexity is between \(mn^n\) and \(m(n+1)n^n2^n\). Finally, it is proved that transforming an \(n\)-state nondeterministic IDPDA to a deterministic one requires exactly \(2^{n^2}\) states, cf. \(2^{\varTheta (n^2)}\) in the literature; the known lower bounds on complementing nondeterministic IDPDA and on transforming them to unambiguous are also improved.
For the entire collection see [Zbl 1398.68030].Reachability problems in nondeterministic polynomial maps on the integershttps://zbmath.org/1517.682022023-09-22T14:21:46.120933Z"Ko, Sang-Ki"https://zbmath.org/authors/?q=ai:ko.sang-ki"Niskanen, Reino"https://zbmath.org/authors/?q=ai:niskanen.reino"Potapov, Igor"https://zbmath.org/authors/?q=ai:potapov.igorSummary: We study the reachability problems in various nondeterministic polynomial maps in \(\mathbb{Z}^n\). We prove that the reachability problem for very simple three-dimensional affine maps (with independent variables) is undecidable and is PSPACE-hard for two-dimensional quadratic maps. Then we show that the complexity of the reachability problem for maps without functions of the form \(\pm x+b\) is lower. In this case the reachability problem is PSPACE-complete in general, and NP-hard for any fixed dimension. Finally we extend the model by considering maps as language acceptors and prove that the universality problem is undecidable for two-dimensional affine maps.
For the entire collection see [Zbl 1398.68030].Owl: a library for \(\omega \)-words, automata, and LTLhttps://zbmath.org/1517.682032023-09-22T14:21:46.120933Z"Křetínský, Jan"https://zbmath.org/authors/?q=ai:kretinsky.jan"Meggendorfer, Tobias"https://zbmath.org/authors/?q=ai:meggendorfer.tobias"Sickert, Salomon"https://zbmath.org/authors/?q=ai:sickert.salomonSummary: We present the library \texttt{Owl} (\textbf{O}mega-\textbf{W}ords, automata, and \textbf{L}TL) for \(\omega \)-automata and linear temporal logic. It forms a backbone of several translations from LTL to automata and related tools by different authors. We describe the functionality of the library and the recent experience, which has already shown the library is apt for easy prototyping of new tools in this area.
For the entire collection see [Zbl 1396.68018].On the unavoidability of primitive words and other languageshttps://zbmath.org/1517.682042023-09-22T14:21:46.120933Z"Leupold, Peter"https://zbmath.org/authors/?q=ai:leupold.peterSummary: Most of the well-known language classes contain very different languages that often have no words at all in common. Therefore it might seem improbable at first sight, that there could be a language non-trivially sharing infinitely many words with each of the individual languages. Non-trivially here means, that the language itself has infinite complement so that there do exist infinite languages that have empty intersection with it.
We formalize this idea of being unavoidable. Then we fill the concept with life by providing examples of languages that are unavoidable for classes of regular, context-free and context-sensitive languages. Primitive words play a central role in many of these examples.Proving non-inclusion of Büchi automata based on Monte Carlo samplinghttps://zbmath.org/1517.682052023-09-22T14:21:46.120933Z"Li, Yong"https://zbmath.org/authors/?q=ai:li.yong.11"Turrini, Andrea"https://zbmath.org/authors/?q=ai:turrini.andrea"Sun, Xuechao"https://zbmath.org/authors/?q=ai:sun.xuechao"Zhang, Lijun"https://zbmath.org/authors/?q=ai:zhang.lijunSummary: The search for a proof of correctness and the search for counterexamples (bugs) are complementary aspects of verification. In order to maximize the practical use of verification tools it is better to pursue them at the same time. While this is well-understood in the termination analysis of programs, this is not the case for the language inclusion analysis of Büchi automata, where research mainly focused on improving algorithms for proving language inclusion, with the search for counterexamples left to the expensive complementation operation.
In this paper, we present \(\mathsf{IMC}^2 \), a specific algorithm for proving Büchi automata non-inclusion \(\mathcal{L}(\mathcal{A}) \not \subseteq \mathcal{L}(\mathcal{B})\), based on Grosu and Smolka's algorithm \(\mathsf{MC}^2\) developed for Monte Carlo model checking against LTL formulas. The algorithm we propose takes \(M = \lceil \ln \delta /\ln (1-\varepsilon ) \rceil\) random lasso-shaped samples from \(\mathcal{A}\) to decide whether to reject the hypothesis \(\mathcal{L}(\mathcal{A}) \not \subseteq \mathcal{L}(\mathcal{B})\), for given error probability \(\varepsilon\) and confidence level \(1 - \delta \). With such a number of samples, \( \mathsf{IMC}^2\) ensures that the probability of witnessing \(\mathcal{L}(\mathcal{A}) \not \subseteq \mathcal{L}(\mathcal{B})\) via further sampling is less than \(\delta \), under the assumption that the probability of finding a lasso counterexample is larger than \(\varepsilon \). Extensive experimental evaluation shows that \(\mathsf{IMC}^2\) is a fast and reliable way to find counterexamples to Büchi automata inclusion.
For the entire collection see [Zbl 1502.68030].On finitely ambiguous Büchi automatahttps://zbmath.org/1517.682062023-09-22T14:21:46.120933Z"Löding, Christof"https://zbmath.org/authors/?q=ai:loding.christof"Pirogov, Anton"https://zbmath.org/authors/?q=ai:pirogov.antonSummary: Unambiguous Büchi automata, i.e. Büchi automata allowing only one accepting run per word, are a useful restriction of Büchi automata that is well-suited for probabilistic model-checking. In this paper we propose a more permissive variant, namely finitely ambiguous Büchi automata, a generalisation where each word has at most \(k\) accepting runs, for some fixed \(k\). We adapt existing notions and results concerning finite and bounded ambiguity of finite automata to the setting of \(\omega\)-languages and present a translation from arbitrary nondeterministic Büchi automata with \(n\) states to finitely ambiguous automata with at most \(3^n\) states and at most \(n\) accepting runs per word.
For the entire collection see [Zbl 1398.68030].The containment problem for unambiguous register automata and unambiguous timed automatahttps://zbmath.org/1517.682072023-09-22T14:21:46.120933Z"Mottet, Antoine"https://zbmath.org/authors/?q=ai:mottet.antoine"Quaas, Karin"https://zbmath.org/authors/?q=ai:quaas.karinSummary: We investigate the complexity of the containment problem ``Does \(L(\mathcal{A})\subseteq L(\mathscr{B})\) hold?'' for register automata and timed automata, where \(\mathscr{B}\) is assumed to be unambiguous and \(\mathcal{A}\) is arbitrary. We prove that the problem is decidable in the case of register automata over \((\mathbb{N},=)\), in the case of register automata over \((\mathbb{Q},<)\) when \(\mathscr{B}\) has a single register, and in the case of timed automata when \(\mathscr{B}\) has a single clock. We give a \textsf{2-EXPSPACE} algorithm in the first case, whose complexity is a single exponential in the case that \(\mathscr{B}\) has a bounded number of registers. In the other cases, we give an \textsf{EXPSPACE} algorithm.The containment problem for unambiguous register automatahttps://zbmath.org/1517.682082023-09-22T14:21:46.120933Z"Mottet, Antoine"https://zbmath.org/authors/?q=ai:mottet.antoine"Quaas, Karin"https://zbmath.org/authors/?q=ai:quaas.karinSummary: We investigate the complexity of the containment problem ``Does \(L(\mathcal{A})\subseteq L(\mathcal{B})\) hold?'', where \(\mathcal{B}\) is an unambiguous register automaton and \(\mathcal{A}\) is an arbitrary register automaton. We prove that the problem is decidable and give upper bounds on the computational complexity in the general case, and when \(\mathcal{B}\) is restricted to have a fixed number of registers.
For the entire collection see [Zbl 1411.68018].Lexicalized syntactic analysis by two-way restarting automatahttps://zbmath.org/1517.682092023-09-22T14:21:46.120933Z"Mráz, František"https://zbmath.org/authors/?q=ai:mraz.frantisek"Otto, Friedrich"https://zbmath.org/authors/?q=ai:otto.friedrich"Pardubská, Dana"https://zbmath.org/authors/?q=ai:pardubska.dana"Plátek, Martin"https://zbmath.org/authors/?q=ai:platek.martinSummary: We study \textit{h-lexicalized two-way restarting automata} that can rewrite at most \(i\) times per cycle for some \(i \geq 1\) (\textsf{hRLWW}(\(i\))-automata). This model is useful for the study of lexical (syntactic) disambiguation, which is a concept from linguistics that is based on certain reduction patterns. We study lexical disambiguation through the formal notion of \textit{h-lexicalized syntactic analysis} (hLSA). The hLSA is a relation between a \textit{basic language} and the corresponding \textit{h-proper language}, which is obtained from the basic language by mapping all basic symbols to input symbols. We stress the sensitivity of hLSA by \textsf{hRLWW}(\(i\))-automata to the size of the window, the number of possible rewrites per cycle, and the degree of (non-)monotonicity of these automata. We introduce the concepts of \textit{contextually transparent languages} and \textit{contextually transparent lexicalized analyses} based on very special reduction patterns, and we present two-dimensional hierarchies of their subclasses based on the size of the window and on the degree of monotonicity. The bottoms of these hierarchies correspond to the regular and the context-free languages. The class of contextually transparent languages forms a proper subclass of the class of context-sensitive languages with syntactically natural properties.On deterministic ordered restart-delete automatahttps://zbmath.org/1517.682102023-09-22T14:21:46.120933Z"Otto, Friedrich"https://zbmath.org/authors/?q=ai:otto.friedrichSummary: We consider deterministic ordered restart-delete automata, which are actually just deterministic ordered restarting automata (det-ORWW-automata) that have an additional delete operation. We show that these automata don't need states, that they accept all deterministic context-free languages, and that they even accept some languages that are not deterministic context-free. On the other hand, these automata only accept languages that are at the same time context-free and Church-Rosser. In addition, closure properties for the class of languages accepted by these automata are studied.
For the entire collection see [Zbl 1398.68030].Finite sequentiality of unambiguous max-plus tree automatahttps://zbmath.org/1517.682112023-09-22T14:21:46.120933Z"Paul, Erik"https://zbmath.org/authors/?q=ai:paul.erikSummary: We show the decidability of the finite sequentiality problem for unambiguous max-plus tree automata. A max-plus tree automaton is called unambiguous if there is at most one accepting run on every tree. The finite sequentiality problem asks whether for a given max-plus tree automaton, there exist finitely many deterministic max-plus tree automata whose pointwise maximum is equivalent to the given automaton.Finite sequentiality of unambiguous max-plus tree automatahttps://zbmath.org/1517.682122023-09-22T14:21:46.120933Z"Paul, Erik"https://zbmath.org/authors/?q=ai:paul.erikSummary: We show the decidability of the finite sequentiality problem for unambiguous max-plus tree automata. A max-plus tree automaton is called unambiguous if there is at most one accepting run on every tree. The finite sequentiality problem asks whether for a given max-plus tree automaton, there exist finitely many deterministic max-plus tree automata whose pointwise maximum is equivalent to the given automaton.
For the entire collection see [Zbl 1411.68018].Finite automatahttps://zbmath.org/1517.682132023-09-22T14:21:46.120933Z"Pin, Jean-Éric"https://zbmath.org/authors/?q=ai:pin.jean-ericThis contribution is a basic introduction to the theory of finite automata. It provides the basic definition of a finite automaton and of the recognizable languages that finite automata recognize. This operational model is presented in full detail with examples. The standard pumping lemma for the recognizable languages is directly derived from this operational characterization. It is also demonstrated that indeed deterministic finite automata are sufficient to recognize all recognizable languages. Additional optimizations of the automaton model (removal of unreachable and otherwise useless states, etc.) are discussed as well. Boolean closure as well as star closure and closure under inverse homomorphisms of the recognizable languages are also proved based purely on automata. The minimization (i.e., finding the unique (up to isomorphism) deterministic finite automaton with the least number of states for a given recognizable language) of deterministic finite automata is discussed based on the partial derivatives and is used as one access to the syntactic monoid of a recognizable language. The special roles of the syntactic monoid and the associated syntactic morphism are explained. Finally, the rational languages are introduced and the main result, stating that the rational and recognizable languages coincide, is presented with proofs for both directions.
The treatment is generally algebraic, but the standard operational models are provided as well. All notions are fully explained and illustrated with suitable examples. Illustrations are generously provided even for rather standard algorithms, which enables readers to check their understanding and intuition of the notions. Additionally, motivation is provided for most notions, and the author perfectly links different approaches for the benefit of the reader. The material covers a solid core of automata theory, which is probably nicely complemented by the remaining chapters of the book. The contribution is self-contained and can be understood by anyone interested in the topic. The algebraic approach might require some additional maturity, but most of the material is accessible even without it. Overall, the contribution is a very reader-friendly introduction to finite automata theory that at the most presumes some minimal background in algebra.
For the entire collection see [Zbl 1470.68001].
Reviewer: Andreas Maletti (Leipzig)Practical ``paritizing'' of Emerson-Lei automatahttps://zbmath.org/1517.682142023-09-22T14:21:46.120933Z"Renkin, Florian"https://zbmath.org/authors/?q=ai:renkin.florian"Duret-Lutz, Alexandre"https://zbmath.org/authors/?q=ai:duret-lutz.alexandre"Pommellet, Adrien"https://zbmath.org/authors/?q=ai:pommellet.adrienSummary: We introduce a new algorithm that takes a \textit{Transition-based Emerson-Lei Automaton} (TELA), that is, an \(\omega \)-automaton whose acceptance condition is an arbitrary Boolean formula on sets of transitions to be seen infinitely or finitely often, and converts it into a \textit{Transition-based Parity Automaton} (TPA). To reduce the size of the output TPA, the algorithm combines and optimizes two procedures based on a \textit{latest appearance record} principle, and introduces a \textit{partial degeneralization}. Our motivation is to use this algorithm to improve our LTL synthesis tool, where producing deterministic parity automata is an intermediate step.
For the entire collection see [Zbl 1502.68030].Finite approximations and similarity of languageshttps://zbmath.org/1517.682152023-09-22T14:21:46.120933Z"Rovan, Branislav"https://zbmath.org/authors/?q=ai:rovan.branislav"Varga, András"https://zbmath.org/authors/?q=ai:varga.andrasSummary: A new framework to measure distances (similarity) between formal languages and between grammars based on distances between words is introduced. It is based on approximating languages by their finite subsets and using monotone sequences of such finite approximations to define an infinite language in the limit. Distances between finite languages are defined and extended to distances between monotone sequences of finite languages leading to distances between infinite languages. The framework captures several distances studied in the literature.
Context-free grammars with energy are introduced to enable finite approximations emphasizing ``syntactically important'' parts of words. Grammars with energy are also used to extend distances between monotone sequences of finite languages to distances between context-free grammars.
A basic toolkit for monotone sequences of finite languages and distances between languages resp. grammars is provided. As part of this toolkit a non-symmetric version of distances is defined, providing additional characterisation of distances in general. Additional properties of distances between grammars are derived by restricting the``energy use'' of grammars with energy.
Some methods of estimating the distances are presented to be used in cases where the distance is not computable or difficult to compute.Eliminating message counters in threshold automatahttps://zbmath.org/1517.682162023-09-22T14:21:46.120933Z"Stoilkovska, Ilina"https://zbmath.org/authors/?q=ai:stoilkovska.ilina"Konnov, Igor"https://zbmath.org/authors/?q=ai:konnov.igor-vasilevich|konnov.igor-v"Widder, Josef"https://zbmath.org/authors/?q=ai:widder.josef"Zuleger, Florian"https://zbmath.org/authors/?q=ai:zuleger.florianSummary: Threshold automata were introduced to give a formal semantics to distributed algorithms in a way that supports automated verification. While transitions in threshold automata are guarded by conditions over the number of globally sent messages, conditions in the pseudocode descriptions of distributed algorithms are usually formulated over the number of locally received messages. In this work, we provide an automated method to close the gap between these two representations. We propose threshold automata with guards over the number of received messages and present abstractions into guards over the number of sent messages, by eliminating the receive message counters. Our approach allows us for the first time to fully automatically verify models of distributed algorithms that are in one-to-one correspondence with their pseudocode. We prove that our method is sound, and present a criterion for completeness w.r.t. \({\mathsf{LTL}}_{\text{-}\mathsf{{X}}}\) properties (satisfied by all our benchmarks).
For the entire collection see [Zbl 1502.68030].Convexity and order in probabilistic call-by-name FPChttps://zbmath.org/1517.682172023-09-22T14:21:46.120933Z"Rennela, Mathys"https://zbmath.org/authors/?q=ai:rennela.mathysSummary: Kegelspitzen are mathematical structures coined by Keimel and Plotkin, in order to encompass the structure of a convex set and the structure of a dcpo. In this paper, we ask ourselves what are Kegelspitzen the model of. We adopt a categorical viewpoint and show that Kegelspitzen model stochastic matrices onto a category of domains. Consequently, Kegelspitzen form a denotational model of pPCF, an abstract functional programming language for probabilistic computing. We conclude the present work with a discussion of the interpretation of (probabilistic) recursive types, which are types for entities which might contain other entities of the same type, such as lists and trees.Probabilistic hyperproperties with nondeterminismhttps://zbmath.org/1517.682182023-09-22T14:21:46.120933Z"Ábrahám, Erika"https://zbmath.org/authors/?q=ai:abraham.erika"Bartocci, Ezio"https://zbmath.org/authors/?q=ai:bartocci.ezio"Bonakdarpour, Borzoo"https://zbmath.org/authors/?q=ai:bonakdarpour.borzoo"Dobe, Oyendrila"https://zbmath.org/authors/?q=ai:dobe.oyendrilaSummary: We study the problem of formalizing and checking probabilistic hyperproperties for models that allow nondeterminism in actions. We extend the temporal logic \textsf{HyperPCTL}, which has been previously introduced for discrete-time Markov chains, to enable the specification of hyperproperties also for Markov decision processes. We generalize \textsf{HyperPCTL} by allowing explicit and simultaneous quantification over schedulers and probabilistic computation trees and show that it can express important quantitative requirements in security and privacy. We show that \textsf{HyperPCTL} model checking over MDPs is in general undecidable for quantification over probabilistic schedulers with memory, but restricting the domain to memoryless non-probabilistic schedulers turns the model checking problem decidable. Subsequently, we propose an SMT-based encoding for model checking this language and evaluate its performance.
For the entire collection see [Zbl 1502.68030].A fragment of linear temporal logic for universal very weak automatahttps://zbmath.org/1517.682192023-09-22T14:21:46.120933Z"Adabala, Keerthi"https://zbmath.org/authors/?q=ai:adabala.keerthi"Ehlers, Rüdiger"https://zbmath.org/authors/?q=ai:ehlers.rudigerSummary: Many temporal specifications used in practical model checking can be represented as universal very weak automata (UVW). They are structurally simple and their states can be labeled by simple temporal logic formulas that they represent. For complex temporal properties, it can be hard to understand why a trace violates a property, so when employing UVWs in model checking, this information helps with interpreting the trace. At the same time, the simple structure of UVWs helps the model checker with finding short traces.
While a translation from computation tree logic (CTL) with only universal path quantifiers to UVWs has been described in earlier work, complex temporal properties that define sequences of allowed events along computations of a system are easier to describe in linear temporal logic (LTL). However, no direct translation from LTL to UVWs with little blow-up is known.
In this paper, we define a fragment of LTL that gives rise to a simple and efficient translation from it to UVW. The logic contains the most common shapes of safety and liveness properties, including all nestings of ``Until''-subformulas. We give a translation from this fragment to UVWs that only has an exponential blow-up in the worst case, which we show to be unavoidable. We demonstrate that the simple shape of UVWs helps with understanding counter-examples in a case study.
For the entire collection see [Zbl 1396.68018].Continuous-time Markov decisions based on partial explorationhttps://zbmath.org/1517.682202023-09-22T14:21:46.120933Z"Ashok, Pranav"https://zbmath.org/authors/?q=ai:ashok.pranav"Butkova, Yuliya"https://zbmath.org/authors/?q=ai:butkova.yuliya"Hermanns, Holger"https://zbmath.org/authors/?q=ai:hermanns.holger"Křetínský, Jan"https://zbmath.org/authors/?q=ai:kretinsky.janSummary: We provide a framework for speeding up algorithms for time-bounded reachability analysis of continuous-time Markov decision processes. The principle is to find a small, but almost equivalent \textit{subsystem} of the original system and only analyse the subsystem. Candidates for the subsystem are identified through simulations and iteratively enlarged until runs are represented in the subsystem with high enough probability. The framework is thus dual to that of abstraction refinement. We instantiate the framework in several ways with several traditional algorithms and experimentally confirm orders-of-magnitude speed ups in many cases.
For the entire collection see [Zbl 1396.68018].Complexity of verification and synthesis of threshold automatahttps://zbmath.org/1517.682212023-09-22T14:21:46.120933Z"Balasubramanian, A. R."https://zbmath.org/authors/?q=ai:balasubramanian.a-r"Esparza, Javier"https://zbmath.org/authors/?q=ai:esparza.javier"Lazić, Marijana"https://zbmath.org/authors/?q=ai:lazic.marijanaSummary: Threshold automata are a formalism for modeling and analyzing fault-tolerant distributed algorithms, recently introduced by Konnov, Veith, and Widder, describing protocols executed by a fixed but arbitrary number of processes. We conduct the first systematic study of the complexity of verification and synthesis problems for threshold automata. We prove that the coverability, reachability, safety, and liveness problems are NP-complete, and that the bounded synthesis problem is \(\varSigma_p^2\) complete. A key to our results is a novel characterization of the reachability relation of a threshold automaton as an existential Presburger formula. The characterization also leads to novel verification and synthesis algorithms. We report on an implementation, and provide experimental results.
For the entire collection see [Zbl 1502.68030].Optimal proofs for linear temporal logic on lasso wordshttps://zbmath.org/1517.682222023-09-22T14:21:46.120933Z"Basin, David"https://zbmath.org/authors/?q=ai:basin.david-a"Bhatt, Bhargav Nagaraja"https://zbmath.org/authors/?q=ai:bhatt.bhargav-nagaraja"Traytel, Dmitriy"https://zbmath.org/authors/?q=ai:traytel.dmitrySummary: Counterexamples produced by model checkers can be hard to grasp. Often it is not even evident why a trace violates a specification. We show how to provide easy-to-check evidence for the violation of a linear temporal logic (LTL) formula on a lasso word, based on a novel sound and complete proof system for LTL on lasso words. Valid proof trees in our proof system follow the syntactic structure of the formula and provide insight on why each Boolean or temporal operator is violated or satisfied. We introduce the notion of optimal proofs with respect to a user-specified preference order and identify sufficient conditions for efficiently computing optimal proofs. We design and evaluate an algorithm that performs this computation, demonstrating that it can produce optimal proofs for complex formulas in under a second.
For the entire collection see [Zbl 1396.68018].Explainable reactive synthesishttps://zbmath.org/1517.682232023-09-22T14:21:46.120933Z"Baumeister, Tom"https://zbmath.org/authors/?q=ai:baumeister.tom"Finkbeiner, Bernd"https://zbmath.org/authors/?q=ai:finkbeiner.bernd"Torfah, Hazem"https://zbmath.org/authors/?q=ai:torfah.hazemSummary: Reactive synthesis transforms a specification of a reactive system, given in a temporal logic, into an implementation. The main advantage of synthesis is that it is automatic. The main disadvantage is that the implementation is usually very difficult to understand. In this paper, we present a new synthesis process that explains the synthesized implementation to the user. The process starts with a simple version of the specification and a corresponding simple implementation. Then, desired properties are added one by one, and the corresponding transformations, repairing the implementation, are explained in terms of counterexample traces. We present SAT-based algorithms for the synthesis of repairs and explanations. The algorithms are evaluated on a range of examples including benchmarks taken from the SYNTCOMP competition.
For the entire collection see [Zbl 1502.68030].PALM: a technique for process algebraic specification mininghttps://zbmath.org/1517.682242023-09-22T14:21:46.120933Z"Belluccini, Sara"https://zbmath.org/authors/?q=ai:belluccini.sara"De Nicola, Rocco"https://zbmath.org/authors/?q=ai:de-nicola.rocco"Re, Barbara"https://zbmath.org/authors/?q=ai:re.barbara"Tiezzi, Francesco"https://zbmath.org/authors/?q=ai:tiezzi.francescoSummary: We propose a technique to automatically generate a formal specification of the model of a system from a set of observations of its behaviour. We aim to free systems modellers from the burden of explicitly formalising the behaviour of an existing system to analyse it. We take advantage of an algorithm introduced by the process mining community, which takes as input an event log and generates a formal specification that can be combined with other specifications to obtain a global model of the overall behaviour of a system. Specifically, we have adapted a known process discovery algorithm to produce a specification in mCRL2, a formal specification language based on process algebras. The availability of mCRL2 specifications enables us to take advantage of its rich toolset for verifying systems properties and for effectively reasoning over distributed scenarios where multiple organizations interact to reach common goals. This is an aspect that is not supported by the approaches based on Petri Nets, usually used for process mining. The methodology has been integrated in a stand-alone tool and has been validated using custom-made and real event logs.
For the entire collection see [Zbl 1507.68030].Verification of indefinite-horizon POMDPshttps://zbmath.org/1517.682252023-09-22T14:21:46.120933Z"Bork, Alexander"https://zbmath.org/authors/?q=ai:bork.alexander"Junges, Sebastian"https://zbmath.org/authors/?q=ai:junges.sebastian"Katoen, Joost-Pieter"https://zbmath.org/authors/?q=ai:katoen.joost-pieter"Quatmann, Tim"https://zbmath.org/authors/?q=ai:quatmann.timSummary: The verification problem in MDPs asks whether, for any policy resolving the nondeterminism, the probability that something bad happens is bounded by some given threshold. This verification problem is often overly pessimistic, as the policies it considers may depend on the complete system state. This paper considers the verification problem for partially observable MDPs, in which the policies make their decisions based on (the history of) the observations emitted by the system. We present an abstraction-refinement framework extending previous instantiations of the Lovejoy-approach. Our experiments show that this framework significantly improves the scalability of the approach.
For the entire collection see [Zbl 1502.68030].Formal verification of executable complementation and equivalence checking for Büchi automatahttps://zbmath.org/1517.682262023-09-22T14:21:46.120933Z"Brunner, Julian"https://zbmath.org/authors/?q=ai:brunner.julianSummary: We develop a complementation procedure and an equivalence checker for nondeterministic Büchi automata. Both are formally verified using the proof assistant Isabelle/Hol. The verification covers everything from the abstract correctness proof down to the generated \textsc{Sml} code.
The complementation follows the rank-based approach. We formalize the abstract algorithm and use refinement to derive an executable implementation. In conjunction with a product operation and an emptiness check, this enables deciding language-wise equivalence between nondeterministic Büchi automata. We also improve and extend our library for transition systems and automata presented in previous research.
Finally, we develop a command-line executable providing complementation and equivalence checking as a verified reference tool. It can be used to test the output of other, unverified tools. We also include some tests that demonstrate that its performance is sufficient to do this in practice.
For the entire collection see [Zbl 1507.68030].Synthesis in pMDPs: a tale of 1001 parametershttps://zbmath.org/1517.682272023-09-22T14:21:46.120933Z"Cubuktepe, Murat"https://zbmath.org/authors/?q=ai:cubuktepe.murat"Jansen, Nils"https://zbmath.org/authors/?q=ai:jansen.nils"Junges, Sebastian"https://zbmath.org/authors/?q=ai:junges.sebastian"Katoen, Joost-Pieter"https://zbmath.org/authors/?q=ai:katoen.joost-pieter"Topcu, Ufuk"https://zbmath.org/authors/?q=ai:topcu.ufukSummary: This paper considers parametric Markov decision processes (pMDPs) whose transitions are equipped with affine functions over a finite set of parameters. The synthesis problem is to find a parameter valuation such that the instantiated pMDP satisfies a (temporal logic) specification under all strategies. We show that this problem can be formulated as a quadratically-constrained quadratic program (QCQP) and is non-convex in general. To deal with the NP-hardness of such problems, we exploit a convex-concave procedure (CCP) to iteratively obtain local optima. An appropriate interplay between CCP solvers and probabilistic model checkers creates a procedure -- realized in the tool PROPheSY -- that solves the synthesis problem for models with thousands of parameters.
For the entire collection see [Zbl 1396.68018].Probabilistic hyperproperties of Markov decision processeshttps://zbmath.org/1517.682282023-09-22T14:21:46.120933Z"Dimitrova, Rayna"https://zbmath.org/authors/?q=ai:dimitrova.rayna"Finkbeiner, Bernd"https://zbmath.org/authors/?q=ai:finkbeiner.bernd"Torfah, Hazem"https://zbmath.org/authors/?q=ai:torfah.hazemSummary: Hyperproperties are properties that describe the correctness of a system as a relation between multiple executions. Hyperproperties generalize trace properties and include information-flow security requirements, like noninterference, as well as requirements like symmetry, partial observation, robustness, and fault tolerance. We initiate the study of the specification and verification of hyperproperties of Markov decision processes (MDPs). We introduce the temporal logic \textit{PHL (Probabilistic Hyper Logic)}, which extends classic probabilistic logics with quantification over schedulers and traces. PHL can express a wide range of hyperproperties for probabilistic systems, including both classical applications, such as probabilistic noninterference, and novel applications in areas such as robotics and planning. While the model checking problem for PHL is in general undecidable, we provide methods both for proving and for refuting formulas from a fragment of the logic. The fragment includes many probabilistic hyperproperties of interest.
For the entire collection see [Zbl 1502.68030].Maximum realizability for linear temporal logic specificationshttps://zbmath.org/1517.682292023-09-22T14:21:46.120933Z"Dimitrova, Rayna"https://zbmath.org/authors/?q=ai:dimitrova.rayna"Ghasemi, Mahsa"https://zbmath.org/authors/?q=ai:ghasemi.mahsa"Topcu, Ufuk"https://zbmath.org/authors/?q=ai:topcu.ufukSummary: Automatic synthesis from linear temporal logic (LTL) specifications is widely used in robotic motion planning and control of autonomous systems. A common specification pattern in such applications consists of an LTL formula describing the requirements on the behaviour of the system, together with a set of additional desirable properties. We study the synthesis problem in settings where the overall specification is unrealizable, more precisely, when some of the desirable properties have to be (temporarily) violated in order to satisfy the system's objective. We provide a quantitative semantics of sets of safety specifications, and use it to formalize the ``best-effort'' satisfaction of such \textit{soft} specifications while satisfying the \textit{hard} LTL specification. We propose an algorithm for synthesizing implementations that are optimal with respect to this quantitative semantics. Our method builds upon the idea of bounded synthesis, and we develop a MaxSAT encoding which allows for maximizing the quantitative satisfaction of the soft specifications. We evaluate our algorithm on scenarios from robotics and power distribution networks.
For the entire collection see [Zbl 1396.68018].Robust controller synthesis for duration calculushttps://zbmath.org/1517.682302023-09-22T14:21:46.120933Z"Dole, Kalyani"https://zbmath.org/authors/?q=ai:dole.kalyani"Gupta, Ashutosh"https://zbmath.org/authors/?q=ai:gupta.ashutosh"Krishna, Shankara Narayanan"https://zbmath.org/authors/?q=ai:krishna.shankara-narayananSummary: In automatic control synthesis, we may need to handle specifications with timing constraints and control such that the system meets the specification as much as possible, which is called robust control. In this paper, we present a method for open loop robust controller synthesis from duration calculus (DC) specifications. For robust synthesis, we propose an approach to evaluate the robustness of DC specifications on a given run of a system. We leverage a CEGIS like method for synthesizing robust control signals. In our method, the DC specifications and the system under control are encoded into mixed integer linear problems, and the optimization problem is solved to yield a control signal. We have implemented a tool (ControlDC) based on the method and applied it on a set of benchmarks.
For the entire collection see [Zbl 1502.68030].Symbolic specification and verification of data-aware BPMN processes using rewriting modulo SMThttps://zbmath.org/1517.682312023-09-22T14:21:46.120933Z"Durán, Francisco"https://zbmath.org/authors/?q=ai:duran.francisco"Rocha, Camilo"https://zbmath.org/authors/?q=ai:rocha.camilo"Salaün, Gwen"https://zbmath.org/authors/?q=ai:salaun.gwenSummary: The \textit{Business Process Model and Notation} (BPMN) is the standard notation for modeling business processes. It relies on a workflow-based language that allows for the modeling of the control-flow graph of an entire process. In this paper, the main focus is on an extension of BPMN with data, which is convenient for describing real-world processes involving complex behavior and data descriptions. By considering this level of expressiveness due to the new features, challenging questions arise regarding the choice of the semantic framework for specifying such an extension of BPMN, as well as how to carry out the symbolic simulation, validation, and correctness of the process models. These issues are addressed first by providing a symbolic executable rewriting logic semantics of BPMN using the rewriting modulo SMT framework, where the execution is driven by rewriting modulo axioms and by querying SMT decision procedures for data conditions. Second, reachability properties, such as deadlock freedom and detection of unreachable states with data exhibiting certain values, can be specified and automatically checked with the help of Maude, thanks to its support for rewriting modulo SMT. The approach presented in this paper has been validated on realistic processes and it is illustrated with a running example.
For the entire collection see [Zbl 1398.68038].Context-aware temporal logic for probabilistic systemshttps://zbmath.org/1517.682322023-09-22T14:21:46.120933Z"Elfar, Mahmoud"https://zbmath.org/authors/?q=ai:elfar.mahmoud"Wang, Yu"https://zbmath.org/authors/?q=ai:wang.yu.11"Pajic, Miroslav"https://zbmath.org/authors/?q=ai:pajic.miroslavSummary: In this paper, we introduce the context-aware probabilistic temporal logic (CAPTL) that provides an intuitive way to formalize system requirements by a set of PCTL objectives with a context-based priority structure. We formally present the syntax and semantics of CAPTL and propose a synthesis algorithm for CAPTL requirements. We also implement the algorithm based on the PRISM-games model checker. Finally, we demonstrate the usage of CAPTL on two case studies: a robotic task planning problem, and synthesizing error-resilient scheduler for micro-electrode-dot-array digital microfluidic biochips.
For the entire collection see [Zbl 1502.68030].Model checking branching properties on Petri nets with transitshttps://zbmath.org/1517.682332023-09-22T14:21:46.120933Z"Finkbeiner, Bernd"https://zbmath.org/authors/?q=ai:finkbeiner.bernd"Gieseking, Manuel"https://zbmath.org/authors/?q=ai:gieseking.manuel"Hecking-Harbusch, Jesko"https://zbmath.org/authors/?q=ai:hecking-harbusch.jesko"Olderog, Ernst-Rüdiger"https://zbmath.org/authors/?q=ai:olderog.ernst-rudigerSummary: To model check concurrent systems, it is convenient to distinguish between the data flow and the control. Correctness is specified on the level of data flow whereas the system is configured on the level of control. Petri nets with transits and Flow-LTL are a corresponding formalism. In Flow-LTL, both the correctness of the data flow and assumptions on fairness and maximality for the control are expressed in linear time. So far, branching behavior cannot be specified for Petri nets with transits. In this paper, we introduce Flow-CTL* to express the intended branching behavior of the data flow while maintaining LTL for fairness and maximality assumptions on the control. We encode physical access control with policy updates as Petri nets with transits and give standard requirements in Flow-CTL*. For model checking, we reduce the model checking problem of Petri nets with transits against Flow-CTL* via automata constructions to the model checking problem of Petri nets against LTL. Thereby, physical access control with policy updates under fairness assumptions for an unbounded number of people can be verified.
For the entire collection see [Zbl 1502.68030].Dependency-based compositional synthesishttps://zbmath.org/1517.682342023-09-22T14:21:46.120933Z"Finkbeiner, Bernd"https://zbmath.org/authors/?q=ai:finkbeiner.bernd"Passing, Noemi"https://zbmath.org/authors/?q=ai:passing.noemiSummary: Despite many recent advances, reactive synthesis is still not really a practical technique. The grand challenge is to scale from small transition systems, where synthesis performs well, to complex multi-component designs. Compositional methods, such as the construction of dominant strategies for individual components, reduce the complexity significantly, but are usually not applicable without extensively rewriting the specification. In this paper, we present a refinement of compositional synthesis that does not require such an intervention. Our algorithm decomposes the system into a sequence of components, such that every component has a strategy that is dominant, i.e., performs at least as good as any possible alternative, provided that the preceding components follow their (already synthesized) strategies. The decomposition of the system is based on a dependency analysis, for which we provide semantic and syntactic techniques. We establish the soundness and completeness of the approach and report on encouraging experimental results.
For the entire collection see [Zbl 1502.68030].Accelerated model checking of parametric Markov chainshttps://zbmath.org/1517.682352023-09-22T14:21:46.120933Z"Gainer, Paul"https://zbmath.org/authors/?q=ai:gainer.paul"Hahn, Ernst Moritz"https://zbmath.org/authors/?q=ai:hahn.ernst-moritz"Schewe, Sven"https://zbmath.org/authors/?q=ai:schewe.svenSummary: Parametric Markov chains occur quite naturally in various applications: they can be used for a conservative analysis of probabilistic systems (no matter how the parameter is chosen, the system works to specification); they can be used to find optimal settings for a parameter; they can be used to visualise the influence of system parameters; and they can be used to make it easy to adjust the analysis for the case that parameters change. Unfortunately, these advancements come at a cost: parametric model checking is -- or rather was -- often slow. To make the analysis of parametric Markov models scale, we need three ingredients: clever algorithms, the right data structure, and good engineering. Clever algorithms are often the main (or sole) selling point; and we face the trouble that this paper focuses on -- the latter ingredients to efficient model checking. Consequently, our easiest claim to fame is in the speed-up we have often realised when comparing to the state of the art.
For the entire collection see [Zbl 1396.68018].Bounded synthesis of reactive programshttps://zbmath.org/1517.682362023-09-22T14:21:46.120933Z"Gerstacker, Carsten"https://zbmath.org/authors/?q=ai:gerstacker.carsten"Klein, Felix"https://zbmath.org/authors/?q=ai:klein.felix.1"Finkbeiner, Bernd"https://zbmath.org/authors/?q=ai:finkbeiner.berndSummary: Most algorithms for the synthesis of reactive systems focus on the construction of finite-state machines rather than actual programs. This often leads to badly structured, unreadable code. In this paper, we present a bounded synthesis approach that automatically constructs, from a given specification in linear-time temporal logic (LTL), a program in Madhusudan's simple imperative language for reactive programs. We develop and compare two principal approaches for the reduction of the synthesis problem to a Boolean constraint satisfaction problem. The first reduction is based on a generalization of bounded synthesis to two-way alternating automata, the second reduction is based on a direct encoding of the program syntax in the constraint system. We report on preliminary experience with a prototype implementation, which indicates that the direct encoding outperforms the automata approach.
For the entire collection see [Zbl 1396.68018].On the satisfiability and model checking for one parameterized extension of linear-time temporal logichttps://zbmath.org/1517.682372023-09-22T14:21:46.120933Z"Gnatenko, A. R."https://zbmath.org/authors/?q=ai:gnatenko.anton-romanovich"Zakharov, V. A."https://zbmath.org/authors/?q=ai:zakharov.vladimir-anatolyevich(no abstract)Robustness verification for classifier ensembleshttps://zbmath.org/1517.682382023-09-22T14:21:46.120933Z"Gross, Dennis"https://zbmath.org/authors/?q=ai:gross.dennis"Jansen, Nils"https://zbmath.org/authors/?q=ai:jansen.nils"Pérez, Guillermo A."https://zbmath.org/authors/?q=ai:perez.guillermo-a"Raaijmakers, Stephan"https://zbmath.org/authors/?q=ai:raaijmakers.stephanSummary: We give a formal verification procedure that decides whether a classifier ensemble is robust against arbitrary randomized attacks. Such attacks consist of a set of deterministic attacks and a distribution over this set. The robustness-checking problem consists of assessing, given a set of classifiers and a labelled data set, whether there exists a randomized attack that induces a certain expected loss against all classifiers. We show the NP-hardness of the problem and provide an upper bound on the number of attacks that is sufficient to form an optimal randomized attack. These results provide an effective way to reason about the robustness of a classifier ensemble. We provide SMT and MILP encodings to compute optimal randomized attacks or prove that there is no attack inducing a certain expected loss. In the latter case, the classifier ensemble is provably robust. Our prototype implementation verifies multiple neural-network ensembles trained for image-classification tasks. The experimental results using the MILP encoding are promising both in terms of scalability and the general applicability of our verification procedure.
For the entire collection see [Zbl 1502.68030].Quantifiers on demandhttps://zbmath.org/1517.682392023-09-22T14:21:46.120933Z"Gurfinkel, Arie"https://zbmath.org/authors/?q=ai:gurfinkel.arie"Shoham, Sharon"https://zbmath.org/authors/?q=ai:shoham.sharon"Vizel, Yakir"https://zbmath.org/authors/?q=ai:vizel.yakirSummary: Automated program verification is a difficult problem. It is undecidable even for transition systems over Linear Integer Arithmetic (LIA). Extending the transition system with theory of Arrays, further complicates the problem by requiring inference and reasoning with universally quantified formulas. In this paper, we present a new algorithm, \textsc{Quic3}, that extends IC3 to infer universally quantified invariants over the combined theory of LIA and Arrays. Unlike other approaches that use either IC3 or an SMT solver as a black box, \textsc{Quic3} carefully manages quantified generalization (to construct quantified invariants) and quantifier instantiation (to detect convergence in the presence of quantifiers). While \textsc{Quic3} is not guaranteed to converge, it is guaranteed to make progress by exploring longer and longer executions. We have implemented \textsc{Quic3} within the Constrained Horn Clause solver engine of Z3 and experimented with it by applying \textsc{Quic3} to verifying a variety of public benchmarks of array manipulating C programs.
For the entire collection see [Zbl 1396.68018].First-order timed runtime verification using BDDshttps://zbmath.org/1517.682402023-09-22T14:21:46.120933Z"Havelund, Klaus"https://zbmath.org/authors/?q=ai:havelund.klaus"Peled, Doron"https://zbmath.org/authors/?q=ai:peled.doron-aSummary: Runtime Verification (RV) expedites the analyses of execution traces for detecting system errors and for statistical and quality analysis. Having started modestly, with checking temporal properties that are based on propositional (yes/no) values, the current practice of RV often involves properties that are parameterized by the data observed in the input trace. The specifications are based on various formalisms, such as automata, temporal logics, rule systems and stream processing. Checking execution traces that are data intensive against a specification that requires strong dependencies between the data poses a nontrivial challenge; in particular if runtime verification has to be performed online, where many events that carry data appear within small time proximities. Towards achieving this goal, we recently suggested to represent relations over the observed data values as BDDs, where data elements are enumerated and then converted into bit vectors. We extend here the capabilities of BDD-based RV with the ability to express timing constraints, where the monitored events include clock values. We show how to efficiently operate on BDDs that represent both relations on (enumerations of) values and time dependencies. We demonstrate our algorithm with an efficient implementation and provide experimental results.
For the entire collection see [Zbl 1502.68030].Verifying recurrent neural networks using invariant inferencehttps://zbmath.org/1517.682412023-09-22T14:21:46.120933Z"Jacoby, Yuval"https://zbmath.org/authors/?q=ai:jacoby.yuval"Barrett, Clark"https://zbmath.org/authors/?q=ai:barrett.clark-w"Katz, Guy"https://zbmath.org/authors/?q=ai:katz.guySummary: Deep neural networks are revolutionizing the way complex systems are developed. However, these automatically-generated networks are opaque to humans, making it difficult to reason about them and guarantee their correctness. Here, we propose a novel approach for verifying properties of a widespread variant of neural networks, called \textit{recurrent neural networks}. Recurrent neural networks play a key role in, e.g., speech recognition, and their verification is crucial for guaranteeing the reliability of many critical systems. Our approach is based on the inference of \textit{invariants}, which allow us to reduce the complex problem of verifying recurrent networks into simpler, non-recurrent problems. Experiments with a proof-of-concept implementation of our approach demonstrate that it performs orders-of-magnitude better than the state of the art.
For the entire collection see [Zbl 1502.68030].Temporal logic verification of stochastic systems using barrier certificateshttps://zbmath.org/1517.682422023-09-22T14:21:46.120933Z"Jagtap, Pushpak"https://zbmath.org/authors/?q=ai:jagtap.pushpak"Soudjani, Sadegh"https://zbmath.org/authors/?q=ai:soudjani.sadegh"Zamani, Majid"https://zbmath.org/authors/?q=ai:zamani.majidSummary: This paper presents a methodology for temporal logic verification of discrete-time stochastic systems. Our goal is to find a lower bound on the probability that a complex temporal property is satisfied by finite traces of the system. Desired temporal properties of the system are expressed using a fragment of linear temporal logic, called \textit{safe LTL over finite traces}. We propose to use barrier certificates for computations of such lower bounds, which is computationally much more efficient than the existing discretization-based approaches. The new approach is discretization-free and does not suffer from the curse of dimensionality caused by discretizing state sets. The proposed approach relies on decomposing the negation of the specification into a union of sequential reachabilities and then using barrier certificates to compute upper bounds for these reachability probabilities. We demonstrate the effectiveness of the proposed approach on case studies with linear and polynomial dynamics.
For the entire collection see [Zbl 1396.68018].Formal policy synthesis for continuous-state systems via reinforcement learninghttps://zbmath.org/1517.682432023-09-22T14:21:46.120933Z"Kazemi, Milad"https://zbmath.org/authors/?q=ai:kazemi.milad"Soudjani, Sadegh"https://zbmath.org/authors/?q=ai:soudjani.sadeghSummary: This paper studies satisfaction of temporal properties on unknown stochastic processes that have continuous state spaces. We show how reinforcement learning (RL) can be applied for computing policies that are finite-memory and deterministic using only the paths of the stochastic process. We address properties expressed in linear temporal logic (LTL) and use their automaton representation to give a path-dependent reward function maximised via the RL algorithm. We develop the required assumptions and theories for the convergence of the learned policy to the optimal policy in the continuous state space. To improve the performance of the learning on the constructed sparse reward function, we propose a sequential learning procedure based on a sequence of labelling functions obtained from the positive normal form of the LTL specification. We use this procedure to guide the RL algorithm towards a policy that converges to an optimal policy under suitable assumptions on the process. We demonstrate the approach on a 4-dim cart-pole system and 6-dim boat driving problem.
For the entire collection see [Zbl 1507.68030].Bounded synthesis of register transducershttps://zbmath.org/1517.682442023-09-22T14:21:46.120933Z"Khalimov, Ayrat"https://zbmath.org/authors/?q=ai:khalimov.ayrat"Maderbacher, Benedikt"https://zbmath.org/authors/?q=ai:maderbacher.benedikt"Bloem, Roderick"https://zbmath.org/authors/?q=ai:bloem.roderickSummary: Reactive synthesis aims at automatic construction of systems from their behavioural specifications. The research mostly focuses on synthesis of systems dealing with Boolean signals. But real-life systems are often described using bit-vectors, integers, etc. Bit-blasting would make such systems unreadable, hit synthesis scalability, and is not possible for infinite data-domains. One step closer to real-life systems are register transducers [\textit{M. Kaminski} and \textit{N. Francez}, Theor. Comput. Sci. 134, No. 2, 329--363 (1994; Zbl 0938.68711)]: they can store data-input into registers and later output the content of a register, but they do not directly depend on the data-input, only on its comparison with the registers. Previously [\textit{R. Ehlers} et al., Lect. Notes Comput. Sci. 8318, 415--433 (2014; Zbl 1428.68183)] it was proven that synthesis of register transducers from register automata is undecidable, but there the authors considered transducers equipped with the unbounded queue of registers. First, we prove the problem becomes decidable if bound the number of registers in transducers, by reducing the problem to standard synthesis of Boolean systems. Second, we show how to use quantified temporal logic, instead of automata, for specifications.
For the entire collection see [Zbl 1396.68018].Parallel graph-based stateless model checkinghttps://zbmath.org/1517.682452023-09-22T14:21:46.120933Z"Lång, Magnus"https://zbmath.org/authors/?q=ai:lang.magnus"Sagonas, Konstantinos"https://zbmath.org/authors/?q=ai:sagonas.konstantinosSummary: Stateless model checking (SMC) is an automatic technique with low memory requirements for finding errors in concurrent programs or for checking for their absence. To be effective, SMC tools require algorithms that combat the combinatorial explosion in the number of process/thread interactions that need to be explored. In recent years, a plethora of such algorithms have emerged, which can be classified broadly in those that explore \textit{interleavings} (i.e., complete serializations of events) and those that explore \textit{traces} (i.e., graphs of events). In either case, an SMC algorithm is \textit{optimal} if it explores exactly one representative from each class of equivalent executions. In this paper, we examine the parallelization of a state-of-the-art graph-based algorithm for SMC under sequential consistency, based on the reads-from relation. The algorithm is provably optimal, and in practice spends only polynomial time per equivalence class. We present the modifications to the algorithm that its parallelization requires and implementation aspects that allow us to make it scalable. We report on the performance and scalability that we were able to achieve on C/pthread programs, and how this performance compares to that of other SMC tools. Finally, we argue for the inherent advantages that graph-based algorithms have over interleaving-based ones for achieving scalability when parallelism enters the picture.
For the entire collection see [Zbl 1502.68030].Parameterized programming for compositional system specificationhttps://zbmath.org/1517.682462023-09-22T14:21:46.120933Z"Martín, Óscar"https://zbmath.org/authors/?q=ai:martin.oscar"Verdejo, Alberto"https://zbmath.org/authors/?q=ai:verdejo.alberto"Martí-Oliet, Narciso"https://zbmath.org/authors/?q=ai:marti-oliet.narcisoSummary: Our overall goal is compositional specification and verification in rewriting logic. In previous work, we described a way to compose system specifications using the operation we call synchronous composition. In this paper, we propose the use of parameterized programming to encapsulate and handle specifications: theories represent interfaces; modules parameterized by such theories instruct on how to assemble the parameter systems using the synchronous composition operation; the implementation of the whole system is then obtained by instantiating the parameters with implementations for the components. We show, and illustrate with examples, how this setting facilitates compositionality.
For the entire collection see [Zbl 1398.68038].Model checking PA-processeshttps://zbmath.org/1517.682472023-09-22T14:21:46.120933Z"Mayr, Richard"https://zbmath.org/authors/?q=ai:mayr.richard-mSummary: PA (Process algebra) is the name that has become common use to denote the algebra with a sequential and parallel operator (without communication), plus recursion. PA-processes subsume both Basic Parallel Processes (BPP)
[\textit{S. Christensen}, Decidability and decomposition in process algebras. Edinburgh: Edinburgh University (PhD thesis) (1993)]
and context-free processes (BPA). They are a simple model for infinite state concurrent systems. We show that the model checking problem for the branching time temporal logic EF is decidable for PA-processes.
For the entire collection see [Zbl 1434.68030].Automated verification of parallel nested DFShttps://zbmath.org/1517.682482023-09-22T14:21:46.120933Z"Oortwijn, Wytse"https://zbmath.org/authors/?q=ai:oortwijn.wytse"Huisman, Marieke"https://zbmath.org/authors/?q=ai:huisman.marieke"Joosten, Sebastiaan J. C."https://zbmath.org/authors/?q=ai:joosten.sebastiaan-j-c"van de Pol, Jaco"https://zbmath.org/authors/?q=ai:van-de-pol.jan-cornelisSummary: Model checking algorithms are typically complex graph algorithms, whose correctness is crucial for the usability of a model checker. However, establishing the correctness of such algorithms can be challenging and is often done manually. Mechanising the verification process is crucially important, because model checking algorithms are often parallelised for efficiency reasons, which makes them even more error-prone.
This paper shows how the VerCors concurrency verifier is used to mechanically verify the parallel nested depth-first search (NDFS) graph algorithm of
\textit{A. Laarman} et al. [Lect. Notes Comput. Sci. 6996, 321--335 (2011; Zbl 1348.68142)].
We also demonstrate how having a mechanised proof supports the easy verification of various optimisations of parallel NDFS. As far as we are aware, this is the first automated deductive verification of a multi-core model checking algorithm.
For the entire collection see [Zbl 1496.68011].Modular verification of concurrent programs via sequential model checkinghttps://zbmath.org/1517.682492023-09-22T14:21:46.120933Z"Rasin, Dan"https://zbmath.org/authors/?q=ai:rasin.dan"Grumberg, Orna"https://zbmath.org/authors/?q=ai:grumberg.orna"Shoham, Sharon"https://zbmath.org/authors/?q=ai:shoham.sharonSummary: This work utilizes the plethora of work on verification of sequential programs for the purpose of verifying concurrent programs. We reduce the verification of a concurrent program to a series of verification tasks of sequential programs. Our approach is modular in the sense that each sequential verification task roughly corresponds to the verification of a single thread, with some additional information about the environment in which it operates. Information regarding the environment is gathered during the run of the algorithm, by need. While our approach is general, it specializes on concurrent programs where the threads are structured hierarchically. The idea is to exploit the hierarchy in order to minimize the amount of information that needs to be transferred between threads. To that end, we verify one of the threads, considered ``main'', as a sequential program. Its verification process initiates queries to its ``environment'' (which may contain multiple threads). Those queries are answered by sequential verification, if the environment consists of a single thread, or, otherwise, by applying the same hierarchical algorithm on the environment. Our technique is fully automatic, and allows us to use any off-the-shelf sequential model checker. We implemented our technique in a tool called CoMuS and evaluated it against established tools for concurrent verification. Our experiments show that it works particularly well on hierarchically structured programs.
For the entire collection see [Zbl 1396.68018].Multi-head monitoring of metric dynamic logichttps://zbmath.org/1517.682502023-09-22T14:21:46.120933Z"Raszyk, Martin"https://zbmath.org/authors/?q=ai:raszyk.martin"Basin, David"https://zbmath.org/authors/?q=ai:basin.david-a"Traytel, Dmitriy"https://zbmath.org/authors/?q=ai:traytel.dmitrySummary: We develop a monitoring algorithm for metric dynamic logic, an extension of metric temporal logic with regular expressions. The monitor computes whether a given formula is satisfied at every position in an input trace of time-stamped events. Our monitor follows the multi-head paradigm: it reads the input simultaneously at multiple positions and moves its reading heads asynchronously. This mode of operation results in unprecedented space complexity guarantees for metric dynamic logic: The monitor's memory consumption neither depends on the event-rate, i.e., the number of events within a fixed time-unit, nor on the numeric constants occurring in the quantitative temporal constraints in the given formula. We formally prove our algorithm correct in the Isabelle proof assistant, integrate it in the Hydra monitoring tool, and empirically demonstrate its strong performance.
For the entire collection see [Zbl 1502.68030].A formally verified motion planner for autonomous vehicleshttps://zbmath.org/1517.682512023-09-22T14:21:46.120933Z"Rizaldi, Albert"https://zbmath.org/authors/?q=ai:rizaldi.albert"Immler, Fabian"https://zbmath.org/authors/?q=ai:immler.fabian"Schürmann, Bastian"https://zbmath.org/authors/?q=ai:schurmann.bastian"Althoff, Matthias"https://zbmath.org/authors/?q=ai:althoff.matthiasSummary: Autonomous vehicles are safety-critical cyber-physical systems. To ensure their correctness, we use a proof assistant to prove safety properties deductively. This paper presents a formally verified motion planner based on manoeuvre automata in Isabelle/HOL. Two general properties which we ensure are numerical soundness (the absence of floating-point errors) and logical correctness (satisfying a plan specified in linear temporal logic). From these two properties, we obtain a motion planner whose correctness only depends on the validity of the models of the ego vehicle and its environment.
For the entire collection see [Zbl 1396.68018].Synthesizing clock-efficient timed automatahttps://zbmath.org/1517.682522023-09-22T14:21:46.120933Z"Saeedloei, Neda"https://zbmath.org/authors/?q=ai:saeedloei.neda"Kluźniak, Feliks"https://zbmath.org/authors/?q=ai:kluzniak.feliksSummary: We describe a new approach to synthesizing a timed automaton from a set of timed scenarios. The set of scenarios specifies a set of behaviours, i.e., sequences of events that satisfy the time constraints imposed by the scenarios. The language of the constructed automaton is equivalent to that set of behaviours. Every location of the automaton appears in at least one accepting run, and its graph is constructed so as to minimise the number of clocks. The construction allows a new clock allocation algorithm whose cost is linear in the number of edges.
For the entire collection see [Zbl 1507.68030].Signal convolution logichttps://zbmath.org/1517.682532023-09-22T14:21:46.120933Z"Silvetti, Simone"https://zbmath.org/authors/?q=ai:silvetti.simone"Nenzi, Laura"https://zbmath.org/authors/?q=ai:nenzi.laura"Bartocci, Ezio"https://zbmath.org/authors/?q=ai:bartocci.ezio"Bortolussi, Luca"https://zbmath.org/authors/?q=ai:bortolussi.lucaSummary: We introduce a new logic called \textit{Signal Convolution Logic} (SCL) that combines temporal logic with convolutional filters from digital signal processing. SCL enables to reason about the percentage of time a formula is satisfied in a bounded interval. We demonstrate that this new logic is a suitable formalism to effectively express non-functional requirements in Cyber-Physical Systems displaying noisy and irregular behaviours. We define both a qualitative and quantitative semantics for it, providing an efficient monitoring procedure. Finally, we prove SCL at work to monitor the \textit{artificial pancreas} controllers that are employed to automate the delivery of insulin for patients with type-1 diabetes.
For the entire collection see [Zbl 1396.68018].Verification of the IBOS browser security properties in reachability logichttps://zbmath.org/1517.682542023-09-22T14:21:46.120933Z"Skeirik, Stephen"https://zbmath.org/authors/?q=ai:skeirik.stephen"Meseguer, José"https://zbmath.org/authors/?q=ai:meseguer.jose"Rocha, Camilo"https://zbmath.org/authors/?q=ai:rocha.camiloSummary: This paper presents a rewriting logic specification of the Illinois Browser Operating System (IBOS) and defines several security properties, including the \textit{same-origin policy} (SOP) in reachability logic. It shows how these properties can be deductively verified using our constructor-based reachability logic theorem prover. This paper also highlights the reasoning techniques used in the proof and three modularity principles that have been crucial to scale up and complete the verification effort.
For the entire collection see [Zbl 1502.68028].Algebra for treeshttps://zbmath.org/1517.682552023-09-22T14:21:46.120933Z"Bojańczyk, Mikołaj"https://zbmath.org/authors/?q=ai:bojanczyk.mikolajThis chapter recalls most relevant developments in the area of algebraic approaches to regular tree or forest languages. It focusses on effective characterizations in the spirit of the famous characterization of starfree languages by their syntactic monoids. To this end, it first illustrates the principal differences between trees and strings on Potthoff's example. It then recalls the classic algebraic approach to regular tree languages in terms of \(\Sigma\)-algebras, where \(\Sigma\) is the ranked alphabet of tree labels. The essential results obtained with the help of this algebraic approach are presented and it is argued why this approach falls short for many interesting questions. These shortcomings are illustrated on the definite tree languages, which can be successfully characterized by equalities on the syntactic algebra, but in a slightly surprising manner. Another successful example for first-order logic with only \(i\)-th child relations is also provided. Next, a basic recipe is provided for constructing new algebras that may help to characterize further interesting subclasses. This recipe is then utilized to present three types of algebras that each have their own advantages and disadvantages.
The first algebraic approach following the recipe concerns preclones, in which the basic objects are all multicontexts sorted according to their number of substitution sites. The free algebra is successfully identified and an application is presented showing that the 2-variable property fails for tree logics. The second application of the recipe yields the forest algebras in which sequences of trees and contexts are the basic objects. Also, the success of this approach is demonstrated by the label-testable tree languages and the logical fragment EF. The final approach following the recipe now simply considers sequences of multicontexts with an arbitrary number of substitution sites. The obtained algebra has only a single sort and fulfills several of the axioms of a semiring, but may fail commutativity of sum, right-distributivity, and absorption from the right. These structures are thus called seminearrings. The identification of the free algebra is again successful and the utility of this approach is demonstrated on the logic EF. Additionally, the author identifies the tree languages that are characterized by actual semirings (without right absorption) and shows that these are exactly the path-testable tree languages. The final approach concerns nesting algebras that are utilized to model the nesting in logical formulas. It is demonstrated that seminearrings are closed under wreath products and that the modelling is successful in principle, but the structure of the wreath product gets lost in the quotients, so potentially hiding additional insight.
The chapter is extremely well written and provides ample intuition, but assumes some familiarity with tree languages and first-order logics on trees. Earlier chapters in the Handbook probably provide those basics, so the author assumes good familiarity with these notions and concepts. Proofs or proof ideas are provided for all major statements and examples are discussed in suitable detail to fully appreciate them. The author covers all major algebraic approaches at the time of drafting the chapter and even provides an update on the work conducted between that first draft and the final version before publication of the chapter (Section 8). Overall, this chapter is an excellent reference to all algebraic approaches to characterizing subclasses of the regular tree languages.
For the entire collection see [Zbl 1470.68001].
Reviewer: Andreas Maletti (Leipzig)Inequalities for one-step productshttps://zbmath.org/1517.682562023-09-22T14:21:46.120933Z"Branco, Mário J. J."https://zbmath.org/authors/?q=ai:branco.mario-j-j"Pin, Jean-Éric"https://zbmath.org/authors/?q=ai:pin.jean-ericSummary: Let \(a\) be a letter of an alphabet \(A\). Given a lattice of languages \(\mathcal{L}\), we describe the set of ultrafilter inequalities satisfied by the lattice \(\mathcal{L}_{a}\) generated by the languages of the form \(L\) or \(LaA^*\), where \(L\) is a language of \(\mathcal{L}\). We also describe the ultrafilter inequalities satisfied by the lattice \(\mathcal{L}_1\) generated by the lattices \(\mathcal{L}_{a}\), for \(a\in A\). When \(\mathcal{L}\) is a lattice of regular languages, we first describe the profinite inequalities satisfied by \(\mathcal{L}_a\) and \(\mathcal{L}_1\) and then provide a small basis of inequalities defining \(\mathcal{L}_1\) when \(\mathcal{L}\) is a Boolean algebra of regular languages closed under quotient.
For the entire collection see [Zbl 1398.68030].Round-bounded control of parameterized systemshttps://zbmath.org/1517.682572023-09-22T14:21:46.120933Z"Bollig, Benedikt"https://zbmath.org/authors/?q=ai:bollig.benedikt"Lehaut, Mathieu"https://zbmath.org/authors/?q=ai:lehaut.mathieu"Sznajder, Nathalie"https://zbmath.org/authors/?q=ai:sznajder.nathalieSummary: We consider systems with unboundedly many processes that communicate through shared memory. In that context, simple verification questions have a high complexity or, in the case of pushdown processes, are even undecidable. Good algorithmic properties are recovered under round-bounded verification, which restricts the system behavior to a bounded number of round-robin schedules. In this paper, we extend this approach to a game-based setting. This allows one to solve synthesis and control problems and constitutes a further step towards a theory of languages over infinite alphabets.
For the entire collection see [Zbl 1396.68018].Synchronous development of asynchronous systemshttps://zbmath.org/1517.682582023-09-22T14:21:46.120933Z"Fischer, Clemens"https://zbmath.org/authors/?q=ai:fischer.clemens"Janssen, Wil"https://zbmath.org/authors/?q=ai:janssen.wilSummary: Formal specifications of communicating systems should describe an abstract view of a system and hide unnecessary implementation details. A problematic implementation detail is the kind of communication used in an open or distributed system. We argue that \textit{synchronous} communication is easier to use and to analyse and should be prefered over \textit{asynchronous} communication at early stages of software development. Therefore we present a new class of systems that have the same semantics both with synchronous and with asynchronous communication. Such systems can be developed and verified on the basis of synchronous communication without losing an efficient asynchronous implementation. As formal framework we use CSP and develop a unified theory of asynchronous and synchronous communication in the style of
[\textit{J. He} et al., ``A theory of synchrony and asynchrony'', in: M. Broy (ed.) and C. B. Jones (ed.), Proceedings of the IFIP working conference on programming concepts and methods. North-Holland: Elsevier. 459--478 (1990)].
Our approach generalises the `delay insensitive circuits approach' where integrated circuits are developed without assumptions on wire delays. Hence, it can be applied to a wide range of applications from IC design to telecommunication systems.
For the entire collection see [Zbl 0915.00046].Urgent partial order reduction for extended timed automatahttps://zbmath.org/1517.682592023-09-22T14:21:46.120933Z"Larsen, Kim G."https://zbmath.org/authors/?q=ai:larsen.kim-gulstrand|larsen.kim-guldstrand"Mikučionis, Marius"https://zbmath.org/authors/?q=ai:mikucionis.marius"Muñiz, Marco"https://zbmath.org/authors/?q=ai:muniz.marco"Srba, Jiří"https://zbmath.org/authors/?q=ai:srba.jiriSummary: We propose a partial order reduction method for reachability analysis of networks of timed automata interacting via synchronous channel communication and via shared variables. Our method is based on (classical) symbolic delay transition systems and exploits the urgent behavior of a system, where time does not introduce dependencies among actions. In the presence of urgent behavior in the network, we apply partial order reduction techniques for discrete systems based on stubborn sets. We first describe the framework in the general setting of symbolic delay time transition systems and then instantiate it to the case of timed automata. We implement our approach in the model checker \textsc{Uppaal} and observe a substantial reduction in the reachable state space for case studies that exhibit frequent urgent behaviour and only a moderate slowdown on models with limited occurence of urgency.
For the entire collection see [Zbl 1502.68030].Petri nets semantics of reaction rules (RR). A language for ecosystems modellinghttps://zbmath.org/1517.682602023-09-22T14:21:46.120933Z"Pommereau, Franck"https://zbmath.org/authors/?q=ai:pommereau.franck"Thomas, Colin"https://zbmath.org/authors/?q=ai:thomas.colin"Gaucherel, Cédric"https://zbmath.org/authors/?q=ai:gaucherel.cedricSummary: The \textsc{eden} framework provides formal modelling and analysis tools to study ecosystems. At the heart of the framework is the \textit{reaction rules} (\textsc{rr}) modelling language, that is equipped with an operational semantics and can be translated into Petri nets with equivalent semantics. In this paper, we formally define the \textsc{rr} language and its semantics, detailing the initial definition from
[the first and the third author, Methods Ecol. Evol. 10, No. 9, 1615--1627 (2019; \url{doi:10.1111/2041-210X.13242})]
and extending it with a notion of \textit{constraints} that allows to model mandatory events. Then, we consider in turn two classes of Petri nets: \textit{priority Petri nets} (\textsc{ppn}), which are safe place/transition Petri nets equipped with transitions priorities, and \textit{extended Petri nets} (\textsc{epn}) which are \textsc{ppn} further extended with read arcs, inhibitor arcs, and reset arcs. For each of these classes, we define the translation of an \textsc{rr} system into a Petri net and prove that the state-space generated with the \textsc{rr} operational semantics is equivalent to the marking graph of the Petri net resulting from the translation. We use a very strong notion of equivalence by considering \textit{labelled transition systems} (\textsc{lts}) isomophism with states and labels matching.
For the entire collection see [Zbl 1492.68011].Real-time rewriting logic semantics for spatial concurrent constraint programminghttps://zbmath.org/1517.682612023-09-22T14:21:46.120933Z"Ramírez, Sergio"https://zbmath.org/authors/?q=ai:ramirez.sergio"Romero, Miguel"https://zbmath.org/authors/?q=ai:romero.miguel"Rocha, Camilo"https://zbmath.org/authors/?q=ai:rocha.camilo"Valencia, Frank"https://zbmath.org/authors/?q=ai:valencia.frank-dSummary: Process calculi provide a language in which the structure of \textit{terms} represents the structure of processes together with an \textit{operational semantics} to represent computational steps. This paper uses rewriting logic for specifying and analyzing a process calculus for \textit{concurrent constraint programming} (\textsf{ccp}), combining spatial and real-time behavior. In these systems, agents can run processes in different computational spaces (e.g., containers) while subject to real-time requirements (e.g., upper bounds in the execution time of a given operation), which can be specified with both discrete and dense linear time. The real-time rewriting logic semantics is fully executable in Maude with the help of rewriting modulo SMT: partial information (i.e., constraints) in the specification is represented by quantifier-free formulas on the shared variables of the system that are under the control of SMT decision procedures. The approach is used to symbolically analyze existential real-time reachability properties of process calculi in the presence of spatial hierarchies for sharing information and knowledge.
For the entire collection see [Zbl 1398.68038].Philosophers may dine -- definitively!https://zbmath.org/1517.682622023-09-22T14:21:46.120933Z"Taha, Safouan"https://zbmath.org/authors/?q=ai:taha.safouan"Wolff, Burkhart"https://zbmath.org/authors/?q=ai:wolff.burkhart"Ye, Lina"https://zbmath.org/authors/?q=ai:ye.linaSummary: The theory of Communicating Sequential Processes going back to Hoare and Roscoe is still today one of the reference theories for concurrent specification and computing. In 1997, a first formalization in Isabelle/HOL of the denotational semantics of the Failure/Divergence Model of CSP was undertaken; in particular, this model can cope with infinite alphabets, in contrast to model-checking approaches limited to finite ones. In this paper, we extend this theory to a significant degree by taking advantage of more powerful automation of modern Isabelle version, which came even closer to recent developments in the semantic foundation of CSP.
More importantly, we use this formal development to analyse a family of refinement notions, comprising classic and new ones. This analysis enabled us to derive a number of properties that allow to deepen the understanding of these notions, in particular with respect to specification decomposition principles in the infinite case. Better definitions allow to clarify a number of obscure points in the classical literature, for example concerning the relationship between deadlock- and livelock-freeness. As a result, we have a modern environment for formal proofs of concurrent systems that allow to combine general infinite processes with locally finite ones in a logically safe way. We demonstrate a number of verification-techniques for classical, generalized examples: The CopyBuffer and Dijkstra's Dining Philosopher Problem of an arbitrary size.
For the entire collection see [Zbl 1507.68030].Faster algorithms for quantitative analysis of MCs and MDPs with small treewidthhttps://zbmath.org/1517.682632023-09-22T14:21:46.120933Z"Asadi, Ali"https://zbmath.org/authors/?q=ai:asadi.ali-naghash"Chatterjee, Krishnendu"https://zbmath.org/authors/?q=ai:chatterjee.krishnendu"Goharshady, Amir Kafshdar"https://zbmath.org/authors/?q=ai:goharshady.amir-kafshdar"Mohammadi, Kiarash"https://zbmath.org/authors/?q=ai:mohammadi.kiarash"Pavlogiannis, Andreas"https://zbmath.org/authors/?q=ai:pavlogiannis.andreasSummary: Discrete-time Markov Chains (MCs) and Markov Decision Processes (MDPs) are two standard formalisms in system analysis. Their main associated \textit{quantitative} objectives are hitting probabilities, discounted sum, and mean payoff. Although there are many techniques for computing these objectives in general MCs/MDPs, they have not been thoroughly studied in terms of parameterized algorithms, particularly when treewidth is used as the parameter. This is in sharp contrast to \textit{qualitative} objectives for MCs, MDPs and graph games, for which treewidth-based algorithms yield significant complexity improvements. In this work, we show that treewidth can also be used to obtain faster algorithms for the quantitative problems. For an MC with \(n\) states and \(m\) transitions, we show that each of the classical quantitative objectives can be computed in \(O((n+m)\cdot t^2)\) time, given a tree decomposition of the MC with width \(t\). Our results also imply a bound of \(O(\kappa \cdot (n+m)\cdot t^2)\) for each objective on MDPs, where \(\kappa\) is the number of strategy-iteration refinements required for the given input and objective. Finally, we make an experimental evaluation of our new algorithms on low-treewidth MCs and MDPs obtained from the DaCapo benchmark suite. Our experiments show that on low-treewidth MCs and MDPs, our algorithms outperform existing well-established methods by one or more orders of magnitude.
For the entire collection see [Zbl 1502.68030].New and improved algorithms for unordered tree inclusionhttps://zbmath.org/1517.682672023-09-22T14:21:46.120933Z"Akutsu, Tatsuya"https://zbmath.org/authors/?q=ai:akutsu.tatsuya"Jansson, Jesper"https://zbmath.org/authors/?q=ai:jansson.jesper"Li, Ruiming"https://zbmath.org/authors/?q=ai:li.ruiming"Takasu, Atsuhiro"https://zbmath.org/authors/?q=ai:takasu.atsuhiro"Tamura, Takeyuki"https://zbmath.org/authors/?q=ai:tamura.takeyukiSummary: The \textit{tree inclusion problem} is, given two node-labeled trees \(P\) and \(T\) (the ``pattern tree'' and the ``target tree''), to locate every minimal subtree in \(T\) (if any) that can be obtained by applying a sequence of node insertion operations to \(P\). Although the \textit{ordered} tree inclusion problem is solvable in polynomial time, the \textit{unordered} tree inclusion problem is NP-hard. The currently fastest algorithm for the latter is a classic algorithm by Kilpeläinen and Mannila from 1995 that runs in \(O(d 2^{2 d} m n)\) time, where \(m\) and \(n\) are the sizes of the pattern and target trees, respectively, and \(d\) is the degree of the pattern tree. Here, we develop a new algorithm that runs in \(O(d 2^d m n^2)\) time, improving the exponential factor from \(2^{2 d}\) to \(2^d\) by considering a particular type of ancestor-descendant relationships that is suitable for dynamic programming. We also study restricted variants of the unordered tree inclusion problem.New and improved algorithms for unordered tree inclusionhttps://zbmath.org/1517.682682023-09-22T14:21:46.120933Z"Akutsu, Tatsuya"https://zbmath.org/authors/?q=ai:akutsu.tatsuya"Jansson, Jesper"https://zbmath.org/authors/?q=ai:jansson.jesper"Li, Ruiming"https://zbmath.org/authors/?q=ai:li.ruiming"Takasu, Atsuhiro"https://zbmath.org/authors/?q=ai:takasu.atsuhiro"Tamura, Takeyuki"https://zbmath.org/authors/?q=ai:tamura.takeyukiSummary: The tree inclusion problem is, given two node-labeled trees \(P\) and \(T\) (the ``pattern tree'' and the ``text tree''), to locate every minimal subtree in \(T\) (if any) that can be obtained by applying a sequence of node insertion operations to \(P\). Although the ordered tree inclusion problem is solvable in polynomial time, the unordered tree inclusion problem is NP-hard. The currently fastest algorithm for the latter is from 1995 and runs in \(O(\operatorname{poly}(m,n)\cdot 2^{2d})= O^*(2^{2d})\) time, where \(m\) and \(n\) are the sizes of the pattern and text trees, respectively, and \(d\) is the maximum outdegree of the pattern tree. Here, we develop a new algorithm that improves the exponent \(2d\) to \(d\) by considering a particular type of ancestor-descendant relationships and applying dynamic programming, thus reducing the time complexity to \(O^*(2^d)\). We then study restricted variants of the unordered tree inclusion problem where the number of occurrences of different node labels and/or the input trees' heights are bounded. We show that although the problem remains NP-hard in many such cases, it can be solved in polynomial time for \(c=2\) and in \(O^*(1.8^d)\) time for \(c=3\) if the leaves of \(P\) are distinctly labeled and each label occurs at most \(c\) times in \(T\). We also present a randomized \(O^*(1.883^d)\)-time algorithm for the case that the heights of \(P\) and \(T\) are one and two, respectively.
For the entire collection see [Zbl 1407.68036].On minimum connecting transition sets in graphshttps://zbmath.org/1517.682722023-09-22T14:21:46.120933Z"Bellitto, Thomas"https://zbmath.org/authors/?q=ai:bellitto.thomas"Bergougnoux, Benjamin"https://zbmath.org/authors/?q=ai:bergougnoux.benjaminSummary: A forbidden transition graph is a graph defined together with a set of permitted transitions i.e. unordered pair of adjacent edges that one may use consecutively in a walk in the graph. In this paper, we look for the smallest set of transitions needed to be able to go from any vertex of the given graph to any other. We prove that this problem is NP-hard and study approximation algorithms. We develop theoretical tools that help to study this problem.
For the entire collection see [Zbl 1398.68016].Token sliding on split graphshttps://zbmath.org/1517.682732023-09-22T14:21:46.120933Z"Belmonte, Rémy"https://zbmath.org/authors/?q=ai:belmonte.remy"Kim, Eun Jung"https://zbmath.org/authors/?q=ai:kim.eun-jung"Lampis, Michael"https://zbmath.org/authors/?q=ai:lampis.michael"Mitsou, Valia"https://zbmath.org/authors/?q=ai:mitsou.valia"Otachi, Yota"https://zbmath.org/authors/?q=ai:otachi.yota"Sikora, Florian"https://zbmath.org/authors/?q=ai:sikora.florianSummary: We consider the complexity of the \textsc{Independent Set Reconfiguration} problem under the Token Sliding rule. In this problem we are given two independent sets of a graph and are asked if we can transform one to the other by repeatedly exchanging a vertex that is currently in the set with one of its neighbors, while maintaining the set independent. Our main result is to show that this problem is PSPACE-complete on split graphs (and hence also on chordal graphs), thus resolving an open problem in this area. We then go on to consider the \(c\)-\textsc{Colorable Reconfiguration} problem under the same rule, where the constraint is now to maintain the set \(c\)-colorable at all times. As one may expect, a simple modification of our reduction shows that this more general problem is PSPACE-complete for all fixed \(c\geq 1\) on chordal graphs. Somewhat surprisingly, we show that the same cannot be said for split graphs: we give a polynomial time \((n^{O(c)})\) algorithm for all fixed values of \(c\), except \(c=1\), for which the problem is PSPACE-complete. We complement our algorithm with a lower bound showing that \(c\)-\textsc{Colorable Reconfiguration} is W[2]-hard on split graphs parameterized by \(c\) and the length of the solution, as well as a tight ETH-based lower bound for both parameters. Finally, we study \(c\)-\textsc{Colorable Reconfiguration} under a relaxed rule called Token Jumping, where exchanged vertices are not required to be adjacent. We show that the problem on chordal graphs is PSPACE-complete even if \(c\) is some fixed constant. We then show that the problem is polynomial-time solvable for strongly chordal graphs even if \(c\) is a part of the input.Token sliding on split graphshttps://zbmath.org/1517.682742023-09-22T14:21:46.120933Z"Belmonte, Rémy"https://zbmath.org/authors/?q=ai:belmonte.remy"Kim, Eun Jung"https://zbmath.org/authors/?q=ai:kim.eun-jung"Lampis, Michael"https://zbmath.org/authors/?q=ai:lampis.michael"Mitsou, Valia"https://zbmath.org/authors/?q=ai:mitsou.valia"Otachi, Yota"https://zbmath.org/authors/?q=ai:otachi.yota"Sikora, Florian"https://zbmath.org/authors/?q=ai:sikora.florianSummary: We consider the complexity of the Independent Set Reconfiguration problem under the Token Sliding rule. In this problem we are given two independent sets of a graph and are asked if we can transform one to the other by repeatedly exchanging a vertex that is currently in the set with one of its neighbors, while maintaining the set independent. Our main result is to show that this problem is PSPACE-complete on split graphs (and hence also on chordal graphs), thus resolving an open problem in this area.\par We then go on to consider the \(c\)-Colorable Reconfiguration problem under the same rule, where the constraint is now to maintain the set \(c\)-colorable at all times. As one may expect, a simple modification of our reduction shows that this more general problem is PSPACE-complete for all fixed \(c\ge 1\) on chordal graphs. Somewhat surprisingly, we show that the same cannot be said for split graphs: we give a polynomial time \((n^{O(c)})\) algorithm for all fixed values of \(c\), except \(c=1\), for which the problem is PSPACE-complete. We complement our algorithm with a lower bound showing that \(c\)-Colorable Reconfiguration is W[2]-hard on split graphs parameterized by \(c\) and the length of the solution, as well as a tight ETH-based lower bound for both parameters.
For the entire collection see [Zbl 1411.68018].Recognizing hyperelliptic graphs in polynomial timehttps://zbmath.org/1517.682762023-09-22T14:21:46.120933Z"Bodewes, Jelco M."https://zbmath.org/authors/?q=ai:bodewes.jelco-m"Bodlaender, Hans L."https://zbmath.org/authors/?q=ai:bodlaender.hans-l"Cornelissen, Gunther"https://zbmath.org/authors/?q=ai:cornelissen.gunther"van der Wegen, Marieke"https://zbmath.org/authors/?q=ai:van-der-wegen.mariekeSummary: Based on analogies between algebraic curves and graphs, Baker and Norine introduced divisorial gonality, a graph parameter for multigraphs related to treewidth, multigraph algorithms and number theory. We consider so-called hyperelliptic graphs (multigraphs of gonality 2) and provide a safe and complete set of reduction rules for such multigraphs, showing that we can recognize hyperelliptic graphs in time \(O(n\log n+m)\), where \(n\) is the number of vertices and \(m\) the number of edges of the multigraph. A corollary is that we can decide with the same runtime whether a two-edge-connected graph \(G\) admits an involution \(\sigma\) such that the quotient \(G/\langle\sigma\rangle\) is a tree.
For the entire collection see [Zbl 1398.68016].On directed feedback vertex set parameterized by treewidthhttps://zbmath.org/1517.682772023-09-22T14:21:46.120933Z"Bonamy, Marthe"https://zbmath.org/authors/?q=ai:bonamy.marthe"Kowalik, Łukasz"https://zbmath.org/authors/?q=ai:kowalik.lukasz"Nederlof, Jesper"https://zbmath.org/authors/?q=ai:nederlof.jesper"Pilipczuk, Michał"https://zbmath.org/authors/?q=ai:pilipczuk.michal"Socała, Arkadiusz"https://zbmath.org/authors/?q=ai:socala.arkadiusz"Wrochna, Marcin"https://zbmath.org/authors/?q=ai:wrochna.marcinSummary: We study the Directed Feedback Vertex Set problem parameterized by the treewidth of the input graph. We prove that unless the Exponential Time Hypothesis fails, the problem cannot be solved in time \(2^{o(t\log t)}\cdot n^{\mathcal{O}(1)}\) on general directed graphs, where \(t\) is the treewidth of the underlying undirected graph. This is matched by a dynamic programming algorithm with running time \(2^{\mathcal{O}(t\log t)}\cdot n^{\mathcal {O}(1)}\). On the other hand, we show that if the input digraph is planar, then the running time can be improved to \(2^{\mathcal{O}(t)}\cdot n^{\mathcal{O}(1)}\).
For the entire collection see [Zbl 1398.68016].Optimality program in segment and string graphshttps://zbmath.org/1517.682782023-09-22T14:21:46.120933Z"Bonnet, Édouard"https://zbmath.org/authors/?q=ai:bonnet.edouard"Rzążewski, Paweł"https://zbmath.org/authors/?q=ai:rzazewski.pawelSummary: Planar graphs are known to allow subexponential algorithms running in time \(2^{O(\sqrt{n})}\) or \(2^{O(\sqrt{n}\log n)}\) for most of the paradigmatic problems, while the brute-force time \(2^{\varTheta(n)}\) is very likely to be asymptotically best on general graphs. Intrigued by an algorithm packing curves in \(2^{O(n^{2/3}\log n)}\) by \textit{J. Fox} and \textit{J. Pach} [SODA 2011, 1161--1165 (2011; Zbl 1377.68275)], we investigate which problems have subexponential algorithms on the intersection graphs of curves (string graphs) or segments (segment intersection graphs) and which problems have no such algorithms under the ETH (Exponential Time Hypothesis). Among our results, we show that, quite surprisingly, 3-Coloring can also be solved in time \(2^{O(n^{2/3}\log ^{O(1)}n)}\) on string graphs while an algorithm running in time \(2^{o(n)}\) for 4-Coloring even on axis-parallel segments (of unbounded length) would disprove the ETH. For 4-Coloring of unit segments, we show a weaker lower bound, excluding a \(2^{o(n^{2/3})}\) algorithm (under the ETH). The construction exploits the celebrated Erdős-Szekeres theorem. The subexponential running time also carries over to Min Feedback Vertex Set, but not to Min Dominating Set and Min Independent Dominating Set.
For the entire collection see [Zbl 1398.68016].On the complexity of minimum maximal uniquely restricted matchinghttps://zbmath.org/1517.682822023-09-22T14:21:46.120933Z"Chaudhary, Juhi"https://zbmath.org/authors/?q=ai:chaudhary.juhi"Panda, B. S."https://zbmath.org/authors/?q=ai:panda.bhawani-sankarSummary: A subset \(M \subseteq E\) of edges of a graph \(G = (V, E)\) is called a \textit{matching} if no two edges of \(M\) share a common vertex. A matching \(M\) in a graph \(G\) is called a \textit{uniquely restricted matching} if, \(G [V(M)]\), the subgraph of \(G\) induced by the set of \(M\)-saturated vertices of \(G\) contains exactly one perfect matching. A uniquely restricted matching \(M\) is \textit{maximal} if \(M\) is not properly contained in any uniquely restricted matching of \(G\). Given a graph \(G\), the \textsc{Min-Max-UR Matching} problem asks to find a maximal uniquely restricted matching in \(G\) of minimum cardinality and \textsc{Decide-Min-Max-UR Matching} problem, the decision version of this problem takes a graph \(G\) and an integer \(k\) and asks whether \(G\) admits a maximal uniquely restricted matching of cardinality at most \(k\). It is known that the \textsc{Decide-Min-Max-UR Matching} problem is \(\mathsf{NP} \)-complete. In this paper, we strengthen this result by proving that the \textsc{Decide-Min-Max-UR Matching} problem remains \(\mathsf{NP} \)-complete for chordal bipartite graphs, star-convex bipartite graphs, chordal graphs, and doubly chordal graphs. On the positive side, we prove that the \textsc{Min-Max-UR Matching} problem is polynomial time solvable for bipartite distance-hereditary graphs and linear time solvable for bipartite permutation graphs, proper interval graphs, and threshold graphs. Finally, we prove that the \textsc{Min-Max-UR Matching} problem is \(\mathsf{APX} \)-complete for graphs with maximum degree 4.On the complexity of minimum maximal uniquely restricted matchinghttps://zbmath.org/1517.682832023-09-22T14:21:46.120933Z"Chaudhary, Juhi"https://zbmath.org/authors/?q=ai:chaudhary.juhi"Panda, B. S."https://zbmath.org/authors/?q=ai:panda.bhawani-sankarSummary: A subset \(M\subseteq E\) of edges of a graph \(G=(V,E)\) is called a \textit{matching} if no two edges of \(M\) share a common vertex. A matching \(M\) in a graph \(G\) is called a \textit{uniquely restricted matching} if \(G[V(M)]\), the subgraph of \(G\) induced by the \(M\)-saturated vertices of \(G\), contains exactly one perfect matching. A uniquely restricted matching \(M\) is \textit{maximal} if \(M\) is not properly contained in any other uniquely restricted matching of \(G\). Given a graph \(G\), the \textsc{Min-Max-UR Matching} problem asks to find a maximal uniquely restricted matching of minimum cardinality in \(G\). In general, the decision version of the \textsc{Min-Max-UR Matching} problem is known to be \({\mathsf{NP}} \)-complete for general graphs and remains so even for bipartite graphs. In this paper, we strengthen this result by proving that this problem remains \({\mathsf{NP}} \)-complete for chordal bipartite graphs and chordal graphs. On the positive side, we prove that the \textsc{Min-Max-UR Matching} problem is polynomial time solvable for bipartite permutation graphs and proper interval graphs. Finally, we show that the \textsc{Min-Max-UR Matching} problem is \(\mathsf{APX} \)-complete for bounded degree graphs.
For the entire collection see [Zbl 1507.68048].Independent sets in vertex-arrival streamshttps://zbmath.org/1517.682852023-09-22T14:21:46.120933Z"Cormode, Graham"https://zbmath.org/authors/?q=ai:cormode.graham"Dark, Jacques"https://zbmath.org/authors/?q=ai:dark.jacques"Konrad, Christian"https://zbmath.org/authors/?q=ai:konrad.christianSummary: We consider the maximal and maximum independent set problems in three models of graph streams:
\begin{itemize}\item[--] In the edge model we see a stream of edges which collectively define a graph; this model is well-studied for a variety of problems. We show that the space complexity for a one-pass streaming algorithm to find a maximal independent set is quadratic (i.e. we must store all edges). We further show that it is not much easier if we only require approximate maximality. This contrasts strongly with the other two vertex-based models, where one can greedily find an exact solution in only the space needed to store the independent set.\item[--] In the ``explicit'' vertex model, the input stream is a sequence of vertices making up the graph. Every vertex arrives along with its incident edges that connect to previously arrived vertices. Various graph problems require substantially less space to solve in this setting than in edge-arrival streams. We show that every one-pass \(c\)-approximation streaming algorithm for maximum independent set (MIS) on explicit vertex streams requires \(\Omega(\frac{n^2}{c^6})\) bits of space, where \(n\) is the number of vertices of the input graph. It is already known that \(\widetilde{\Theta}(\frac{n^2}{c^2})\) bits of space are necessary and sufficient in the edge arrival model [\textit{M. M. Halldórsson} et al., Lect. Notes Comput. Sci. 7391, 449--460 (2012; Zbl 1272.68333)], thus the MIS problem is not significantly easier to solve under the explicit vertex arrival order assumption. Our result is proved via a reduction from a new multi-party communication problem closely related to pointer jumping.\item[--] In the ``implicit'' vertex model, the input stream consists of a sequence of objects, one per vertex. The algorithm is equipped with a function that maps pairs of objects to the presence or absence of edges, thus defining the graph. This model captures, for example, geometric intersection graphs such as unit disc graphs. Our final set of results consists of several improved upper and lower bounds for interval and square intersection graphs, in both explicit and implicit streams. In particular, we show a gap between the hardness of the explicit and implicit vertex models for interval graphs.\end{itemize}
For the entire collection see [Zbl 1414.68003].Computing small pivot-minorshttps://zbmath.org/1517.682862023-09-22T14:21:46.120933Z"Dabrowski, Konrad K."https://zbmath.org/authors/?q=ai:dabrowski.konrad-kazimierz"Dross, François"https://zbmath.org/authors/?q=ai:dross.francois"Jeong, Jisu"https://zbmath.org/authors/?q=ai:jeong.jisu"Kanté, Mamadou Moustapha"https://zbmath.org/authors/?q=ai:kante.mamadou-moustapha"Kwon, O-joung"https://zbmath.org/authors/?q=ai:kwon.ojoung"Oum, Sang-il"https://zbmath.org/authors/?q=ai:oum.sang-il"Paulusma, Daniël"https://zbmath.org/authors/?q=ai:paulusma.danielSummary: A graph \(G\) contains a graph \(H\) as a pivot-minor if \(H\) can be obtained from \(G\) by applying a sequence of vertex deletions and edge pivots. Pivot-minors play an important role in the study of rank-width. However, so far, pivot-minors have only been studied from a structural perspective. We initiate a systematic study into their complexity aspects. We first prove that the Pivot-Minor problem, which asks if a given graph \(G\) contains a given graph \(H\) as a pivot-minor, is NP-complete. If \(H\) is not part of the input, we denote the problem by \(H\)-Pivot-Minor. We give a certifying polynomial-time algorithm for \(H\)-Pivot-Minor for every graph \(H\) with \(|V(H)|\leq 4\) except when \(H\in\{K_4,C_3+P_1,4P_1\}\), via a structural characterization of \(H\)-pivot-minor-free graphs in terms of a set \(\mathcal{F}_H\) of minimal forbidden induced subgraphs.
For the entire collection see [Zbl 1398.68016].Subexponential-time and FPT algorithms for embedded flat clustered planarityhttps://zbmath.org/1517.682872023-09-22T14:21:46.120933Z"Da Lozzo, Giordano"https://zbmath.org/authors/?q=ai:da-lozzo.giordano"Eppstein, David"https://zbmath.org/authors/?q=ai:eppstein.david"Goodrich, Michael T."https://zbmath.org/authors/?q=ai:goodrich.michael-t"Gupta, Siddharth"https://zbmath.org/authors/?q=ai:gupta.siddharthSummary: The C-Planarity problem asks for a drawing of a clustered graph, i.e., a graph whose vertices belong to properly nested clusters, in which each cluster is represented by a simple closed region with no edge-edge crossings, no region-region crossings, and no unnecessary edge-region crossings. We study C-Planarity for embedded flat clustered graphs, graphs with a fixed combinatorial embedding whose clusters partition the vertex set. Our main result is a subexponential-time algorithm to test C-Planarity for these graphs when their face size is bounded. Furthermore, we consider a variation of the notion of embedded tree decomposition in which, for each face, including the outer face, there is a bag that contains every vertex of the face. We show that C-Planarity is fixed-parameter tractable with the embedded-width of the underlying graph and the number of disconnected clusters as parameters.
For the entire collection see [Zbl 1398.68016].Graph amalgamation under logical constraintshttps://zbmath.org/1517.682892023-09-22T14:21:46.120933Z"de Oliveira Oliveira, Mateus"https://zbmath.org/authors/?q=ai:de-oliveira-oliveira.mateusSummary: We say that a graph \(G\) is an \(H\)-amalgamation of graphs \(G_1\) and \(G_2\) if \(G\) can be obtained by gluing \(G_1\) and \(G_2\) along isomorphic copies of \(H\). In the Amalgamation Recognition problem we are given connected graphs \(H,G_1,G_2,G\) and the goal is to determine whether \(G\) is an \(H\)-amalgamation of \(G_1\) and \(G_2\). Our main result states that Amalgamation Recognition can be solved in time \(2^{O(\varDelta\cdot t)}\cdot n^{O(t)}\) where \(n,t,\varDelta\) are the number of vertices, the treewidth and the maximum degree of \(G\) respectively.
We generalize the techniques used in our algorithm for \(H\)-amalgamation recognition to the setting in which some of the graphs \(H,G_1,G_2,G\) are not given explicit at the input but are instead required to satisfy some topological property expressible in the counting monadic second order logic of graphs (CMSO logic). In this way, when restricting ourselves to graphs of constant treewidth and degree our approach generalizes certain algorithmic decomposition theorems from structural graph theory from the context of clique-sums to the context in which the interface graph \(H\) is given at the input.
For the entire collection see [Zbl 1398.68016].\(\forall\exists\mathbb {R}\)-completeness and area-universalityhttps://zbmath.org/1517.682902023-09-22T14:21:46.120933Z"Dobbins, Michael Gene"https://zbmath.org/authors/?q=ai:dobbins.michael-gene"Kleist, Linda"https://zbmath.org/authors/?q=ai:kleist.linda"Miltzow, Tillmann"https://zbmath.org/authors/?q=ai:miltzow.tillmann"Rzążewski, Paweł"https://zbmath.org/authors/?q=ai:rzazewski.pawelSummary: In the study of geometric problems, the complexity class \(\exists\mathbb{R}\) plays a crucial role since it exhibits a deep connection between purely geometric problems and real algebra. Sometimes \(\exists\mathbb {R}\) is referred to as the ``real analogue'' to the class NP. While NP is a class of computational problems that deals with existentially quantified Boolean variables, \(\exists\mathbb{R}\) deals with existentially quantified real variables.
In analogy to \(\varPi_2^p\) and \(\varSigma_2^p\) in the famous polynomial hierarchy, we study the complexity classes \(\forall\exists\mathbb{R}\) and \(\exists\forall\mathbb{R}\) with real variables. Our main interest is focused on the Area Universality problem, where we are given a plane graph \(G\), and ask if for each assignment of areas to the inner faces of \(G\) there is an area-realizing straight-line drawing of \(G\). We conjecture that the problem Area Universality is \(\forall\exists\mathbb{R}\)-complete and support this conjecture by a series of partial results, where we prove \(\exists\mathbb{R}\)- and \(\forall\exists\mathbb{R}\)-completeness of variants of Area Universality. To do so, we also introduce first tools to study \(\forall\exists\mathbb{R}\). Finally, we present geometric problems as candidates for \(\forall\exists\mathbb{R}\)-complete problems. These problems have connections to the concepts of imprecision, robustness, and extendability.
For the entire collection see [Zbl 1398.68016].Measuring what matters: a hybrid approach to dynamic programming with treewidthhttps://zbmath.org/1517.682912023-09-22T14:21:46.120933Z"Eiben, Eduard"https://zbmath.org/authors/?q=ai:eiben.eduard"Ganian, Robert"https://zbmath.org/authors/?q=ai:ganian.robert"Hamm, Thekla"https://zbmath.org/authors/?q=ai:hamm.thekla"Kwon, O-joung"https://zbmath.org/authors/?q=ai:kwon.ojoungSummary: We develop a framework for applying treewidth-based dynamic programming on graphs with ``hybrid structure'', i.e., with parts that may not have small treewidth but instead possess other structural properties. Informally, this is achieved by defining a refinement of treewidth which only considers parts of the graph that do not belong to a pre-specified tractable graph class. Our approach allows us to not only generalize existing fixed-parameter algorithms exploiting treewidth, but also fixed-parameter algorithms which use the size of a modulator as their parameter. As the flagship application of our framework, we obtain a parameter that combines treewidth and rank-width to obtain fixed-parameter algorithms for \textsc{Chromatic Number}, \textsc{Hamiltonian Cycle}, and \textsc{Max-Cut}.Measuring what matters: a hybrid approach to dynamic programming with treewidthhttps://zbmath.org/1517.682922023-09-22T14:21:46.120933Z"Eiben, Eduard"https://zbmath.org/authors/?q=ai:eiben.eduard"Ganian, Robert"https://zbmath.org/authors/?q=ai:ganian.robert"Hamm, Thekla"https://zbmath.org/authors/?q=ai:hamm.thekla"Kwon, O-Joung"https://zbmath.org/authors/?q=ai:kwon.ojoungSummary: We develop a framework for applying treewidth-based dynamic programming on graphs with ``hybrid structure'', i.e., with parts that may not have small treewidth but instead possess other structural properties. Informally, this is achieved by defining a refinement of treewidth which only considers parts of the graph that do not belong to a pre-specified tractable graph class. Our approach allows us to not only generalize existing fixed-parameter algorithms exploiting treewidth, but also fixed-parameter algorithms which use the size of a modulator as their parameter. As the flagship application of our framework, we obtain a parameter that combines treewidth and rank-width to obtain fixed-parameter algorithms for Chromatic Number, Hamiltonian Cycle, and Max-Cut.
For the entire collection see [Zbl 1423.68036].Covering a graph with nontrivial vertex-disjoint paths: existence and optimizationhttps://zbmath.org/1517.682952023-09-22T14:21:46.120933Z"Gómez, Renzo"https://zbmath.org/authors/?q=ai:gomez.renzo"Wakabayashi, Yoshiko"https://zbmath.org/authors/?q=ai:wakabayashi.yoshikoSummary: Let \(G\) be a connected graph and \(\mathcal{P}\) be a set of pairwise vertex-disjoint paths in \(G\). We say that \(\mathcal{P}\) is a path cover if every vertex of \(G\) belongs to a path in \(\mathcal{P}\). In the Minimum Path Cover problem, one wishes to find a path cover of minimum cardinality. In this problem, known to be \({\textsc{NP}}\)-hard, the set \(\mathcal{P}\) may contain trivial (single-vertex) paths. We study the problem of finding a path cover composed only of nontrivial paths. First, we show that the Corresponding Existence problem can be reduced to a matching problem on a bipartite graph via the Edmonds-Gallai Decomposition. This reduction gives, in polynomial time, a certificate for both the yes-answer and the no-answer. When trivial paths are forbidden, for the feasible instances, one may consider either minimizing or maximizing the number of paths in the path cover. We show that the maximization problem has a close relation with the maximum matchings of a graph, and can be solved in polynomial time. For the minimization problem on feasible instances, we show that its computational complexity is equivalent to the Minimum Path Cover problem. We also show a linear-time algorithm on (edge-weighted) trees.
For the entire collection see [Zbl 1398.68016].Approximability of open \(k\)-monopoly problemshttps://zbmath.org/1517.683022023-09-22T14:21:46.120933Z"Mishra, Sounaka"https://zbmath.org/authors/?q=ai:mishra.sounaka"Krishna, B. Arjuna"https://zbmath.org/authors/?q=ai:krishna.b-arjuna"Rajakrishnan, Shijin"https://zbmath.org/authors/?q=ai:rajakrishnan.shijinSummary: We consider approximability of two optimization problems called Minimum Open \(k\)-Monopoly (Min-Open-\(k\)-Monopoly) and Minimum Partial Open \(k\)-Monopoly (Min-P-Open-\(k\)-Monopoly), where \(k\) is a fixed positive integer. The objective, in Min-Open-\(k\)-Monopoly, is to find a minimum cardinality vertex set \(S\subseteq V\) in a given graph \(G=(V,E)\) such that \(|N(v)\cap S|\geq\frac{1}{2}|N(v)|+k\), for every vertex \(v \in V\). On the other hand, given a graph \(G=(V,E)\), in Min-P-Open-\(k\)-Monopoly it is required to find a minimum cardinality vertex set \(S\subseteq V\) such that \(|N(v)\cap S|\geq\frac{1}{2} |N(v)|+k\), for every \(v\in V\setminus S\). We prove that Min-Open-\(k\)-Monopoly and Min-P-Open-\(k\)-Monopoly are approximable within a factor of \(O(\log n)\). Then, we show that these two problems cannot be approximated within a factor of \((\frac{1}{3}- \epsilon)\ln n\) and \((\frac{1}{4}-\epsilon)\ln n\), respectively, for any \(\varepsilon>0\), unless \(\mathsf{NP}\subseteq\mathsf{Dtime}(n^{O(\log\log n)})\). For 4-regular graphs, we prove that these two problems are \textsf{APX}-complete. Min-Open-1-Monopoly can be approximated within a factor of \(\frac{26}{21}\approx 1.2381\) where as Min-P-Open-1-Monopoly can be approximated within a factor of 1.65153. For \(k\geq 2\), we also present approximation algorithms for these two problems for \((2k+2)\)-regular graphs.On the maximum edge-pair embedding bipartite matchinghttps://zbmath.org/1517.683052023-09-22T14:21:46.120933Z"Nguyen, Cam Ly"https://zbmath.org/authors/?q=ai:nguyen.cam-ly"Suppakitpaisarn, Vorapong"https://zbmath.org/authors/?q=ai:suppakitpaisarn.vorapong"Surarerks, Athasit"https://zbmath.org/authors/?q=ai:surarerks.athasit"Vajanopath, Phanu"https://zbmath.org/authors/?q=ai:vajanopath.phanuSummary: Given a set of edge pairs in a bipartite graph, we want to find a bipartite matching that includes a maximum number of those edge pairs. While the problem has many applications to wireless localization, to the best of our knowledge, there is no theoretical work for the problem. In this work, unless \(\mathrm{P = NP}\), we show that there is no constant approximation for the problem. Suppose that \(k\) denotes the maximum number of input edge pairs such that a particular node can be in. Inspired by experimental results, we consider the case that \(k\) is small. While there is a simple polynomial-time algorithm for the problem when \(k\) is one, we show that the problem is NP-hard when \(k\) is greater than one. We also devise an efficient \(O(k)\)-approximation algorithm for the problem.
For the entire collection see [Zbl 1435.68040].On the maximum edge-pair embedding bipartite matchinghttps://zbmath.org/1517.683062023-09-22T14:21:46.120933Z"Nguyen, Cam Ly"https://zbmath.org/authors/?q=ai:nguyen.cam-ly"Suppakitpaisarn, Vorapong"https://zbmath.org/authors/?q=ai:suppakitpaisarn.vorapong"Surarerks, Athasit"https://zbmath.org/authors/?q=ai:surarerks.athasit"Vajanopath, Phanu"https://zbmath.org/authors/?q=ai:vajanopath.phanuSummary: Given a set of edge pairs in a complete bipartite graph, we want to find a bipartite matching that includes the maximum number of those edge pairs. While the problem has many applications to wireless localization and computer vision, to the best of our knowledge, there is no theoretical work for the problem. In this work, unless \(\mathrm{P = NP}\), we show that there is no constant approximation for the problem. Then, we consider two special cases of the problem. Suppose that \(k\) denotes the maximum number of input edge pairs such that a particular node can be in. Inspired by experimental results, the first case is for when \(k\) is not large. While there is a simple polynomial-time algorithm for the problem when \(k\) is one, we show that the problem is NP-hard when \(k\) is greater than one. We also devise an efficient \(O(k)\)-approximation algorithm for the problem. For the second case, every pair of nodes in the same partition of the input bipartite graph are labeled with one of \(\chi\) colors. We want to match, between the two partitions, a pair of nodes to a pair of nodes with the same color. Denote \(n\) as the number of nodes, we give an \(O(\sqrt{ \chi n})\)-approximation algorithm for this case.Faster parameterized algorithm for cluster vertex deletionhttps://zbmath.org/1517.683082023-09-22T14:21:46.120933Z"Tsur, Dekel"https://zbmath.org/authors/?q=ai:tsur.dekelSummary: In the \textsc{Cluster Vertex Deletion} problem the input is a graph \(G\) and an integer \(k\). The goal is to decide whether there is a set of vertices \(S\) of size at most \(k\) such that the deletion of the vertices of \(S\) from \(G\) results in a graph in which every connected component is a clique. We give an algorithm for \textsc{Cluster Vertex Deletion} whose running time is \(O^\ast (1.811^k)\).Upper bounds on the length of minimal solutions to certain quadratic word equationshttps://zbmath.org/1517.683152023-09-22T14:21:46.120933Z"Day, Joel D."https://zbmath.org/authors/?q=ai:day.joel-d"Manea, Florin"https://zbmath.org/authors/?q=ai:manea.florin"Nowotka, Dirk"https://zbmath.org/authors/?q=ai:nowotka.dirkSummary: It is a long standing conjecture that the problem of deciding whether a quadratic word equation has a solution is in NP. It has also been conjectured that the length of a minimal solution to a quadratic equation is at most exponential in the length of the equation, with the latter conjecture implying the former. We show that both conjectures hold for some natural subclasses of quadratic equations, namely the classes of regular-reversed, \(k\)-ordered, and variable-sparse quadratic equations. We also discuss a connection of our techniques to the topic of unavoidable patterns, and the possibility of exploiting this connection to produce further similar results.
For the entire collection see [Zbl 1423.68036].Involutive Fibonacci wordshttps://zbmath.org/1517.683182023-09-22T14:21:46.120933Z"Kari, Lila"https://zbmath.org/authors/?q=ai:kari.lila"Kulkarni, Manasi S."https://zbmath.org/authors/?q=ai:kulkarni.manasi-s"Mahalingam, Kalpana"https://zbmath.org/authors/?q=ai:mahalingam.kalpana"Wang, Zihao"https://zbmath.org/authors/?q=ai:wang.zihaoSummary: ``Fibonacci strings'' were first defined by \textit{D. E. Knuth} in his [The art of computer programming. Vol. 1: Fundamental algorithms. London: Addison-Wesley Publishing Company (1968; Zbl 0191.17903)] as being an infinite sequence of strings obtained from two initial letters \(f_1 =a\) and \(f_2 =b\), by the recursive definition \(f_{n+2}=f_{n+1} \cdot f_n\), for all positive integers \(n \geq 1\), where ``\(\cdot\)'' denotes word concatenation. In this paper, we first propose a unified terminology that allows readers to identify the different types of Fibonacci words, and corresponding results, that appear under the umbrella term ``Fibonacci words'' in the extensive literature on the topic. Motivated by ideas stemming from theoretical studies of DNA computing, we then define and exploreinvolutive Fibonacci words \((\phi\)-Fibonacci words and indexed \(\phi\)-Fibonacci words, where \(\phi\) denotes either a morphic or an antimorphic involution), and study various properties of such words.Faithful and effective reward schemes for model-free reinforcement learning of omega-regular objectiveshttps://zbmath.org/1517.683312023-09-22T14:21:46.120933Z"Hahn, Ernst Moritz"https://zbmath.org/authors/?q=ai:hahn.ernst-moritz"Perez, Mateo"https://zbmath.org/authors/?q=ai:perez.mateo"Schewe, Sven"https://zbmath.org/authors/?q=ai:schewe.sven"Somenzi, Fabio"https://zbmath.org/authors/?q=ai:somenzi.fabio"Trivedi, Ashutosh"https://zbmath.org/authors/?q=ai:trivedi.ashutosh"Wojtczak, Dominik"https://zbmath.org/authors/?q=ai:wojtczak.dominikSummary: Omega-regular properties -- specified using linear time temporal logic or various forms of omega-automata -- find increasing use in specifying the objectives of reinforcement learning (RL). The key problem that arises is that of faithful and effective translation of the objective into a scalar reward for model-free RL. A recent approach exploits Büchi automata with restricted nondeterminism to reduce the search for an optimal policy for an \(\omega\)-regular property to that for a simple reachability objective. A possible drawback of this translation is that reachability rewards are sparse, being reaped only at the end of each episode. Another approach reduces the search for an optimal policy to an optimization problem with two interdependent discount parameters. While this approach provides denser rewards than the reduction to reachability, it is not easily mapped to off-the-shelf RL algorithms. We propose a reward scheme that reduces the search for an optimal policy to an optimization problem with a single discount parameter that produces dense rewards and is compatible with off-the-shelf RL algorithms. Finally, we report an experimental comparison of these and other reward schemes for model-free RL with omega-regular objectives.
For the entire collection see [Zbl 1502.68030].Formal specification for deep neural networkshttps://zbmath.org/1517.683452023-09-22T14:21:46.120933Z"Seshia, Sanjit A."https://zbmath.org/authors/?q=ai:seshia.sanjit-arunkumar"Desai, Ankush"https://zbmath.org/authors/?q=ai:desai.ankush"Dreossi, Tommaso"https://zbmath.org/authors/?q=ai:dreossi.tommaso"Fremont, Daniel J."https://zbmath.org/authors/?q=ai:fremont.daniel-j"Ghosh, Shromona"https://zbmath.org/authors/?q=ai:ghosh.shromona"Kim, Edward"https://zbmath.org/authors/?q=ai:kim.edward-d"Shivakumar, Sumukh"https://zbmath.org/authors/?q=ai:shivakumar.sumukh"Vazquez-Chanlatte, Marcell"https://zbmath.org/authors/?q=ai:vazquez-chanlatte.marcell"Yue, Xiangyu"https://zbmath.org/authors/?q=ai:yue.xiangyuSummary: The increasing use of deep neural networks in a variety of applications, including some safety-critical ones, has brought renewed interest in the topic of verification of neural networks. However, verification is most meaningful when performed with high-quality formal specifications. In this paper, we survey the landscape of formal specification for deep neural networks, and discuss the opportunities and challenges for formal methods for this domain.
For the entire collection see [Zbl 1396.68018].F-transducers for contextual text rewritinghttps://zbmath.org/1517.683962023-09-22T14:21:46.120933Z"Mihov, Stoyan"https://zbmath.org/authors/?q=ai:mihov.stoyan"Schulz, Klaus U."https://zbmath.org/authors/?q=ai:schulz.klaus-uSummary: Rule-based text rewriting is a form of language processing where a given input text/string is rewritten to a new output form using some form of knowledge base plus contextual rules. Contextual rewrite dictionaries, to be defined below, represent a general input format for such knowledge bases with contextual rules. We present an algorithm for translating a given contextual rewrite dictionary into an f-transducer. This transducer can be applied to input texts, realizing the intended form of text rewriting. F-transducers are deterministic transducers that use failure transitions in order to reduce the size. A second algorithm is given for composing f-transducers. Using composition, cascaded forms of text rewriting can be realized in a single run over the input text. Put together, a general system for rule-based text rewriting is obtained. The strength of the approach relies on four points. First, the translation algorithm is highly optimized: using the algorithm even huge knowledge bases with contextual conditions can be efficiently converted into f-transducers. Second, since f-tranducers act in a deterministic way a very efficient form of text rewriting is obtained. Third, f-transducers can also be directly applied to text streams. Fourth, composition and the general format of contextual rewrite dictionaries guarantee high flexibility as to the forms of text (stream) rewriting that can be realized.Computing the depth distribution of a set of boxeshttps://zbmath.org/1517.684012023-09-22T14:21:46.120933Z"Barbay, Jérémy"https://zbmath.org/authors/?q=ai:barbay.jeremy"Pérez-Lantero, Pablo"https://zbmath.org/authors/?q=ai:perez-lantero.pablo"Rojas-Ledesma, Javiel"https://zbmath.org/authors/?q=ai:rojas-ledesma.javielSummary: Motivated by the analysis of range queries in databases, we introduce the computation of the \textsf{depth distribution} of a set \(\mathcal{B}\) of \(n\) \(d\)-dimensional boxes (i.e., axis aligned \(d\)-dimensional hyperrectangles), which generalizes the computation of the \textsf{Klee's measure} and \textsf{maximum depth} of \(\mathcal{B} \). We present an algorithm to compute the \textsf{depth distribution} running in time within \(\mathcal{O}( n^{\frac{ d + 1}{ 2}} \log n)\), using space within \(\mathcal{O}(n \log n)\), and refine these upper bound for various measures of difficulty of the input instances. Moreover, we introduce conditional lower bounds for this problem which not only provide insights on how fast the depth distribution can be computed, but also clarify the relation between the \textsc{Depth Distribution} problem and other fundamental problems in computer science.A rule-based system for computation and deduction in Mathematicahttps://zbmath.org/1517.684252023-09-22T14:21:46.120933Z"Marin, Mircea"https://zbmath.org/authors/?q=ai:marin.mircea"Dundua, Besik"https://zbmath.org/authors/?q=ai:dundua.besik"Kutsia, Temur"https://zbmath.org/authors/?q=ai:kutsia.temurSummary: \( \rho\)Log is a system for rule-based programming implemented in Mathematica, a state-of-the-art system for computer algebra. It is based on the usage of (1) conditional rewrite rules to express both computation and deduction, and of (2) patterns with sequence variables, context variables, ordinary variables, and function variables, which enable natural and concise specifications beyond the expressive power of first-order logic. Rules can be labeled with various kinds of strategies, which control their application. Our implementation is based on a rewriting-based calculus proposed by us, called \( \rho\)Log too. We describe the capabilities of our system, the underlying \( \rho\)Log calculus and its main properties, and indicate some applications.
For the entire collection see [Zbl 1502.68028].Constructing antidictionaries of long texts in output-sensitive spacehttps://zbmath.org/1517.684282023-09-22T14:21:46.120933Z"Ayad, Lorraine A. K."https://zbmath.org/authors/?q=ai:ayad.lorraine-a-k"Badkobeh, Golnaz"https://zbmath.org/authors/?q=ai:badkobeh.golnaz"Fici, Gabriele"https://zbmath.org/authors/?q=ai:fici.gabriele"Héliou, Alice"https://zbmath.org/authors/?q=ai:heliou.alice"Pissis, Solon P."https://zbmath.org/authors/?q=ai:pissis.solon-pSummary: A word \(x\) that is absent from a word \(y\) is called \textit{minimal} if all its proper factors occur in \(y\). Given a collection of \(k\) words \(y_1,\dots,y_k\) over an alphabet \(\Sigma\), we are asked to compute the set \(\mathrm{M}^{\ell}_{\{y_1,\dots,y_k\}}\) of minimal absent words of length at most \(\ell\) of the collection \(\{y_1,\dots,y_k\}\). The set \(\mathrm{M}^{\ell}_{\{y_1,\dots,y_k\}}\) contains all the words \(x\) such that \(x\) is absent from all the words of the collection while there exist \(i,j\), such that the maximal proper suffix of \(x\) is a factor of \(y_i\) and the maximal proper prefix of \(x\) is a factor of \(y_j\). In data compression, this corresponds to computing the antidictionary of \(k\) documents. In bioinformatics, it corresponds to computing words that are absent from a genome of \(k\) chromosomes. Indeed, the set \(\mathrm{M}^{\ell}_y\) of minimal absent words of a word \(y\) is equal to \(\mathrm{M}^{\ell}_{\{y_1,\dots,y_k\}}\) for any decomposition of \(y\) into a collection of words \(y_1,\dots,y_k\) such that there is an overlap of length at least \(\ell-1\) between any two consecutive words in the collection. This computation generally requires \(\Omega(n)\) space for \(n=|y|\) using any of the plenty available \(\mathcal{O}(n)\)-time algorithms. This is because an \(\Omega (n)\)-sized text index is constructed over \(y\) which can be impractical for large \(n\). We do the identical computation incrementally using output-sensitive space. This goal is reasonable when \(\|\mathrm{M}^{\ell}_{\{y_1,\dots,y_N\}}\|=o(n)\), for all \(N\in [1,k]\), where \(\Vert S\Vert\) denotes the sum of the lengths of words in set \(S\). For instance, in the human genome, \(n\approx 3\times 10^9\) but \(\|\mathrm{M}^{12}_{\{y_1,\dots,y_k\}}\| \approx 10^6 \). We consider a constant-sized alphabet for stating our results. We show that \textit{all} \(\mathrm{M}^{\ell}_{y_1},\dots,\mathrm{M}^{\ell}_{\{y_1,\dots ,y_k\}}\) can be computed in \(\mathcal{O}(kn+\sum^k_{N=1}\|\mathrm{M}^{\ell}_{\{y_1,\dots,y_N\}}\|)\) total time using \(\mathcal{O}(\text{\textsc{MaxIn}}+\text{\textsc{MaxOut}})\) space, where \textsc{MaxIn} is the length of the longest word in \(\{y_1,\dots,y_k\}\) and \(\text{\textsc{MaxOut}}=\max\limits\{\|\mathrm{M}^{\ell}_{\{y_1,\dots,y_N\}}\| :N\in [1,k]\}\). Proof-of-concept experimental results are also provided confirming our theoretical findings and justifying our contribution.Verified textbook algorithms. A biased surveyhttps://zbmath.org/1517.684432023-09-22T14:21:46.120933Z"Nipkow, Tobias"https://zbmath.org/authors/?q=ai:nipkow.tobias"Eberl, Manuel"https://zbmath.org/authors/?q=ai:eberl.manuel"Haslbeck, Maximilian P. L."https://zbmath.org/authors/?q=ai:haslbeck.maximilian-p-lSummary: This article surveys the state of the art of verifying standard textbook algorithms. We focus largely on the classic text by \textit{T. H. Cormen} et al. [Introduction to algorithms. 3rd ed. Cambridge, MA: MIT Press (2009; Zbl 1187.68679)]. Both correctness and running time complexity are considered.
For the entire collection see [Zbl 1502.68030].Local approach to quantum-inspired classificationhttps://zbmath.org/1517.810172023-09-22T14:21:46.120933Z"Blanzieri, Enrico"https://zbmath.org/authors/?q=ai:blanzieri.enrico"Leporini, Roberto"https://zbmath.org/authors/?q=ai:leporini.roberto"Pastorello, Davide"https://zbmath.org/authors/?q=ai:pastorello.davideSummary: In the context of quantum-inspired machine learning, remarkable mathematical tools for solving classification problems are given by some methods of quantum state discrimination. In this respect, quantum-inspired classifiers based on nearest centroid and Helstrom discrimination have been efficiently implemented on classical computers. We present a local approach combining the kNN algorithm to some quantum-inspired classifiers.Information-theoretical discord for a class of three-qubit X stateshttps://zbmath.org/1517.810272023-09-22T14:21:46.120933Z"Wei, Jia-Ning"https://zbmath.org/authors/?q=ai:wei.jianing"Duan, Zhou-Bo"https://zbmath.org/authors/?q=ai:duan.zhoubo"Zhang, Jun"https://zbmath.org/authors/?q=ai:zhang.jun.5Summary: Based on the definition of multipartite quantum discord proposed in [\textit{C. Radhakrishnan} et al., Phys. Rev. Lett. 124, No. 11, Article ID 110401, 6 p. (2020; \url{doi:10.1103/PhysRevLett.124.110401})], we give the analytic expression for the information-theoretical multipartite quantum discord of one type of three-qubit X states which depend on four real parameters. In addition, we present the level surfaces of multipartite quantum discord of X states. As an application, we investigate the dynamic behavior of multipartite quantum discord for the three-qubit X states under the phase flip channel, which presents the sudden change of multipartite quantum discord.Criteria for SLOCC and LU equivalence of generic multi-qudit stateshttps://zbmath.org/1517.810292023-09-22T14:21:46.120933Z"Chang, Jingmei"https://zbmath.org/authors/?q=ai:chang.jingmei"Jing, Naihuan"https://zbmath.org/authors/?q=ai:jing.naihuan"Zhang, Tinggui"https://zbmath.org/authors/?q=ai:zhang.tingguiSummary: In this paper, we study the stochastic local operation and classical communication (SLOCC) and local unitary (LU) equivalence for multi-qudit states by mode-\(n\) matricization of the coefficient tensors. We establish a new scheme of using the CANDECOMP/PARAFAC (CP) decomposition of tensors to find necessary and sufficient conditions between the mode-\(n\) unfolding and SLOCC\&LU equivalence for pure multi-qudit states. For multipartite mixed states, we present a necessary and sufficient condition for LU equivalence and necessary condition for SLOCC equivalence.Ray-marching Thurston geometrieshttps://zbmath.org/1517.810372023-09-22T14:21:46.120933Z"Coulon, Rémi"https://zbmath.org/authors/?q=ai:coulon.remi"Matsumoto, Elisabetta A."https://zbmath.org/authors/?q=ai:matsumoto.elisabetta-a"Segerman, Henry"https://zbmath.org/authors/?q=ai:segerman.henry"Trettel, Steve J."https://zbmath.org/authors/?q=ai:trettel.steve-jSummary: We describe algorithms that produce accurate real-time interactive in-space views of the eight Thurston geometries using ray-marching. We give a theoretical framework for our algorithms, independent of the geometry involved. In addition to scenes within a geometry \(X\), we also consider scenes within quotient manifolds and orbifolds \(X / \Gamma\). We adapt the Phong lighting model to non-Euclidean geometries. The most difficult part of this is the calculation of light intensity, which relates to the area density of geodesic spheres. We also give extensive practical details for each geometry.Entangled state engineering in the 4-coupled qubits systemhttps://zbmath.org/1517.810392023-09-22T14:21:46.120933Z"Salmanogli, Ahmad"https://zbmath.org/authors/?q=ai:salmanogli.ahmadSummary: This article studies the behavior of the avoided level crossing in the 4-coupled qubit to each other and mainly focuses on how to engineer it. This phenomenon occurs due to the two transitions out of the ground state in a two-coupled qubit, contributing to the entangled states. This essential and unique behavior can be engineered in a quantum circuit. For this reason, a quantum circuit containing 4 qubits is designed, and its quantum Hamiltonian and dynamic equation of the motion are theoretically derived. Analysis of the entanglement between each coupled qubit using the entanglement metric reveals that the strength of the qubit-qubit coupling factor and the qubit's non-linearity play an essential role in engineering the photonic mode entanglement. The results show that the avoided level crossing appears in the photonic mode entanglement. In other words, two or more transitions from the ground state to the multiple excited states for each bias current. However, the interesting point is that the avoided level crossing just occurs for the qubits connected capacitively to the driven field (the first qubit in this work), not for all.A tree-type multiparty quantum key agreement protocol against collusive attackshttps://zbmath.org/1517.810412023-09-22T14:21:46.120933Z"Yang, Hao"https://zbmath.org/authors/?q=ai:yang.hao.2"Lu, Songfeng"https://zbmath.org/authors/?q=ai:lu.songfeng"Zhu, Jianxin"https://zbmath.org/authors/?q=ai:zhu.jianxin"Wu, Junjun"https://zbmath.org/authors/?q=ai:wu.junjun"Zhou, Qing"https://zbmath.org/authors/?q=ai:zhou.qing"Li, Tong"https://zbmath.org/authors/?q=ai:li.tong|li.tong.1Summary: Multiparty quantum key agreement (MQKA) requires sharing a secure and fair key among participants. However, several malicious participants may collude together to steal the privacy of honest participants or determine the shared key, privately. In this work, we propose a tree-type MQKA protocol against collusive attacks, in which the entanglement swapping technology of multi-particle entangled states is used to construct the shared key. Compared with the previous MQKA protocols against collusive attacks, our scheme consumes fewer qubits and only needs to transmit quantum states once, which significantly reduces the consumption of quantum resources.The new discontinuous Galerkin methods based numerical relativity program \texttt{Nmesh}https://zbmath.org/1517.830082023-09-22T14:21:46.120933Z"Tichy, Wolfgang"https://zbmath.org/authors/?q=ai:tichy.wolfgang"Ji, Liwei"https://zbmath.org/authors/?q=ai:ji.liwei"Adhikari, Ananya"https://zbmath.org/authors/?q=ai:adhikari.ananya"Rashti, Alireza"https://zbmath.org/authors/?q=ai:rashti.alireza"Pirog, Michal"https://zbmath.org/authors/?q=ai:pirog.michalSummary: Interpreting gravitational wave observations and understanding the physics of astrophysical compact objects such as black holes or neutron stars requires accurate theoretical models. Here, we present a new numerical relativity computer program, called Nmesh, that has the design goal to become a next generation program for the simulation of challenging relativistic astrophysics problems such as binary black hole or neutron star mergers. In order to efficiently run on large supercomputers, Nmesh uses a discontinuous Galerkin method together with a domain decomposition and mesh refinement that parallelizes and scales well. In this work, we discuss the various numerical methods we use. We also present results of test problems such as the evolution of scalar waves, single black holes and neutron stars, as well as shock tubes. In addition, we introduce a new positivity limiter that allows us to stably evolve single neutron stars without an additional artificial atmosphere, or other more traditional limiters.A new lower bound for deterministic truthful schedulinghttps://zbmath.org/1517.900462023-09-22T14:21:46.120933Z"Giannakopoulos, Yiannis"https://zbmath.org/authors/?q=ai:giannakopoulos.yiannis"Hammerl, Alexander"https://zbmath.org/authors/?q=ai:hammerl.alexander"Poças, Diogo"https://zbmath.org/authors/?q=ai:pocas.diogoSummary: We study the problem of truthfully scheduling \(m\) tasks to \(n\) selfish unrelated machines, under the objective of makespan minimization, as was introduced in the seminal work of \textit{N. Nisan} and \textit{A. Ronen} [``Algorithmic mechanism design (extended abstract)'', in: Proceedings of the 31st annual ACM symposium on theory of computing, STOC 1999. New York, NY: Association for Computing Machinery (ACM). 129--140 (1999; \url{doi:10.1145/301250.30128})]. Closing the current gap of \([2.618,n]\) on the approximation ratio of deterministic truthful mechanisms is a notorious open problem in the field of algorithmic mechanism design. We provide the first such improvement in more than a decade, since the lower bounds of 2.414 (for \(n=3)\) and 2.618 (for \(n\rightarrow\infty)\) by \textit{G. Christodoulou} et al. [``A lower bound for scheduling mechanisms'', in: Proceedings of the 18th annual ACM-SIAM symposium on discrete algorithms, SODA 2007. New York, NY: Association for Computing Machinery (ACM). 1163--1170 (2007; \url{doi:10.5555/1283383.1283508})] and \textit{E. Koutsoupias} and \textit{A. Vidali} [``A lower bound of \(1+\varphi\) for truthful scheduling mechanisms'', in: Proceedings of the 2007 international symposium on mathematical foundations of computer science, MFCS 2007. Berlin, Heidelberg: Springer. 454--464 (2007; \url{doi:10.1007/978-3-540-74456-6_41})], respectively. More specifically, we show that the currently best lower bound of 2.618 can be achieved even for just \(n=4\) machines; for \(n=5\) we already get the first improvement, namely 2.711; and allowing the number of machines to grow arbitrarily large we can get a lower bound of 2.755.EPTAS for load balancing problem on parallel machines with a non-renewable resourcehttps://zbmath.org/1517.900502023-09-22T14:21:46.120933Z"Jaykrishnan, G."https://zbmath.org/authors/?q=ai:jaykrishnan.g"Levin, Asaf"https://zbmath.org/authors/?q=ai:levin.asafSummary: The problem considered is the non-preemptive scheduling of independent jobs that consume a resource (which is non-renewable and replenished regularly) on parallel uniformly related machines. The input defines the speed of machines, size of jobs, the quantity of the resource required by the jobs, the replenished quantities, and replenishment dates of the resource. Every job can start processing only after the required quantity of the resource is allocated to the job. The objective function is a generalization of makespan minimization and minimization of the \(l_p\)-norm of the vector of loads of the machines. We present an EPTAS for this problem. Prior to our work only a PTAS was known in this non-renewable resource settings only for the special case of our problem of makespan minimization on identical machines.A new perspective on single-machine scheduling problems with late work related criteriahttps://zbmath.org/1517.900582023-09-22T14:21:46.120933Z"Shabtay, Dvir"https://zbmath.org/authors/?q=ai:shabtay.dvirSummary: This paper provides two new perspectives on single-machine scheduling problems in which the objective involves penalties regarding late work. Both of this perspectives have been neglected in the previous literature. We begin by presenting a parameterized complexity analysis of the \(\mathcal{NP}\)-hard problem of minimizing the total late work on a single machine. We do so with respect to the following four parameters: (i) the number of different processing times \((v_p)\); (ii) the number of different due dates \((v_d)\); (iii) the maximal processing time \((p_{\max})\); and (iv) the maximal due date \((d_{\max})\). We use results from the literature to conclude that the problem is hard with respect to \(wrt\) parameter \(v_d\) and is tractable (i.e., solvable in \(FPT\) time) \(wrt.p_{\max}\). We then provide two \(FPT\) algorithms showing that the problem is also tractable \(wrt.\) to \(v_p\) and \(d_{\max}\). We continue by analyzing a single-machine scheduling problem with assignable due dates where the cost function to be minimized includes penalties due to weighted early and tardy work. We assume that each job can be assigned a different due-date, the value of which is subject to a job-dependent upper bound. We provide an efficient method to optimally assign due dates for a given job schedule. We then use this result to reduce the problem to a purely combinatorial problem, which we show is \(\mathcal{NP}\)-hard in general, but solvable in either \textit{FPT} time or polynomial time for some special cases.New complexity results for shop scheduling problems with agreement graphshttps://zbmath.org/1517.900592023-09-22T14:21:46.120933Z"Tellache, Nour ElHouda"https://zbmath.org/authors/?q=ai:tellache.nour-el-houdaSummary: We investigate the problem of scheduling jobs on open shop and flow shop systems of two machines, subject to the constraints that only some jobs can be scheduled simultaneously on different machines. These constraints are given by a simple undirected graph \(G\), called the agreement graph. The objective is to minimize the makespan. We first show that the open shop problem with two distinct values of release times is NP-hard even for operation sizes in \(\{1,2\}\) and we present a restricted case that can be solved in polynomial time. Then, we consider the problem with null release times and we show that when restricted to arbitrary trees, the problem is NP-hard. We also present a linear algorithm when restricted to caterpillars and we show that this algorithm can be used to solve the case of cycles in polynomial time. For the flow shop problem, we show that the problem is NP-hard for trees and that this result holds even if the preemption is allowed.Lower bounds for non-convex stochastic optimizationhttps://zbmath.org/1517.900872023-09-22T14:21:46.120933Z"Arjevani, Yossi"https://zbmath.org/authors/?q=ai:arjevani.yossi"Carmon, Yair"https://zbmath.org/authors/?q=ai:carmon.yair"Duchi, John C."https://zbmath.org/authors/?q=ai:duchi.john-c"Foster, Dylan J."https://zbmath.org/authors/?q=ai:foster.dylan-j"Srebro, Nathan"https://zbmath.org/authors/?q=ai:srebro.nathan"Woodworth, Blake"https://zbmath.org/authors/?q=ai:woodworth.blakeSummary: We lower bound the complexity of finding \(\epsilon \)-stationary points (with gradient norm at most \(\epsilon )\) using stochastic first-order methods. In a well-studied model where algorithms access smooth, potentially non-convex functions through queries to an unbiased stochastic gradient oracle with bounded variance, we prove that (in the worst case) any algorithm requires at least \(\epsilon^{-4}\) queries to find an \(\epsilon \)-stationary point. The lower bound is tight, and establishes that stochastic gradient descent is minimax optimal in this model. In a more restrictive model where the noisy gradient estimates satisfy a mean-squared smoothness property, we prove a lower bound of \(\epsilon^{-3}\) queries, establishing the optimality of recently proposed variance reduction techniques.Analysis of the Frank-Wolfe method for convex composite optimization involving a logarithmically-homogeneous barrierhttps://zbmath.org/1517.901082023-09-22T14:21:46.120933Z"Zhao, Renbo"https://zbmath.org/authors/?q=ai:zhao.renbo"Freund, Robert M."https://zbmath.org/authors/?q=ai:freund.robert-mSummary: We present and analyze a new generalized Frank-Wolfe method for the composite optimization problem \((P): {\min }_{x\in{\mathbb{R}}^n} \; f(\mathsf{A} x) + h(x)\), where \(f\) is a \(\theta \)-logarithmically-homogeneous self-concordant barrier, \( \mathsf{A}\) is a linear operator and the function \(h\) has a bounded domain but is possibly non-smooth. We show that our generalized Frank-Wolfe method requires \(O((\delta_0 + \theta + R_h)\ln (\delta_0) + (\theta + R_h)^2/\varepsilon )\) iterations to produce an \(\varepsilon \)-approximate solution, where \(\delta_0\) denotes the initial optimality gap and \(R_h\) is the variation of \(h\) on its domain. This result establishes certain intrinsic connections between \(\theta \)-logarithmically homogeneous barriers and the Frank-Wolfe method. When specialized to the \(D\)-optimal design problem, we essentially recover the complexity obtained by \textit{L. G. Khachiyan} [Math. Oper. Res. 21, No. 2, 307--320 (1996; Zbl 0856.68066)] using the Frank-Wolfe method with exact line-search. We also study the (Fenchel) dual problem of \((P)\), and we show that our new method is equivalent to an adaptive-step-size mirror descent method applied to the dual problem. This enables us to provide iteration complexity bounds for the mirror descent method despite the fact that the dual objective function is non-Lipschitz and has unbounded domain. In addition, we present computational experiments that point to the potential usefulness of our generalized Frank-Wolfe method on Poisson image de-blurring problems with TV regularization, and on simulated PET problem instances.Correction to: ``Convexifactors, generalized convexity, and optimality conditions''https://zbmath.org/1517.901582023-09-22T14:21:46.120933Z"Dutta, J."https://zbmath.org/authors/?q=ai:dutta.joydeep"Chandra, S."https://zbmath.org/authors/?q=ai:chandra.sharat|chandra.soumen|chandra.suryansh|chandra.sumir|chandra.sushil|chandra.saroj-kumar|chandra.subha|chandra.sarvesh|chandra.sanjeev|chandra.subhash-ajay|chandra.saurabh|chandra.shiva|chandra.sudip-ratan|chandra.shekhar-s|chandra.samarth|chandra.subodh|chandra.sujan|chandra.suresh|chandra.swarniv|chandra.sarthak|chandra.satish|chandra.sanjay|chandra.susheel|chandra.shalini"Rimpi"https://zbmath.org/authors/?q=ai:rimpi."Lalitha, C. S."https://zbmath.org/authors/?q=ai:lalitha.c-sFrom the text: We correct an error in the proof of Theorem 3.5 in [\textit{J. Dutta} and \textit{S. Chandra}, ibid. 113, No. 1, 41--64 (2002; Zbl 1172.90500)].Quadratic multiparty randomized encodings beyond honest majority and their applicationshttps://zbmath.org/1517.940542023-09-22T14:21:46.120933Z"Applebaum, Benny"https://zbmath.org/authors/?q=ai:applebaum.benny"Ishai, Yuval"https://zbmath.org/authors/?q=ai:ishai.yuval"Karni, Or"https://zbmath.org/authors/?q=ai:karni.or"Patra, Arpita"https://zbmath.org/authors/?q=ai:patra.arpitaSummary: Multiparty randomized encodings [\textit{B. Applebaum} et al., SIAM J. Comput. 50, No. 1, 68--97 (2021; Zbl 1509.68076)] reduce the task of securely computing a complicated multiparty functionality \(f\) to the task of securely computing a simpler functionality \(g\). The reduction is non-interactive and preserves information-theoretic security against a passive (semi-honest) adversary, also referred to as privacy. The special case of a degree-2 encoding \(g\) (2MPRE) has recently found several applications to secure multiparty computation (MPC) with either information-theoretic security or making black-box access to cryptographic primitives. Unfortunately, as all known constructions are based on information-theoretic MPC protocols in the plain model, they can only be private with an honest majority.
In this paper, we break the honest-majority barrier and present the first construction of general 2MPRE that remains secure in the presence of a dishonest majority. Our construction encodes every \(n\)-party functionality \(f\) by a 2MPRE that tolerates at most \(t=\lfloor 2n/3\rfloor\) passive corruptions.
We derive several applications including: (1) The first non-interactive client-server MPC protocol with perfect privacy against any coalition of a minority of the servers and up to \(t\) of the \(n\) clients; (2) Completeness of 3-party functionalities under non-interactive \(t\)-private reductions; and (3) A single-round \(t\)-private reduction from general-MPC to an ideal oblivious transfer (OT). These positive results partially resolve open questions that were posed in several previous works. We also show that \(t\)-private 2MPREs are necessary for solving (2) and (3), thus establishing new equivalence theorems between these three notions.
Finally, we present a new approach for constructing fully-private 2MPREs based on multi-round protocols in the OT-hybrid model that achieve perfect privacy against active attacks. Moreover, by slightly restricting the power of the active adversary, we derive an equivalence between these notions. This forms a surprising, and quite unique, connection between a non-interactive passively-private primitive to an interactive actively-private primitive.
For the entire collection see [Zbl 1514.94004].On prover-efficient public-coin emulation of interactive proofshttps://zbmath.org/1517.940562023-09-22T14:21:46.120933Z"Arnon, Gal"https://zbmath.org/authors/?q=ai:arnon.gal"Rothblum, Guy N."https://zbmath.org/authors/?q=ai:rothblum.guy-nSummary: A central question in the study of interactive proofs is the relationship between private-coin proofs, where the verifier is allowed to hide its randomness from the prover, and public-coin proofs, where the verifier's random coins are sent to the prover. The seminal work of \textit{S. Goldwasser} and \textit{M. Sipser} [in: Proceedings of the 18th annual ACM symposium on theory of computing, STOC 1986, Berkeley, CA, USA, May 28--30, 1986. New York, NY: Association for Computing Machinery (ACM). 59--68 (1986; \url{doi:10.1145/12130.12137})] showed how to transform private-coin proofs into public-coin ones. However, their transformation incurs a super-polynomial blowup in the running time of the honest prover.\par In this work, we study transformations from private-coin proofs to public-coin proofs that preserve (up to polynomial factors) the running time of the prover. We re-consider this question in light of the emergence of doubly-efficient interactive proofs, where the honest prover is required to run in polynomial time and the verifier should run in near-linear time. Can every private-coin doubly-efficient interactive proof be transformed into a public-coin doubly-efficient proof? Adapting a result of \textit{S. Vadhan} [in: Proceedings of the thirty-second annual ACM symposium on theory of computing, STOC 2000. Portland, Oregon, USA, May 21--23, 2000. New York, NY: ACM Press. 200--207 (2000; Zbl 1296.68061)], we show that, assuming one-way functions exist, there is no general-purpose black-box private-coin to public-coin transformation for doubly-efficient interactive proofs.\par Our main result is a loose converse: if (auxiliary-input infinitely-often) one-way functions do not exist, then there exists a general-purpose efficiency-preserving transformation. To prove this result, we show a general condition that suffices for transforming a doubly-efficient private coin protocol: every such protocol induces an efficiently computable function, such that if this function is efficiently invertible (in the sense of one-way functions), then the proof can be efficiently transformed into a public-coin proof system with a polynomial-time honest prover.\par This result motivates a study of other general conditions that allow for efficiency-preserving private to public coin transformations. We identify an additional (incomparable) condition to that used in our main result. This condition allows for transforming any private coin interactive proof where (roughly) it is possible to efficiently approximate the number of verifier coins consistent with a partial transcript. This allows for transforming any constant-round interactive proof that has this property (even if it is not doubly-efficient). We demonstrate the applicability of this final result by using it to transform a private-coin protocol of \textit{G. N. Rothblum} et al. [in: Proceedings of the 45th annual ACM symposium on theory of computing, STOC '13. Palo Alto, CA, USA, June 1--4, 2013. New York, NY: Association for Computing Machinery (ACM). 793--802 (2013; Zbl 1293.68250)], obtaining a doubly-efficient public-coin protocol for verifying that a given graph is close to bipartite in a setting for which such a protocol was not previously known.
For the entire collection see [Zbl 1465.94005].Improvement of algebraic attacks for solving superdetermined MinRank instanceshttps://zbmath.org/1517.940592023-09-22T14:21:46.120933Z"Bardet, Magali"https://zbmath.org/authors/?q=ai:bardet.magali"Bertin, Manon"https://zbmath.org/authors/?q=ai:bertin.manonSummary: The MinRank (MR) problem is a computational problem that arises in many cryptographic applications. In [\textit{J. Verbel} et al., Lect. Notes Comput. Sci. 11505, 167--186 (2019; Zbl 1509.94136)], the authors introduced a new way to solve superdetermined instances of the MinRank problem, starting from the bilinear Kipnis-Shamir (KS) modeling. They use linear algebra on specific Macaulay matrices, considering only multiples of the initial equations by one block of variables, the so called ``kernel'' variables. Later, \textit{M. Bardet} et al. [ibid. 12491, 507--536 (2020; Zbl 1511.94051)] introduced a new Support Minors modeling (SM), that consider the Plücker coordinates associated to the kernel variables, i.e. the maximal minors of the Kernel matrix in the KS modeling.
In this paper, we give a complete algebraic explanation of the link between the (KS) and (SM) modelings (for any instance). We then show that superdetermined MinRank instances can be seen as easy instances of the SM modeling. In particular, we show that performing computation at the smallest possible degree (the ``first degree fall'') and the smallest possible number of variables is not always the best strategy. We give complexity estimates of the attack for generic random instances.
We apply those results to the DAGS cryptosystem, that was submitted to the first round of the NIST standardization process. We show that the algebraic attack from \textit{É. Barelli} and \textit{A. Couvreur} [ibid. 11272, 93--118 (2018; Zbl 1446.94098)], improved in \textit{M. Bardet} et al. [ibid 11666, 86--101 (2019; \url{doi.org/10.1007/978-3-030-25922-8_5})], is a particular superdetermined MinRank instance. Here, the instances are not generic, but we show that it is possible to analyse the particular instances from DAGS and provide a way to select the optimal parameters (number of shortened positions) to solve a particular instance.
For the entire collection see [Zbl 1514.94001].Adaptive oblivious transfer with access control from lattice assumptionshttps://zbmath.org/1517.941242023-09-22T14:21:46.120933Z"Libert, Benoît"https://zbmath.org/authors/?q=ai:libert.benoit"Ling, San"https://zbmath.org/authors/?q=ai:ling.san"Mouhartem, Fabrice"https://zbmath.org/authors/?q=ai:mouhartem.fabrice"Nguyen, Khoa"https://zbmath.org/authors/?q=ai:nguyen.khoa"Wang, Huaxiong"https://zbmath.org/authors/?q=ai:wang.huaxiongSummary: Adaptive oblivious transfer (OT) is a protocol where a sender initially commits to a database \(\{ M_i \}_{i = 1}^N\). Then, a receiver can query the sender up to \(k\) times with private indexes \(\rho_1, \ldots, \rho_k\) so as to obtain \(M_{\rho_1}, \ldots, M_{\rho_k}\) and nothing else. Moreover, for each \(i \in [k]\), the receiver's choice \(\rho_i\) may depend on previously obtained messages \(\{ M_{\rho_j} \}_{j < i}\). Oblivious transfer with access control (OT-AC) is a flavor of adaptive OT where database records are protected by distinct access control policies that specify which credentials a receiver should obtain in order to access each \(M_i\). So far, all known OT-AC protocols only support access policies made of conjunctions or rely on ad hoc assumptions in pairing-friendly groups (or both). In this paper, we provide an OT-AC protocol where access policies may consist of any branching program of polynomial length, which is sufficient to realize any access policy in \(\mathsf{NC1} \). The security of our protocol is proved under the Learning-with-Errors \(( \mathsf{LWE} )\) and Short-Integer-Solution \(( \mathsf{SIS} )\) assumptions. As a result of independent interest, we provide protocols for proving the correct evaluation of a committed branching program on a committed input.