Petri Nets, an Interesting Discovery

The term "Petri Net" has come to my mind someday while I'm taking the course "Theory of Discrete-State Systems", but it had been so dim because I didn't attend the class the day Petri Net introduced. Later, when dealing with parallelism, I found that it will be much easier to represent "action activation", "event synchronization", and so on with the concept "transition" in Petri Net. And some other day, when I myself read the slides about introduction to Petri Net, I was strongly impressed by the thought that "Only equipped with an N (tokens), Petri Net has turned Finite Automaton to a universal machine, i.e. Turing-equivalent machine!" That idea came to me very naturally, since Turing Machine is different from Finite Automaton only in term "Finite", i.e. TM has infinite memory (equivalent to a natural number). But yesterday, in an attempt to simulate the "N-memory" using Petri Net, I faced a serious problem that Petri Net is incapable of expressing an important class of relations/operations: equivalence (x=y), negation (¬p). After struggling with the problem, I have found that Petri Net is "only one step next to heaven", and that "step" is to add the concept of "null token" or "transition priority". Before celebrating my "stunning result", I have done a search with Mr.Google and got some interesting things!

• Name of the game: The "Petri Net" I referred above is in fact, P/T Net, which stands for Place/Transition Net, but also Pe-Tri Net (to my mind)! In general, "Petri Nets" is a family of modeling frameworks including P/T Net's subtypes and P/T Net's extensions.


• More than making explicit: With explicit transitions, Petri Nets revive the notation of action in traditional flowchart, and make the interactions between concurrent processes much easier. With tokens, Petri Nets do not only make the instruction pointer(or instruction pointers in non-deterministic/parallel models) explicit, but also give means to represent resources as well as memories.


• The lack in expresiveness: P/T Net can simulate an N-memory NM, with inc(NM), dec(NM), NZero(NM), but Zero(NM). Using enabling property of transitions, we can define a Boolean logic with p⋀q, p⋁q, but ¬p. I have tried to combine parallel P/T Net components using "connectors"(extra nets) and preserve the pre-built structure of those components, i.e. without "splitting stransitions"(or transitions). But I failed because without not, or cannot be converted to and.


• One step to heaven: To be Turing-equivalent, P/T Net needs only one of these extensions:
  • Zero-testing/Inhibitory arcs, i.e. "not" arcs: Those arcs with a circular mark (inhibitor) at the transition end will enable the connected transitions only if the source place is empty. Normal arc: ○→☐, Inhibitory arc: ○―◦☐.
  • Transition priority: If both enabled, the transition with higher priority will be fired. This will solve the "conflict" in firing, and makes the choice between transitions more deterministic (it is still non-deterministic between transitions with equal priority).
  • Batch processing arcs: These arcs will process all token(s) in source places at once! This is proposed by some Japaneses in Modeling power of Petri nets with batch processing arcs, IEIC Technical Report.
  • Anti-places: If a place P is bounded m(P) ≼ M(P), we can construct an anti-place P^- of P such that m(P^-) = M(P) － m(p).
  However, Turing's "heaven" is not easy at all! Only with that one extension, all of the P/T Net's familiar properties (reachability, deadlock, liveness, reversibility, boundedness, covering) will be undecidable!!! Note: With P/T Net, we have algorithms to check all of those properties, already.

Một chứng minh xây dựng tuyệt vời cho Bài toán Dừng

Chẹp chẹp chẹp! Hay thiệt là hay!

Mới có hơn một tháng mà khi mình quay lại thì thấy Wikipedia đã chuyển cách chứng minh bài toán dừng từ Phản chứng sang Lập luận Đường chéo! Chứng minh bằng phản chứng vốn không được "xây dựng" cho lắm, trong khi lập luận đường chéo (chính thống) thì "có vẻ" xây dựng hơn nhiều. "Có vẻ" ở đây là nhiều khi những điều kiện tiền đề của lập luận có ẩn chứa việc "phán" một cách không xây dựng, ví dụ "tiên đề lựa chọn".

Tìm kiếm trên mạng, mình toàn thấy những "chứng minh đường chéo... giả" mà thôi. Chẳng qua chỉ là những chứng minh bằng phản chứng rồi tưởng tượng ra một đường chéo nào đó chứ chẳng liên quan gì đến lập luận đường chéo gốc của Cantor (hoàn toàn không dùng phản chứng). Còn chứng minh trên Wikipedia, vốn được lấy từ chứng minh của peter_douglass trên sci.logic, thì chính xác là lập luận đường chéo theo kiểu của Cantor. Và hơn thế nữa, nó hoàn toàn xây dựng chứ không ẩn giấu những tiền đề không xây dựng như tiên đề lựa chọn. Nó tránh được tiên đề lựa chọn là vì tập hợp các chương trình dừng (tương ứng với hàm tính được) là một tập hợp liệt kê được, nên mỗi một phần tử trong bảng giá trị đều có thể được chỉ ra (xây dựng) bởi một chương trình (thuật toán) cụ thể.