6 - Parikh’s Theorem

Question 1

draw the inclusions and how we prove it for pharik, SLS, presburger

Answer 1

everything is the same:

Presburger-definable = SLS (Ginsbur & Spanier)
SLS = Ψ(REG) (easy)
Ψ(REG) ⊆ Ψ(CF) (by definition, REG ⊆ CF)
Ψ(CF) ⊆ SLS (Parikh)

Question 2

phariks theorem

Answer 2

Consider a CFG G. Ψ(L(G)) is Semi-linear

Parikh image of G is a finite union of the parik images of subtrees (something like that)

Question 3

reachability in petri nets is decidable?

Answer 3

yes (Mayr ‘81) EXPACE-hard

NP-complete for communication free Petri nets (Esparza ‘98)

Question 4

Verma, Seidl

Answer 4

Ψ(CF) ⊆ Presburguer-Definable

2 steps:

1) Translate given CFG G into a communication-free petri net Ng
2) Turn the communication-free Petri net Ng into an ∃PA formula φg

Construction for part (1)
We are interested in the parikh image, therefore the petri net will have 1 marking on initial state, and 1 transition for each expansion rule, with weights. Ex:
S-> aSa | bSb | c
yelds 1 p for each rule, 1 transition for each symbol, weight 2 for a, for example

Construction for part (2)
2 constraints
3 kinds of subformulas
1) For each non-terminal A ∈ V, tehere is an equation
2) Ensure Xa is consistent with yp
3) Express requirement b

Question 5

2-counter machines (important)

Answer 5

Automaton with finite set of counters C
Σ = {inc,dec,zero} x C

Counter machines are petri nets that can actively test for zero

Theorem (Minsky ‘67):
2-counter machines are turing-complete

Theorem (Ibarra ‘79)
For any n-counter machine with r-reversals, there is a n*(1+r/2)-counter machine which counters does only 1 reversal each

Question 6

closed under intersection ??

not sure if this question is for parikh…

Answer 6

direciton 1:
- slsl can have presb forumla

direction 2:
- quant el, slsl for base case and the use intersection

intersection
2 parts
rought part
a and b represent the sets that they do (escape)