arxiv: 2604.24151 · v1 · submitted 2026-04-27 · 💻 cs.FL · cs.CC

Recognition: unknown

Regular Grammars as Effective Representations of Recognizable Sets of Series-Parallel Graphs

Marius Bozga , Radu Iosif , Florian Zuleger

Authors on Pith no claims yet

Pith reviewed 2026-05-07 17:28 UTC · model grok-4.3

classification 💻 cs.FL cs.CC

keywords series-parallel graphsregular grammarsrecognizable setsfinite algebrasCMSO definabilitylanguage inclusionExpTime complexity

0 comments

The pith

Regular grammars yield singly-exponential finite algebras for recognizable sets of series-parallel graphs.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper shows that recognizable sets of series-parallel graphs can be given concise syntactic representations through regular grammars. It supplies a construction that turns any such grammar into a finite recognizing algebra whose size is only singly exponential in the grammar size. This tightens the earlier double-exponential bound and yields ExpTime-completeness for intersection and language inclusion. A sympathetic reader would care because the result turns an abstract logical characterization into something that can be manipulated by algorithms with controlled cost. The work treats series-parallel graphs as the central case for bounded-tree-width graphs where recognizability coincides with CMSO definability.

Core claim

Building on regular grammars for series-parallel graphs, recognizable sets admit concise and effective syntactic representations. The central construction produces a finite recognizer algebra of size singly exponential in the size of the input grammar. This improves the prior double-exponential bound and implies that intersection and language inclusion problems for grammars are ExpTime-complete.

What carries the argument

The translation from a regular grammar for series-parallel graphs into a finite algebra that recognizes exactly the same set, with size controlled by a single exponential blow-up.

If this is right

Intersection of languages given by two regular grammars is ExpTime-complete.
Language inclusion between two regular grammars is ExpTime-complete.
Recognizable sets of series-parallel graphs possess syntactic representations that support effective decision procedures.
Basic operations on such sets become feasible within exponential time once a grammar is provided.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

The same singly-exponential translation might be lifted to other bounded-tree-width graph families that admit regular grammar presentations.
Verification tools for graph properties could adopt these grammars to obtain better practical performance than earlier double-exponential constructions allowed.
Lower-bound matching constructions or minimization procedures for the resulting algebras remain open for further investigation.

Load-bearing premise

The input is already a correct regular grammar for the desired set of series-parallel graphs and the standard equivalence between recognizability and CMSO definability preserves the language exactly under the translation.

What would settle it

Exhibit a regular grammar for which every recognizing algebra requires size larger than singly exponential in the grammar size, or two grammars whose inclusion problem lies outside ExpTime.

Figures

Figures reproduced from arXiv: 2604.24151 by Florian Zuleger, Marius Bozga, Radu Iosif.

**Figure 1.** Figure 1: Series (a) and parallel (b) composition. of bounded embeddable tree-width, an over-approximation of the tree-width that considers only spanning-tree decompositions, have been proposed in [7]. In this work, the bound on the embeddable tree-width of graphs is not fixed. However, the recognizability of the language of a regular grammar is established via translation to CMSO, leaving the cardinality of the re… view at source ↗

**Figure 2.** Figure 2: The structure of rules from Γ k The edges s α−→ s ′ stand for the rules s → pα◦s ′ , respectively. We note that Γ k has O(2k ) nonterminals, because there are n def = 2k+1 −1 words u, v ∈ S 0≤ℓ≤k {a, b} ℓ . Since there are O(n) meta-rules of the form s →∗ u or s →∗ u ◦ s ′ , that generate at most k rules each, the grammar Γ k has O(k · 2 k ) = O(n · log2 n) rules. Second, suppose, for a contradiction, that… view at source ↗

**Figure 3.** Figure 3: The definition (a) and behavior (b) of the π mapping. π(x) def = y if fn(x) = fm(y), for some y ∈ vars(m) ⊥ otherwise The definition of π is illustrated in view at source ↗

**Figure 4.** Figure 4: Linear products of 2-threshold variables Then, we get from (6) that: sup(nf(t)) = nf(σ (−1)(sup(nf(t ♯ )))) = nf(σ (−1)( X m♯∈nf(t ♯) {m♯ | deg(m♯ ) = max deg(nf(t ♯ ))})) = nf   X m♯∈nf(t ♯) {σ (−1)(m♯ ) | deg(m♯ ) = max deg(nf(t ♯ ))}   Note that σ (−1) is a substitution ensuring that σ (−1)(m♯ ) is a reduced monomial on S θ variables of same degree as m♯ , for every reduced monomial m♯ in nf(t ♯ ). … view at source ↗

**Figure 5.** Figure 5: Linear products of threshold variables The property (7) is then sufficient to establish the conclusion of the lemma, as follows. Consider len(t) > ||Sβ ⊎ Sπ ||1. Then, t ♯ ∈ Prods(Sums(S ♯ )) and len(t ♯ ) = len(t) > ||S♯ ||1. Using Lemma 5 (iii) there exists t ′♯ ∈ Prods(Sums(S ♯ )) such that t ′♯ ≺ t ♯ and forall u ∈ [t ′♯ , t♯ ] it holds sup(nf(u)) = sup(nf(t ♯ )). Then, we construct t ′ def = σ (−1)(t … view at source ↗

**Figure 6.** Figure 6: Construction of t ′ from t1 and t ′ 1 – let J1 ⊆ [1, len(t1)] such that t ′ 1 = Q j∈J1 (1+ℓj ) and let J2 def = [1, len(t1)]\J1. We can check that ||J2|| ≥ π(s0), that is, because ||J2|| = len(t1) − len(t ′ 1 ) > ||Sβ ⊎ Sπ \ {s0}||1 + (π(s0)−1)−||Sβ ⊎ Sπ \ {s0}||1 = (π(s0)−1). That is, at least π0(s0) more factors are added in t1 with respect to t ′ 1 . Consider J ′ 2 ⊎J ′′ 2 a partition of J2 such that ||… view at source ↗

**Figure 7.** Figure 7: Linear products with enforced divisibilities The property (9) is then sufficient to establish the conclusion of the lemma, as follows. Let t satisfying the lemma hypothesis. Then, σ(t) ∈ Prods(s ♯ 0 -Sums(S β ⊎ S♯ )) and len(σ(t)) = len(t) > ||Sβ ⊎ S♯ ||1. Therefore, using Lemma 7 there exists t ′′ ≺ σ(t) such that nf(t ′′) = nf(σ(t)). We construct t ′ def = σ (−1)(t ′′) and check that t ′ ≺ t (as t ′′ ≺ σ… view at source ↗

read the original abstract

Series-parallel (SP) graphs are binary edge-labeled graphs with a designated source and target vertex, built using serial and parallel composition. A set of graphs is recognizable if membership depends only on its image under a homomorphism into a finite algebra. For SP-graphs, and more generally, for graphs of bounded tree-width, recognizability coincides with definability in Counting Monadic Second-Order (CMSO) logic. Despite this strong logical characterization, the conciseness and algorithmic effectiveness of syntactic representations of recognizable sets of SP (and bounded-tree-width) graphs remain poorly understood. Building on previously introduced regular grammars for SP-graphs, we show that recognizable sets admit concise and effective syntactic representations. The main contribution is an improved construction of finite recognizer algebras whose size is singly-exponential in the size of a regular grammar, improving upon the previously known double-exponential bound. As a consequence, the problems of intersection and language inclusion for sets represented by regular grammars are shown to be ExpTime-complete, thus improving on a previously known 2ExpTime upper bound.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Desk Editor's Note private letter to a colleague

The paper tightens the bound on recognizer algebra size for SP-graph languages from double-exponential to singly-exponential and proves matching ExpTime-completeness for intersection and inclusion.

read the letter

The main takeaway is a singly-exponential construction that turns a regular grammar for series-parallel graphs into a finite recognizer algebra while keeping the exact language. This drops intersection and inclusion from a 2ExpTime upper bound to ExpTime-complete, with a matching lower bound that was not known before. The construction works by inductive operations on serial and parallel composition that avoid the state explosion in earlier methods. It builds directly on the existing regular grammar framework without needing new logical machinery beyond the standard recognizability definition. The size analysis looks clean on the surface, with no obvious hidden exponential factors mentioned in the abstract or stress-test note. The paper stays focused on SP-graphs and treats the CMSO equivalence as background rather than reproving it. A minor soft spot is that readers will need the prior papers on regular grammars to follow the details, and any practical implementation would still face the exponential constants even if the asymptotic bound improved. The results hold up internally with no circularity or fitting issues. This is for people working on automata for graphs, verification of bounded tree-width systems, or complexity of operations on recognizable languages. A reader who already knows the regular grammar setup will get the most out of the tighter bounds and the completeness proof. It deserves a serious referee because the improvement is concrete, the lower bound is new, and the claims are stated precisely enough to check. I would send it out for peer review.

Referee Report

0 major / 1 minor

Summary. The paper shows that recognizable sets of series-parallel graphs admit concise syntactic representations via regular grammars. Building on prior definitions of regular grammars for SP-graphs, the main technical contribution is an inductive construction of finite recognizer algebras whose size is singly exponential in the size of the input grammar (improving the prior double-exponential bound). As a consequence, the intersection and language-inclusion problems for sets given by regular grammars are shown to be ExpTime-complete.

Significance. If the singly-exponential construction holds, the result supplies effective, concise representations for recognizable sets of bounded-tree-width graphs and tightens the complexity of decision problems from 2ExpTime to ExpTime. This strengthens the algorithmic link between recognizability (equivalently CMSO definability) and syntactic representations, with potential utility for verification and automata-based algorithms on series-parallel graphs.

minor comments (1)

The abstract and introduction would benefit from a one-sentence outline of the key operations (serial/parallel composition handling) that avoid the previous state explosion, to help readers quickly locate the improvement.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for the positive assessment of the manuscript, the accurate summary of our contributions, and the recommendation to accept. We appreciate the recognition that the singly-exponential algebra construction tightens the complexity of intersection and inclusion from 2ExpTime to ExpTime.

Circularity Check

0 steps flagged

No significant circularity; construction is independent of inputs

full rationale

The paper's central derivation is an explicit inductive construction that translates a regular grammar over serial/parallel compositions into a finite recognizer algebra while preserving the recognized language and achieving singly-exponential size. This is presented as a direct syntactic translation using operations on the grammar productions; the size bound follows from counting the states generated by the construction rather than from any fitted parameter or self-referential equation. The reference to 'previously introduced regular grammars' supplies only the input syntax and is not invoked to justify the new size bound or language preservation. CMSO equivalence is cited solely as background context and plays no role in the algebra-size argument. No step reduces by construction to its own inputs or to a self-citation chain.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The work rests on the known equivalence of recognizability and CMSO definability for bounded-tree-width graphs and on the prior definition of regular grammars for SP-graphs; no new free parameters or invented entities are introduced.

axioms (1)

domain assumption For SP-graphs and more generally graphs of bounded tree-width, recognizability coincides with definability in Counting Monadic Second-Order logic.
Stated explicitly in the abstract as background fact used to motivate the syntactic representation question.

pith-pipeline@v0.9.0 · 5491 in / 1291 out tokens · 59164 ms · 2026-05-07T17:28:21.275121+00:00 · methodology

discussion (0)

Reference graph

Works this paper leans on

41 extracted references · 12 canonical work pages

[1]

Alur, R., Madhusudan, P.: Adding nesting structure to words. J. ACM56(3) (May 2009).https://doi.org/10.1145/1516512.1516518,https://doi.org/10.1145/ 1516512.1516518

work page doi:10.1145/1516512.1516518 2009
[2]

Alur, R., Stanford, C., Watson, C.: A robust theory of series parallel graphs. Proc. ACM Program. Lang.7(POPL) (Jan 2023).https://doi.org/10.1145/3571230, https://doi.org/10.1145/3571230 16

work page doi:10.1145/3571230 2023
[3]

Boiret, A., Hugot, V., Niehren, J., Treinen, R.: Automata for unordered trees. Inf. Comput.253, 304–335 (2017)

2017
[4]

In: Flum, J., Gr¨ adel, E., Wilke, T

Bojanczyk, M., Walukiewicz, I.: Forest algebras. In: Flum, J., Gr¨ adel, E., Wilke, T. (eds.) Logic and Automata: History and Perspectives [in Honor of Wolfgang Thomas]. Texts in Logic and Games, vol. 2, pp. 107–132. Amsterdam University Press (2008)

2008
[5]

CoRRabs/2408.01226(2024).https://doi.org/10.48550/ARXIV.2408.01226, https://doi.org/10.48550/arXiv.2408.01226

Bozga, M., Iosif, R., Zuleger, F.: Regular grammars for graph sets of tree-width≤. CoRRabs/2408.01226(2024).https://doi.org/10.48550/ARXIV.2408.01226, https://doi.org/10.48550/arXiv.2408.01226

work page doi:10.48550/arxiv.2408.01226 2024
[6]

Bozga, M., Iosif, R., Zuleger, F.: Regular grammars for sets of graphs of tree-width
[7]

In: 2025 40th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS). pp. 704–717 (2025).https://doi.org/10.1109/LICS65433.2025.00059

work page doi:10.1109/lics65433.2025.00059 2025
[8]

In: Bjørner, N.S., Heule, M., Voronkov, A

Chimes, M., Iosif, R., Zuleger, F.: Tree-verifiable graph grammars. In: Bjørner, N.S., Heule, M., Voronkov, A. (eds.) LPAR 2024: Proceedings of 25th Confer- ence on Logic for Programming, Artificial Intelligence and Reasoning, Port Louis, Mauritius, May 26-31, 2024. EPiC Series in Computing, vol. 100, pp. 165–180. EasyChair (2024)

2024
[9]

HAL (2008), https://inria.hal.science/hal-03367725

Comon, H., Dauchet, M., Gilleron, R., Jacquemard, F., Lugiez, D., L¨ oding, C., Tison, S., Tommasi, M.: Tree Automata Techniques and Applications. HAL (2008), https://inria.hal.science/hal-03367725

2008
[10]

Courcelle, B.: The monadic second-order logic of graphs. i. recognizable sets of finite graphs. Information and Computation85(1), 12–75 (1990). https://doi.org/https://doi.org/10.1016/0890-5401(90)90043-H,https:// www.sciencedirect.com/science/article/pii/089054019090043H

work page doi:10.1016/0890-5401(90)90043-h 1990
[11]

Courcelle, B.: The monadic second-order logic of graphs v: on closing the gap between definability and recognizability. Theoretical Computer Sci- ence80(2), 153–202 (1991).https://doi.org/https://doi.org/10.1016/ 0304-3975(91)90387-H,https://www.sciencedirect.com/science/article/ pii/030439759190387H

work page arXiv 1991
[12]

Encyclopedia of Mathematics and its Applications, Cambridge University Press (2012).https://doi.org/10.1017/ CBO9780511977619

Courcelle, B., Engelfriet, J.: Graph Structure and Monadic Second-Order Logic: A Language-Theoretic Approach. Encyclopedia of Mathematics and its Applications, Cambridge University Press (2012).https://doi.org/10.1017/ CBO9780511977619

2012
[13]

In: Bojanczyk, M., Merelli, E., Woodruff, D.P

Doumane, A.: Regular expressions for tree-width 2 graphs. In: Bojanczyk, M., Merelli, E., Woodruff, D.P. (eds.) 49th International Colloquium on Automata, Languages, and Programming, ICALP 2022, July 4-8, 2022, Paris, France. LIPIcs, vol. 229, pp. 121:1–121:20. Schloss Dagstuhl - Leibniz-Zentrum f¨ ur Informatik (2022).https://doi.org/10.4230/LIPICS.ICALP...

work page doi:10.4230/lipics.icalp.2022.121 2022
[14]

In: Proc

Elgaard, J., Klarlund, N., Møller, A.: MONA 1.x: new techniques for WS1S and WS2S. In: Proc. 10th International Conference on Computer-Aided Verification, CAV ’98. LNCS, vol. 1427, pp. 516–520. Springer-Verlag (June/July 1998)

1998
[15]

Engelfriet, J.: Context-Free Graph Grammars, pp. 125–213. Springer Berlin Heidel- berg, Berlin, Heidelberg (1997).https://doi.org/10.1007/978-3-642-59126-6_ 3,https://doi.org/10.1007/978-3-642-59126-6_3

work page doi:10.1007/978-3-642-59126-6_ 1997
[16]

In: Larsen, K.G., Saha, B

Kurkofka, J., Planken, T.: A tutte-type canonical decomposition of 3- and 4- connected graphs. In: Larsen, K.G., Saha, B. (eds.) Proceedings of the 2026 An- nual ACM-SIAM Symposium on Discrete Algorithms, SODA 2026, Vancouver, BC, Canada, January 11-14, 2026. pp. 2942–3021. SIAM (2026).https://doi.org/10. 1137/1.9781611978971.110,https://doi.org/10.1137/1...

work page doi:10.1137/1.9781611978971.110 2026
[17]

In: Flanagan, C., K¨ onig, B

Leng´ al, O., ˇSim´ aˇ cek, J., Vojnar, T.: Vata: A library for efficient manipulation of non-deterministic tree automata. In: Flanagan, C., K¨ onig, B. (eds.) Tools and Algorithms for the Construction and Analysis of Systems. pp. 79–94. Springer Berlin Heidelberg, Berlin, Heidelberg (2012)

2012
[18]

Pin, J.E.: Mathematical foundations of automata theory.https://www.irif.fr/ ~jep/PDF/MPRI/MPRI.pdf(2025)

2025
[19]

R´ emila, E.: An Introduction to Automata on Graphs, pp. 345–352. Springer Netherlands, Dordrecht (1999).https://doi.org/10.1007/978-94-015-9153-9_ 15,https://doi.org/10.1007/978-94-015-9153-9_15

work page doi:10.1007/978-94-015-9153-9_ 1999
[20]

Journal of Com- puter and System Sciences1(4), 317–322 (1967).https://doi.org/https: //doi.org/10.1016/S0022-0000(67)80022-9,https://www.sciencedirect

Thatcher, J.: Characterizing derivation trees of context-free grammars through a generalization of finite automata theory. Journal of Com- puter and System Sciences1(4), 317–322 (1967).https://doi.org/https: //doi.org/10.1016/S0022-0000(67)80022-9,https://www.sciencedirect. com/science/article/pii/S0022000067800229

work page doi:10.1016/s0022-0000(67)80022-9 1967
[21]

In: Pehrson, B., Simon, I

Thomas, W.: Finite-state recognizability and logic: from words to graphs. In: Pehrson, B., Simon, I. (eds.) Technology and Foundations - Information Processing ’94, Volume 1, Proceedings of the IFIP 13th World Computer Congress, Hamburg, Germany, 28 August - 2 September, 1994. IFIP Transactions, vol. A-51, pp. 499–

1994
[22]

North-Holland (1994)

1994
[23]

Cambridge university press (2001)

Tutte, W.: Graph theory. Cambridge university press (2001)

2001
[24]

Whitney, H.: On the abstract properties of linear dependence. American Journal of Mathematics57(3), 509–533 (1935),http://www.jstor.org/stable/2371182 A Proofs Proposition 3 (Propositions 2.9 and 2.10 in [17]).LetA= (A,{f A}f∈F ) be an algebra andL,K ⊆Abe sets recognized by algebrasBandC, with accepting setsF⊆BandG⊆C, respectively. Then,A\Lis recognized b...

work page arXiv 1935
[25]

⇐” This direction uses a symmetric argument. Lemma 1.his a homomorphism betweenSPandA. Proof (Proof of Lemma 1).We prove several points, for alla∈ΣandG 1, G2 ∈ SP: h(aSP ) =a A: “⊆

there existss ′ ∈ Sand derivationss a∗⇒ Γ t1 ◦s ′ ands ′ a∗⇒ Γ t2 ◦q, where ti is a ground term such thatt SP i =G i, fori= 1,2. Byp⇝ ∗ mwe mean the existence of a derivationp⇒ ∗ Γ s1 ∥. . .∥s n, using only rules fromR A ∪ RB, such thatm=s 1 ·. . .·s n. The⇝and⇝ ∗ relations enjoy the following property: Lemma 17.For each nonterminalp∈ Pand monomialm∈T p, ...
[26]

Since nf p(m′ i)∈h p(Gi) andm= nf p(m′ 1 ·m ′

Note that, sincev(s, i) SP is a S-graph, it must be either a subgraph ofG 1 or ofG 2. Since nf p(m′ i)∈h p(Gi) andm= nf p(m′ 1 ·m ′
[27]

⊆” This direction is trivial, by the definition ofF. “⊇

= nf p(nf p(m′ 1)·nf p(m′ 2)), by Lemma 13, we obtainm∈(h(G 1)∥ A h(G2))p. ”⊇” Letm∈(h(G 1)∥ A h(G2))p for somep∈ P. Then, there existm i ∈ hp(Gi), fori= 1,2, such thatm= nf p(m1 ·m 2). Then, there exist viewsm ′ i ofG i such thatm i = nf p(m′ i). By Lemma 13, we obtainm= nf p(m′ 1 ·m ′ 2). Sincem ′ 1 ·m ′ 2 is a view ofG 1 ∥SP G2, we obtainm∈h p(G1 ∥SP G...
[28]

ifa=⟨t p⟩p∈P ∈F∩A P then there exists an axiomp∈ P ∩Xand a nonempty monomialm∈t p such thatp⇝m
[29]

Proof.(1) Leta=⟨t p⟩p∈P ∈A P ∩FandGbe a P-graph such thath(G) =a

ifa∈F∩A S then(s,⊥)∈a, for an axioms∈ S ∩ X. Proof.(1) Leta=⟨t p⟩p∈P ∈A P ∩FandGbe a P-graph such thath(G) =a. SinceF=h(L(Γ)), by definition, we obtainG∈ L(Γ). Since, moreover,Gis a P-graph, there exists an axiomp∈ P ∩ Xsuch thatp⇒ ∗ Γ vis a complete derivation andv SP =G. This derivation can be w.l.o.g. considered to be of the form: p⇒ ∗ Γ ∥ s∈S s∥ks ⇒∗ ...
[30]

= (1 +s 1)p1 ·...·(1 +s n1)pn1 σ(−1)(m♯
[31]

Then, any reduced monomialmin nf(σ (−1)(m♯ 1)) is obtained from some products r1 1 ·...·s rn1 n1 oc- curring inσ (−1)(m♯ 1)

= (1 +s 1)q1 ·...·(1 +s n1)qn1 · (1 +s n1+1)qn1 +1 ·...·(1 +s n2)qn2 for some pairwise distinct variabless 1, ...,s n2, for positivep 1, ...,p n1,q 1, ..., qn2 such thatq i ≥p i for alli∈[1, n 1], and somen 1 ≤n 2. Then, any reduced monomialmin nf(σ (−1)(m♯ 1)) is obtained from some products r1 1 ·...·s rn1 n1 oc- curring inσ (−1)(m♯ 1). Or, exactly the s...
[32]

i.e., by making the same choices ofs 1, ...,s n1 variables inσ (−1)(m♯
[33]

part, and choosing 1’s from the other additional factors inσ (−1)(m♯ 2). Using the fact above, we obtain immediately that nf(σ(−1)(nf(t ♯))) = nf(σ (−1)(sup(nf(t ♯))) because every monomial derived from a non-maximal monomial ofσ (−1)(nf(t ♯)) (that is,t 1 in Fig. 5) can be also derived from some maximal monomial in σ(−1)(sup(nf(t ♯))) (that is,t 2 in Fig...
[34]

Obviously, such a partitioning exists because| |J2| | ≥π0(s0)

ConsiderJ ′ 2 ⊎J ′′ 2 a partition ofJ 2 such that| |J ′′ 2 | |=π 0(s0). Obviously, such a partitioning exists because| |J2| | ≥π0(s0). –definet ′ def=Q j∈J1(s0 +ℓ j)· Q j∈J ′ 2 (s0 +ℓ j). It is now an easy check thatt ′ satisfies the requirements as stated in the lemma. First,t ′ ≺t, as precisely π(s0) factors are removed int ′ with respect tot. Second, l...
[35]

= nf(t 1). Third, we check nf(t ′) = nf(t) because nf(t ′) = X m1∈nf(t ′′ 1 ) s(k−π(s 0)−deg(m1)) modπ(s 0) 0 ·m 1 = X m1∈nf(t 1) s(k−deg(m1)) modπ(s 0) 0 ·m 1 = nf(t) Lemma 8.For each periodic variables 0 ∈ S π and linear productt∈Prods(s 0-Sums(S β ⊎ S π)) of length len(t)>| |S β| |1 +P s∈S π(lcm(π(s), π(s 0))−1), there existst ′ ≺tsuch thatnf(t ′) = nf...
[36]

Moreover, note that| |Sβ ⊎ S ♯| |1 =| |Sβ| |1+P s∈S π(lcm(π(s), π(s 0))− 1)

dividesπ(s ♯) for every vari- ables ♯ ∈ S ♯. Moreover, note that| |Sβ ⊎ S ♯| |1 =| |Sβ| |1+P s∈S π(lcm(π(s), π(s 0))− 1). Furthermore, define the substitutionsσ:S π → S ♯ andσ (−1) :S ♯ → S π by taking respectivelyσ(s) def=s ♯,σ (−1)(s♯) def=s, for everys∈ S π. Then, using the above notations we prove that computations depicted in Fig 7 commute, that is, ...
[37]

Then K(| |Sβ p ⊎ S π+ p | |, b(Sβ p ,S π+ p ))≤2 (Bmax+P 2 max/2)·| |S| |2·(| |S| |+1)

+P 2 max · | |S| | ·(| |S| |+ 1)/2 = (Bmax +P 2 max/2)· | |S| | ·(| |S| |+ 1). Then K(| |Sβ p ⊎ S π+ p | |, b(Sβ p ,S π+ p ))≤2 (Bmax+P 2 max/2)·| |S| |2·(| |S| |+1). We compute: | |Xp| | ≤2max(Bmax,Pmax)·| |S| |2 ·2 (Bmax+P 2 max/2)·| |S| |2·(| |S| |+1) ≤2 (Bmax+P 2 max/2)·| |S| |·(| |S| |+2) because max(Bmax, Pmax)≤B max +P max ≤B max +P 2 max/2, and th...
[38]

, Γn, doesL(Γ 1)∩

Given regular grammarsΓ 1, . . . , Γn, doesL(Γ 1)∩. . .∩ L(Γ n) =∅hold?
[39]

, Γn be an instance of the intersection problem, whereΓ i = (Pi ⊎ Si,R i,X i), for eachi∈[1, n]

Given grammarsΓ 1 andΓ 2 such thatΓ 2 is regular, doesL(Γ 1)⊆ L(Γ 2) hold? Proof (Proof of Theorem 4).We prove theEXPTIMEupper bound for each of the considered problems: (1) LetΓ 1, . . . , Γn be an instance of the intersection problem, whereΓ i = (Pi ⊎ Si,R i,X i), for eachi∈[1, n]. We denoteP def=Pn i=1 | |Pi| |,S def=Pn i=1 | |Si| |,R def= 39 Pn i=1 | ...
[40]

=L(Γ 1)∩(SP\ L(Γ 2)). By Theorem 3 and Lemma 12,Γ ′ 1 can be built in time: | |R1| | · | |A2| |α(Γ1) ·(| |P2| | · | |R2| |)O(1) ·θ(Γ 2)O(S2) | {z } τ ·θ(Γ 1) =| |R1| | ·2α(Γ1)·O(| |P2| |·| |S2| |3·| |R2| |3·θ(Γ2)2) | {z } | |A2| |α(Γ1 ) · (| |P2| | · | |R2| |)O(1) ·θ(Γ 2)O(S2) | {z } τ ·θ(Γ 1) = 2(| |R1| |·α(Γ1)·| |P2| |·| |S2| |·| |R2| |·θ(Γ2))O(1) = 2N ...
[41]

TheEXPTIME-hard lower bound follows from theEXPTIME-hardness of the same problems for sets of terms represented by finite tree automata [8, Theorems 1.7.5 and 1.7.7]

can be decided in timeO(size(Γ ′ 1)2), the inclusion problem has anEXPTIMEupper bound. TheEXPTIME-hard lower bound follows from theEXPTIME-hardness of the same problems for sets of terms represented by finite tree automata [8, Theorems 1.7.5 and 1.7.7]. The encoding of terms as SP-graphs and of bottom-up tree automata as regular grammars are detailed in t...