arxiv: 2605.07968 · v1 · submitted 2026-05-08 · 💻 cs.FL

Recognition: 2 theorem links

· Lean Theorem

Measure Many Quantum Finite Automata on Infinite Words

A Baskar, Abhisek Midya

Authors on Pith no claims yet

Pith reviewed 2026-05-11 02:41 UTC · model grok-4.3

classification 💻 cs.FL

keywords quantum automataBüchi acceptanceinfinite wordsmeasure-many quantum finite automataclosure propertiesdecidabilityquantum computationformal languages

0 comments

The pith

Measure-many quantum Büchi automata accept infinite words precisely when they equal the limit of a measure-many quantum finite automaton language.

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

The paper defines measure-many quantum Büchi automata (MMQBA) that process infinite words through unitary evolution interrupted by repeated projective measurements. It proves that the languages these automata accept are exactly the limits of languages accepted by ordinary measure-many quantum finite automata under the same cutpoint. This characterization supports proofs that MMQBA are closed under union but not under intersection or complement, that emptiness is semi-decidable, and that universality, inclusion, equivalence, and membership are undecidable. A reader would care because the result supplies a concrete way to translate questions about ongoing quantum processes into questions about finite-word quantum automata whose limits can be analyzed directly.

Core claim

MMQBA languages are precisely of the form lim(L(M, p)) for MMQFA M and cutpoint p, with a decomposition of the non-halting subspace into components that remain non-halting or eventually halt, which justifies the limit construction and enables the closure and decidability results.

What carries the argument

The three-part Büchi acceptance condition requiring that the run visits accepting states infinitely often, that the limiting cumulative acceptance probability is at least p, and that the limiting cumulative rejection probability is strictly less than p.

If this is right

Any language accepted by an MMQBA equals the limit of the language accepted by some MMQFA at the same cutpoint.
MMQBA are closed under union.
The emptiness problem for MMQBA is semi-decidable.
Universality, inclusion, equivalence, and membership problems for MMQBA are undecidable.
MMQBA are not closed under intersection or complementation.

Where Pith is reading between the lines

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

The limit characterization transfers any property of MMQFA languages that is preserved under limits to the corresponding MMQBA languages.
The decomposition of the non-halting subspace isolates the quantum states whose long-term behavior determines acceptance, separating them from states that reach halting measurements.
Semi-decidability of emptiness yields a procedure that can confirm when an MMQBA accepts no infinite word, though it may run forever when the language is nonempty.

Load-bearing premise

The limiting cumulative acceptance and rejection probabilities must exist for every infinite run that satisfies the infinite-visit requirement.

What would settle it

An explicit infinite word and MMQBA such that the word meets the three-part acceptance condition yet the accepted language cannot be written as lim(L(M, p)) for any MMQFA M would falsify the characterization.

read the original abstract

We define a quantum computational model over infinite words, called Measure-Many Quantum B\"uchi Automata (MMQBA), which extends Measure-many Quantum Finite automata (MMQFA) to the infinite word setting with B\"uchi acceptance condition. In MMQBA, the quantum state evolves through unitary transformations followed by repeated projective measurements. An infinite word is accearaq2ppted with respect to a cutpoint p is in (0, 1] if (i) the run visits accepting states infinitely often, (ii) the limiting cumulative acceptance probability is at least p, and (iii) the limiting cumulative rejection lprobability is strictly less than p. We formalize the semantics of MMQBA, establish a language-theoretic characterization showing that MMQBA languages are precisely of the form lim(L(M, p)) for MMQFA M , and develop a decomposition of the non-halting subspace. We prove that MMQBA is closed under union but not under intersection or complementation. On the algorithmic side, we show that the emptiness problem is semi-decidable, while universality, inclusion, equivalence, and membership remain undecidable.

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 defines MMQBA as a Büchi lift of MMQFA with a limit characterization and some closure/decidability facts, but the stress-test concern about guaranteed convergence of the probabilities is worth checking in the proofs.

read the letter

This paper extends the measure-many quantum finite automata model to infinite words by adding a Büchi condition that requires the run to hit accepting states infinitely often plus limits on cumulative acceptance and rejection probabilities relative to a cutpoint p. They formalize the semantics, prove the languages are exactly the limits of ordinary MMQFA languages, give a decomposition of the non-halting subspace, show closure under union but not intersection or complement, and establish that emptiness is semi-decidable while the other decision problems are undecidable. The characterization and the algorithmic results are the concrete new pieces. The decomposition step is a reasonable way to handle the infinite-run case and lets them reduce back to the finite-word setting. The soft spot is exactly the one flagged in the stress-test. The decomposition by itself does not automatically force the cumulative probability sequences to converge; repeated measurements can produce periodic or non-convergent behavior unless the effective operator satisfies extra spectral conditions. If the paper only assumes the limits exist rather than deriving them from the decomposition, both the main equivalence and the semi-decidability claim rest on an unsecured step. I would want to see the explicit argument that convergence holds. This is aimed at people already working in quantum automata and formal language theory. It is worth sending to peer review because the model is a natural extension and the stated results are checkable, even if one part of the argument needs extra scrutiny. Recommendation: send it out, but ask the referees to focus on whether the limits are proved to exist under the given decomposition.

Referee Report

3 major / 2 minor

Summary. The paper introduces Measure-Many Quantum Büchi Automata (MMQBA) as an extension of Measure-Many Quantum Finite Automata (MMQFA) to infinite words, using a Büchi-style acceptance condition that requires visiting accepting states infinitely often along with the existence of limiting cumulative acceptance probability ≥ p and rejection probability < p. It claims a language-theoretic characterization equating MMQBA languages to lim(L(M, p)) for MMQFA M, develops a decomposition of the non-halting subspace, proves closure under union (but not intersection or complement), and establishes that emptiness is semi-decidable while universality, inclusion, equivalence, and membership are undecidable.

Significance. If the central claims hold, the work extends quantum automata theory to infinite words and supplies a concrete bridge between finite-word MMQFA languages and their infinite-word limits, together with closure and decidability results that delineate the model's expressive power. The explicit decomposition and semi-decidability proof for emptiness constitute concrete technical contributions that could support further algorithmic study of quantum ω-languages.

major comments (3)

[§3] §3 (decomposition of the non-halting subspace): the argument that the three-part acceptance condition is well-defined relies on the claim that the limiting cumulative acceptance and rejection probabilities exist whenever the Büchi visit condition holds. The decomposition alone does not establish convergence of the cumulative sequences; without an additional spectral argument (e.g., that the restriction of the effective operator to the relevant subspace is diagonalizable over ℂ with eigenvalues of modulus 1 only at 1, or an explicit proof that the sequences are eventually monotonic), the limits may fail to exist for periodic or oscillatory behavior inside the subspace. This gap directly affects the characterization in §4 and the closure-under-union proof in §5.
[§4] §4 (characterization theorem): the equality MMQBA languages = lim(L(M, p)) is stated to follow from the decomposition, yet the proof sketch does not address the case in which the cumulative probability sequences oscillate and the limits therefore do not exist. If such non-convergent runs are possible under the Büchi condition, the “precisely of the form” direction fails.
[§5] §5 (closure under union): the construction that combines two MMQBA automata into one whose language is the union presupposes that the limiting probabilities exist for the combined automaton whenever they exist for the components. Because the existence question is left open by the decomposition, the closure claim is not yet secured.

minor comments (2)

[Abstract] Abstract contains typographical errors (“accearaq2ppted”, “lprobability”) that should be corrected before publication.
[§3] Notation for the limiting operator and the non-halting projection is introduced without an explicit summary table; adding such a table would improve readability of the decomposition argument.

Simulated Author's Rebuttal

3 responses · 0 unresolved

We thank the referee for the careful reading and for highlighting the need to ensure the acceptance condition is rigorously well-defined. We address each major comment below. The key point is that the cumulative sequences are partial sums of non-negative terms and hence monotonic, so their limits exist in the extended reals; we will add an explicit clarification of this fact.

read point-by-point responses

Referee: [§3] §3 (decomposition of the non-halting subspace): the argument that the three-part acceptance condition is well-defined relies on the claim that the limiting cumulative acceptance and rejection probabilities exist whenever the Büchi visit condition holds. The decomposition alone does not establish convergence of the cumulative sequences; without an additional spectral argument (e.g., that the restriction of the effective operator to the relevant subspace is diagonalizable over ℂ with eigenvalues of modulus 1 only at 1, or an explicit proof that the sequences are eventually monotonic), the limits may fail to exist for periodic or oscillatory behavior inside the subspace. This gap directly affects the characterization in §4 and the closure-under-union proof in §5.

Authors: We agree that the decomposition by itself does not address convergence, but the cumulative acceptance (resp. rejection) probability up to step n is defined as the sum of the per-step acceptance (resp. rejection) probabilities from 1 to n. Each per-step probability is non-negative, so the partial-sum sequence is non-decreasing and the limit therefore always exists in [0, +∞]. We will insert a short paragraph in §3 making this monotonicity explicit and noting how the case of an infinite limit is handled under the Büchi condition. No spectral argument is required for existence. revision: partial
Referee: [§4] §4 (characterization theorem): the equality MMQBA languages = lim(L(M, p)) is stated to follow from the decomposition, yet the proof sketch does not address the case in which the cumulative probability sequences oscillate and the limits therefore do not exist. If such non-convergent runs are possible under the Büchi condition, the “precisely of the form” direction fails.

Authors: The characterization proof in §4 inherits the same convergence question. As explained in our response to the §3 comment, the cumulative sequences are monotonic partial sums and therefore converge (possibly to +∞). We will add a cross-reference to the new monotonicity paragraph and a brief case analysis for the infinite-limit situation, thereby completing the “precisely of the form” direction. revision: partial
Referee: [§5] §5 (closure under union): the construction that combines two MMQBA automata into one whose language is the union presupposes that the limiting probabilities exist for the combined automaton whenever they exist for the components. Because the existence question is left open by the decomposition, the closure claim is not yet secured.

Authors: The union construction in §5 is well-defined once limits exist for the product automaton. Because the per-step probabilities remain non-negative in the product, the cumulative sequences are again monotonic and converge. We will add a sentence in §5 invoking the monotonicity argument already supplied in the revised §3; the closure proof then goes through without further change. revision: partial

Circularity Check

0 steps flagged

No significant circularity; characterization via explicit limit construction is self-contained

full rationale

The paper defines MMQBA semantics directly via the three-part Büchi-style acceptance condition on infinite runs (visiting acceptors infinitely often plus existence of limiting cumulative probabilities), then states a language-theoretic characterization that MMQBA languages equal lim(L(M, p)) for MMQFA M. This is an explicit construction rather than a reduction of the claim to its own inputs. The non-halting subspace decomposition is introduced to support the infinite-run analysis, and closure, non-closure, and decidability results are presented as independently proven. No self-citations, fitted parameters renamed as predictions, or ansatzes smuggled via prior work appear as load-bearing steps in the derivation chain. The results remain externally falsifiable via the stated acceptance conditions and limit construction.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 1 invented entities

The central claim rests on standard quantum mechanics for state evolution plus the newly introduced acceptance condition and limit construction; no free parameters are fitted to data.

axioms (2)

standard math Unitary transformations and projective measurements act on finite-dimensional Hilbert spaces
Invoked for the evolution and measurement steps in the automaton definition.
domain assumption Limiting cumulative probabilities exist for infinite runs
Required for the acceptance condition to be well-defined.

invented entities (1)

Measure-Many Quantum Büchi Automata (MMQBA) no independent evidence
purpose: Quantum model for languages over infinite words with repeated measurements and Büchi acceptance
Newly defined model whose properties are the subject of the paper.

pith-pipeline@v0.9.0 · 5496 in / 1457 out tokens · 58281 ms · 2026-05-11T02:41:01.040359+00:00 · methodology

discussion (0)

Lean theorems connected to this paper

Citations machine-checked in the Pith Canon. Every link opens the source theorem in the public Lean library.

IndisputableMonolith/Foundation/AlexanderDuality.lean alexander_duality_circle_linking unclear
Lemma 1 (Non-halting subspace decomposition). Let M be an MMQBA with state space C^Q, and let S_non denote the non-halting subspace. Then there exist subspaces S1, S2 ⊆ S_non such that S_non = S1 ⊕ S2...
IndisputableMonolith/Cost/FunctionalEquation.lean washburn_uniqueness_aczel unclear
Theorem 2 (limit-characterization). For every L' ⊆ Σ^ω, there exist an MMQBA M' and a cutpoint p' > 1/2 such that L' = L(M', p') iff there exist an MMQFA M and a cutpoint p > 1/2 such that L' = lim(L(M, p))

Reference graph

Works this paper leans on

36 extracted references · 36 canonical work pages

[1]

In: Proceedings 39th Annual Symposium on Foundations of Computer Science (Cat

Ambainis, A., Freivalds, R.: 1-way quantum finite automata: strengths, weaknesses and generalizations. In: Proceedings 39th Annual Symposium on Foundations of Computer Science (Cat. No. 98CB36280). pp. 332–341. IEEE (1998)

work page 1998
[2]

Springer, 3rd edn

Axler, S.: Linear Algebra Done Right. Springer, 3rd edn. (2015) Measure Many Quantum Finite Automata on Infinite Words 27

work page 2015
[3]

In: 20th Annual IEEE Symposium on Logic in Computer Science (LICS’05)

Baier, C., Grosser, M.: Recognizing/spl omega/-regular languages with probabilis- tic automata. In: 20th Annual IEEE Symposium on Logic in Computer Science (LICS’05). pp. 137–146. IEEE (2005)

work page 2005
[4]

SIAM Journal on Computing31(5), 1456–1478 (2002)

Brodsky, A., Pippenger, N.: Characterizations of 1-way quantum finite automata. SIAM Journal on Computing31(5), 1456–1478 (2002)

work page 2002
[5]

Interna- tional Journal of Quantum Information2(01), 45–54 (2004)

Brunet, O., Jorrand, P.: Dynamic quantum logic for quantum programs. Interna- tional Journal of Quantum Information2(01), 45–54 (2004)

work page 2004
[6]

Electronic Notes in Theoretical Computer Science158, 19–39 (2006)

Chadha, R., Mateus, P., Sernadas, A.: Reasoning about imperative quantum pro- grams. Electronic Notes in Theoretical Computer Science158, 19–39 (2006)

work page 2006
[7]

Dzelme-Berzina, I.: Quantum finite automata and logic. Ph.D. thesis, PhD thesis, Ph. D. thesis, University of Latvia, Riga (2010)

work page 2010
[8]

Physical Review Letters83(15), 3077 (1999)

Eisert, J., Wilkens, M., Lewenstein, M.: Quantum games and quantum strategies. Physical Review Letters83(15), 3077 (1999)

work page 1999
[9]

Theoretical Computer Science386(1-2), 151–166 (2007)

Feng, Y., Duan, R., Ji, Z., Ying, M.: Proof rules for the correctness of quantum programs. Theoretical Computer Science386(1-2), 151–166 (2007)

work page 2007
[10]

Journal of Computer and System Sciences79(7), 1181–1198 (2013)

Feng, Y., Yu, N., Ying, M.: Model checking quantum markov chains. Journal of Computer and System Sciences79(7), 1181–1198 (2013)

work page 2013
[11]

In: International Conference on Computer Aided Verification

Gay, S.J., Nagarajan, R., Papanikolaou, N.: Qmc: A model checker for quantum systems: Tool paper. In: International Conference on Computer Aided Verification. pp. 543–547. Springer (2008)

work page 2008
[12]

In: Pro- ceedings of the thirty-ninth annual ACM symposium on Theory of computing

Gutoski, G., Watrous, J.: Toward a general theory of quantum games. In: Pro- ceedings of the thirty-ninth annual ACM symposium on Theory of computing. pp. 565–574 (2007)

work page 2007
[13]

In: Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science

Katoen, J.P.: The probabilistic model checking landscape. In: Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science. pp. 31–45 (2016)

work page 2016
[14]

In: Proceedings 38th annual symposium on foundations of computer science

Kondacs, A., Watrous, J.: On the power of quantum finite state automata. In: Proceedings 38th annual symposium on foundations of computer science. pp. 66–

work page
[15]

Theo- retical Computer Science237(1-2), 275–306 (2000)

Moore, C., Crutchfield, J.P.: Quantum automata and quantum grammars. Theo- retical Computer Science237(1-2), 275–306 (2000)

work page 2000
[16]

In: Proc

Richard, B., et al.: On a decision method in restricted second order arithmetic. In: Proc. of the International Congress on Logic, Method and Philosophy of Science,

work page
[17]

Stanford University Press (1962)

work page 1962
[18]

In: Formal Models and Semantics, pp

Thomas, W.: Automata on infinite objects. In: Formal Models and Semantics, pp. 133–191. Elsevier (1990)

work page 1990
[19]

Theoretical Computer Science 1012, 114740 (2024)

Wang, Q., Ying, M.: Quantum büchi automata. Theoretical Computer Science 1012, 114740 (2024)

work page 2024
[20]

ACM Transactions on Computational Logic (TOCL)15(3), 1–31 (2014)

Ying, M., Li, Y., Yu, N., Feng, Y.: Model-checking linear-time properties of quan- tum systems. ACM Transactions on Computational Logic (TOCL)15(3), 1–31 (2014)

work page 2014
[21]

In: Proceedings of the 3rd Innovations in Theoretical Computer Science Conference

Zhang, S.: Quantum strategic game theory. In: Proceedings of the 3rd Innovations in Theoretical Computer Science Conference. pp. 39–59 (2012) Appendix: Additional Example and Technical Proofs Example 1.LetL=a(a+b) ω,Σ={a, b}wheren≥1. WedefinetheMMQBAM= (Q, Σ, δ, q 0, Qacc, Qrej)whereQ={q 0, q1, q2}, Qacc = {q1}, Qrej ={q 2}, cut pointp= 0.8andq 0 is the i...

work page 2012
[22]

= 1 3 |q0⟩ − √ 2 3 |q1⟩=ψ 2 wherex 2 =aa, acc 2 = 2 3 + 2 9 , rej 2 = 0, ψ ′ 1 = Pnon(ψ1) = 1√ 3 |q0⟩. –Va(ψ′

work page
[23]

√ 3 |q0⟩ − √ 2 3

= 1 3. √ 3 |q0⟩ − √ 2 3. √ 3 |q1⟩=ψ 3 wherex 3 =aaa, acc 3 = 2 3 + 2 9 + 2 27 , rej 3 = 0, ψ ′ 2 =P non(ψ2) = 1 3 |q0⟩. –Vb(ψ′

work page
[24]

√ 3 |q0⟩+ 2 9

= 1 9. √ 3 |q0⟩+ 2 9. √ 3 |q1⟩+ 2 9. √ 3 |q2⟩=ψ 4 wherex 4 =aaab, acc 4 = 2 3 + 2 9 + 2 27 + 4 81.3 , rej 4 = 4 81.3 , ψ ′ 3 =P non(ψ3) = 1 3 √ 3 |q0⟩. –Vb(ψ′

work page
[25]

√ 3 |q0⟩+ 2 27

= 1 27. √ 3 |q0⟩+ 2 27. √ 3 |q1⟩+ 2 27. √ 3 |q2⟩=ψ 5 wherex 4 =aaabb, acc 5 = 2 3 + 2 9 + 2 27 + 4 81.3 + 4 27.27.3 , rej 5 = 4 81.3 + 4 27.27.3 , ψ ′ 4 =P non(ψ4) = 1 27 √ 3 |q0⟩. –In general, at stepj≥1the cumulative acceptance probability satisfies accj =    2 3 , j= 1, 2 3 + 2 9 +· · ·+ 2 3j ,1≤j≤3, 2 3 + 2 9 + 2 27 + jX k=4 4 3·9 k...

work page
[26]

Example 5.LetL=a(a+b) ω,Σ={a, b}wheren≥1

Henceb ω is rejected for any cutpoint p > 1 2. Example 5.LetL=a(a+b) ω,Σ={a, b}wheren≥1. WedefinetheMMQBAM= (Q, Σ, δ, q 0, Qacc, Qrej)whereQ={q 0, q1, q2, q3}, Qacc = {q2}, Qrej ={q 3}, cut pointp= 0.8andq 0 is the initial state. Va =   0 0 0 1 2 3 1√ 2 1 3. √ 2 0 2 3 − 1√ 2 1 3. √ 2 0 1 3 0− 4 3. √ 2 0   , V b =   0 0 0 1 0 1√ 2 − ...

work page
[27]

For everyψ∈S 1 and every infinite input wordx= #σ 1σ2 · · · ∈Γ ω, the run ofMremains entirely withinS 1, and the cumulative halting probability is zero such that ∀k≥1, ψ ′ k ∈S 1, ∞X k=1 ∥Phalt(ψk)∥2 = 0

work page
[28]

Letψ∈S non be the initial state and define the run as follows: ψ0 :=ψ, ψ 1 :=V σ1 ψ0, ψ ′ 1 :=P non(ψ1)

For everyψ∈S 2,lim k→∞ ∥ψ′ k∥= 0 Proof.LetV σ be the unitary transition operator for input symbolσ∈Σ, and define the projected transition operator asV′ σ :=P nonVσ. Letψ∈S non be the initial state and define the run as follows: ψ0 :=ψ, ψ 1 :=V σ1 ψ0, ψ ′ 1 :=P non(ψ1). For everyk≥2, define recursively: ψk :=V σk ψ′ k−1, ψ ′ k :=P non(ψk). The state space ...

work page
[29]

Cumulative acceptance too small.For allj > k, we may haveaccj < p

Sincep ′ > 1 2, this violates the MMQBA rejection bound, and therefore x /∈L(M′, p′). Cumulative acceptance too small.For allj > k, we may haveaccj < p. Then limj→∞ accj ≤p, and sincep > 1 2 butlim acc j does not reachp′, the MMQBA acceptance cutpoint requirement fails. Hencex /∈L(M′, p′). Measure Many Quantum Finite Automata on Infinite Words 39 Büchi co...

work page
[30]

limj→∞ accj ≥p ′, 3.lim j→∞ rejj < p ′

infinitely many indicesjwith∥P acc(ψj)∥2 >0(Büchi condition), 2. limj→∞ accj ≥p ′, 3.lim j→∞ rejj < p ′. We construct the following words to analyze the run ofM-x1 =aab k1 , x2 = aabk1 aabk2 , x3 =aab k1 aabk2 aabk3, which can be extended to an infinite sequence x=aab k1 aabk2 aabk3 · · · ∈Σ ω. Let the initial state ofMbe represented as ψ0. The state evol...

work page
[31]

IfP(x)never halts, then along the unique run onaω there are only finitely many (indeed, zero) projections intoQacc (Büchi fails), and the cumulative acceptance and rejection masses satisfylimj→∞ accj = 0andlim j→∞ rejj = 0< p

work page
[32]

IfP(x)halts in exactlyksteps, then at stepkthe run projects into an accepting halting subspace with nonzero amplitude, and from every subse- quent step it leaks a fixed, nonzero amount intoQacc andnomass intoQ rej. Consequently: (a) Büchi holds because accepting projections occur at allj≥k; (b)rej j is monotone and bounded by0< p, hencelim j→∞ rejj < p; (...

work page
[33]

Therefore all three conditions of Definition 3.1 hold, and we conclude thataω ∈ L(MP,x, p)

Although some rejecting projections may occur, they are bounded so thatlim j→∞ rejj < p. Therefore all three conditions of Definition 3.1 hold, and we conclude thataω ∈ L(MP,x, p). 46 Abhisek Midya and A Baskar Combining the two directions, we haveaω ∈L(M P,x, p)⇐ ⇒P(x)halts. Therefore, if the assumed algorithmAfor membership existed, we could decide the ...

work page
[34]

Then the following statements are equivalent:

work page
[35]

The languageL(M, p)is nonempty

work page
[36]

Proof.(1)⇒(2) :AssumeL(M, p)̸=∅

There exists a wordw=uv ω ∈Σ ω, whereu∈Σ ∗ andv∈Σ +, such that the run ofMonw Measure Many Quantum Finite Automata on Infinite Words 47 –visits final states infinitely often, –satisfieslim j→∞ accj ≥p, and –satisfieslim j→∞ rejj < p. Proof.(1)⇒(2) :AssumeL(M, p)̸=∅. Then there exists an infinite input word w=σ 1σ2σ3 · · · ∈Σ ω such that the run ofMonwsati...

work page