2025-11-28T02:22:19.173778

On Probabilistic $ω$-Pushdown Systems, and $ω$-Probabilistic Computational Tree Logic

Lin, Lin
In this paper, we obtain the following equally important new results: We first extend the notion of {\em probabilistic pushdown automaton} to {\em probabilistic $ω$-pushdown automaton} for the first time and study the model-checking question of {\em stateless probabilistic $ω$-pushdown system ($ω$-pBPA)} against $ω$-PCTL (defined by Chatterjee, Sen, and Henzinger in \cite{CSH08}), showing that model-checking of {\em stateless probabilistic $ω$-pushdown systems ($ω$-pBPA)} against $ω$-PCTL is generally undecidable. Our approach is to construct $ω$-PCTL formulas encoding the {\em Post Correspondence Problem}. We then study in which case there exists an algorithm for model-checking {\it stateless probabilistic $ω$-pushdown systems} and show that the problem of model-checking {\it stateless probabilistic $ω$-pushdown systems} against $ω$-{\it bounded probabilistic computational tree logic} ($ω$-bPCTL) is decidable, and further show that this problem is in $NP$-hard.
academic

Über probabilistische ω-Pushdown-Systeme und ω-probabilistische Computational Tree Logic

Grundinformationen

  • Papier-ID: 2209.10517
  • Titel: On Probabilistic ω-Pushdown Systems, and ω-Probabilistic Computational Tree Logic
  • Autoren: Deren Lin, Tianrong Lin
  • Klassifizierung: cs.LO (Logik in der Informatik), cs.FL (Formale Sprachen), quant-ph (Quantenphysik)
  • Veröffentlichungszeit: arXiv-Preprint, neueste Version v16 eingereicht am 9. November 2025
  • Papierlink: https://arxiv.org/abs/2209.10517

Zusammenfassung

Dieses Papier erzielt zwei gleichermaßen bedeutende neue Ergebnisse in den Bereichen probabilistische ω-Pushdown-Systeme und ω-probabilistische Computational Tree Logic:

  1. Erstmalige Erweiterung von probabilistischen Pushdown-Automaten zu probabilistischen ω-Pushdown-Automaten. Es wird das Modellprüfungsproblem von zustandslosen probabilistischen ω-Pushdown-Systemen (ω-pBPA) für ω-PCTL-Logik untersucht und bewiesen, dass dieses Problem typischerweise unentscheidbar ist. Der Beweis erfolgt durch Konstruktion von ω-PCTL-Formeln, die das Post-Korrespondenz-Problem (PCP) kodieren.
  2. Untersuchung der Bedingungen, unter denen Modellprüfungsalgorithmen existieren. Es wird bewiesen, dass das Modellprüfungsproblem von zustandslosen probabilistischen ω-Pushdown-Systemen für ω-beschränkte probabilistische Computational Tree Logic (ω-bPCTL) entscheidbar ist, und es wird weiter bewiesen, dass dieses Problem NP-schwer ist.

Forschungshintergrund und Motivation

1. Forschungsfrage

Dieses Papier untersucht das Modellprüfungsproblem für probabilistische unendliche Zustandssysteme, mit besonderem Fokus auf die Verifikation von probabilistischen ω-Pushdown-Systemen als neuartige formale Modelle.

2. Bedeutung des Problems

  • Theoretische Bedeutung: Modellprüfung ist ein Kernwerkzeug der formalen Verifikation mit wichtigen Anwendungen in Bereichen wie der Verifikation digitaler Schaltkreise
  • Logische Grundlagen: Berechnungstheorie basiert hauptsächlich auf Konzepten, die von Logikern wie Church und Turing definiert wurden; Logik spielt eine grundlegende Rolle in der Informatik
  • Praktische Anforderungen: Traditionelle Modellprüfung wird hauptsächlich auf endliche Zustandssysteme und nicht-probabilistische Programme angewendet, während der Verifikationsbedarf für probabilistische unendliche Zustandssysteme wächst

3. Einschränkungen bestehender Methoden

  • Einschränkungen von PCTL/PCTL*: Traditionelle probabilistische Computational Tree Logic kann ω-reguläre Eigenschaften nicht beschreiben und hat keine Fähigkeit, unendlich wiederholte Ereignisse (Liveness-Eigenschaften) auszudrücken
  • Forschungslücke: Obwohl Chatterjee et al. 2008 ω-PCTL definierten, wurde das Konzept probabilistischer ω-Pushdown-Automaten zuvor nie vorgeschlagen
  • Ungelöste Probleme: Das Modellprüfungsproblem von zustandslosen probabilistischen Pushdown-Systemen für PCTL wurde erstmals in EKM06 gestellt und erst durch die jüngste Arbeit der Autoren LL24 gelöst

4. Forschungsmotivation

  • Erweiterung probabilistischer Pushdown-Systeme zur ω-Version zur Behandlung unendlichen Verhaltens
  • Nutzung der starken Ausdruckskraft von ω-PCTL zur Beschreibung von Eigenschaften probabilistischer ω-Pushdown-Systeme
  • Bestimmung der Entscheidungsgrenzen und Rechenkomplexität des Modellprüfungsproblems

Kernbeiträge

  1. Erstmalige Definition probabilistischer ω-Pushdown-Automaten: Erweiterung klassischer probabilistischer Pushdown-Automaten zur ω-Version, Etablierung eines probabilistischen Pushdown-Modells zur Behandlung unendlicher Eingabesequenzen
  2. Beweis der Unentscheidbarkeit von ω-pBPA für ω-PCTL (Satz 1):
    • Beweis der Unentscheidbarkeit durch Kodierung des modifizierten Post-Korrespondenz-Problems als ω-PCTL-Formel
    • Ableitung zweier Folgerungen: ω-pBPA für ω-PCTL* ist unentscheidbar (Folgerung 2); ω-pPDS für ω-PCTL* ist unentscheidbar (Folgerung 3)
  3. Bestimmung der Entscheidungsgrenze (Satz 4):
    • Beweis, dass die Modellprüfung von ω-pBPA für ω-bPCTL (beschränkte Version) entscheidbar ist
    • Weiterer Beweis, dass dieses Problem NP-schwer ist
  4. Technische Innovationen:
    • Konstruktion raffinierter ω-PCTL-Formeln Ψ₁ und Ψ₂ zur Kodierung von PCP
    • Etablierung einer Äquivalenzbeziehung zwischen Stringgleichheit und Wahrscheinlichkeitssumme gleich 1 mittels Wahrscheinlichkeitsfunktionen ρ und ρ̄
    • Realisierung der Entscheidbarkeit durch Beschränkung der Formelkomplexität mittels beschränktem Until-Operator U≤k

Methodische Details

Aufgabendefinition

Modellprüfungsproblem: Gegeben ein probabilistisches ω-Pushdown-System Δ und eine ω-PCTL- (oder ω-bPCTL-) Formel Ψ, entscheiden, ob M̂_Δ ⊨_L Ψ gilt, wobei M̂_Δ die durch Δ induzierte unendliche Zustandsmarkow-Kette ist und L eine einfache Zuweisungsfunktion ist.

Kernrahmen der technischen Methode

1. Definition probabilistischer ω-Pushdown-Automaten (Definition 3.1)

8-Tupel Θ = (Q, Σ, Γ, δ, q₀, Z, Final, P), wobei:

  • Q: endliche Zustandsmenge
  • Σ: endliches Eingabealphabet
  • Γ: endliches Stackalphabet
  • δ: Übergangsfunktion
  • q₀: Anfangszustand
  • Z: initiales Stacksymbol
  • Final ⊆ Q: Endzustandsmenge
  • P: Wahrscheinlichkeitsfunktion, erfüllend ∑_{(q,α)} P((p,a,X)→(q,α)) = 1 für jedes (p,a,X)

Erfolgreiche Läufe: Ein unendlicher Lauf r erfüllt Inf(r) ∩ Final ≠ ∅, wobei Inf(r) die Menge der Zustände ist, die in r unendlich oft vorkommen.

2. Zustandslose Version: ω-pBPA (Definition 3.4)

Vereinfacht zu 5-Tupel (Γ, δ, Z, Final, P), Konfigurationsraum Γ*, Final ⊆ Γ (Stacksymbole statt Zustände).

3. ω-PCTL-Logik (Abschnitt 3.1)

Syntax:

Φ ::= true | p | ¬Φ | Φ₁ ∧ Φ₂ | P_⊳◁r(φ)
φ ::= XΦ | Φ₁UΦ₂ | φ^ω
φ^ω ::= Buchi(Φ) | coBuchi(Φ) | φ^ω₁ ∧ φ^ω₂ | φ^ω₁ ∨ φ^ω₂

Schlüsselsemantik:

  • Buchi(Φ): ∀i≥0.∃j≥i. M̂,πj ⊨_L Φ (Φ unendlich oft erfüllt)
  • coBuchi(Φ): ∃i≥0.∀j≥i. M̂,πj ⊨_L Φ (schließlich immer Φ erfüllt)

Beweis der Unentscheidbarkeit (Abschnitt 4)

Konstruktionsstrategie

Gegeben eine modifizierte PCP-Instanz {(u'ᵢ, v'ᵢ) : 1≤i≤n}, konstruiere ω-pBPA Θ', so dass eine Lösung existiert genau dann, wenn eine bestimmte ω-PCTL-Formel erfüllt ist.

Stackalphabet-Design

Γ = {Z,Z',C,F,S,N} ∪ (Σ×Σ) ∪ {X_(x,y)} ∪ {G^j_i : 1≤i≤n, 1≤j≤m+1}

Zweiphasen-Arbeitsmechanismus

Phase 1: Lösung raten (Regel (1))

Z → G¹₁Z' | ... | G¹ₙZ'  (gleichmäßige Wahrscheinlichkeit 1/n)
G^j_i → G^(j+1)_i (uᵢ(j), vᵢ(j))  (Wahrscheinlichkeit 1)
G^(m+1)_i → C | G¹₁ | ... | G¹ₙ  (gleichmäßige Wahrscheinlichkeit 1/(n+1))

Der Ratungsprozess generiert Sequenz j₁j₂...jₖ, entsprechend Stringpaaren (u_{j₁},v_{j₁})...(u_{jₖ},v_{jₖ}).

Phase 2: Lösung verifizieren (Regel (2))

C → N (Wahrscheinlichkeit 1)
N → F | S (je Wahrscheinlichkeit 1/2)
(x,y) → X_(x,y) | ε (je Wahrscheinlichkeit 1/2)
Z' → Z' (Wahrscheinlichkeit 1, zur Konstruktion unendlicher Pfade)

Schlüssel-Kodierungsformeln (Formel (3))

Ψ₁ = (¬S ∧ ⋀_{z∈Σ}¬X_(B,z)) U ([⋁_{z∈Σ}X_(A,z)] ∨ [Z' ∧ P=1(Buchi(Z'))])

Ψ₂ = (¬F ∧ ⋀_{z∈Σ}¬X_(z,A)) U ([⋁_{z∈Σ}X_(z,B)] ∨ [Z' ∧ P=1(Buchi(Z'))])

Wahrscheinlichkeits-Kodierungsfunktionen (Lemma 4.2)

Definiere Funktionen ρ und ρ̄, die Strings auf 0,1 abbilden:

ρ(x₁...xₙ) = ∑ᵢ ϑ(xᵢ)/2ⁱ
ρ̄(x₁...xₙ) = ∑ᵢ ϑ̄(xᵢ)/2ⁱ

wobei ϑ(A)=1, ϑ(B)=0, ϑ(Z')=1; ϑ̄(A)=0, ϑ̄(B)=1, ϑ̄(Z')=1.

Schlüsseleigenschaft: u'{j₁}...u'{jₖ} = v'{j₁}...v'{jₖ} ⟺ ρ(u'{j₁}...u'{jₖ}Z') + ρ̄(v'{j₁}...v'{jₖ}Z') = 1

Hauptlemmakette

  • Lemma 4.3: P({π∈Run(FαZ') : π⊨L Ψ₁}) = ρ(u'{j₁}...u'_{jₖ}Z')
  • Lemma 4.4: u'{j₁}...u'{jₖ} = v'{j₁}...v'{jₖ} ⟺ P(FαZ',Ψ₁) + P(SαZ',Ψ₂) = 1
  • Lemma 4.6: PCP hat Lösung ⟺ Θ',Z ⊨_L P>0(trueUC ∧ P=1(XP=t/2(Ψ₁) ∧ P=(1-t)/2(Ψ₂)))

Beweis der Entscheidbarkeit und Komplexität (Abschnitt 5)

ω-bPCTL-Definition

Ersetze Until-Operator U durch beschränkten Until-Operator U≤k:

M,π ⊨_L Φ₁U≤kΦ₂ ⟺ ∃0≤i≤k. M,π[i]⊨_L Φ₂ ∧ ∀j<i. M,π[j]⊨_L Φ₁

Entscheidbarkeit (Satz 5)

Da U≤k nur endlich viele Schritte prüft, wird das Problem entscheidbar.

NP-Schwere-Beweis

Durch Reduktion von beschränktem PCP (bekannt als NP-vollständig):

  • Konstruiere komplexeres ω-pBPA Δ, Stackalphabet enthält {1,2,...,n} zur Kodierung der geratenen Schranke k
  • Übergansregeln (7) kodieren gleichzeitig das Raten der Schranke und das Raten der Lösung
  • Konstruiere Formel (12), so dass beschränktes PCP Lösung hat ⟺ Modellprüfungsformel erfüllt ist
  • Reduktion kann in Polynomialzeit durchgeführt werden

Experimentelle Einrichtung

Hinweis: Dieses Papier ist ein rein theoretisches Informatik-Papier und enthält keinen experimentellen Teil. Alle Ergebnisse werden durch mathematische Beweise erhalten und beinhalten keine Datensätze, experimentelle Bewertungen oder empirische Analysen.

Experimentelle Ergebnisse

Nicht zutreffend: Dieses Papier hat keinen Abschnitt mit experimentellen Ergebnissen; alle Schlussfolgerungen sind theoretische Beweise.

Verwandte Arbeiten

1. Modellprüfung probabilistischer Pushdown-Systeme

  • EKM06: Erste Untersuchung der Modellprüfung probabilistischer Pushdown-Systeme, stellt das Problem von pBPA für PCTL (erst durch LL24 gelöst)
  • BBFK14: Beweis der Unentscheidbarkeit von pPDS für PCTL, pBPA für PCTL* unentscheidbar
  • Brá07: Untersuchung der Verifikation probabilistischer rekursiver Ordnungsprogramme

2. Logiken für ω-reguläre Eigenschaften

  • CSH08: Chatterjee et al. definieren ω-PCTL, kann ω-reguläre Eigenschaften ausdrücken
  • CCT16: Untersuchung von teilweise beobachtbaren Markow-Entscheidungsprozessen mit ω-regulären Zielen (Parität-Ziele)
  • LL14: Alternative ω-Erweiterung einer verzweigten Computational Tree Logic (aber schwer zu probabilisieren)

3. Theorie der ω-Pushdown-Automaten

  • CG77: Cohen und Gold klassische Arbeiten zu ω-kontextfreien Sprachen
  • DDK22: Logische Theorie der ω-Pushdown-Automaten

4. Innovationen dieses Papiers

  • Erstmalige Anwendung probabilistischer Erweiterungen auf ω-Pushdown-Automaten
  • Erste Untersuchung des Modellprüfungsproblems für ω-pBPA/ω-pPDS
  • Bestimmung der Entscheidungsgrenzen für ω-PCTL und ω-bPCTL

Schlussfolgerungen und Diskussion

Hauptschlussfolgerungen

  1. Unentscheidbarkeitsergebnisse:
    • Modellprüfung von ω-pBPA für ω-PCTL ist typischerweise unentscheidbar (Satz 1)
    • ω-pBPA für ω-PCTL* unentscheidbar (Folgerung 2)
    • ω-pPDS für ω-PCTL* unentscheidbar (Folgerung 3)
  2. Entscheidbarkeit und Komplexität:
    • Modellprüfung von ω-pBPA für ω-bPCTL ist entscheidbar (Satz 4)
    • Dieses Problem ist NP-schwer (Satz 4)
  3. Technische Beiträge:
    • Erfolgreiche Definition eines formalen Modells probabilistischer ω-Pushdown-Automaten
    • Etablierung einer Äquivalenzbeziehung zwischen PCP und Erfüllbarkeit von ω-PCTL-Formeln
    • Realisierung der Entscheidbarkeit durch Beschränkung der Schritte des Until-Operators

Einschränkungen

  1. Fehlende Algorithmen: Obwohl die Entscheidbarkeit für ω-bPCTL bewiesen wurde, wird kein konkreter Algorithmus angegeben
  2. Unbekannte Komplexitätsobergrenze: Nur NP-Schwere bewiesen, nicht bestimmt, ob das Problem in NP liegt; genaue Komplexität bleibt offen
  3. Beschränkung auf einfache Zuweisungen: Um nicht-entscheidbare Eigenschaften zu vermeiden, werden nur einfache Zuweisungsfunktionen betrachtet (Definition 3.5), was die Ausdruckskraft des Modells begrenzt
  4. Praktische Anwendbarkeit nicht verifiziert: Als rein theoretische Arbeit werden praktische Anwendungsszenarien oder Implementierbarkeit nicht diskutiert

Zukünftige Richtungen

Das Papier stellt explizit folgende offene Probleme:

  1. Algorithmendesign: Finde einen konkreten Algorithmus für die Modellprüfung von ω-pBPA für ω-bPCTL
  2. Genaue Komplexität: Bestimme, ob das Problem in NP liegt, ob es NP-vollständig ist
  3. Erfüllbarkeitsproblem: Untersuche das Erfüllbarkeitsproblem für ω-PCTL (ähnlich wie LTL-Erfüllbarkeit PSPACE-schwer ist):
    • Gegeben eine ω-PCTL-Zustandsformel φ, existiert ein probabilistisches ω-Pushdown-System Δ, so dass M̂_Δ,s ⊨_L φ?
  4. Andere Logik-Varianten: Erkunde andere Einschränkungen von ω-PCTL, suche nach Gleichgewicht zwischen Entscheidbarkeit und Ausdruckskraft

Tiefgreifende Bewertung

Stärken

  1. Starke theoretische Innovativität:
    • Erstmalige Einführung probabilistischer ω-Pushdown-Automaten, füllt Lücke in diesem Feld
    • Geschickte Kodierung von PCP als ω-PCTL-Formel, Beweisstechnik ist originell
    • Der Ansatz, Entscheidbarkeit durch beschränkte Operatoren zu erreichen, ist inspirierend
  2. Strenge und vollständige Beweise:
    • Lemma-Kette ist klar, von Lemma 4.1 bis 4.6 wird Unentscheidbarkeit schrittweise aufgebaut
    • Design der Wahrscheinlichkeits-Kodierungsfunktionen ρ und ρ̄ ist raffiniert, nutzt Binärexpansion zur Etablierung von Äquivalenz
    • Reduktionsbeweis ist detailliert, berücksichtigt alle kritischen Fälle
  3. Bedeutsamkeit der Ergebnisse:
    • Bestimmt Unentscheidbarkeit der ω-PCTL-Modellprüfung, zieht theoretische Grenzen für das Feld
    • NP-Schwere-Ergebnis bietet Komplexitätsuntergrenzen für Algorithmendesign
    • Folgerungen 2 und 3 erweitern die Anwendbarkeit der Unentscheidbarkeitsergebnisse
  4. Klare Darstellung:
    • Papierstruktur ist vernünftig, von Hintergrund über Definitionen zu Beweisen klar strukturiert
    • Symbolsystem ist vollständig, Definitionen präzise
    • Schlüsseltechnische Punkte haben ausreichende intuitive Erklärungen

Schwächen

  1. Fehlende Algorithmusimplementierung:
    • Satz 4 beweist Entscheidbarkeit, gibt aber keinen Algorithmus an; praktischer Wert begrenzt
    • Keine Diskussion von Zeit-/Raumkomplexität des Algorithmus
    • Fehlende konstruktive Beweise für Algorithmen-Korrektheit und Terminierung
  2. Unvollständige Komplexitätscharakterisierung:
    • Nur NP-Schwere bewiesen, nicht bestimmt, ob in NP
    • Möglicherweise präzisere Komplexitätsklassen (wie PSPACE, EXPTIME, etc.)
    • Keine Diskussion parametrisierter Komplexität (z.B. bei festem n, m oder k)
  3. Unzureichende Diskussion praktischer Anwendungen:
    • Keine konkreten Anwendungsszenarien für probabilistische ω-Pushdown-Systeme gegeben
    • Fehlende Verbindung zu praktischen Verifikationsproblemen
    • Keine Diskussion der Modellierungsfähigkeit und Einschränkungen
  4. Technische Detailfragen:
    • Die Beschränkung auf einfache Zuweisungen (Definition 3.5) ist stark, könnte Modellkraft übermäßig einschränken
    • Ob die Beschränkung k≤n in der beschränkten PCP-Reduktion notwendig ist, wird nicht ausreichend begründet
    • Einige Beweisschritte (z.B. induktiver Beweis von Lemma 5.3) sind länglich, möglicherweise vereinfachbar
  5. Unzureichender Vergleich verwandter Arbeiten:
    • Kein detaillierter Vergleich mit nicht-probabilistischen Versionen von ω-Pushdown-Automaten
    • Beziehung zu anderen probabilistischen Modellen (z.B. probabilistische Turingmaschinen) nicht diskutiert
    • Fehlende Verbindung zu Quantenberechnungsmodellen (obwohl Klassifizierung quant-ph enthält)

Einfluss

  1. Theoretischer Beitrag:
    • Legt Grundlagen für Theorie probabilistischer ω-Automaten
    • Bietet neue Fallstudien für Komplexitätsforschung in Modellprüfung
    • Könnte andere Forschung zu unendlichen Zustandssystemen inspirieren
  2. Praktischer Wert:
    • Direkter praktischer Wert begrenzt (fehlende Algorithmen)
    • Aber weist Richtung für zukünftiges Algorithmendesign
    • Unentscheidbarkeitsergebnisse vermeiden vergebliche Algorithmensuche
  3. Reproduzierbarkeit:
    • Als theoretischer Beweis prinzipiell vollständig reproduzierbar
    • Aber Beweiskomplexität ist hoch, erfordert tiefe Kenntnisse in formalen Sprachen und Wahrscheinlichkeitstheorie
    • Keine formale Verifikation (z.B. Coq/Isabelle-Beweise) bereitgestellt

Anwendungsszenarien

  1. Theoretische Forschung:
    • Formale Sprachen und Automatentheorie
    • Rechenkomplexitätstheorie
    • Modellprüfungstheorie
  2. Potenzielle Anwendungsfelder:
    • Formale Verifikation probabilistischer Systeme
    • Korrektheitsbeweis randomisierter Algorithmen
    • Verifikation probabilistischer Eigenschaften nebenläufiger Systeme
    • Stochastische Modellierung biologischer und physikalischer Systeme
  3. Nicht geeignete Szenarien:
    • Ingenieurverifikationsprojekte, die praktische Werkzeuge benötigen (derzeit fehlende Algorithmusimplementierung)
    • Endliche Zustandssysteme (bereits effizientere Methoden vorhanden)
    • Echtzeitsysteme, die schnelle Entscheidung benötigen (NP-Schwere bedeutet schlechte Worst-Case-Effizienz)

Literaturverzeichnis

Das Papier zitiert 41 Referenzen; Schlüsselreferenzen umfassen:

  1. BK08 Baier & Katoen: Principles of Model Checking - Klassisches Lehrbuch der Modellprüfung
  2. CSH08 Chatterjee et al.: Ursprüngliche Definition der ω-PCTL-Logik
  3. EKM06 Esparza et al.: Bahnbrechende Arbeiten zur Modellprüfung probabilistischer Pushdown-Systeme
  4. BBFK14 Brázdil et al.: Unentscheidbarkeitsergebnisse für pPDS und pBPA
  5. CG77 Cohen & Gold: Klassische Theorie ω-kontextfreier Sprachen
  6. GJ79 Garey & Johnson: NP-Vollständigkeitstheorie, Komplexität beschränkten PCP
  7. Pos46 Post: Originalarbeit zum Post-Korrespondenz-Problem
  8. LL24 Arbeiten der Autoren: Lösung des offenen Problems von pBPA für PCTL

Gesamtbewertung: Dies ist ein hochqualitatives theoretisches Informatik-Papier, das wichtige Beiträge zur Theorie probabilistischer Automaten und Modellprüfung leistet. Die Unentscheidbarkeitsbeweis-Techniken sind raffiniert, und die Entscheidbarkeitsergebnisse und Komplexitätsresultate für die beschränkte Version vervollständigen das theoretische Bild. Hauptmängel sind die fehlende Algorithmusimplementierung und unvollständige Komplexitätscharakterisierung, aber als grundlegende theoretische Arbeit ist ihr Wert unbestreitbar. Das Papier eignet sich für Veröffentlichung in Top-Fachzeitschriften der theoretischen Informatik (wie JACM, LMCS, TCS, etc.).