Semantik von nebenläufigen Stacks

• Dyck-Sprache, gegeben durch Grammatik mit Regeln S→ε, S→Push(i) S Pop(i) S
• Datenstruktur ist (klassischer) Stack Spursprache ist Präfixsprache der Dyck-Sprache
• Nebenläufigkeit: Operationen Push_k(i), Pop_k(i)

  Op. mit unterschiedlichem Index sind vertauschbar

• nebenläufiger Stack: jede Spur ist vertauschungs- äquivalent zu Präfix eines Dyck-Wortes
• später Abschwächung: betrachte nur ``ruhende'' Spuren (kein Thread blockiert eine Ressource)